Rank-2 polymorphism & type inference
Zhanyong Wan
zhanyong.wan@yale.edu
Mon, 04 Dec 2000 11:04:24 -0500
Hello,
I'm playing with Haskell's rank-2 polymorphism extension and am puzzled
by the following example:
-----------------------------------------------------------
module R2Test where
class SubType a b where
super :: a -> b
data Sub c a = Sub
data Super c a = Super
instance SubType (Sub c a) (Super c a)
f :: (forall c. Sub c a -> Super c b) -> Sub c a -> Super c b
f g x = undefined
x :: Sub c Int
x = undefined
y :: Super c Int
y = f (\a -> super a) x
----------------------------------------------------------
I though the definition of y should type-check because (roughly):
1. We know x :: Sub c Int, y :: Super c Int
2. Hence in f :: (forall c. Sub c a -> Super c b) -> Sub c a -> Super c
b, we know a is Int and b is Int.
3. Hence (\a -> super a) :: (forall c. Sub c Int -> Super c Int), and we
are all set.
However, Hugs 98 Feb 2000 (with the -98 switch) gives me:
ERROR "R2Test.hs" (line 19): Cannot justify constraints in application
*** Expression : \a -> super a
*** Type : Sub b _1 -> Super b _2
*** Given context : ()
*** Constraints : SubType (Sub b _1) (Super b _2)
and GHC 4.08.1 (with the -fglasgow-exts switch) gives:
R2Test.hs:19:
Could not deduce `SubType (Sub c a) (Super c Int)'
from the context: ()
Probable cause: missing `SubType (Sub c a) (Super c Int)'
in the type signature of an expression
or missing instance declaration for `SubType (Sub c
a) (Super
c Int)'
arising from use of `super' at R2Test.hs:16
In the right-hand side of a lambda abstraction: super a
If I remove the "forall c." from the type signature for f, then both
compilers accept my code.
My question is: how does the type inference algorithm work in the
presence of rank-2 types? Does anyone know of any documentation on
this? Thanks!
-- Zhanyong
# Zhanyong Wan http://pantheon.yale.edu/~zw23/ ____
# Yale University, Dept of Computer Science /\___\
# P.O.Box 208285, New Haven, CT 06520-8285 ||___|