Rank-2 polymorphism & type inference
Zhanyong Wan
zhanyong.wan@yale.edu
Mon, 04 Dec 2000 16:30:46 -0500
Hi,
After sending out my question, I noticed that hugs and ghc understood my
code differently: from the error messages, we can see that hugs view (\a
-> super a) as having type Sub b _1 -> Super b _2, while ghc thinks it
is Sub c a -> Super c Int. To verify it, I changed my code s.t. y is
defined as
y = f (\(a :: Sub c Int) -> super a) x
instead of
y = f (\a -> super a) x
Guess what happened: ghc *accepted* the code, and hugs *rejected* it
with message:
ERROR "R2Test.hs" (line 19): Cannot justify constraints in application
*** Expression : \a -> super a
*** Type : Sub b Int -> Super b _2
*** Given context : ()
*** Constraints : SubType (Sub b Int) (Super b _2)
Aha, this is something interesting! Either there is no standard for the
Haskell rank-2 type inference algorithm (which is a sad thing), or one
of hugs and ghc is wrong here. Now the hugs/ghc guys on the list can no
longer remain silent -- you got to defend yourselves! :-) Could anyone
explain to me what the right behavior is supposed to be here? Thanks.
-- Zhanyong
Zhanyong Wan wrote:
>
> 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!