Fwd: Decomposition of given equalities

[Thijs Alkemade]

[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>