On Fri, Aug 31, 2012 at 9:37 AM, Richard Eisenberg <eir@cis.upenn.edu> wrote:

I ran into this same issue in my own experimentation: if a type variable x has a kind with only one constructor K, GHC does not supply the equality x ~ K y for some fresh type variable y. Perhaps it should. I too had to use similar workarounds to what you have come up with.

One potential problem is the existence of the Any type, which inhabits every kind. Say x gets unified with Any. Then, we would have Any ~ K y, which is an inconsistent coercion (equating two types with distinct ground head types). However, because the RHS is a promoted datatype, we know that this coercion can never be applied to a term. Because equality is homogeneous (i.e. ~ can relate only two types of the same kind), I'm not convinced the existence of Any ~ K y is so bad. (Even with heterogeneous equality, it might work out, given that there is more than one type constructor that results in *...)

I think it may have to.

Working the example further runs into a similar problem.

When you go to implement indexed bind, there isn't a way to convince GHC that

(Snd ij ~ i, Fst ij ~ j) entails (ij ~ '(i,j))

I'm working around it (for now) with unsafeCoerce. :-(

But it with an explicitly introduced equality this code would just work, like it does in other platforms.

https://github.com/ekmett/indexed/blob/master/src/Indexed/Thrist.hs#L21

Regarding the m -> k fundep: my experiments suggest that this dependency is implied when you have (m :: k), but I guess not when you have k appear in the kind of m in a more complicated way. Currently, there are no kind-level functions, so it appears that m -> k could be implied whenever k appears anywhere in the kind of m. If (when!) there are kind-level functions, we'll have to be more careful.

-Edward