Opened 10 months ago
Closed 9 months ago
#15039 closed bug (fixed)
Bizarre prettyprinting of inferred Coercible constraint in partial type signature
Reported by:  RyanGlScott  Owned by:  

Priority:  normal  Milestone:  8.6.1 
Component:  Compiler (Type checker)  Version:  8.4.1 
Keywords:  PartialTypeSignatures, TypeInType  Cc:  partialsigs/should_compile/T15039a, partialsigs/should_compile/T15039b, partialsigs/should_compile/T15039c, partialsigs/should_compile/T15039d 
Operating System:  Unknown/Multiple  Architecture:  Unknown/Multiple 
Type of failure:  Poor/confusing error message  Test Case:  
Blocked By:  Blocking:  
Related Tickets:  Differential Rev(s):  Phab:D4696  
Wiki Page: 
Description
Consider the following GHCi session:
$ ghci GHCi, version 8.4.1: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci λ> import Data.Type.Coercion λ> foo :: _ => Coercion a b; foo = Coercion <interactive>:2:8: error: • Found type wildcard ‘_’ standing for ‘Coercible a b :: TYPE ('GHC.Types.TupleRep '[])’ Where: ‘a’, ‘b’ are rigid type variables bound by the inferred type of foo :: Coercible a b => Coercion a b at <interactive>:2:2740 To use the inferred type, enable PartialTypeSignatures • In the type signature: foo :: _ => Coercion a b λ> :set fprintexplicitkinds λ> foo :: _ => Coercion a b; foo = Coercion <interactive>:4:8: error: • Found type wildcard ‘_’ standing for ‘(a :: *) ~~ (b :: *) :: TYPE ('GHC.Types.TupleRep ('[] GHC.Types.RuntimeRep))’ Where: ‘a’, ‘b’ are rigid type variables bound by the inferred type of foo :: ((a :: *) ~~ (b :: *)) => Coercion * a b at <interactive>:4:2740 To use the inferred type, enable PartialTypeSignatures • In the type signature: foo :: _ => Coercion a b
There are two things quite strange about this:
 In both error messages, GHC claims that
