[Haskell-cafe] type families and type signatures
Manuel M T Chakravarty
chak at cse.unsw.edu.au
Tue Apr 8 03:15:18 EDT 2008
> 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
>> 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).
More information about the Haskell-Cafe