Opened 4 months ago

Closed 2 months ago

#13963 closed bug (fixed)

Runtime representation confusingly displayed

Reported by: Iceland_jack Owned by:
Priority: normal Milestone: 8.4.1
Component: Compiler Version: 8.0.1
Keywords: TypeInType, LevityPolymorphism Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: ghci/scripts/T13963
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 (6)

comment:1 Changed 4 months 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 4 months ago by goldfire

Keywords: TypeInType LevityPolymorphism added

comment:3 Changed 4 months 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''

comment:4 Changed 3 months ago by goldfire

OK. I've fixed this. Here is the new output:

Pair :: TYPE rep -> TYPE rep' -> RuntimeRep -> *
Pair Int :: * -> RuntimeRep -> *
Pair Int Float :: RuntimeRep -> *
Pair Int Float LiftedRep :: *

I'd say this is correct, because in the Pair Int case, we already have to choose the representation -- and we never regeneralize over RuntimeRep arguments.

Patch will land with several others, in due course.

comment:5 Changed 2 months ago by Ben Gamari <ben@…>

In 8f99cd6/ghc:

Fix #13963.

This commit fixes several things:

1. RuntimeRep arg suppression was overeager for *visibly*-quantified
RuntimeReps, which should remain.

2. The choice of whether to used a Named TyConBinder or an anonymous
was sometimes wrong. Now, we do an extra little pass right before
constructing the tycon to fix these.

3. TyCons that normally cannot appear unsaturated can appear unsaturated
in :kind. But this fact was not propagated into the type checker.
It now is.

comment:6 Changed 2 months ago by RyanGlScott

Milestone: 8.4.1
Resolution: fixed
Status: newclosed
Test Case: ghci/scripts/T13963
Note: See TracTickets for help on using tickets.