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