PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?
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
(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.
> 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.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Glasgow-haskell-users