content: {-# LANGUAGE GADTs, ExistentialQuantification, ScopedTypeVariables,
               RankNTypes #-}
  
  -- Here's an example from Doaitse Swiestra (Sept 06)
  -- which requires use of scoped type variables
  -- 
  -- It's a cut-down version of a larger program
  --
  -- It's also one which was sensitive to syntactic order
  -- in GHC 6.4; but not in 6.6
  
  module ShouldCompile where
  
  data Exists f = forall a . Exists (f a)
  
  data Ref env a where
    Zero :: Ref (a,env') a
    Suc  :: Ref env' a -> Ref (x,env') a
  
  data Find env final = Find (forall a . Ref env a -> Maybe (Ref final a))
  
  data Equal a b where
    Eq :: Equal a a
  
  sym :: Equal a b -> Equal b a
  sym Eq = Eq
  
  match' :: Ref env' a -> Ref env'' a -> Bool
  match' _ _ = True
  
  match :: Ref env a -> Ref env b -> Maybe (Equal a b)
  match Zero Zero      = Just Eq
  match (Suc x)(Suc y) = match x y
  match _ _            = Nothing
  
  -- Notice the essential type sig for the argument to Exists
  f1 :: forall env.  (Exists (Ref env)) -> Exists (Find  env)
  f1 (Exists (ref1 :: Ref env b))
    = Exists ( Find (\ ref2 -> case match ref2 ref1 of
                                  Just Eq -> Just Zero
                                  _       -> Nothing
                    ):: Find env (b,())
     )
  
  
  -- same as 'f1' except that 'ref1' and 'ref2' are swapped in the  
  -- application of 'match'
  f2 :: forall env.  (Exists (Ref env)) -> Exists (Find  env)
  f2 (Exists (ref1 :: Ref env b))
     = Exists (Find (\ ref2 -> case match ref1 ref2 of
                                      Just Eq -> Just Zero
                                      _       -> Nothing
                      ) :: Find env (b,())
       )
  
  