[Haskell-cafe] GADT pattern match in non-rigid context

[João Paulo]

Dear all,

The following is a (I'm afraid too large!) fragment of a program  
implementing a GADT-based generic zipper:

**********************************************
data Zipper path where
     Zipper :: hole  -> Context (Up (left, hole, right) up) -> Zipper  
(Up (left, hole, right) up)

data Context path where
     ContTop :: Context (Up (Top, a, Top) Top)
     Cont    :: Left l (h -> r) -> Right r h_parent -> Context (Up  
(l_parent, h_parent, r_parent) path) -> Context (Up (l, h, r) (Up  
(l_parent, h_parent, r_parent) path))

data Up a b
data Top

data Left contains expects where
     LeftUnit :: a -> Left Top a
     LeftCons :: Left c (b -> a) -> b -> Left (c -> b) a

data Right provides final where
     RightNull :: Right final final
     RightCons :: b -> Right a final -> Right (b -> a) final

data Erase c a = forall b. (Typeable b) => Erase (c b a)

ff :: (Typeable l, Data h, Typeable r, Typeable up)
              => Zipper (Up (l, h, r) up) -> Erase Left h
ff (Zipper h c) = (gfoldl erased_left_cons erased_left_unit h)

gg ::  (Typeable l_down, Typeable h_down, Data h) => Erase Left h ->  
Maybe (Left (l_down -> h_down) h)
gg (Erase l) = cast l

move_down :: (Typeable l_down, Typeable h_down, Typeable l, Data h,  
Typeable r, Typeable up)
              => Zipper (Up (l, h, r) up) -> Maybe (Zipper (Up  
(l_down, h_down, h) (Up (l, h, r) up)))
move_down z@(Zipper h c)
           = case gg (ff z) of
#                 Just (LeftCons l' h_down)
			-> Just (Zipper h_down (Cont l' RightNull c))
                   Nothing -> Nothing

instance Typeable Top where
     typeOf _ = mkTyConApp (mkTyCon "Top") []

instance Typeable2 Left where
     typeOf2 _ = mkTyConApp (mkTyCon "Left") []

instance Typeable2 Up where
     typeOf2 _ = mkTyConApp (mkTyCon "Up") []

erased_left_cons :: (Typeable b)
                     => Erase Left (b -> a) -> b -> Erase Left a
erased_left_cons (Erase c) b = Erase (LeftCons c b)

erased_left_unit :: a -> Erase Left a
erased_left_unit a = Erase (LeftUnit a)
**********************************************

Compiling it with GHC 6.10.4 yelds the error:


***
GADT pattern match in non-rigid context for `LeftCons'
       Solution: add a type signature
In the pattern: LeftCons l' h_down                    [marked with #  
in the code]

***

The suggestion is quite clear :D (in fact, I think this compiler  
suggestion is the result of previous interactions in this mailing list)

The thing is that, in order to add a type signature to the suggested  
pattern, I believe I have to use the type variables in the signature  
of function 'move_down' (which I don't think is possible);

Can anyone help me with this? I believe this code has compiled before,  
on previous GHC versions...

Thank you very much,
João


--
João Paulo Fernandes
Universidade do Minho
www.di.uminho.pt/~jpaulo