Opened 11 days ago

Last modified 9 days ago

#13963 new bug

Runtime representation confusingly displayed

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.0.1
Keywords: TypeInType, LevityPolymorphism Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

8.3.20170605:

> :set -XRankNTypes -XTypeInType 
> import GHC.Exts (TYPE, RuntimeRep(LiftedRep))
> type Pair (a::TYPE rep) (b::TYPE rep') rep'' = forall (r::TYPE rep''). (a -> b -> r) -> r
> :kind Pair
Pair :: * -> * -> *
> :kind Pair Int
Pair Int :: * -> *
> :kind Pair Int Float
Pair Int Float :: *
> :kind Pair Int Float LiftedRep
Pair Int Float LiftedRep :: *

It still behaves oddly with -fprint-explicit-runtime-reps enabled

> :set -fprint-explicit-runtime-reps 
> :kind Pair
Pair :: * -> * -> forall (rep'' :: RuntimeRep) -> *
> :kind Pair Int
Pair Int :: * -> forall (rep'' :: RuntimeRep) -> *
> :kind Pair Int Float
Pair Int Float :: *
> :kind Pair Int Float LiftedRep 
Pair Int Float LiftedRep :: *

I would have also expected to see Pair's kind displayed something like this

forall {rep :: RuntimeRep} {rep' :: RuntimeRep}. TYPE rep -> TYPE rep' -> forall (rep'' :: RuntimeRep) -> *

which is how the kind of the corresponding newtype gets displayed

> newtype Pair2 (a::TYPE rep) (b::TYPE rep') rep'' = P2 (forall (r::TYPE rep''). (a -> b -> r) -> r)
> :kind Pair2
Pair2 :: forall {rep :: RuntimeRep} {rep' :: RuntimeRep}.
         TYPE rep -> TYPE rep' -> forall (rep'' :: RuntimeRep) -> *

Change History (3)

comment:1 Changed 11 days ago by Iceland_jack

For comparison here is the newtype Pair2 becoming fully saturated

> :kind Pair2 
Pair2 :: forall {rep :: RuntimeRep} {rep' :: RuntimeRep}.
         TYPE rep -> TYPE rep' -> forall (rep'' :: RuntimeRep) -> *
> :kind Pair2 Int#
Pair2 Int# :: * -> forall (rep'' :: RuntimeRep) -> *
> :kind Pair2 Int# Double#
Pair2 Int# Double# :: forall (rep'' :: RuntimeRep) -> *
> :kind Pair2 Int# Double# LiftedRep
Pair2 Int# Double# LiftedRep :: *

Is the kind of Pair Int# not TYPE rep' -> forall (rep'' :: RuntimeRep) -> *

comment:2 Changed 9 days ago by goldfire

Keywords: TypeInType LevityPolymorphism added

comment:3 Changed 9 days ago by Iceland_jack

I guess, since the type synonym returns r that its kind should actually be

forall {rep :: RuntimeRep} {rep' :: RuntimeRep}. 
  TYPE rep 
  -> 
  TYPE rep'  
  -> 
  forall (rep'' :: RuntimeRep) 
  ->
  TYPE rep''
Note: See TracTickets for help on using tickets.