If the type checker really deduces the type 'forall a b . C a b => a -
> a' then an inference algorithm that works seems easy. Do type
inference for f, then check that the signature the user has given is
alpha-convertible with the deduced type (well, in general it's more
complicated than that, of course).
If the type checker doesn't really deduce 'forall a b . C a b => a ->
a' then it shouldn't print what it does.
So I'm curious, what is the exact deduced type?
-- Lennart
On Dec 11, 2006, at 07:16 , Simon Peyton-Jones wrote:
| Tell me how this make sense:
| 1. I enter the definition for f.
| 2. I ask ghc for the type of f and get an answer.
| 3. I take the answer and tell ghc this is the type of f, and ghc
| tells me I'm wrong.
| Somewhere in this sequence something is going wrong.
I agree! Indeed I wrote:
| It doesn't get much simpler than that! With the type sig, GHC
can't see that the (C a b) provided can
| satisfy the (C a b1) which arises from the call to op. However,
without the constraint, GHC simply
| abstracts over the constrains arising in the RHS, namely (C a
b1), and hence infers the type
| f :: C a b1 => a -> a
| It is extremely undesirable that the inferred type does not work
as a type signature, but I don't see
| how to fix it
If you have an idea for an inference algorithm that would typecheck
this program, I'd be glad to hear it. Just to summarise, the
difficulty is this:
I have a dictionary of type (C a b1)
I need a dictionary of type (C a b2)
There is no functional dependency between C's parameters
Simon
PS: the complete program is this:
class C a b where
op :: a -> a
f :: C a b => a -> a
f x = op x
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
