[Resending to the list, I used the wrong address. Sorry for the duplicate copies.]
On 19 dec. 2013, at 05:30, Richard Eisenberg <e...@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”)
signature.asc
Description: Message signed with OpenPGP using GPGMail
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
