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