An interesting example. The message that GHC produces if you leave
the type signature in is:
Cls.hs:13:
Ambiguous type variable(s) `a' in the constraint `X a'
arising from use of `h' at Cls.hs:13
In the first argument of `g', namely `(h b)'
In the first argument of `f', namely `(g (h b))'
This is actually quite right. If h is *polymorphic* in its own right hand
side
(as it becomes if you give a type signature) then the call (h b)
returns a result of type (a c), and requires (X a). But alas, g then
cosumes
the value of type (a c) and returns one of type c -- so there is no way to
figure out what type 'a' is.
When h is monomorphic in its own right hand side, things are fine.
I have to admit that this is the first time I've seen an example where
adding a type signature makes a program *un* typable!
Simon
| -----Original Message-----
| From: Levent Erkok [mailto:[EMAIL PROTECTED]]
| Sent: 02 June 2000 02:09
| To: [EMAIL PROTECTED]
| Subject: types: checking vs. inferring
|
|
| Hi,
|
| I've come accross an interesting bit of code:
| ==============================================================
| ==============
| class X a where
| u :: a b -> a b
|
| f :: X a => b -> a b
| f = f
|
| g :: X a => a b -> b
| g = g
|
| -- h :: X a => b -> a c
| h b = f (g (h b))
| ==============================================================
| ================
|
| Hugs admits the script as it is. When asked for the type of
| h, it says:
|
| Main> :t h
| h :: X a => b -> a c
|
| But, when you add the type of h to the script (i.e. uncomment the
| type declaration for h), it says:
|
| Type checking
| ERROR "a.hs" (line 11): Cannot justify constraints in
| explicitly typed binding
| *** Expression : h
| *** Type : X a => b -> a c
| *** Given context : X a
| *** Constraints : X d
|
| Looks like polymorphic recursion in the presence of type
| classes confuses the
| type checker (?)
|
| This is interesting since if I tell tell the system what it
| can deduce, it gets
| confused. GHC behaves similarly, so I suspect this is a
| Haskell problem, rather
| than a particular implementation. Any comments?
|
| -Levent.
|
