On Fri, Aug 31, 2012 at 9:37 AM, Richard Eisenberg <e...@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
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users