Ganesh Sittampalam:
On Mon, 7 Apr 2008, Manuel M T Chakravarty wrote:
Ganesh Sittampalam:
The following program doesn't compile in latest GHC HEAD, although
it does if I remove the signature on foo'. Is this expected?
Yes, unfortunately, this is expected, although it is very
unintuitive. This is for the following reason.
Let's alpha-rename the signatures and use explicit foralls for
clarity:
foo :: forall a. Id a -> Id a
foo' :: forall b. Id b -> Id b
GHC will try to match (Id a) against (Id b). As Id is a type
synonym family, it would *not* be valid to derive (a ~ b) from
this. After all, Id could have the same result for different
argument types. (That's not the case for your one instance, but
maybe in another module, there are additional instances for Id,
where that is the case.)
Can't it derive (Id a ~ Id b), though?
That's what it does derive as a proof obligation and finds it can't
prove. The error message you are seeing is GHC's way of saying, I
cannot assert that (Id a ~ Id b) holds.
Now, as GHC cannot show that a and b are the same, it can also not
show that (Id a) and (Id b) are the same. It does look odd when
you use the same type variable in both signatures, especially as
Haskell allows you to leave out the quantifiers, but the 'a' in the
signature of foo and the 'a' in the signatures of foo' are not the
same thing; they just happen to have the same name.
Sure, but forall a . Id a ~ Id a is the same thing as forall b . Id
b ~ Id b.
Thanks for the explanation, anyway. I'll need to have another think
about what I'm actually trying to do (which roughly speaking is to
specialise a general function over type families using a signature
which I think I need for other reasons).
Generally speaking, is there any way to give a signature to foo'?
Sorry, but in the heat of explaining what GHC does, I missed the
probably crucial point. Your function foo is useless, as is foo'.
Not only can't you rename foo (to foo'), but you generally can't use
it. It's signature is ambiguous. Try evaluating (foo (1::Int)). The
problem is related to the infamous (show . read).
Manuel
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
