[Haskell-cafe] type families and type signatures
ganesh.sittampalam at credit-suisse.com
Tue Apr 8 03:23:57 EDT 2008
Manuel Chakravarty wrote:
>> 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
>> 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.
No, I meant can't it derive that equality when matching (Id a) against (Id b)?
As you say, it can't derive (a ~ b) at that point, but (Id a ~ Id b) is known,
> > 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).
My real code is somewhat analogous to (foo :: (Id Int -> Id Int)) (1::Int).
Isn't that unambiguous in the same way as (show.read) is if I give show or
read a signature?
Please access the attached hyperlink for an important electronic communications disclaimer:
More information about the Haskell-Cafe