PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

Edward Kmett ekmett at gmail.com
Fri Aug 31 18:12:30 CEST 2012


On Fri, Aug 31, 2012 at 9:37 AM, Richard Eisenberg <eir at 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20120831/27422f89/attachment.htm>


More information about the Glasgow-haskell-users mailing list