Fwd: Decomposition of given equalities
Thijs Alkemade
me at thijsalkema.de
Thu Dec 19 11:32:20 UTC 2013
[Resending to the list, I used the wrong address. Sorry for the duplicate copies.]
On 19 dec. 2013, at 05:30, Richard Eisenberg <eir at cis.upenn.edu> wrote:
> I'd say GHC has it right in this case.
>
> (f a ~ g b) exactly implies (f ~ g) and (a ~ b) if and only if the kinds match up. If, say, (f :: k1 -> *), (g :: k2 -> *), (a :: k1), and (b :: k2), then (f ~ g) and (a ~ b) are ill-kinded. In Gabor's initial problem, we have (with all type, kind, and coercion variables made explicit)
But even when it can know the kinds match up it doesn’t decompose it. For example:
—
{-# LANGUAGE TypeFamilies #-}
foo :: (f a ~ g b) => f a -> g b
foo = id
—
Ends up with 2 errors (7.6.3):
Could not deduce (a ~ b)
from the context (f a ~ g b)
Could not deduce (f ~ g)
from the context (f a ~ g b)
So the wanted constraint f a ~ g b was decomposed, meaning the kind of a and b, and f and g were already found to be equal. Even with an explicit kind signature on every variable it doesn't work:
foo :: (f a ~ g b) => (f :: * -> *) (a :: *) -> (g :: * -> *) (b :: *)
I can’t think of an example where f a ~ g b holds, but the kinds of a and b are different.
Thijs (“xnyhps”)
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 841 bytes
Desc: Message signed with OpenPGP using GPGMail
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20131219/3d0ac794/attachment.sig>
More information about the Glasgow-haskell-users
mailing list