testsuite/tests/gadt/doaitse.hs

   1 {-# LANGUAGE GADTs, ExistentialQuantification, ScopedTypeVariables,
   2              RankNTypes #-}
   3
   4 -- Here's an example from Doaitse Swiestra (Sept 06)
   5 -- which requires use of scoped type variables
   6 --
   7 -- It's a cut-down version of a larger program
   8 --
   9 -- It's also one which was sensitive to syntactic order
  10 -- in GHC 6.4; but not in 6.6
  11
  12 module ShouldCompile where
  13
  14 data Exists f = forall a . Exists (f a)
  15
  16 data Ref env a where
  17   Zero :: Ref (a,env') a
  18   Suc  :: Ref env' a -> Ref (x,env') a
  19
  20 data Find env final = Find (forall a . Ref env a -> Maybe (Ref final a))
  21
  22 data Equal a b where
  23   Eq :: Equal a a
  24
  25 sym :: Equal a b -> Equal b a
  26 sym Eq = Eq
  27
  28 match' :: Ref env' a -> Ref env'' a -> Bool
  29 match' _ _ = True
  30
  31 match :: Ref env a -> Ref env b -> Maybe (Equal a b)
  32 match Zero Zero      = Just Eq
  33 match (Suc x)(Suc y) = match x y
  34 match _ _            = Nothing
  35
  36 -- Notice the essential type sig for the argument to Exists
  37 f1 :: forall env.  (Exists (Ref env)) -> Exists (Find  env)
  38 f1 (Exists (ref1 :: Ref env b))
  39   = Exists ( Find (\ ref2 -> case match ref2 ref1 of
  40                                 Just Eq -> Just Zero
  41                                 _       -> Nothing
  42                   ):: Find env (b,())
  43    )
  44
  45
  46 -- same as 'f1' except that 'ref1' and 'ref2' are swapped in the
  47 -- application of 'match'
  48 f2 :: forall env.  (Exists (Ref env)) -> Exists (Find  env)
  49 f2 (Exists (ref1 :: Ref env b))
  50    = Exists (Find (\ ref2 -> case match ref1 ref2 of
  51                                     Just Eq -> Just Zero
  52                                     _       -> Nothing
  53                     ) :: Find env (b,())
  54      )
  55