[Haskell-cafe] Existential problem

[Daniel Fischer]

Am Mittwoch, 30. März 2005 10:17 schrieb Niklas Broberg:
> I just can't see why the following code will not type check. I have
> scaled it down as much as possible:
>
> -------------------------------------
> -- IO with an extra level annotation
> newtype IO' t a = MkIO' (IO a)
>
from here on you wrote just IO, not IO'.

> -- levels
> data H
> data L
>
> -- Explicitly recursive continuation type
> data C t a = forall t2 . C (C t2 a -> IO t a)

If you write

data C t a = C (forall t2 . C t2 a -> IO' t a),

it will compile (versions 6.2.2, 6.4). Whether that'll do exactly what you 
want, I don't know :-(

>
> transition :: Bool -> IO tx () -> IO t () -> IO t ()
> transition b c d = undefined
>
> s1 :: C t () -> IO H ()
> s1 (C k) = trans (True)
>                     (k (C s1))  -- :: IO t ()
>                     (s1 (C k))  -- :: IO H ()

trans = transition, I suppose?

> --------------------------------------
> The error message is:
>     Inferred type is less polymorphic than expected
>         Quantified type variable `t2' is unified with `H'
>     When checking an existential match that binds
>         k :: C t2 a -> IO t a
>     The pattern(s) have type(s): C t1 ()
>     The body has type: IO H ()
>     In the definition of `s1':
>         s1 (C k) = trans (True) (k (C s1)) (s1 (C k))

6.4's error message is:
Niklas.hs:21:26:
    Couldn't match the rigid variable `t2' against `H'
      `t2' is bound by the pattern for `C' at Niklas.hs:20:4-6
      Expected type: C t21 () -> IO' t2 ()
      Inferred type: C t21 () -> IO' H ()
    In the first argument of `C', namely `s1'
    In the first argument of `k', namely `(C s1)'

hugs gives
ERROR "./Niklas.hs":20 - Type error in application
*** Expression     : k (C s1)
*** Term           : C s1
*** Type           : C H ()
*** Does not match : C _3 ()
*** Because        : cannot instantiate Skolem constant

Now I'm not an expert, but I think it's roughly thus:
by the original definition, from the pattern 'C k', it follows that there is 
some type, call it t1, such that k has type
C t1 () -> IO' t ().
Now applying k to C s1 requires t1 to be H, which may or may not be the case, 
that can't be decided by pattern matching. Says the user's guide (I'm not 
quite certain that this is about the case in hand):

In general, you can only pattern-match on an existentially-quantified 
constructor in a case expression or in the patterns of a function definition. 
The reason for this restriction is really an implementation one. 
Type-checking binding groups is already a nightmare without existentials 
complicating the picture. Also an existential pattern binding at the top 
level of a module doesn't make sense, because it's not clear how to prevent 
the existentially-quantified type "escaping". So for now, there's a 
simple-to-state restriction. We'll see how annoying it is. 

If you shift the forall, the argument of C is required to be polymorphic, so 
all compilation problems disappear.

>
> The thing is, I'm perfectly happy with t2 being unified with H for
> this particular definition of s1, but I want to use it in other cases
> as well. The code that follows the one above is
>
> s2 :: C t () -> IO L ()
> s2 (C k) = trans (True)
>                     (k (C s2))  -- :: IO t ()
>                     (s2 (C k))  -- :: IO L ()
>
> main = s1 (C s2)
>
> where t2 instead gets unified with L for the definition of s2. Could
> someone tell me why this does not work? I'm using GHC 6.2.2.
>
> Thanks,
>
> /Niklas

I would like a detailed explanation, too.

Daniel