Coercible a b
/a ~~ b
has kindTYPE (TupleRep '[])
. This is wrong, and should beCoercible
.  For some reason, enabling
fprintexplicitkinds
causes the inferred constraint to be(~~)
instead ofCoercible
, which is just plain wrong.
Change History (11)
comment:2 Changed 10 months ago by
Keywords:  TypeInType added 

comment:3 Changed 10 months ago by
Well, that's one half of the mystery (2). Do you know why (1) is happening?
comment:4 Changed 10 months ago by
The idea is that, with fprintexplicitkinds
, (a ~~ b)
should be printed as ((a :: *) ~~ (b :: *))
, with the explicit kinds. But (a ~# b)
should also be printed as ((a :: *) ~~ (b :: *))
, so as not to expose the user to ~#
. Note that (a ~ b)
is just printed as (a ~ b)
, even with fprintexplicitkinds
, which seems wrong. And, of course, ~R#
should never be printed with ~~
.
What to do? Here are the cases. Assume a :: *
, b :: *
, and c :: k
.
 Homogeneous equality
a ~ b
.
 Homogeneous use of heterogeneous equality
a ~~ b
.
 Heterogeneous use of heterogeneous equality
a ~~ c
.
 Homogeneous use of unlifted equality
a ~# b
.
 Heterogeneous use of unlifted equality
a ~# c
.
 Homegeneous representational equality
Coercible a b
.
 Homogeneous use of representational unlifted equality
a ~#R b
.
 Heterogeneous use of representational unlifted equality
a ~R# c
.
Note that there is no heterogeneous representational lifted equality (the counterpert to ~~
). There could be, but there seems to be no use for it.
For each case, we must decide how to print
 By default
 With
fprintexplicitkinds
 With
fprintequalityrelations
 With
fprintexplicitkinds fprintequalityrelations
.
I propose:

a ~ b
(a :: *) ~ (b :: *)
a ~ b
(a :: *) ~ (b :: *)
2.
a ~ b
(a :: *) ~ (b :: *)
a ~~ b
(a :: *) ~~ (b :: *)
3.
a ~~ c
(a :: *) ~~ (c :: k)
a ~~ c
(a :: *) ~~ (c :: k)
4.
a ~ b
(a :: *) ~ (b :: *)
a ~# b
(a :: *) ~# (b :: *)
5.
a ~~ c
(a :: *) ~~ (c :: k)
a ~# c
(a :: *) ~# (c :: k)
6.
Coercible a b
Coercible * a b
Coercible a b
Coercible * a b
7.
Coercible a b
Coercible * a b
a ~R# b
(a :: *) ~R# (b :: *)
8.
a ~R# c
(a :: *) ~R# (c :: k)
a ~R# c
(a :: *) ~R# (c :: k)
Here are the rules:
 With
fprintequalityrelations
, print the true equality relation.  Without
fprintequalityrelations
: If the equality is representational and homogeneous, use
Coercible
.  Otherwise, if the equality is representational, use
~R#
.  If the equality is nominal and homogeneous, use
~
.  Otherwise, if the equality is nominal, use
~~
.
 If the equality is representational and homogeneous, use
 With
fprintexplicitkinds
, print kinds on both sides of an infix operator, as above; or print the kind withCoercible
.  Without
fprintexplicitkinds
, don't print kinds.
I believe that my examples above conform to these rules.
Do we agree with this approach?
comment:6 Changed 10 months ago by
comment:4 sounds fine, but it only addresses problem (2). What about problem (1)? We still have GHC reporting that the kind of Coercible a b
is TYPE (TupleRep '[])
, which is utterly bogus.
It seems like if fprintequalityrelations
is disabled, then we'd want to print the kind Constraint
instead, yes? Is that feasible with the way partial type signature reporting currently works?
comment:7 Changed 10 months ago by
I think comment:6 is a red herring. Why is GHC attempting to report about ~R#
at all here? The type of the hole is really Coercible a b
. I don't think this is a prettyprinting issue.
Instead, the solver needs to be taught somewhere to transmute a ~R# b
constraints to Coercible a b
constraints. But where? Do we do this for nominal equality anywhere?
comment:8 Changed 10 months ago by
Instead, the solver needs to be taught somewhere to transmute a ~R# b constraints to Coercible a b constraints. But where? Do we do this for nominal equality anywhere?
We do not transmute unsolved a ~# b
constraints into a ~ b
. Rather we prettyprint the unsolved a ~# b
constraint as a ~ b
.
But if we do that and print the kind of the constraint, the two will be inconsistent. It appears that this only shows up for holes. Maybe we should refrain from printing the kind of a holefiller if it's a constraint?
comment:9 Changed 9 months ago by
Differential Rev(s):  → Phab:D4696 

Status:  new → patch 
comment:11 Changed 9 months ago by
Cc:  partialsigs/should_compile/T15039a partialsigs/should_compile/T15039b partialsigs/should_compile/T15039c partialsigs/should_compile/T15039d added 

Resolution:  → fixed 
Status:  patch → closed 
I know what is going on here. When we first introduced explicit equalities Richard arranged to make the prettyprinter conceal some of the menagerie, with some adhoc rules sketched in
IfaceType
:There's a flag to control this:
fprintequalityrelations
, and using that flag makes both oddities go away.In this particular case, although it displays
Coercible a b
, it is really pretty printinga ~R# b
! And that is why the kind looks wrong: it's the kind ofa ~R# b
. So concealing the reality is jolly confusing here.Moreover, for reasons I don't understand,
fprintexplicitkinds
affects the behhaviour too, hence oddness (2).It's all in
IfaceType.ppr_equality
, which I reproduce belowWhat to do? I'm not sure. But that's what is going on.