Rank-2 polymorphism & type inference

[Zhanyong Wan]

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!