Sittampalam, Ganesh:
Manuel Chakravarty wrote:
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.
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,
surely?
No, it is not know. Why do you think it is?
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?
No. The problem with a functions that has an ambiguous signature is
that it contains type variables that are impossible to constrain by
applying the function. Providing a type signature at the application
site makes this no easier. Why? Consider what a type annotation
means. By writing e :: t, you express your intent to use e at type t,
but you also force the compiler to check that whatever type it derives
for e is more general than t. It is this check for type subsumption
that is the tricky bit when typing TFs (or FDs). See <http://www.cse.unsw.edu.au/~chak/papers/SPCS08.html
> for more detail on why this is a hard problem.
The problem with an ambiguous signature is that the subsumption check
always fails, because the ambiguous signature contains some type
variables for which the type checker cannot deduce a type instance.
(You as a human reader may be able to *guess* an instance, but HM-
based inference does generally not guess. It's a deterministic
process.)
The problem is really with foo and its signature, not with any use of
foo. The function foo is (due to its type) unusable. Can't you
change foo?
Manuel
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
