diff options
Diffstat (limited to 'testsuite/tests/gadt')
106 files changed, 3054 insertions, 0 deletions
diff --git a/testsuite/tests/gadt/Arith.hs b/testsuite/tests/gadt/Arith.hs new file mode 100644 index 0000000000..a98ee729a9 --- /dev/null +++ b/testsuite/tests/gadt/Arith.hs @@ -0,0 +1,146 @@ +{-# LANGUAGE GADTs #-}
+
+module Arith where
+
+data E a b = E (a -> b) (b -> a)
+
+eqRefl :: E a a
+eqRefl = E id id
+
+-- just to construct unique strings
+data W
+data M a
+
+-- terms
+data Var a where
+ VarW :: Var W
+ VarM :: Var (M a)
+
+-- expose s in the type level making sure it is a string
+data Abs s e1 where
+ Abs :: (Var s) -> e1 -> Abs (Var s) e1
+
+data App e1 e2 = App e1 e2
+data Lit = Lit
+
+data TyBase = TyBase
+data TyArr t1 t2 = TyArr t1 t2
+
+-- (x:ty) in G
+data IN g p where
+ INOne :: IN (g,(x,ty)) (x,ty)
+ INShift :: IN g0 (x,ty) -> IN (g0,a) (x,ty)
+
+data INEX g x where
+ INEX :: IN g (x,v) -> INEX g x
+
+
+-- G1 subseteq G2
+type SUP g1 g2 = forall a. IN g1 a -> IN g2 a
+
+-- typing derivations
+data DER g a ty where
+ DVar :: IN (g,g0) ((Var a),ty) -> DER (g,g0) (Var a) ty -- the g,g0 makes sure that env is non-empty
+ DApp :: DER g a1 (TyArr ty1 ty2) ->
+ DER g a2 ty1 -> DER g (App a1 a2) ty2
+ DAbs :: DER (g,(Var a,ty1)) e ty2 ->
+ DER g (Abs (Var a) e) (TyArr ty1 ty2)
+ DLit :: DER g Lit TyBase
+
+-- G |- \x.x : a -> a
+test1 :: DER g (Abs (Var W) (Var W)) (TyArr ty ty)
+test1 = DAbs (DVar INOne)
+
+-- G |- (\x.x) Lit : Lit
+test2 :: DER g (App (Abs (Var W) (Var W)) Lit) TyBase
+test2 = DApp (DAbs (DVar INOne)) DLit
+
+-- G |- \x.\y. x y : (C -> C) -> C -> C
+test3 :: DER g (Abs (Var W) (Abs (Var (M W)) (App (Var W) (Var (M W))))) (TyArr (TyArr ty ty) (TyArr ty ty))
+test3 = DAbs (DAbs (DApp (DVar (INShift INOne)) (DVar INOne)))
+
+data ISVAL e where
+ ISVALAbs :: ISVAL (Abs (Var v) e)
+ ISVALLit :: ISVAL Lit
+
+data React e1 e2 where
+ SUBSTReact :: React (Abs (Var y) e) v
+
+-- evaluation
+data EDER e1 e2 where
+ -- EVar :: IN (a,val) -> ISVAL val -> EDER c a val
+ EApp1 :: EDER e1 e1' -> EDER (App e1 e2) (App e1' e2)
+ EApp2 :: ISVAL v1 -> EDER e2 e2' -> EDER (App v1 e2) (App v1 e2')
+ EAppAbs :: ISVAL v2 -> React (Abs (Var v) e) v2 -> EDER (App (Abs (Var v) e) v2) e1
+
+-- (\x.x) 3 -> 3
+-- test4 :: EDER (App (Abs (Var W) (Var W)) Lit) Lit
+-- test4 = EAppAbs ISVALLit SUBSTEqVar
+
+
+-- existential
+data REDUCES e1 where
+ REDUCES :: EDER e1 e2 -> REDUCES e1
+
+-- data WFEnv x c g where
+-- WFOne :: ISVAL v -> DER g v ty -> WFEnv (Var x) (c,(Var x,v)) (g,(Var x,ty))
+-- WFShift :: WFEnv v c0 g0 -> WFEnv v (c0,(y,y1)) (g0,(z,z1))
+
+-- data WFENVWRAP c g where
+-- WFENVWRAP :: (forall v ty . IN g (v,ty) -> WFEnv v c g) -> WFENVWRAP c g
+
+
+-- data INEXVAL c x where
+-- INEXVAL :: IN c (x,v) -> ISVAL v -> INEXVAL c x
+
+-- -- the first cool theorem!
+-- fromTEnvToEnv :: IN g (x,ty) -> WFEnv x c g -> INEXVAL c x
+-- fromTEnvToEnv INOne (WFOne isv _) = INEXVAL INOne isv
+-- fromTEnvToEnv (INShift ind1) (WFShift ind2) =
+-- case (fromTEnvToEnv ind1 ind2) of
+-- INEXVAL i isv -> INEXVAL (INShift i) isv
+
+
+data ISLAMBDA v where ISLAMBDA :: ISLAMBDA (Abs (Var x) e)
+data ISLIT v where ISLIT :: ISLIT Lit
+
+data EXISTAbs where
+ EXISTSAbs :: (Abs (Var x) e) -> EXISTAbs
+
+bot = bot
+
+canFormsLam :: ISVAL v -> DER g v (TyArr ty1 ty2) -> ISLAMBDA v
+canFormsLam ISVALAbs _ = ISLAMBDA
+-- canFormsLam ISVALLit _ = bot <== unfortunately I cannot catch this ... requires some exhaustiveness check :-(
+
+canFormsLit :: ISVAL v -> DER g v TyBase -> ISLIT v
+canFormsLit ISVALLit _ = ISLIT
+
+data NULL
+
+progress :: DER NULL e ty -> Either (ISVAL e) (REDUCES e)
+
+progress (DAbs prem) = Left ISVALAbs
+progress (DLit) = Left ISVALLit
+-- progress (DVar iw) = bot <== here is the cool trick! I cannot even wite this down!
+progress (DApp e1 e2) =
+ case (progress e1) of
+ Right (REDUCES r1) -> Right (REDUCES (EApp1 r1))
+ Left isv1 -> case (progress e2) of
+ Right (REDUCES r2) -> Right (REDUCES (EApp2 isv1 r2))
+ Left isv2 -> case (canFormsLam isv1 e1) of
+ ISLAMBDA -> Right (REDUCES (EAppAbs isv2 SUBSTReact))
+
+
+-- case fromTEnvToEnv iw (f iw) of
+-- INEXVAL i isv -> Right (REDUCES (EVar i isv))
+-- progress (WFENVWRAP f) (DApp e1 e2) =
+-- case (progress (WFENVWRAP f) e1) of
+-- Right (REDUCES r1) -> Right (REDUCES (EApp1 r1))
+-- Left isv1 -> case (progress (WFENVWRAP f) e2) of
+-- Right (REDUCES r2) -> Right (REDUCES (EApp2 isv1 r2))
+-- Left isv2 -> case (canFormsLam isv1 e1) of
+-- ISLAMBDA -> EAppAbs isv2 e1
+
+
+
diff --git a/testsuite/tests/gadt/CasePrune.hs b/testsuite/tests/gadt/CasePrune.hs new file mode 100644 index 0000000000..4048c94c5f --- /dev/null +++ b/testsuite/tests/gadt/CasePrune.hs @@ -0,0 +1,28 @@ +{-# LANGUAGE GADTs, GeneralizedNewtypeDeriving #-} + +-- See Trac #1251 and the comments +-- Note [Pruning dead case alternatives] in types/Unify.lhs + +module Main( main ) where + +data T a where MkT :: T Int + +class C a where ic :: T a + +instance C Int where ic = MkT + +newtype A = MkA Int deriving( C ) + +-- axiom CoA : A ~ Int +-- Hence C Int ~ C A + +-- instance C A where +-- ic :: T A +-- ic = MkT + +icA = ic :: T A -- There are no (non-bot) values of this type + +main = print (icA `seq` "ok") + + + diff --git a/testsuite/tests/gadt/CasePrune.stdout b/testsuite/tests/gadt/CasePrune.stdout new file mode 100644 index 0000000000..52c33a57c7 --- /dev/null +++ b/testsuite/tests/gadt/CasePrune.stdout @@ -0,0 +1 @@ +"ok" diff --git a/testsuite/tests/gadt/Gadt17_help.hs b/testsuite/tests/gadt/Gadt17_help.hs new file mode 100644 index 0000000000..30b57133d5 --- /dev/null +++ b/testsuite/tests/gadt/Gadt17_help.hs @@ -0,0 +1,34 @@ +{-# LANGUAGE GADTs #-} +{-# OPTIONS_GHC -O #-} + +module Gadt17_help ( + TernOp (..), applyTernOp + ) where + +data TypeWitness a where + TWInt :: TypeWitness Int + TWBool :: TypeWitness Bool + TWFloat :: TypeWitness Float + TWDouble :: TypeWitness Double + +instance (Eq a) => Eq (TypeWitness a) where + (==) TWInt TWInt = True + (==) TWBool TWBool = True + (==) TWFloat TWFloat = True + (==) TWDouble TWDouble = True + (==) _ _ = False + +data TernOp a b c d where + OpIf :: TypeWitness a -> TernOp Bool a a a + OpTernFunc :: TypeWitness a -> TypeWitness b -> TypeWitness c + -> TypeWitness d -> (a -> b -> c -> d) -> TernOp a b c d + +instance Show (TernOp a b c d) where + show (OpIf {}) = "OpIf" + show (OpTernFunc {}) = "OpTernFunc <function>" + + +applyTernOp :: TernOp a b c d -> a -> b -> c -> d +applyTernOp (OpIf {}) cond x y = if (cond) then x else y +applyTernOp (OpTernFunc _ _ _ _ f) x y z = f x y z + diff --git a/testsuite/tests/gadt/Gadt23_AST.hs b/testsuite/tests/gadt/Gadt23_AST.hs new file mode 100644 index 0000000000..75b07c7611 --- /dev/null +++ b/testsuite/tests/gadt/Gadt23_AST.hs @@ -0,0 +1,10 @@ +{-# LANGUAGE GADTs, KindSignatures #-} + +module Gadt23_AST where + +data Exp_; + +data AST :: * -> * -> * where + Var :: String -> AST Exp_ tag + Tag :: tag -> AST a tag -> AST a tag + diff --git a/testsuite/tests/gadt/Makefile b/testsuite/tests/gadt/Makefile new file mode 100644 index 0000000000..7a2288f6a9 --- /dev/null +++ b/testsuite/tests/gadt/Makefile @@ -0,0 +1,22 @@ +TOP=../.. +include $(TOP)/mk/boilerplate.mk +include $(TOP)/mk/test.mk + +.PHONY: gadt17 gadt23 + +# A mulit-module test that made GHC 6.4.1 crash +gadt17: + @$(RM) gadt17.hi Gadt17_help.hi + @$(RM) A$(OBJSUFFIX) + '$(TEST_HC)' $(TEST_HC_OPTS) -c Gadt17_help.hs + '$(TEST_HC)' $(TEST_HC_OPTS) -c gadt17.hs + +gadt23: + $(RM) gadt23 gadt23.hi gadt23.o Gadt23_AST.hi Gadt23_AST.o + '$(TEST_HC)' $(TEST_HC_OPTS) -v0 --make gadt23.hs + # We want to "touch gadt23.hs" really, but we then have issues with + # everything happening in the same second so the touch having no + # effect. Thus make gadt23.hi/o older instead. + touch -t 01010000 gadt23.hi gadt23.o + '$(TEST_HC)' $(TEST_HC_OPTS) -v0 --make gadt23.hs + diff --git a/testsuite/tests/gadt/Nilsson.hs b/testsuite/tests/gadt/Nilsson.hs new file mode 100644 index 0000000000..bb2fa1ba20 --- /dev/null +++ b/testsuite/tests/gadt/Nilsson.hs @@ -0,0 +1,293 @@ +{-# LANGUAGE GADTs, ScopedTypeVariables #-} + +-- Supplied by Henrik Nilsson, showed up a bug in GADTs + +module Nilsson where + +data Event a = NoEvent | Event a + +fromEvent :: Event a -> a +fromEvent = undefined + +usrErr :: String -> String -> String -> a +usrErr = undefined + +type DTime = Double -- [s] + +data SF a b = SF {sfTF :: a -> Transition a b} + +data SF' a b where + SFArr :: (DTime -> a -> Transition a b) -> FunDesc a b -> SF' a b + + SFAcc :: (DTime -> Event a -> Transition (Event a) b) + -> (c -> a -> (c, b)) -> c -> b + -> SF' (Event a) b + SFCpAXA :: (DTime -> a -> Transition a d) + -> FunDesc a b -> SF' b c -> FunDesc c d + -> SF' a d + SF' :: (DTime -> a -> Transition a b) -> SF' a b + +-- A transition is a pair of the next state (in the form of a signal +-- function) and the output at the present time step. + +type Transition a b = (SF' a b, b) + + +sfTF' :: SF' a b -> (DTime -> a -> Transition a b) +sfTF' (SFArr tf _) = tf +sfTF' (SFAcc tf _ _ _) = tf +-- sfTF' (SFSScan ...) +sfTF' (SFCpAXA tf _ _ _) = tf +sfTF' (SF' tf) = tf + +-- "Smart" constructors. The corresponding "raw" constructors should not +-- be used directly for construction. + +sfArr :: FunDesc a b -> SF' a b +sfArr FDI = sfId +sfArr (FDC b) = sfConst b +sfArr (FDE f fne) = sfArrE f fne +sfArr (FDG f) = sfArrG f + + +sfId :: SF' a a +sfId = sf + where + sf = SFArr (\_ a -> (sf, a)) FDI + + +sfConst :: b -> SF' a b +sfConst b = sf + where + sf = SFArr (\_ _ -> (sf, b)) (FDC b) + + +sfNever :: SF' a (Event b) +sfNever = sfConst NoEvent + + +-- Assumption: fne = f NoEvent +sfArrE :: (Event a -> b) -> b -> SF' (Event a) b +sfArrE f fne = sf + where + sf = SFArr (\_ ea -> (sf, case ea of NoEvent -> fne ; _ -> f ea)) + (FDE f fne) + +sfArrG :: (a -> b) -> SF' a b +sfArrG f = sf + where + sf = SFArr (\_ a -> (sf, f a)) (FDG f) + + +sfAcc :: (c -> a -> (c, b)) -> c -> b -> SF' (Event a) b +sfAcc f c bne = sf + where + sf = SFAcc (\dt ea -> case ea of + NoEvent -> (sf, bne) + Event a -> let + (c', b) = f c a + in + (sfAcc f c' bne, b)) + f + c + bne + +-- sfAccHld would be very similar. The only difference is that +-- what's now called "bne" would be updated at each event. +-- +-- So maybe one could use the SAME constructor, just different +-- transition functions? It really depends on what assumptions +-- one need to make when optimizing. + + +-- Motivation for event-processing function type +-- (alternative would be function of type a->b plus ensuring that it +-- only ever gets invoked on events): +-- * Now we need to be consistent with other kinds of arrows. +-- * We still want to be able to get hold of the original function. + +data FunDesc a b where + FDI :: FunDesc a a -- Identity function + FDC :: b -> FunDesc a b -- Constant function + FDE :: (Event a -> b) -> b -> FunDesc (Event a) b -- Event-processing fun + FDG :: (a -> b) -> FunDesc a b -- General function + +fdFun :: FunDesc a b -> (a -> b) +fdFun FDI = id +fdFun (FDC b) = const b +fdFun (FDE f _) = f +fdFun (FDG f) = f + +fdComp :: FunDesc a b -> FunDesc b c -> FunDesc a c +fdComp FDI fd2 = fd2 +fdComp fd1 FDI = fd1 +fdComp (FDC b) fd2 = FDC ((fdFun fd2) b) +fdComp _ (FDC c) = FDC c +fdComp (FDE f1 f1ne) fd2 = FDE (f2 . f1) (f2 f1ne) + where + f2 = fdFun fd2 +fdComp (FDG f1) (FDE f2 f2ne) = FDG f + where + f a = case f1 a of + NoEvent -> f2ne + f1a -> f2 f1a +fdComp (FDG f1) fd2 = FDG (fdFun fd2 . f1) + + +-- Verifies that the first argument is NoEvent. Returns the value of the +-- second argument that is the case. Raises an error otherwise. +-- Used to check that functions on events do not map NoEvent to Event +-- wherever that assumption is exploited. +vfyNoEv :: Event a -> b -> b +vfyNoEv NoEvent b = b +vfyNoEv _ _ = usrErr "AFRP" "vfyNoEv" + "Assertion failed: Functions on events must not \ + \map NoEvent to Event." + +compPrim :: SF a b -> SF b c -> SF a c +compPrim (SF {sfTF = tf10}) (SF {sfTF = tf20}) = SF {sfTF = tf0} + where + tf0 a0 = (cpXX sf1 sf2, c0) + where + (sf1, b0) = tf10 a0 + (sf2, c0) = tf20 b0 + + -- Naming convention: cp<X><Y> where <X> and <Y> is one of: + -- X - arbitrary signal function + -- A - arbitrary pure arrow + -- C - constant arrow + -- E - event-processing arrow + -- G - arrow known not to be identity, constant (C) or + -- event-processing (E). + + cpXX :: SF' a b -> SF' b c -> SF' a c + cpXX (SFArr _ fd1) sf2 = cpAX fd1 sf2 + cpXX sf1 (SFArr _ fd2) = cpXA sf1 fd2 + cpXX (SFAcc _ f1 s1 bne) (SFAcc _ f2 s2 cne) = + sfAcc f (s1, s2) (vfyNoEv bne cne) + where + f (s1, s2) a = + case f1 s1 a of + (s1', NoEvent) -> ((s1', s2), cne) + (s1', Event b) -> + let (s2', c) = f2 s2 b in ((s1', s2'), c) + cpXX (SFCpAXA _ fd11 sf12 fd13) (SFCpAXA _ fd21 sf22 fd23) = + cpAXA fd11 (cpXX (cpXA sf12 (fdComp fd13 fd21)) sf22) fd23 + cpXX sf1 sf2 = SF' tf + where + tf dt a = (cpXX sf1' sf2', c) + where + (sf1', b) = (sfTF' sf1) dt a + (sf2', c) = (sfTF' sf2) dt b + + cpAXA :: FunDesc a b -> SF' b c -> FunDesc c d -> SF' a d + cpAXA FDI sf2 fd3 = cpXA sf2 fd3 + cpAXA fd1 sf2 FDI = cpAX fd1 sf2 + cpAXA (FDC b) sf2 fd3 = cpCXA b sf2 fd3 + cpAXA fd1 sf2 (FDC d) = sfConst d + cpAXA fd1 (SFArr _ fd2) fd3 = sfArr (fdComp (fdComp fd1 fd2) fd3) + + cpAX :: FunDesc a b -> SF' b c -> SF' a c + cpAX FDI sf2 = sf2 + cpAX (FDC b) sf2 = cpCX b sf2 + cpAX (FDE f1 f1ne) sf2 = cpEX f1 f1ne sf2 + cpAX (FDG f1) sf2 = cpGX f1 sf2 + + cpXA :: SF' a b -> FunDesc b c -> SF' a c + cpXA sf1 FDI = sf1 + cpXA sf1 (FDC c) = sfConst c + cpXA sf1 (FDE f2 f2ne) = cpXE sf1 f2 f2ne + cpXA sf1 (FDG f2) = cpXG sf1 f2 + + cpCX :: b -> SF' b c -> SF' a c + cpCX b (SFArr _ fd2) = sfConst ((fdFun fd2) b) + cpCX b (SFAcc _ _ _ cne) = sfConst (vfyNoEv b cne) + cpCX b (SFCpAXA _ fd21 sf22 fd23) = + cpCXA ((fdFun fd21) b) sf22 fd23 + cpCX b sf2 = SFCpAXA tf (FDC b) sf2 FDI + where + tf dt _ = (cpCX b sf2', c) + where + (sf2', c) = (sfTF' sf2) dt b + +-- For SPJ: The following version did not work. +-- The commented out one below did work, by lambda-lifting cpCXAux + cpCXA :: b -> SF' b c -> FunDesc c d -> SF' a d + cpCXA b sf2 FDI = cpCX b sf2 + cpCXA _ _ (FDC c) = sfConst c + cpCXA b (sf2 :: SF' b c) (fd3 :: FunDesc c d) = cpCXAAux sf2 + where + f3 = fdFun fd3 + + cpCXAAux :: SF' b c -> SF' a d + cpCXAAux (SFArr _ fd2) = sfConst (f3 ((fdFun fd2) b)) + cpCXAAux (SFAcc _ _ _ cne) = sfConst (vfyNoEv b (f3 cne)) + cpCXAAux (SFCpAXA _ fd21 sf22 fd23) = cpCXA ((fdFun fd21) b) sf22 (fdComp fd23 fd3) + +{- -- For SPJ: This version works + cpCXA :: b -> SF' b c -> FunDesc c d -> SF' a d + cpCXA b sf2 FDI = cpCX b sf2 + cpCXA _ _ (FDC c) = sfConst c + cpCXA b sf2 fd3 = cpCXAAux b fd3 (fdFun fd3) sf2 + where + -- f3 = fdFun fd3 + -- Really something like: cpCXAAux :: SF' b c -> SF' a d + cpCXAAux :: b -> FunDesc c d -> (c -> d) -> SF' b c -> SF' a d + cpCXAAux b fd3 f3 (SFArr _ fd2) = sfConst (f3 ((fdFun fd2) b)) + cpCXAAux b fd3 f3 (SFAcc _ _ _ cne) = sfConst (vfyNoEv b (f3 cne)) + cpCXAAux b fd3 f3 (SFCpAXA _ fd21 sf22 fd23) = cpCXA ((fdFun fd21) b) sf22 (fdComp fd23 fd3) +-} + + cpGX :: (a -> b) -> SF' b c -> SF' a c + cpGX f1 (SFArr _ fd2) = sfArr (fdComp (FDG f1) fd2) + cpGX f1 (SFCpAXA _ fd21 sf22 fd23) = + cpAXA (fdComp (FDG f1) fd21) sf22 fd23 + cpGX f1 sf2 = SFCpAXA tf (FDG f1) sf2 FDI + where + tf dt a = (cpGX f1 sf2', c) + where + (sf2', c) = (sfTF' sf2) dt (f1 a) + + cpXG :: SF' a b -> (b -> c) -> SF' a c + cpXG (SFArr _ fd1) f2 = sfArr (fdComp fd1 (FDG f2)) + cpXG (SFAcc _ f1 s bne) f2 = sfAcc f s (f2 bne) + where + f s a = let (s', b) = f1 s a in (s', f2 b) + cpXG (SFCpAXA _ fd11 sf12 fd22) f2 = + cpAXA fd11 sf12 (fdComp fd22 (FDG f2)) + cpXG sf1 f2 = SFCpAXA tf FDI sf1 (FDG f2) + where + tf dt a = (cpXG sf1' f2, f2 b) + where + (sf1', b) = (sfTF' sf1) dt a + + cpEX :: (Event a -> b) -> b -> SF' b c -> SF' (Event a) c + cpEX f1 f1ne (SFArr _ fd2) = sfArr (fdComp (FDE f1 f1ne) fd2) + cpEX f1 f1ne (SFAcc _ f2 s cne) = sfAcc f s (vfyNoEv f1ne cne) + where + f s a = f2 s (fromEvent (f1 (Event a))) + cpEX f1 f1ne (SFCpAXA _ fd21 sf22 fd23) = + cpAXA (fdComp (FDE f1 f1ne) fd21) sf22 fd23 + cpEX f1 f1ne sf2 = SFCpAXA tf (FDE f1 f1ne) sf2 FDI + where + tf dt ea = (cpEX f1 f1ne sf2', c) + where + (sf2', c) = case ea of + NoEvent -> (sfTF' sf2) dt f1ne + _ -> (sfTF' sf2) dt (f1 ea) + + cpXE :: SF' a (Event b) -> (Event b -> c) -> c -> SF' a c + cpXE (SFArr _ fd1) f2 f2ne = sfArr (fdComp fd1 (FDE f2 f2ne)) + cpXE (SFAcc _ f1 s bne) f2 f2ne = sfAcc f s (vfyNoEv bne f2ne) + where + f s a = let (s', eb) = f1 s a + in + case eb of NoEvent -> (s', f2ne); _ -> (s', f2 eb) + cpXE (SFCpAXA _ fd11 sf12 fd13) f2 f2ne = + cpAXA fd11 sf12 (fdComp fd13 (FDE f2 f2ne)) + cpXE sf1 f2 f2ne = SFCpAXA tf FDI sf1 (FDE f2 f2ne) + where + tf dt a = (cpXE sf1' f2 f2ne, + case eb of NoEvent -> f2ne; _ -> f2 eb) + where + (sf1', eb) = (sfTF' sf1) dt a diff --git a/testsuite/tests/gadt/Session.hs b/testsuite/tests/gadt/Session.hs new file mode 100644 index 0000000000..4403b6f869 --- /dev/null +++ b/testsuite/tests/gadt/Session.hs @@ -0,0 +1,45 @@ +{-# LANGUAGE GADTs, KindSignatures #-} + +-- See Trac #1323; crashed GHC 6.6 + +module Main where + +data Zero = Zero + deriving (Show) + +-- Change this newtype to a data and all's well +-- and it's not like the class restriction actually restricts +-- the type rather than the constructor +newtype Succ p = Succ p deriving (Show) + +class TyNum a where +instance TyNum Zero where +instance (TyNum p) => TyNum (Succ p) where + +data List :: * -> * -> * where + Nil :: List a Zero + Cons :: (TyNum p) => a -> List a p -> List a (Succ p) + +instance (Show a) => Show (List a l) where + show Nil = "Nil" + show (Cons a t) = "Cons " ++ (show a) ++ " (" ++ (show t) ++ ")" + +zipL :: List a l -> List b l -> List (a, b) l +zipL Nil Nil = Nil -- this line is fine +zipL (Cons l ls) (Cons r rs) = Cons (l,r) (zipL ls rs) -- this line blows up + +l1 = Cons 5 (Cons 3 Nil) +l2 = Cons True (Cons False Nil) + +main = print $ zipL l1 l2 + +{- +$ ghc --make Test.hs +[1 of 1] Compiling Main ( Test.hs, Test.o ) +ghc-6.6: panic! (the 'impossible' happened) + (GHC version 6.6 for x86_64-unknown-linux): + Pattern match failure in do expression at simplCore/Simplify.lhs:1540:8-21 + +Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug +-} + diff --git a/testsuite/tests/gadt/Session.stdout b/testsuite/tests/gadt/Session.stdout new file mode 100644 index 0000000000..e07f8c1c64 --- /dev/null +++ b/testsuite/tests/gadt/Session.stdout @@ -0,0 +1 @@ +Cons (5,True) (Cons (3,False) (Nil)) diff --git a/testsuite/tests/gadt/T1999.hs b/testsuite/tests/gadt/T1999.hs new file mode 100644 index 0000000000..70f8531d17 --- /dev/null +++ b/testsuite/tests/gadt/T1999.hs @@ -0,0 +1,12 @@ +{-# LANGUAGE FlexibleContexts, FlexibleInstances, GADTs #-} + +module Bug where + +class C a where + f :: G a -> () + +instance (C ()) => C (b c) where + f (G x) = f x where + +data G a where + G :: G () -> G (b c) diff --git a/testsuite/tests/gadt/T1999a.hs b/testsuite/tests/gadt/T1999a.hs new file mode 100644 index 0000000000..d8dbc077b9 --- /dev/null +++ b/testsuite/tests/gadt/T1999a.hs @@ -0,0 +1,10 @@ +{-# LANGUAGE GADTs #-} +-- Trac #1999 + +module ShouldCompile where + +data EqTypes a b where + EqConstr :: EqTypes a b -> EqTypes (s a) (s b) + +eqUnConstr :: EqTypes (s a) (s b) -> EqTypes a b +eqUnConstr (EqConstr eq) = eq
\ No newline at end of file diff --git a/testsuite/tests/gadt/T2040.hs b/testsuite/tests/gadt/T2040.hs new file mode 100644 index 0000000000..2ff4777523 --- /dev/null +++ b/testsuite/tests/gadt/T2040.hs @@ -0,0 +1,27 @@ +{-# LANGUAGE GADTs, ScopedTypeVariables, FlexibleContexts, + MultiParamTypeClasses #-} +{-# OPTIONS_GHC -Wall #-} + +module T2040 where + +data Teq a b where Teq :: Teq a a + +class C a b where proof :: Teq a b + +data S a = S a + +data W b where + -- This would make every version of GHC happy + -- W :: (C a c , c ~ S b) => W a -> W c + W :: C a (S b) => W a -> W (S b) + +foo :: W (S ()) -> W (S ()) -> () +foo (W (_ :: W a1)) (W (_ :: W a2)) = + case proof :: Teq a1 (S ()) of + Teq -> () + +foo2 :: W (S ()) -> W (S ()) -> () +foo2 (W (_ :: W a1)) (W (_ :: W a2)) = + case proof :: Teq a1 (S ()) of + Teq -> case proof :: Teq a2 (S ()) of + Teq -> ()
\ No newline at end of file diff --git a/testsuite/tests/gadt/T2151.hs b/testsuite/tests/gadt/T2151.hs new file mode 100644 index 0000000000..339d231e80 --- /dev/null +++ b/testsuite/tests/gadt/T2151.hs @@ -0,0 +1,13 @@ +{-# LANGUAGE GADTs #-} + +module T2151 where + +data Type a where + Func :: Type a -> Type b -> Type (a -> b) + PF :: Type a -> Type (PF a) + +data PF a where + ID :: PF (a -> a) + +test :: Type a -> a -> a +test (PF (Func _ _)) ID = ID diff --git a/testsuite/tests/gadt/T2587.hs b/testsuite/tests/gadt/T2587.hs new file mode 100644 index 0000000000..bcd0a443ac --- /dev/null +++ b/testsuite/tests/gadt/T2587.hs @@ -0,0 +1,18 @@ +{-# LANGUAGE GADTs, ExistentialQuantification #-}
+{-# OPTIONS_GHC -O -fno-warn-overlapping-patterns #-}
+
+-- Trac #2587
+-- Actually this bug related to free variables and
+-- type lets, but ostensibly it has a GADT flavour
+-- Hence being in the GADT directory.
+
+module GadtBug(bug) where
+
+data Existential = forall a . Existential (Gadt a)
+
+data Gadt a where Value :: Gadt Double
+
+bug = [ match undefined | ps <- undefined, _ <- ps ]
+ where
+ match (Existential _) = undefined
+ match (Existential _) = undefined
diff --git a/testsuite/tests/gadt/T3013.hs b/testsuite/tests/gadt/T3013.hs new file mode 100644 index 0000000000..3b123a0d80 --- /dev/null +++ b/testsuite/tests/gadt/T3013.hs @@ -0,0 +1,13 @@ +{-# LANGUAGE GADTs #-} +-- Trac 3013. +-- This isn't strictly a GADT test, but it uses GADT syntax + +module T3013 where + +data T where + A, B :: T + C :: T + D, E :: Int -> T + +f :: T -> T +f A = D 3 diff --git a/testsuite/tests/gadt/T3163.hs b/testsuite/tests/gadt/T3163.hs new file mode 100644 index 0000000000..13e5ff7de6 --- /dev/null +++ b/testsuite/tests/gadt/T3163.hs @@ -0,0 +1,9 @@ +{-# LANGUAGE GADTs, RankNTypes, ImpredicativeTypes #-} + +-- Test Trac #3163 + +module Report where + +data Taker a where + Unreached :: Taker (forall s. s) + diff --git a/testsuite/tests/gadt/T3163.stderr b/testsuite/tests/gadt/T3163.stderr new file mode 100644 index 0000000000..e60ffcc47c --- /dev/null +++ b/testsuite/tests/gadt/T3163.stderr @@ -0,0 +1,5 @@ + +T3163.hs:8:5: + Illegal polymorphic or qualified type: forall s. s + In the definition of data constructor `Unreached' + In the data type declaration for `Taker' diff --git a/testsuite/tests/gadt/T3169.hs b/testsuite/tests/gadt/T3169.hs new file mode 100644 index 0000000000..b52ec2cf87 --- /dev/null +++ b/testsuite/tests/gadt/T3169.hs @@ -0,0 +1,16 @@ +{-# LANGUAGE TypeFamilies, ScopedTypeVariables #-} +module T3169 where + +import Prelude hiding ( lookup ) + +class Key k where + type Map k :: * -> * + lookup :: k -> Map k elt -> Maybe elt + +instance (Key a, Key b) => Key (a,b) where + type Map (a,b) = MP a b + lookup (a,b) (m :: Map (a,b) elt) + = case lookup a m :: Maybe (Map b elt) of + Just (m2 :: Map b elt) -> lookup b m2 :: Maybe elt + +data MP a b elt = MP (Map a (Map b elt)) diff --git a/testsuite/tests/gadt/T3169.stderr b/testsuite/tests/gadt/T3169.stderr new file mode 100644 index 0000000000..100077066c --- /dev/null +++ b/testsuite/tests/gadt/T3169.stderr @@ -0,0 +1,11 @@ + +T3169.hs:13:13: + Couldn't match type `elt' with `Map b elt' + `elt' is a rigid type variable bound by + the type signature for + lookup :: (a, b) -> Map (a, b) elt -> Maybe elt + at T3169.hs:12:3 + Expected type: Maybe (Map b elt) + Actual type: Maybe elt + In the return type of a call of `lookup' + In the expression: lookup a m :: Maybe (Map b elt) diff --git a/testsuite/tests/gadt/T3638.hs b/testsuite/tests/gadt/T3638.hs new file mode 100644 index 0000000000..abb6a86169 --- /dev/null +++ b/testsuite/tests/gadt/T3638.hs @@ -0,0 +1,10 @@ +{-# LANGUAGE GADTs #-} + +module T3638 where + +data T a where TInt :: T Int + +foo :: T Int -> Int +foo TInt = 0 + +{-# RULES "foo" forall x. foo x = case x of { TInt -> 0 } #-} diff --git a/testsuite/tests/gadt/T3651.hs b/testsuite/tests/gadt/T3651.hs new file mode 100644 index 0000000000..9f671905c8 --- /dev/null +++ b/testsuite/tests/gadt/T3651.hs @@ -0,0 +1,17 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE TypeFamilies #-} + +module T3651 where + +data Z a where + U :: Z () + B :: Z Bool + +unsafe1 :: Z a -> Z a -> a +unsafe1 B U = () + +unsafe2 :: a ~ b => Z b -> Z a -> a +unsafe2 B U = () + +unsafe3 :: a ~ b => Z a -> Z b -> a +unsafe3 B U = True diff --git a/testsuite/tests/gadt/T3651.stderr b/testsuite/tests/gadt/T3651.stderr new file mode 100644 index 0000000000..d15e27aefa --- /dev/null +++ b/testsuite/tests/gadt/T3651.stderr @@ -0,0 +1,21 @@ + +T3651.hs:11:11: + Couldn't match type `()' with `Bool' + Inaccessible code in + a pattern with constructor U :: Z (), in an equation for `unsafe1' + In the pattern: U + In an equation for `unsafe1': unsafe1 B U = () + +T3651.hs:14:11: + Couldn't match type `()' with `Bool' + Inaccessible code in + a pattern with constructor U :: Z (), in an equation for `unsafe2' + In the pattern: U + In an equation for `unsafe2': unsafe2 B U = () + +T3651.hs:17:11: + Couldn't match type `()' with `Bool' + Inaccessible code in + a pattern with constructor U :: Z (), in an equation for `unsafe3' + In the pattern: U + In an equation for `unsafe3': unsafe3 B U = True diff --git a/testsuite/tests/gadt/all.T b/testsuite/tests/gadt/all.T new file mode 100644 index 0000000000..83f0836e55 --- /dev/null +++ b/testsuite/tests/gadt/all.T @@ -0,0 +1,110 @@ +setTestOpts(only_compiler_types(['ghc'])) + +# setTestOpts(only_ways(['normal'])); +# Not only-normal: want optimisation too, to check coercion optimiser + +# In fast mode, we omit all the compile_and_run tests except a couple + +test('gadt1', normal, compile, ['']) +test('gadt2', skip_if_fast, compile_and_run, ['']) +test('gadt3', normal, compile, ['']) +test('gadt4', skip_if_fast, compile_and_run, ['']) +test('gadt5', skip_if_fast, compile_and_run, ['']) +test('gadt6', normal, compile, ['']) +test('gadt7', normal, compile, ['']) +test('gadt8', normal, compile, ['']) +test('gadt9', normal, compile, ['']) +test('gadt10', normal, compile_fail, ['']) +test('gadt11', normal, compile_fail, ['']) +test('gadt13', normal, compile, ['']) +test('gadt14', normal, compile, ['']) +test('gadt15', normal, compile, ['']) +test('gadt16', normal, compile, ['']) + +test('gadt17', + extra_clean(['Gadt17_help.hi', 'Gadt17_help.o']), + run_command, + ['$MAKE -s --no-print-directory gadt17']) + +test('gadt18', normal, compile, ['']) +test('gadt19', normal, compile, ['']) +test('gadt20', normal, compile, ['']) +test('gadt21', normal, compile_fail, ['']) +test('gadt22', normal, compile, ['']) + +test('gadt23', + extra_clean(['Gadt23_AST.hi', 'Gadt23_AST.o']), + run_command, + ['$MAKE -s --no-print-directory gadt23']) + +test('gadt24', normal, compile, ['']) + +test('red-black', normal, compile, ['']) +test('type-rep', skip_if_fast, compile_and_run, ['']) +test('equal', normal, compile, ['']) +test('nbe', normal, compile, ['']) +test('while', normal, compile_and_run, ['']) +test('rw', normal, compile_fail, ['']) +test('lazypat', normal, compile_fail, ['']) +test('lazypatok', expect_fail, compile, ['']) +test('tc', normal, compile_and_run, ['']) +test('arrow', normal, compile, ['']) +test('tdpe', normal, compile, ['']) +test('Nilsson', skip_if_fast, compile, ['']) + +if config.fast: + test('records', normal, compile, ['']) +else: + test('records', normal, compile_and_run, ['']) +test('ubx-records', skip_if_fast, compile_and_run, ['']) +test('records-fail1', normal, compile_fail, ['']) + +test('doaitse', normal, compile, ['']) +test('josef', normal, compile, ['']) + +# Interaction of fundeps with GADTs doesn't work well +test('gadt-fd', expect_broken(345), compile, ['']) + +test('karl1', normal, compile, ['']) +test('karl2', normal, compile, ['']) +test('data1', normal, compile, ['']) +test('data2', normal, compile, ['']) + +test('termination', normal, compile, ['']) +test('set', normal, compile, ['']) +test('scoped', normal, compile, ['']) +test('gadt-escape1', normal, compile, ['']) + +# New ones from Dimitrios + +# test('gadt-dim1', normal, compile, ['']) +# test('gadt-dim2', normal, compile_fail, ['']) +# test('gadt-dim3', normal, compile_fail, ['']) +# test('gadt-dim4', normal, compile, ['']) +# test('gadt-dim5', normal, compile, ['']) +# test('gadt-dim6', normal, compile, ['']) +# test('gadt-dim7', normal, compile, ['']) +# test('gadt-dim8', normal, compile, ['']) +# test('Arith', normal, compile, ['']) + +test('Session', normal, compile_and_run, ['']) +test('CasePrune', normal, compile_and_run, ['']) + +test('T1999', normal, compile, ['']) +test('T1999a', expect_broken(1999), compile, ['']) + +test('T2587', normal, compile, ['']) +test('T2040', normal, compile, ['']) +test('T2151', normal, compile, ['']) +test('T3013', normal, compile, ['']) +test('T3163', normal, compile_fail, ['']) +test('gadt25', normal, compile, ['']) +test('T3651', normal, compile_fail, ['']) +test('T3638', normal, compile, ['']) + +test('gadtSyntax001', if_compiler_lt('ghc', '7.1', expect_fail), compile, ['']) +test('gadtSyntaxFail001', if_compiler_lt('ghc', '7.1', expect_fail), compile_fail, ['']) +test('gadtSyntaxFail002', if_compiler_lt('ghc', '7.1', expect_fail), compile_fail, ['']) +test('gadtSyntaxFail003', if_compiler_lt('ghc', '7.1', expect_fail), compile_fail, ['']) +test('T3169', normal, compile_fail, ['']) + diff --git a/testsuite/tests/gadt/arrow.hs b/testsuite/tests/gadt/arrow.hs new file mode 100644 index 0000000000..1abc535a0b --- /dev/null +++ b/testsuite/tests/gadt/arrow.hs @@ -0,0 +1,24 @@ +{-# LANGUAGE GADTs #-} + +module Opt where +import Control.Arrow +import Control.Category +import Prelude hiding (id, (.)) + +data Opt arr a b where + Lift :: arr a b -> Opt arr a b + First :: Opt arr a b -> Opt arr (a,c) (b,c) + +runOpt :: Arrow arr => Opt arr a b -> arr a b +runOpt (Lift f) = f +runOpt (First f) = first (runOpt f) + +instance Arrow arr => Category (Opt arr) where + id = Lift id + First f . First g = First (f . g) + f . g = Lift (runOpt f . runOpt g) + +instance Arrow arr => Arrow (Opt arr) where + arr = Lift . arr + + first = First diff --git a/testsuite/tests/gadt/data1.hs b/testsuite/tests/gadt/data1.hs new file mode 100644 index 0000000000..9dac84000e --- /dev/null +++ b/testsuite/tests/gadt/data1.hs @@ -0,0 +1,17 @@ +{-# LANGUAGE GADTs #-}
+
+-- Trac #289
+
+module ShouldCompile where
+
+class C a where
+ f :: a -> Bool
+
+data T a where
+ MkT :: (C a) => a -> T a
+
+tf1 :: T Int -> Bool
+tf1 (MkT aa) = f aa
+
+tf2 :: T a -> Bool
+tf2 (MkT aa) = f aa
diff --git a/testsuite/tests/gadt/data2.hs b/testsuite/tests/gadt/data2.hs new file mode 100644 index 0000000000..5b8a009d05 --- /dev/null +++ b/testsuite/tests/gadt/data2.hs @@ -0,0 +1,19 @@ +{-# LANGUAGE GADTs, ExistentialQuantification #-}
+
+-- Trac #289
+
+module ShouldCompile where
+
+class Foo a where
+ foo :: a -> Int
+
+data T = forall a. T (G a)
+data G a where
+ A :: G a
+ B :: Foo a => a -> G a
+
+doFoo :: T -> Int
+doFoo (T A) = 2
+doFoo (T (B x)) = foo x
+
+
diff --git a/testsuite/tests/gadt/doaitse.hs b/testsuite/tests/gadt/doaitse.hs new file mode 100644 index 0000000000..51525bb573 --- /dev/null +++ b/testsuite/tests/gadt/doaitse.hs @@ -0,0 +1,55 @@ +{-# LANGUAGE GADTs, ExistentialQuantification, ScopedTypeVariables, + Rank2Types #-} + +-- 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,()) + ) + diff --git a/testsuite/tests/gadt/equal.hs b/testsuite/tests/gadt/equal.hs new file mode 100644 index 0000000000..b6c0bf572e --- /dev/null +++ b/testsuite/tests/gadt/equal.hs @@ -0,0 +1,30 @@ +{-# LANGUAGE GADTs #-} + +module ShouldCompile where + +data Rep t where + Rint :: Rep Int + Rchar :: Rep Char + Runit :: Rep () + Rpair :: Rep a -> Rep b -> Rep (a,b) + Rsum :: Rep a -> Rep b -> Rep (Either a b) + Rcon :: String -> Rep t -> Rep t + +data Equal a b where + Eq :: Equal c c + +test :: Rep a -> Rep b -> Maybe (Equal a b) +test Rint Rint = return Eq +test Rchar Rchar = return Eq +test Runit Runit = return Eq +test (Rpair x y) (Rpair a b) + = do { Eq <- test x a; Eq <- test y b; return Eq } +test (Rsum x y) (Rsum a b) + = do { Eq <- test x a; Eq <- test y b; return Eq } +test (Rcon s1 x) (Rcon s2 y) + = if s1==s2 then test x y else Nothing +test _ _ = Nothing + +f :: Equal a b -> a -> b -> b +f Eq x y = x + diff --git a/testsuite/tests/gadt/gadt-dim1.hs b/testsuite/tests/gadt/gadt-dim1.hs new file mode 100644 index 0000000000..641f04d0e6 --- /dev/null +++ b/testsuite/tests/gadt/gadt-dim1.hs @@ -0,0 +1,11 @@ +{-# LANGUAGE GADTs #-} + +module ShouldCompile where + +data T a where + C :: Int -> T Int + D :: Bool -> T Bool + +foo :: T a -> a +foo (C x) = x +foo (D x) = x diff --git a/testsuite/tests/gadt/gadt-dim2.hs b/testsuite/tests/gadt/gadt-dim2.hs new file mode 100644 index 0000000000..239275b42d --- /dev/null +++ b/testsuite/tests/gadt/gadt-dim2.hs @@ -0,0 +1,11 @@ +{-# LANGUAGE GADTs #-} + +module ShouldFail2 where + +data T a where + C :: Int -> T Int + D :: Bool -> T Bool + +-- should fail because variable is wobbly +foo (C x) = x +foo (D b) = b diff --git a/testsuite/tests/gadt/gadt-dim3.hs b/testsuite/tests/gadt/gadt-dim3.hs new file mode 100644 index 0000000000..ae43147c92 --- /dev/null +++ b/testsuite/tests/gadt/gadt-dim3.hs @@ -0,0 +1,25 @@ +{-# LANGUAGE GADTs #-} + +module ShouldSucceed5 where + + +data T a where + C :: T Bool + D :: T Int + + +data Y a where + E :: Y Bool + + +-- should succeed, the first branch is simply inaccessible +foo :: T Bool -> Bool +foo (D) = True +foo (C) = False + +-- should succeed, the branch is inaccessible and not even type checked +baz :: Y Int -> Int +baz (E) = "dimitris!" + +-- should fail => it is an attempt to call an inaccessible branch +test = baz (E) diff --git a/testsuite/tests/gadt/gadt-dim4.hs b/testsuite/tests/gadt/gadt-dim4.hs new file mode 100644 index 0000000000..feb16c7de1 --- /dev/null +++ b/testsuite/tests/gadt/gadt-dim4.hs @@ -0,0 +1,21 @@ +{-# LANGUAGE GADTs #-} + +module ShouldSucceed1 where + +data T1 a where + C :: (T2 b) -> b -> T1 Int + D :: Bool -> T1 Bool + + -- should this work? +data T2 a where + F :: Int -> T2 Int + + +-- Should work, even though we start as wobbly +-- the existential makes us rigid again +foo x = case x of + C (F _) z -> (z + 1) + + + + diff --git a/testsuite/tests/gadt/gadt-dim5.hs b/testsuite/tests/gadt/gadt-dim5.hs new file mode 100644 index 0000000000..126cc710df --- /dev/null +++ b/testsuite/tests/gadt/gadt-dim5.hs @@ -0,0 +1,13 @@ +{-# LANGUAGE GADTs #-} + +module ShouldSucceed2 where + +data T a where + C :: Int -> T Int + D :: Bool -> T Bool + + +foo :: T a -> a +foo (C x) = x + 1 +foo (D x) = True + diff --git a/testsuite/tests/gadt/gadt-dim6.hs b/testsuite/tests/gadt/gadt-dim6.hs new file mode 100644 index 0000000000..a8075e225b --- /dev/null +++ b/testsuite/tests/gadt/gadt-dim6.hs @@ -0,0 +1,13 @@ +{-# LANGUAGE GADTs #-} + +module ShouldSucceed3 where + + +data T a where + C :: T b -> b -> T Int + D :: T Bool + +-- Tests scoped annotations +foo :: T a -> a -> a +foo (C y (x::b)) (z::a) = z + 1 + diff --git a/testsuite/tests/gadt/gadt-dim7.hs b/testsuite/tests/gadt/gadt-dim7.hs new file mode 100644 index 0000000000..0ea3633fa3 --- /dev/null +++ b/testsuite/tests/gadt/gadt-dim7.hs @@ -0,0 +1,24 @@ +{-# LANGUAGE GADTs #-} + +module ShouldSucceed4 where + +data Z +data S a + + +data Add n m r where + PZero :: Add Z m m + PSucc :: Add n m p -> Add (S n) m (S p) + + +data XList n a where + XNil :: XList Z a + XCons :: a -> XList n a -> XList (S n) a + + +-- simple safe append function +append :: (Add n m r) -> XList n a -> XList m a -> XList r a +append PZero XNil l = l +append (PSucc prf) (XCons x xs) l = XCons x (append prf xs l) + + diff --git a/testsuite/tests/gadt/gadt-dim8.hs b/testsuite/tests/gadt/gadt-dim8.hs new file mode 100644 index 0000000000..9735c73fdf --- /dev/null +++ b/testsuite/tests/gadt/gadt-dim8.hs @@ -0,0 +1,26 @@ +{-# LANGUAGE GADTs #-} + +module ShouldSucceed5 where + + +data T a where + C :: T Bool + D :: T Int + + +data Y a where + E :: T Bool + + +-- should succeed, the first branch is simply inaccessible +foo :: T Bool -> Bool +foo (D) = True +foo (C) = False + +-- should succeed, the branch is inaccessible and not een type checked +baz :: Y Int -> Int +baz (E) = "dimitris!" + + + + diff --git a/testsuite/tests/gadt/gadt-escape1.hs b/testsuite/tests/gadt/gadt-escape1.hs new file mode 100644 index 0000000000..4ff33b299b --- /dev/null +++ b/testsuite/tests/gadt/gadt-escape1.hs @@ -0,0 +1,20 @@ +{-# LANGUAGE GADTs, ExistentialQuantification #-} + +module Escape where + +data ExpGADT t where + ExpInt :: Int -> ExpGADT Int + +data Hidden = forall t . Hidden (ExpGADT t) (ExpGADT t) + +hval = Hidden (ExpInt 0) (ExpInt 1) + +-- With the type sig this is ok, but without it maybe +-- should be rejected becuase the result type is wobbly +-- weird1 :: ExpGADT Int + +weird1 = case (hval :: Hidden) of Hidden (ExpInt _) a -> a + -- Hidden t (ExpInt (co :: t ~ Int) _ :: ExpGADT t) (a :: ExpGADT t) + +weird2 :: ExpGADT Int +weird2 = case (hval :: Hidden) of Hidden (ExpInt _) a -> a diff --git a/testsuite/tests/gadt/gadt-escape1.stderr b/testsuite/tests/gadt/gadt-escape1.stderr new file mode 100644 index 0000000000..e69de29bb2 --- /dev/null +++ b/testsuite/tests/gadt/gadt-escape1.stderr diff --git a/testsuite/tests/gadt/gadt-fd.hs b/testsuite/tests/gadt/gadt-fd.hs new file mode 100644 index 0000000000..4db7b62889 --- /dev/null +++ b/testsuite/tests/gadt/gadt-fd.hs @@ -0,0 +1,23 @@ +{-# LANGUAGE GADTs #-}
+
+-- Trac #345
+
+module ShouldCompile where
+
+data Succ n
+data Zero
+
+class Plus x y z | x y -> z
+instance Plus Zero x x
+instance Plus x y z => Plus (Succ x) y (Succ z)
+
+infixr 5 :::
+
+data List :: * -> * -> * where
+ Nil :: List a Zero
+ (:::) :: a -> List a n -> List a (Succ n)
+
+append :: Plus x y z => List a x -> List a y -> List a z
+append Nil ys = ys
+append (x ::: xs) ys = x ::: append xs ys
+
diff --git a/testsuite/tests/gadt/gadt1.hs b/testsuite/tests/gadt/gadt1.hs new file mode 100644 index 0000000000..3412d90cf2 --- /dev/null +++ b/testsuite/tests/gadt/gadt1.hs @@ -0,0 +1,7 @@ +{-# LANGUAGE GADTs, Rank2Types #-} + +module ShouldCompile where + +-- Checks for bindInstsOfPatId +f :: (forall a. Eq a => a -> a) -> Bool +f g = g True
\ No newline at end of file diff --git a/testsuite/tests/gadt/gadt10.hs b/testsuite/tests/gadt/gadt10.hs new file mode 100644 index 0000000000..6217405a0b --- /dev/null +++ b/testsuite/tests/gadt/gadt10.hs @@ -0,0 +1,6 @@ +{-# LANGUAGE GADTs #-} + +module ShouldFail where + +-- Kind error +data RInt a where R :: RInt diff --git a/testsuite/tests/gadt/gadt10.stderr b/testsuite/tests/gadt/gadt10.stderr new file mode 100644 index 0000000000..100c84bab7 --- /dev/null +++ b/testsuite/tests/gadt/gadt10.stderr @@ -0,0 +1,7 @@ + +gadt10.hs:6:24: + `RInt' is not applied to enough type arguments + Expected kind `?', but `RInt' has kind `k0 -> *' + In the type `RInt' + In the definition of data constructor `R' + In the data type declaration for `RInt' diff --git a/testsuite/tests/gadt/gadt11.hs b/testsuite/tests/gadt/gadt11.hs new file mode 100644 index 0000000000..a5000442fa --- /dev/null +++ b/testsuite/tests/gadt/gadt11.hs @@ -0,0 +1,12 @@ +{-# LANGUAGE GADTs #-} + +module ShouldFail where + +-- Wrong return type +data X f = X (f ()) + +data B a where + B1 :: X [] + B2 :: B [Int] + + diff --git a/testsuite/tests/gadt/gadt11.stderr b/testsuite/tests/gadt/gadt11.stderr new file mode 100644 index 0000000000..721b148495 --- /dev/null +++ b/testsuite/tests/gadt/gadt11.stderr @@ -0,0 +1,6 @@ + +gadt11.hs:9:3: + Data constructor `B1' returns type `X []' + instead of an instance of its parent type `B a' + In the definition of data constructor `B1' + In the data type declaration for `B' diff --git a/testsuite/tests/gadt/gadt13.hs b/testsuite/tests/gadt/gadt13.hs new file mode 100644 index 0000000000..bd25262ca6 --- /dev/null +++ b/testsuite/tests/gadt/gadt13.hs @@ -0,0 +1,14 @@ +{-# LANGUAGE GADTs #-} + +-- This should fail, because there is no annotation on shw, +-- but it succeeds in 6.4.1 + +module ShouldFail where + +data Term a where + B :: Bool -> Term Bool + I :: Int -> Term Int + +shw (I t) = ("I "++) . shows t +-- shw (B t) = ("B "++) . shows t + diff --git a/testsuite/tests/gadt/gadt13.stderr b/testsuite/tests/gadt/gadt13.stderr new file mode 100644 index 0000000000..e69de29bb2 --- /dev/null +++ b/testsuite/tests/gadt/gadt13.stderr diff --git a/testsuite/tests/gadt/gadt14.hs b/testsuite/tests/gadt/gadt14.hs new file mode 100644 index 0000000000..c5bdbcb5de --- /dev/null +++ b/testsuite/tests/gadt/gadt14.hs @@ -0,0 +1,8 @@ +{-# LANGUAGE GADTs #-}
+
+-- Check that trailing parens are ok in data con signatures
+
+module ShouldCompile where
+
+data T where
+ MkT :: Int -> (Int -> T)
diff --git a/testsuite/tests/gadt/gadt15.hs b/testsuite/tests/gadt/gadt15.hs new file mode 100644 index 0000000000..c6d3cc9442 --- /dev/null +++ b/testsuite/tests/gadt/gadt15.hs @@ -0,0 +1,11 @@ +{-# LANGUAGE GADTs #-} + +-- Triggered a desugaring bug in earlier verison + +module Shouldcompile where + +data T a where + T1 :: Int -> T Int + +f :: (T a, a) -> Int +f (T1 x, z) = z diff --git a/testsuite/tests/gadt/gadt16.hs b/testsuite/tests/gadt/gadt16.hs new file mode 100644 index 0000000000..133c833903 --- /dev/null +++ b/testsuite/tests/gadt/gadt16.hs @@ -0,0 +1,47 @@ +{-# LANGUAGE GADTs #-} + +{- This code, courtesy of Markus Lauer (markus.lauer-2006@lauerit.de) + was rejected by the sophisticated wobbly-type impl in 6.4.1, and + with a terrible error message: + Sample.hs:22:40: + Couldn't match `MayFail' against `MayFail' + Expected type: Result s b + Inferred type: Result MayFail a + In the first argument of `Return', namely `Fail' + In a case alternative: Fail -> return Fail + + Strangely it is accepted by the simplified impl in GHC 6.5. -} + +module Sample where + +data Safe +data MayFail + +data Result s a where + Ok :: a -> Result s a + Fail :: Result MayFail a + +newtype M s a = M { unM :: IO (Result s a) } + +instance Monad (M s) where + + return x = M (return (Ok x)) + + {- this one gives a type error in 6.4.1 -} + M m >>= k = M (do res <- m + case res of + Ok x -> unM (k x) + Fail -> return Fail + ) + + {- while this one works -} + -- M m >>= k = M (f m (unM . k)) + -- where + -- f :: IO (Result s a) -> (a -> IO (Result s b)) -> IO (Result s b) + -- f m k = do res <- m + -- case res of + -- Ok x -> k x + -- Fail -> return Fail + + + diff --git a/testsuite/tests/gadt/gadt17.hs b/testsuite/tests/gadt/gadt17.hs new file mode 100644 index 0000000000..acef8100dc --- /dev/null +++ b/testsuite/tests/gadt/gadt17.hs @@ -0,0 +1,14 @@ +{-# LANGUAGE GADTs #-} +{-# OPTIONS_GHC -O #-} + +-- This one showed up a bug that required type refinement in TcIface +-- See the call to coreRefineTys in TcIface +-- +-- Tests for bug: http://hackage.haskell.org/trac/ghc/ticket/685 + +module ShouldCompile where + +import Gadt17_help ( TernOp (..), applyTernOp ) + +liftTernOpObs :: TernOp a b c d -> a -> b -> c -> d +liftTernOpObs op x y z = applyTernOp op x y z diff --git a/testsuite/tests/gadt/gadt18.hs b/testsuite/tests/gadt/gadt18.hs new file mode 100644 index 0000000000..4ac12efa84 --- /dev/null +++ b/testsuite/tests/gadt/gadt18.hs @@ -0,0 +1,18 @@ +{-# LANGUAGE GADTs #-}
+-- A simple GADT test from Roman
+-- which nevertheless showed up a bug at one stage
+
+module ShouldCompile where
+
+data T a where
+ T1 :: () -> T ()
+ T2 :: T a -> T b -> T (a,b)
+
+class C a where
+ f :: T a -> a
+
+instance C () where
+ f (T1 x) = x
+
+instance (C a, C b) => C (a,b) where
+ f (T2 x y) = (f x, f y)
diff --git a/testsuite/tests/gadt/gadt19.hs b/testsuite/tests/gadt/gadt19.hs new file mode 100644 index 0000000000..34b0d291b5 --- /dev/null +++ b/testsuite/tests/gadt/gadt19.hs @@ -0,0 +1,16 @@ +{-# LANGUAGE GADTs #-} + +-- Involves an equality that is not an existential + +module Foo2 where + +data T t a where + T :: a -> T () a + +foo :: (a -> a) -> T t a -> T t a +foo f (T x) = T (f x) + +bar :: T t Int -> T t Int +bar t@(T _) = foo (+1) t + + diff --git a/testsuite/tests/gadt/gadt2.hs b/testsuite/tests/gadt/gadt2.hs new file mode 100644 index 0000000000..886b702ce7 --- /dev/null +++ b/testsuite/tests/gadt/gadt2.hs @@ -0,0 +1,18 @@ +{-# LANGUAGE ExplicitForAll,GADTs #-} + +-- Pattern match uses dictionaries bound higher up in the pattern + +module Main where + +data T = forall a. Integral a => T a + +f :: T -> Bool +f (T 0) = True +f (T n) = False + +g :: T -> Ordering +g (T n) | n >= 3 = if n>3 then GT else EQ +g (T n) = LT + +main = do print [f (T 0), f (T 1)] + print [g (T 2), g (T 3), g (T 4)] diff --git a/testsuite/tests/gadt/gadt2.stdout b/testsuite/tests/gadt/gadt2.stdout new file mode 100644 index 0000000000..75df5cd9a1 --- /dev/null +++ b/testsuite/tests/gadt/gadt2.stdout @@ -0,0 +1,2 @@ +[True,False] +[LT,EQ,GT] diff --git a/testsuite/tests/gadt/gadt20.hs b/testsuite/tests/gadt/gadt20.hs new file mode 100644 index 0000000000..c754831ce5 --- /dev/null +++ b/testsuite/tests/gadt/gadt20.hs @@ -0,0 +1,19 @@ +{-# LANGUAGE GADTs, KindSignatures #-} + +-- Test for trac #810 +-- Should be able to infer bool :: Bool and integer :: Integer, so +-- we should know that they both have Show instances. + +module Foo where + +data Pair :: (* -> *) -> * where + Pair :: a b -> b -> Pair a + +data Sel :: * -> * where + A :: Sel Bool + B :: Sel Integer + +showSnd :: Pair Sel -> String +showSnd (Pair A bool) = show bool +showSnd (Pair B integer) = show integer + diff --git a/testsuite/tests/gadt/gadt21.hs b/testsuite/tests/gadt/gadt21.hs new file mode 100644 index 0000000000..b452d083c1 --- /dev/null +++ b/testsuite/tests/gadt/gadt21.hs @@ -0,0 +1,23 @@ +{-# LANGUAGE GADTs, ExistentialQuantification, KindSignatures, Rank2Types #-} + +-- Fails (needs the (Ord a) in TypeSet +-- c.f. gadt22.hs + +module Expr where + +import Data.Set (Set) + +data Type a where + TypeInt :: Type Int + TypeSet :: {- Ord a => -} Type a -> Type (Set a) + TypeFun :: Type a -> Type b -> Type (a -> b) + +data Expr :: * -> * where + Const :: Type a -> a -> Expr a + +data DynExpr = forall a. DynExpr (Expr a) + +withOrdDynExpr :: DynExpr -> (forall a. Ord a => Expr a -> b) -> Maybe b +withOrdDynExpr (DynExpr e@(Const (TypeSet _) _)) f = Just (f e) +withOrdDynExpr (DynExpr e@(Const TypeInt _)) f = Just (f e) +withOrdDynExpr _ _ = Nothing diff --git a/testsuite/tests/gadt/gadt21.stderr b/testsuite/tests/gadt/gadt21.stderr new file mode 100644 index 0000000000..061c563465 --- /dev/null +++ b/testsuite/tests/gadt/gadt21.stderr @@ -0,0 +1,20 @@ + +gadt21.hs:21:60: + Could not deduce (Ord a1) arising from a use of `f' + from the context (a ~ Set a1) + bound by a pattern with constructor + TypeSet :: forall a. Type a -> Type (Set a), + in an equation for `withOrdDynExpr' + at gadt21.hs:21:35-43 + Possible fix: + add (Ord a1) to the context of + the data constructor `TypeSet' + or the data constructor `DynExpr' + or the type signature for + withOrdDynExpr :: DynExpr + -> (forall a. Ord a => Expr a -> b) + -> Maybe b + In the first argument of `Just', namely `(f e)' + In the expression: Just (f e) + In an equation for `withOrdDynExpr': + withOrdDynExpr (DynExpr e@(Const (TypeSet _) _)) f = Just (f e) diff --git a/testsuite/tests/gadt/gadt22.hs b/testsuite/tests/gadt/gadt22.hs new file mode 100644 index 0000000000..f456198ff1 --- /dev/null +++ b/testsuite/tests/gadt/gadt22.hs @@ -0,0 +1,26 @@ +{-# LANGUAGE GADTs, ExistentialQuantification, KindSignatures, Rank2Types #-} + +-- Succeeds (needs the (Ord a) in TypeSet +-- c.f. gadt21.hs + +-- However, it's a useful test because it unearthed a bug +-- in free-variable-finding + +module Expr where + +import Data.Set (Set) + +data Type a where + TypeInt :: Type Int + TypeSet :: Ord a => Type a -> Type (Set a) + TypeFun :: Type a -> Type b -> Type (a -> b) + +data Expr :: * -> * where + Const :: Type a -> a -> Expr a + +data DynExpr = forall a. DynExpr (Expr a) + +withOrdDynExpr :: DynExpr -> (forall a. Ord a => Expr a -> b) -> Maybe b +withOrdDynExpr (DynExpr e@(Const (TypeSet _) _)) f = Just (f e) +withOrdDynExpr (DynExpr e@(Const TypeInt _)) f = Just (f e) +withOrdDynExpr _ _ = Nothing diff --git a/testsuite/tests/gadt/gadt23.hs b/testsuite/tests/gadt/gadt23.hs new file mode 100644 index 0000000000..95e2710292 --- /dev/null +++ b/testsuite/tests/gadt/gadt23.hs @@ -0,0 +1,15 @@ +{-# LANGUAGE GADTs #-} + +module Main where + +import Gadt23_AST + +data Foo = Foo { bar :: Int } + +convert :: AST a tag -> AST a Foo +convert t = case t of + Var v -> Tag (Foo 42) $ Var v + Tag t e -> Tag (Foo 42) $ convert e + +main = return () + diff --git a/testsuite/tests/gadt/gadt24.hs b/testsuite/tests/gadt/gadt24.hs new file mode 100644 index 0000000000..86cece09dd --- /dev/null +++ b/testsuite/tests/gadt/gadt24.hs @@ -0,0 +1,14 @@ +{-# LANGUAGE GADTs #-} + +-- Test for Trac #1396 +-- Panics in GHC 6.6.1 + +module ShouldCompile where + +data Right provides final where + RightNull :: Right final final + RightCons :: b -> Right a final -> Right (b -> a) final + +collapse_right :: right -> Right right final -> final +--collapse_right f (RightNull) = f +collapse_right f (RightCons b r) = collapse_right (f b) r diff --git a/testsuite/tests/gadt/gadt25.hs b/testsuite/tests/gadt/gadt25.hs new file mode 100644 index 0000000000..99aecad3fb --- /dev/null +++ b/testsuite/tests/gadt/gadt25.hs @@ -0,0 +1,41 @@ +{-# LANGUAGE GADTs #-} + +-- From the ghc-users mailing list + +module Foo where + +data TValue t where + TList :: [a] -> TValue [a] + +instance (Eq b) => Eq (TValue b) where + (==) (TList p) (TList q) = (==) p q + +{- My reply to the list + +Here's the reasoning (I have done a bit of renaming). + +* The TList constructor really has type + TList :: forall a. forall x. (a~[x]) => [x] -> TValue a + +* So in the pattern match we have + (Eq b) available from the instance header + TList p :: TValue b + x is a skolem, existentially bound by the pattern + p :: [x] + b ~ [x] available from the pattern match + +* On the RHS we find we need (Eq [x]). + +* So the constraint problem we have is + (Eq b, b~[x]) => Eq [x] + ["Given" => "Wanted"] + Can we prove this? From the two given constraints we can see + that we also have Eq [x], and that certainly proves Eq [x]. + + +Nevertheless, it's a bit delicate. If we didn't notice all the +consequences of the "given" constraints, we might use the top-level Eq +a => Eq [a] instance to solve the wanted Eq [x]. And now we need Eq +x, which *isn't* a consequence of (Eq b, b~[x]). + +-}
\ No newline at end of file diff --git a/testsuite/tests/gadt/gadt3.hs b/testsuite/tests/gadt/gadt3.hs new file mode 100644 index 0000000000..b58301e131 --- /dev/null +++ b/testsuite/tests/gadt/gadt3.hs @@ -0,0 +1,18 @@ +{-# LANGUAGE GADTs #-} + +module ShouldCompile where + +data T where + T1 :: Int -> T + T2 :: Bool -> Bool -> T + +data S a where + S1 :: a -> S a + S2 :: Int -> S Int + +f (T1 i) = i>0 +f (T2 a b) = a && b + +g :: S a -> a +g (S1 x) = x +g (S2 i) = i diff --git a/testsuite/tests/gadt/gadt4.hs b/testsuite/tests/gadt/gadt4.hs new file mode 100644 index 0000000000..0d78135597 --- /dev/null +++ b/testsuite/tests/gadt/gadt4.hs @@ -0,0 +1,18 @@ +{-# LANGUAGE GADTs #-} + +module Main where + +data Term a where + Lit :: Int -> Term Int + IsZero :: Term Int -> Term Bool + If :: Term Bool -> Term a -> Term a -> Term a + + +eval :: Term a -> a +eval (Lit n) = n +eval (IsZero t) = eval t == 0 +eval (If t1 t2 t3) = if eval t1 then eval t2 else eval t3 + +term = If (IsZero (Lit 1)) (Lit 2) (Lit 3) + +main = print (eval term)
\ No newline at end of file diff --git a/testsuite/tests/gadt/gadt4.stdout b/testsuite/tests/gadt/gadt4.stdout new file mode 100644 index 0000000000..00750edc07 --- /dev/null +++ b/testsuite/tests/gadt/gadt4.stdout @@ -0,0 +1 @@ +3 diff --git a/testsuite/tests/gadt/gadt5.hs b/testsuite/tests/gadt/gadt5.hs new file mode 100644 index 0000000000..5db3deef8c --- /dev/null +++ b/testsuite/tests/gadt/gadt5.hs @@ -0,0 +1,23 @@ +{-# LANGUAGE GADTs #-} + +module Main where + +data Term a where + Lit :: Int -> Term Int + IsZero :: Term Int -> Term Bool + If :: Term Bool -> Term a -> Term a -> Term a + Pr :: Term a -> Term b -> Term (a, b) + Fst :: Term (a, b) -> Term a + Snd :: Term (a, b) -> Term b + +eval :: Term v -> v +eval (Lit n) = n +eval (IsZero t) = eval t == 0 +eval (If t1 t2 t3) = if eval t1 then eval t2 else eval t3 +eval (Pr t1 t2) = (eval t1, eval t2) +eval (Fst t) = case (eval t) of { (a,b) -> a } +eval (Snd t) = case (eval t) of { (a,b) -> b } + +term = If (IsZero (Lit 1)) (Pr (Lit 2) (Lit 3)) (Pr (Lit 3) (Lit 4)) + +main = print (eval term)
\ No newline at end of file diff --git a/testsuite/tests/gadt/gadt5.stdout b/testsuite/tests/gadt/gadt5.stdout new file mode 100644 index 0000000000..764f565258 --- /dev/null +++ b/testsuite/tests/gadt/gadt5.stdout @@ -0,0 +1 @@ +(3,4) diff --git a/testsuite/tests/gadt/gadt6.hs b/testsuite/tests/gadt/gadt6.hs new file mode 100644 index 0000000000..606d04e8a4 --- /dev/null +++ b/testsuite/tests/gadt/gadt6.hs @@ -0,0 +1,9 @@ +{-# LANGUAGE GADTs #-} + +module ShouldCompile where + +data T a where + T :: b -> (b->Int) -> a -> T a + +f (T b f a) = a + diff --git a/testsuite/tests/gadt/gadt7.hs b/testsuite/tests/gadt/gadt7.hs new file mode 100644 index 0000000000..9c775d2f23 --- /dev/null +++ b/testsuite/tests/gadt/gadt7.hs @@ -0,0 +1,34 @@ +{-# LANGUAGE GADTs, RankNTypes, ScopedTypeVariables #-} + +-- From Yann Regis-Gianas at INRIA + +module ShouldCompile where + +data T a where + K :: T Int + +-- Should fail +i1 :: T a -> a -> Int +i1 t y = (\t1 y1 -> case t1 of K -> y1) t y + +-- No type signature; should type-check +i1b t y = (\t1 y1 -> case t1 of K -> y1) t y + +i2 :: T a -> a -> Int +i2 t (y::b) = case t of { K -> y+(1::Int) } + +i3 :: forall a. T a -> a -> Int +i3 t y + = let t1 = t in + let y1 = y in + case t1 of K -> y1 + +i4 :: forall a. T a -> a -> Int +i4 (t :: T a) (y :: a) + = let t1 = t in + let y1 = y in + case t1 of K -> y1 + + + + diff --git a/testsuite/tests/gadt/gadt7.stderr b/testsuite/tests/gadt/gadt7.stderr new file mode 100644 index 0000000000..e69de29bb2 --- /dev/null +++ b/testsuite/tests/gadt/gadt7.stderr diff --git a/testsuite/tests/gadt/gadt8.hs b/testsuite/tests/gadt/gadt8.hs new file mode 100644 index 0000000000..1cad8f65cc --- /dev/null +++ b/testsuite/tests/gadt/gadt8.hs @@ -0,0 +1,15 @@ +{-# LANGUAGE GADTs, KindSignatures #-} + +-- Test a couple of trivial things: +-- explicit layout +-- trailing semicolons +-- kind signatures +module ShouldCompile where + +data Expr :: * -> * where { + EInt :: Int -> Expr Int ; + EBool :: Bool -> Expr Bool ; + EIf :: (Expr Bool) -> (Expr a) -> (Expr a) -> Expr a ; + -- Note trailing semicolon, should be ok + } + diff --git a/testsuite/tests/gadt/gadt9.hs b/testsuite/tests/gadt/gadt9.hs new file mode 100644 index 0000000000..df9e0bceb2 --- /dev/null +++ b/testsuite/tests/gadt/gadt9.hs @@ -0,0 +1,15 @@ +{-# LANGUAGE GADTs #-}
+
+-- This one requires careful handling in
+-- TcUnify.unifyTyConApp, to preserve rigidity.
+
+module ShouldCompile where
+
+data X a b where
+ X :: X a a
+
+data Y x a b where
+ Y :: x a b -> x b c -> Y x a c
+
+doy :: Y X a b -> Y X a b
+doy (Y X X) = Y X X
diff --git a/testsuite/tests/gadt/gadtSyntax001.hs b/testsuite/tests/gadt/gadtSyntax001.hs new file mode 100644 index 0000000000..fa6b8ce646 --- /dev/null +++ b/testsuite/tests/gadt/gadtSyntax001.hs @@ -0,0 +1,9 @@ + +{-# LANGUAGE GADTSyntax #-} + +module GadtSyntax001 where + +data Foo a b where + C1 :: a -> Int -> b -> Foo b a + C2 :: a -> Char -> Foo a b + Cs :: Foo a b diff --git a/testsuite/tests/gadt/gadtSyntaxFail001.hs b/testsuite/tests/gadt/gadtSyntaxFail001.hs new file mode 100644 index 0000000000..8fd8bfdf5b --- /dev/null +++ b/testsuite/tests/gadt/gadtSyntaxFail001.hs @@ -0,0 +1,9 @@ + +{-# LANGUAGE GADTSyntax #-} + +module GadtSyntaxFail001 where + +data Foo a b where + C1 :: a -> Int -> b -> Foo b a + C2 :: a -> Char -> Foo a Int + Cs :: Foo a b diff --git a/testsuite/tests/gadt/gadtSyntaxFail001.stderr b/testsuite/tests/gadt/gadtSyntaxFail001.stderr new file mode 100644 index 0000000000..363ad04d5a --- /dev/null +++ b/testsuite/tests/gadt/gadtSyntaxFail001.stderr @@ -0,0 +1,6 @@ + +gadtSyntaxFail001.hs:8:5: + Data constructor `C2' has existential type variables, a context, or a specialised result type + (Use -XExistentialQuantification or -XGADTs to allow this) + In the definition of data constructor `C2' + In the data type declaration for `Foo' diff --git a/testsuite/tests/gadt/gadtSyntaxFail002.hs b/testsuite/tests/gadt/gadtSyntaxFail002.hs new file mode 100644 index 0000000000..cb33d6795e --- /dev/null +++ b/testsuite/tests/gadt/gadtSyntaxFail002.hs @@ -0,0 +1,9 @@ + +{-# LANGUAGE GADTSyntax #-} + +module GadtSyntaxFail002 where + +data Foo a b where + C1 :: a -> Int -> b -> Foo b a + C2 :: a -> Char -> Foo a a + Cs :: Foo a b diff --git a/testsuite/tests/gadt/gadtSyntaxFail002.stderr b/testsuite/tests/gadt/gadtSyntaxFail002.stderr new file mode 100644 index 0000000000..c8bdbab224 --- /dev/null +++ b/testsuite/tests/gadt/gadtSyntaxFail002.stderr @@ -0,0 +1,6 @@ + +gadtSyntaxFail002.hs:8:5: + Data constructor `C2' has existential type variables, a context, or a specialised result type + (Use -XExistentialQuantification or -XGADTs to allow this) + In the definition of data constructor `C2' + In the data type declaration for `Foo' diff --git a/testsuite/tests/gadt/gadtSyntaxFail003.hs b/testsuite/tests/gadt/gadtSyntaxFail003.hs new file mode 100644 index 0000000000..10c67200fc --- /dev/null +++ b/testsuite/tests/gadt/gadtSyntaxFail003.hs @@ -0,0 +1,9 @@ + +{-# LANGUAGE GADTSyntax #-} + +module GadtSyntaxFail003 where + +data Foo a b where + C1 :: a -> Int -> c -> Foo b a + C2 :: a -> Char -> Foo a b + Cs :: Foo a b diff --git a/testsuite/tests/gadt/gadtSyntaxFail003.stderr b/testsuite/tests/gadt/gadtSyntaxFail003.stderr new file mode 100644 index 0000000000..436bb76ca2 --- /dev/null +++ b/testsuite/tests/gadt/gadtSyntaxFail003.stderr @@ -0,0 +1,6 @@ + +gadtSyntaxFail003.hs:7:5: + Data constructor `C1' has existential type variables, a context, or a specialised result type + (Use -XExistentialQuantification or -XGADTs to allow this) + In the definition of data constructor `C1' + In the data type declaration for `Foo' diff --git a/testsuite/tests/gadt/josef.hs b/testsuite/tests/gadt/josef.hs new file mode 100644 index 0000000000..3be7dc28dc --- /dev/null +++ b/testsuite/tests/gadt/josef.hs @@ -0,0 +1,69 @@ +{-# LANGUAGE GADTs, KindSignatures, + MultiParamTypeClasses, FunctionalDependencies #-} + +-- Program from Josef Svenningsson + +-- Just a short explanation of the program. It contains +-- some class declarations capturing some definitions from +-- category theory. Further down he have a data type for well typed +-- lambda expressions using GADTs. Finally we have a +-- function defining the semantics for lambda terms called +-- 'interp'. + +-- Made GHC 6.4 bleat +-- Quantified type variable `t' is unified with +-- another quantified type variable `terminal' +-- When trying to generalise the type inferred for `interp' + + +module Bug where + +class Category arr where + idA :: arr a a + comp :: arr a b -> arr b c -> arr a c + +class Category arr => + Terminal terminal arr | arr -> terminal where + terminal :: arr a terminal + +class Category arr => + ProductCategory prod arr | arr -> prod where + first :: arr (prod a b) a + second :: arr (prod a b) b + pair :: arr a b -> arr a c -> arr a (prod b c) + +class Category arr => + CoproductCategory coprod arr | arr -> coprod where + inLeft :: arr a (coprod a b) + inRight :: arr b (coprod a b) + ccase :: arr a c -> arr b c -> arr (coprod a b) c + +class ProductCategory prod arr => + Exponential exp prod arr | arr -> exp where + eval :: arr (prod (exp a b) a) b + curryA :: arr (prod c a) b -> arr c (exp a b) + + +class (Exponential exp prod arr, Terminal terminal arr) => + CartesianClosed terminal exp prod arr | arr -> terminal exp prod + +data V prod env t where + Z :: V prod (prod env t) t + S :: V prod env t -> V prod (prod env x) t + +data Lambda terminal (exp :: * -> * -> *) prod env t where + Unit :: Lambda foo exp prod env foo + Var :: V prod env t -> Lambda terminal exp prod env t +{- Lam :: Lambda terminal exp prod (prod env a) t + -> Lambda terminal exp prod env (exp a t) + App :: Lambda terminal exp prod env (exp t t') + -> Lambda terminal exp prod env t -> Lambda terminal exp prod env t' +-} + +interp :: CartesianClosed terminal exp prod arr => + Lambda terminal exp prod s t -> arr s t +interp (Unit) = terminal -- Terminal terminal arr => arr a terminal +-- interp (Var Z) = second +-- interp (Var (S v)) = first `comp` interp (Var v) +-- interp (Lam e) = curryA (interp e) +-- interp (App e1 e2) = pair (interp e1) (interp e2) `comp` eval diff --git a/testsuite/tests/gadt/karl1.hs b/testsuite/tests/gadt/karl1.hs new file mode 100644 index 0000000000..e3af7adb1d --- /dev/null +++ b/testsuite/tests/gadt/karl1.hs @@ -0,0 +1,79 @@ +{-# LANGUAGE GADTs, KindSignatures #-}
+
+-- See Trac #301
+-- This particular one doesn't use GADTs per se,
+-- but it does use dictionaries in constructors
+
+module Expr1 where
+
+data Expr :: * -> * where -- Not a GADT at all
+ Const :: Show a => a -> Expr a
+ -- Note the Show constraint here
+ Var :: Var a -> Expr a
+
+newtype Var a = V String
+
+instance Show (Var a) where show (V s) = s
+
+--------------------------
+e1 :: Expr Int
+e1 = Const 42
+
+e2 :: Expr Bool
+e2 = Const True
+
+e3 :: Expr Integer
+e3 = Var (V "mersenne100")
+
+--------------------------
+eval :: Expr a -> a
+eval (Const c) = c
+eval (Var v) = error ("free variable `" ++ shows v "'")
+
+{-
+ Up to here, everything works nicely:
+
+ \begin{verbatim}
+ *Expr0> eval e1
+ 42
+ *Expr0> eval e2
+ True
+ *Expr1> eval e3
+ *** Exception: free variable `mersenne100'
+ \end{verbatim}
+
+ But let us now try to define a |shows| function.
+
+ In the following, without the type signature we get:
+ \begin{verbatim}
+ *Expr1> :t showsExpr
+ showsExpr :: forall a. (Show a) => Expr a -> String -> String
+ *Expr1> showsExpr e1 ""
+ "42"
+ *Expr1> showsExpr e2 ""
+ "True"
+ *Expr1> showsExpr e3 ""
+ "mersenne100"
+ \end{verbatim}
+
+ However, in the last case, the instance |Show Integer| was not used,
+ so should not have been required.
+ Therefore I would expect it to work as it is now, i.e.,
+ with the type signature:
+-}
+
+showsExpr :: Expr a -> ShowS
+showsExpr (Const c) = shows c
+showsExpr (Var v) = shows v
+
+{-
+
+We used to get a complaint about the |Const| alternative (then line
+63) that documents that the constraint in the type of |Const| must
+have been ignored:
+
+ No instance for (Show a)
+ arising from use of `shows' at Expr1.lhs:63:22-26
+ Probable fix: add (Show a) to the type signature(s) for `showsExpr'
+ In the definition of `showsExpr': showsExpr (Const c) = shows c
+-}
diff --git a/testsuite/tests/gadt/karl2.hs b/testsuite/tests/gadt/karl2.hs new file mode 100644 index 0000000000..a701400689 --- /dev/null +++ b/testsuite/tests/gadt/karl2.hs @@ -0,0 +1,136 @@ +{-# LANGUAGE GADTs, KindSignatures #-}
+
+module Expr0 where
+
+-- See Trac #301
+-- This one *does* use GADTs (Fct)
+
+data Expr :: * -> * where
+ Const :: Show a => a -> Expr a
+ Apply :: Fct a b -> Expr a -> Expr b
+
+data Fct :: * -> * -> * where
+ Succ :: Fct Int Int
+ EqZero :: Fct Int Bool
+ Add :: Fct Int (Int -> Int)
+
+------------------------------
+e1 :: Expr Int
+e1 = Apply Succ (Const 41)
+
+e2 :: Expr Bool
+e2 = Apply EqZero e1
+
+e3 :: Expr (Int -> Int)
+e3 = Apply Add e1
+
+------------------------------
+eval :: Expr a -> a
+eval (Const c) = c
+eval (Apply f a) = evalFct f $ eval a
+
+evalFct :: Fct a b -> a -> b
+evalFct Succ = succ
+evalFct EqZero = (0 ==)
+evalFct Add = (+)
+
+
+{- Up to here, everything works nicely:
+
+ \begin{verbatim}
+ *Expr0> eval e1
+ 42
+ *Expr0> eval e2
+ False
+ *Expr0> eval e3 5
+ 47
+ \end{verbatim}
+
+ But let us now try to define a |Show| instance.
+ For |Fct|, this is not a problem:
+-}
+
+instance Show (Fct a b) where
+ show Succ = "S"
+ show EqZero = "isZero"
+ show Add = "add"
+
+showsExpr :: Expr a -> ShowS
+showsExpr (Const c) = shows c
+showsExpr (Apply f a) =
+ ('(' :) . shows f . (' ' :) . showsExpr a . (')' :)
+
+instance Show (Expr a) where
+ showsPrec _ (Const c) = shows c
+ showsPrec _ (Apply f a) =
+ ('(' :) . shows f . (' ' :) . shows a . (')' :)
+
+{- But we used to get a complaint about the |Const| alternative (then
+ line 56) that documents that the constraint in the type of |Const|
+ must have been ignored:
+
+ \begin{verbatim}
+ No instance for (Show a)
+ arising from use of `shows' at Expr0.lhs:56:22-26
+ Probable fix: add (Show a) to the type signature(s) for `showsExpr'
+ In the definition of `showsExpr': showsExpr (Const c) = shows c
+ \end{verbatim}
+
+ But if we do that, the recursive call is of course still unsatisfied:
+ \begin{verbatim}
+ No instance for (Show a)
+ arising from use of `showsExpr' at Expr0.lhs:65:34-42
+ Probable fix: add (Show a) to the existential context for `Apply'
+ In the first argument of `(.)', namely `showsExpr a'
+ In the second argument of `(.)', namely `(showsExpr a) . ((')' :))'
+ In the second argument of `(.)', namely
+ `((' ' :)) . ((showsExpr a) . ((')' :)))'
+ \end{verbatim}
+
+ Following also the advice given in this last error message
+ actually makes GHC accept this, and then we can say:
+
+ \begin{verbatim}
+ *Expr0> showsExpr e1 ""
+ "(S 41)"
+ *Expr0> showsExpr e2 ""
+ "(isZero (S 41))"
+ \end{verbatim}
+
+ However, following this advice is counterintuitive
+ and should be unnecessary
+ since the |Show| instance for argument types
+ is only ever used in the const case.
+ We get:
+
+ \begin{verbatim}
+ *Expr0> showsExpr e3 ""
+
+ <interactive>:1:0:
+ No instance for (Show (Int -> Int))
+ arising from use of `showsExpr' at <interactive>:1:0-8
+ Probable fix: add an instance declaration for (Show (Int -> Int))
+ In the definition of `it': it = showsExpr e3 ""
+ \end{verbatim}
+
+ But of course we would expect the following:
+
+ \begin{verbatim}
+ *Expr0> showsExpr e3 ""
+ "(add (S 41))"
+ \end{verbatim}
+
+
+ \bigskip
+ The error messages are almost the same
+ if we define a |Show| instance directly
+ (line 90 was the |Const| alternative):
+
+ \begin{verbatim}
+ Could not deduce (Show a) from the context (Show (Expr a))
+ arising from use of `shows' at Expr0.lhs:90:26-30
+ Probable fix: add (Show a) to the class or instance method `showsPrec'
+ \end{verbatim}
+-}
+
+
diff --git a/testsuite/tests/gadt/lazypat.hs b/testsuite/tests/gadt/lazypat.hs new file mode 100644 index 0000000000..f16da207aa --- /dev/null +++ b/testsuite/tests/gadt/lazypat.hs @@ -0,0 +1,7 @@ +{-# LANGUAGE GADTs, ExistentialQuantification #-}
+
+module ShouldFail where
+
+data T = forall a. T a (a->Int)
+
+f ~(T x f) = f x
\ No newline at end of file diff --git a/testsuite/tests/gadt/lazypat.stderr b/testsuite/tests/gadt/lazypat.stderr new file mode 100644 index 0000000000..d64f40e487 --- /dev/null +++ b/testsuite/tests/gadt/lazypat.stderr @@ -0,0 +1,7 @@ + +lazypat.hs:7:5: + An existential or GADT data constructor cannot be used + inside a lazy (~) pattern + In the pattern: T x f + In the pattern: ~(T x f) + In an equation for `f': f ~(T x f) = f x diff --git a/testsuite/tests/gadt/lazypatok.hs b/testsuite/tests/gadt/lazypatok.hs new file mode 100644 index 0000000000..bf1282fe39 --- /dev/null +++ b/testsuite/tests/gadt/lazypatok.hs @@ -0,0 +1,14 @@ +{-# LANGUAGE GADTs #-}
+
+-- It's not clear whether this one should succed or fail,
+-- Arguably it should succeed because the type refinement on
+-- T1 should make (y::Int). Currently, though, it succeeds
+
+module ShouldFail where
+
+data T a where
+ T1 :: Int -> T Int
+
+f :: (T a, a) -> Int
+f ~(T1 x, y) = x+y
+
diff --git a/testsuite/tests/gadt/lazypatok.stderr b/testsuite/tests/gadt/lazypatok.stderr new file mode 100644 index 0000000000..e69de29bb2 --- /dev/null +++ b/testsuite/tests/gadt/lazypatok.stderr diff --git a/testsuite/tests/gadt/nbe.hs b/testsuite/tests/gadt/nbe.hs new file mode 100644 index 0000000000..0547131df9 --- /dev/null +++ b/testsuite/tests/gadt/nbe.hs @@ -0,0 +1,176 @@ +{-# LANGUAGE GADTs, Rank2Types #-} + +module Main where + +-- abstract syntax ------------------------------------------------------------- +data Ty t where + Bool :: Ty Bool + Arr :: Ty a -> Ty b -> Ty (a -> b) + +data Exp g t where + Var :: Var g t -> Exp g t + Lam :: Ty a -> Exp (g,a) b -> Exp g (a->b) + App :: Exp g (s -> t) -> Exp g s -> Exp g t + If :: Exp g Bool -> Exp g t -> Exp g t -> Exp g t + ETrue :: Exp g Bool + EFalse :: Exp g Bool + +data Var g t where + ZVar :: Var (h,t) t + SVar :: Var h t -> Var (h,s) t + +-- smart constructors ---------------------------------------------------------- +lamE :: Ty s -> (Exp (g,s) s -> Exp (g,s) t) -> Exp g (s -> t) +lamE s f = Lam s (f (Var ZVar)) + +ifE :: Exp g Bool -> Exp g t -> Exp g t -> Exp g t +ifE t ETrue EFalse = t +ifE t e e' = if eqE e e' then e else If t e e' + +-- boring equality tests ------------------------------------------------------- +eqB :: BoxExp t -> BoxExp s -> Bool +eqB (Box e) (Box e_) = eqE e e_ + +eqE :: Exp g t -> Exp h s -> Bool +eqE (Var x) (Var y) = eqV x y +eqE (Lam s e) (Lam s_ e_) = eqT s s_ && eqE e e_ +eqE (App e1 e2) (App e1_ e2_) = eqE e1 e1_ && eqE e2 e2_ +eqE (If e1 e2 e3) (If e1_ e2_ e3_) = eqE e1 e1_ && (eqE e2 e2_ && eqE e3 e3_) +eqE (ETrue) (ETrue) = True +eqE (EFalse) (EFalse) = True +eqE _ _ = False + +eqT :: Ty t -> Ty s -> Bool +eqT (Arr s t) (Arr s_ t_) = eqT s s_ && eqT t t_ +eqT Bool Bool = True +eqT _ _ = False + +eqV :: Var g t -> Var h s -> Bool +eqV (SVar x) (SVar y) = eqV x y +eqV ZVar ZVar = True +eqV _ _ = False + +-- evaluation ------------------------------------------------------------------ +var :: Var g t -> g -> t +var ZVar (_,t) = t +var (SVar x) (h,s) = var x h + +eval :: Exp g t -> g -> t +eval (Var x) g = var x g +eval (Lam _ e) g = \a -> eval e (g,a) +eval (App e e') g = eval e g (eval e' g) +eval (ETrue) g = True +eval (EFalse) g = False +eval (If c t e) g = if eval c g then eval t g else eval e g + +-- type inference -------------------------------------------------------------- +data TyEnv g where + Nil :: TyEnv g + Cons :: Ty t -> TyEnv h -> TyEnv (h,t) + +infer :: TyEnv g -> Exp g t -> Ty t +infer g (Var x) = inferVar g x +infer g (Lam t e) = Arr t (infer (Cons t g) e) +infer g (App e e') = case infer g e of Arr _ t -> t +infer g (ETrue) = Bool +infer g (EFalse) = Bool +infer g (If _ e _) = infer g e + +inferVar :: TyEnv g -> Var g t -> Ty t +inferVar (Cons t h) (SVar x) = inferVar h x +inferVar (Cons t h) (ZVar) = t + +-- tree monad ------------------------------------------------------------------ + +data Tree a = Val a | Choice (Tree a) (Tree a) +-- doesn't yet force trees to be fully balanced: +-- Val :: a -> Tree a Z +-- Choice :: Tree a n -> Tree a n -> Tree a (S n) + +instance Monad Tree where + return x = Val x + (Val a) >>= f = f a + (Choice l r) >>= f = Choice (l >>= f) (r >>= f) + +tmap :: Monad m => (a->b) -> m a -> m b +tmap f x = do { a <- x; return (f a) } + +flatten t = flatten_ t [] + where + flatten_ (Val a) k = a:k + flatten_ (Choice l r) k = flatten_ l (flatten_ r k) + + +-- quote & friends ------------------------------------------------------------- + +-- for values -------------------------- +enumV :: Ty t -> Tree t +questionsV :: Ty t -> [t -> Bool] + + +enumV Bool = Choice (Val True) (Val False) +enumV (Arr s t) = mkEnum (questionsV s) (enumV t) + where + mkEnum [] t = tmap const t + mkEnum (q:qs) es = do + f1 <- mkEnum qs es + f2 <- mkEnum qs es + return (\d -> if q d then f1 d else f2 d) + +questionsV Bool = return (\x -> x) +questionsV (Arr s t) = do + d <- flatten (enumV s) + q <- questionsV t + return (\f -> q (f d)) + +-- for expressions --------------------- +enumE :: Ty t -> Tree (Exp g t) +questionsE :: Ty t -> [Exp g t -> Exp g Bool] + +enumE Bool = Choice (Val ETrue) (Val EFalse) +enumE (Arr s t) = tmap (lamE s) (mkEnumE (questionsE s) (enumE t)) + where + mkEnumE [] t = tmap const t + mkEnumE (q:qs) es = do + f1 <- mkEnumE qs es + f2 <- mkEnumE qs es + return (\d -> ifE (q d) (f1 d) (f2 d)) + +questionsE Bool = return (\x -> x) +questionsE (Arr s t) = do + d <- flatten (enumE s) + q <- questionsE t + return (\f -> q (App f d)) + +-- should be +-- find (List (Exp g Bool) n) -> Tree (Exp g a) n -> Exp g a +find :: [Exp g Bool] -> Tree (Exp g a) -> Exp g a +find [] (Val a) = a +find (b:bs) (Choice l r) = ifE b (find bs l) (find bs r) +find _ _ = error "bad arguments to find" + +quote :: Ty t -> t -> Exp g t +quote Bool t = case t of True -> ETrue; False -> EFalse +quote (Arr s t) f = lamE s (\e -> find (do q <- questionsE s; return (q e)) + (tmap (quote t . f) (enumV s))) + +-- normalization (by evaluation) ----------------------------------------------- +data BoxExp t = Box (forall g. Exp g t) + +normalize :: Ty t -> BoxExp t -> BoxExp t +normalize s (Box e) = Box (quote s (eval e ())) + +-- examples -------------------------------------------------------------------- +b2b = Arr Bool Bool +b22b = Arr b2b b2b +zero = Var ZVar +one = Var (SVar ZVar) +once = Box (Lam b2b (Lam Bool (App one zero))) +twice = Box (Lam b2b (Lam Bool (App one (App one zero)))) +thrice = Box (Lam b2b (Lam Bool (App one (App one (App one zero))))) + +test = [ eqB (nf b22b thrice) (nf b22b once) + , eqB (nf b22b twice) (nf b22b once)] + where nf = normalize + +main = print test
\ No newline at end of file diff --git a/testsuite/tests/gadt/nbe.stdout b/testsuite/tests/gadt/nbe.stdout new file mode 100644 index 0000000000..a5f190762c --- /dev/null +++ b/testsuite/tests/gadt/nbe.stdout @@ -0,0 +1 @@ +[True,False] diff --git a/testsuite/tests/gadt/records-fail1.hs b/testsuite/tests/gadt/records-fail1.hs new file mode 100644 index 0000000000..8eefee51e7 --- /dev/null +++ b/testsuite/tests/gadt/records-fail1.hs @@ -0,0 +1,11 @@ +{-# LANGUAGE GADTs #-} + +-- Tests record syntax for GADTs + +module ShouldFail where + +data T a where + T1 { x :: a, y :: b } :: T (a,b) + T4 { x :: Int } :: T [a] + +
\ No newline at end of file diff --git a/testsuite/tests/gadt/records-fail1.stderr b/testsuite/tests/gadt/records-fail1.stderr new file mode 100644 index 0000000000..0ef628b5a6 --- /dev/null +++ b/testsuite/tests/gadt/records-fail1.stderr @@ -0,0 +1,5 @@ + +records-fail1.hs:7:1: + Constructors T1 and T4 have a common field `x', + but have different result types + In the data type declaration for `T' diff --git a/testsuite/tests/gadt/records.hs b/testsuite/tests/gadt/records.hs new file mode 100644 index 0000000000..e28add3fb6 --- /dev/null +++ b/testsuite/tests/gadt/records.hs @@ -0,0 +1,25 @@ +{-# LANGUAGE GADTs #-} + +-- Tests record syntax for GADTs + +module Main where + +data T a where + T1 :: { x :: a, y :: b } -> T (a,b) + T2 :: { x :: a } -> T (a,b) + T3 :: { z :: Int } -> T Bool + +f xv yv = T1 { x = xv, y = yv } + +g :: T a -> T a +g (T1 {x=xv, y=yv}) = T2 { x = xv } + +-- h :: Num a => T a any -> a +h v = x v + 1 + +main = do { let t1 = T1 { y = "foo", x = 4 } + t2 = g t1 + ; print (h (f 8 undefined)) + ; print (h t2) + } +
\ No newline at end of file diff --git a/testsuite/tests/gadt/records.stdout b/testsuite/tests/gadt/records.stdout new file mode 100644 index 0000000000..f224d49c08 --- /dev/null +++ b/testsuite/tests/gadt/records.stdout @@ -0,0 +1,2 @@ +9 +5 diff --git a/testsuite/tests/gadt/red-black.hs b/testsuite/tests/gadt/red-black.hs new file mode 100644 index 0000000000..29bb324310 --- /dev/null +++ b/testsuite/tests/gadt/red-black.hs @@ -0,0 +1,41 @@ +{-# LANGUAGE GADTs #-} + +module ShouldCompile where + +-- data RBTree = forall n. Root (SubTree Black n) + +-- Kind Colour +data Red +data Black + +-- Kind Nat +data Z +data S a + +data SubTree c n where + Leaf :: SubTree Black Z + RNode :: SubTree Black n -> Int -> SubTree Black n -> SubTree Red n + BNode :: SubTree cL m -> Int -> SubTree cR m -> SubTree Black (S m) + Fix :: SubTree Red n -> SubTree Black n + + +ins :: Int -> SubTree c n -> SubTree c n +ins n Leaf = (Fix (RNode Leaf n Leaf)) +ins n (BNode x m y) | n <= m = black (ins n x) m y +ins n (BNode x m y) | n > m = black x m (ins n y) +ins n (RNode x m y) | n <= m = RNode (ins n x) m y +ins n (RNode x m y) | n > m = RNode x m (ins n y) + +black :: SubTree c n -> Int -> SubTree d n -> SubTree Black (S n) +black (RNode (Fix u) v c) w (x@(RNode _ _ _)) = Fix(RNode (blacken u) v (BNode c w x)) + +black (RNode (Fix u) v c) w (x@(BNode _ _ _)) = BNode u v (RNode c w x) +black (RNode a v (Fix (RNode b u c))) w (x@(BNode _ _ _)) = BNode (RNode a v b) u (RNode c w x) +black (Fix x) n (Fix y) = BNode x n y +black x n (Fix y) = BNode x n y +black (Fix x) n y = BNode x n y +black x n y = BNode x n y + +blacken :: SubTree Red n -> SubTree Black (S n) +blacken (RNode l e r) = (BNode l e r) + diff --git a/testsuite/tests/gadt/rw.hs b/testsuite/tests/gadt/rw.hs new file mode 100644 index 0000000000..0d0018ac30 --- /dev/null +++ b/testsuite/tests/gadt/rw.hs @@ -0,0 +1,29 @@ +{-# LANGUAGE GADTs #-}
+
+module Main where
+
+import Data.IORef
+
+data T a where
+ Li:: Int -> T Int
+ Lb:: Bool -> T Bool
+ La:: a -> T a
+
+writeInt:: T a -> IORef a -> IO ()
+writeInt v ref = case v of
+ ~(Li x) -> writeIORef ref (1::Int)
+
+readBool:: T a -> IORef a -> IO ()
+readBool v ref = case v of
+ ~(Lb x) ->
+ readIORef ref >>= (print . not)
+
+tt::T a -> IO ()
+tt v = case v of
+ ~(Li x) -> print "OK"
+
+main = do
+ tt (La undefined)
+ ref <- newIORef undefined
+ writeInt (La undefined) ref
+ readBool (La undefined) ref
diff --git a/testsuite/tests/gadt/rw.stderr b/testsuite/tests/gadt/rw.stderr new file mode 100644 index 0000000000..dbac243ab6 --- /dev/null +++ b/testsuite/tests/gadt/rw.stderr @@ -0,0 +1,19 @@ + +rw.hs:14:47: + Couldn't match type `a' with `Int' + `a' is a rigid type variable bound by + the type signature for writeInt :: T a -> IORef a -> IO () + at rw.hs:13:1 + In the second argument of `writeIORef', namely `(1 :: Int)' + In the expression: writeIORef ref (1 :: Int) + In a case alternative: ~(Li x) -> writeIORef ref (1 :: Int) + +rw.hs:19:51: + Couldn't match type `a' with `Bool' + `a' is a rigid type variable bound by + the type signature for readBool :: T a -> IORef a -> IO () + at rw.hs:17:1 + Expected type: a -> Bool + Actual type: Bool -> Bool + In the second argument of `(.)', namely `not' + In the second argument of `(>>=)', namely `(print . not)' diff --git a/testsuite/tests/gadt/scoped.hs b/testsuite/tests/gadt/scoped.hs new file mode 100644 index 0000000000..cafa738697 --- /dev/null +++ b/testsuite/tests/gadt/scoped.hs @@ -0,0 +1,33 @@ +{-# LANGUAGE GADTs, ScopedTypeVariables #-} + +-- Tests for scoped type variables and GADTs + +module GADT where + +data C x y where + C :: a -> C a a + +data D x y where + D :: C b c -> D a c + +------- All these should be ok + +-- Rejected! +g1 :: forall x y . C x y -> () +-- C (..) :: C x y +-- Inside match on C, x=y +g1 (C (p :: y)) = () + +-- OK! +g2 :: forall x y . C x y -> () +-- C (..) :: C x y +-- Inside match on C, x=y +g2 (C (p :: x)) = () + +-- Rejected! +g3 :: forall x y . D x y -> () +-- D (..) :: D x y +-- C (..) :: C sk y +-- sk = y +-- p :: sk +g3 (D (C (p :: y))) = () diff --git a/testsuite/tests/gadt/set.hs b/testsuite/tests/gadt/set.hs new file mode 100644 index 0000000000..3a78bbb64b --- /dev/null +++ b/testsuite/tests/gadt/set.hs @@ -0,0 +1,45 @@ +{-# LANGUAGE GADTs #-} + +-- Provoked by +-- http://www.haskell.org/pipermail/haskell-cafe/2007-January/021086.html + +module ShouldCompile where + +import Data.Set as Set + +data Teq a b where Teq :: Teq a a + +--------------------- +data SetM1 a where + SM1 :: Ord w => Teq w a -> Set.Set w -> SetM1 a + +unionA1 :: SetM1 a -> SetM1 a -> SetM1 a +unionA1 (SM1 Teq m1) (SM1 Teq m2) + = SM1 Teq (m1 `Set.union` m2) + +unionB1 :: SetM1 a -> SetM1 a -> SetM1 a +unionB1 (SM1 p1 m1) (SM1 p2 m2) + = case p1 of Teq -> case p2 of Teq -> SM1 Teq (m1 `Set.union` m2) + +unionC1 :: SetM1 a -> SetM1 a -> SetM1 a +unionC1 (SM1 p1 m1) (SM1 p2 m2) + = case (p1,p2) of (Teq,Teq) -> SM1 Teq (m1 `Set.union` m2) + + +--------------------- +data SetM2 a where + SM2 :: Ord w => Teq a w -> Set.Set w -> SetM2 a + -- Different order of args in Teq + +unionA2 :: SetM2 a -> SetM2 a -> SetM2 a +unionA2 (SM2 Teq m1) (SM2 Teq m2) + = SM2 Teq (m1 `Set.union` m2) + +unionB2 :: SetM2 a -> SetM2 a -> SetM2 a +unionB2 (SM2 p1 m1) (SM2 p2 m2) + = case p1 of Teq -> case p2 of Teq -> SM2 Teq (m1 `Set.union` m2) + +unionC2 :: SetM2 a -> SetM2 a -> SetM2 a +unionC2 (SM2 p1 m1) (SM2 p2 m2) + = case (p1,p2) of (Teq,Teq) -> SM2 Teq (m1 `Set.union` m2) + diff --git a/testsuite/tests/gadt/tc.hs b/testsuite/tests/gadt/tc.hs new file mode 100644 index 0000000000..247b9eb615 --- /dev/null +++ b/testsuite/tests/gadt/tc.hs @@ -0,0 +1,122 @@ +{-# LANGUAGE GADTs, ExistentialQuantification #-}
+
+-- This typechecker, written by Stephanie Weirich at Dagstuhl (Sept 04)
+-- demonstrates that it's possible to write functions of type
+-- tc :: String -> Term a
+-- where Term a is our strongly-typed GADT.
+-- That is, generate a typed term from an untyped source; Lennart
+-- Augustsson set this as a challenge.
+--
+-- In fact the main function goes
+-- tc :: UTerm -> exists ty. (Ty ty, Term ty)
+-- so the type checker returns a pair of an expression and its type,
+-- wrapped, of course, in an existential.
+
+module Main where
+
+-- Untyped world --------------------------------------------
+data UTerm = UVar String
+ | ULam String UType UTerm
+ | UApp UTerm UTerm
+ | UConBool Bool
+ | UIf UTerm UTerm UTerm
+
+data UType = UBool | UArr UType UType
+
+-- Typed world -----------------------------------------------
+data Ty t where
+ Bool :: Ty Bool
+ Arr :: Ty a -> Ty b -> Ty (a -> b)
+
+data Term g t where
+ Var :: Var g t -> Term g t
+ Lam :: Ty a -> Term (g,a) b -> Term g (a->b)
+ App :: Term g (s -> t) -> Term g s -> Term g t
+ ConBool :: Bool -> Term g Bool
+ If :: Term g Bool -> Term g a -> Term g a -> Term g a
+
+data Var g t where
+ ZVar :: Var (h,t) t
+ SVar :: Var h t -> Var (h,s) t
+
+data Typed thing = forall ty. Typed (Ty ty) (thing ty)
+
+-- Typechecking types
+data ExType = forall t. ExType (Ty t)
+
+tcType :: UType -> ExType
+tcType UBool = ExType Bool
+tcType (UArr t1 t2) = case tcType t1 of { ExType t1' ->
+ case tcType t2 of { ExType t2' ->
+ ExType (Arr t1' t2') }}
+
+-- The type environment and lookup
+data TyEnv g where
+ Nil :: TyEnv g
+ Cons :: String -> Ty t -> TyEnv h -> TyEnv (h,t)
+
+lookupVar :: String -> TyEnv g -> Typed (Var g)
+lookupVar _ Nil = error "Variable not found"
+lookupVar v (Cons s ty e)
+ | v==s = Typed ty ZVar
+ | otherwise = case lookupVar v e of
+ Typed ty v -> Typed ty (SVar v)
+
+-- Comparing types
+newtype C1 c a2 d = C1 { unC1 :: c (d -> a2) }
+newtype C2 c b1 d = C2 { unC2 :: c (b1 -> d) }
+
+cast2 :: Ty a -> Ty b -> (c a -> c b)
+cast2 Bool Bool x = x
+cast2 (Arr a1 a2) (Arr b1 b2) f
+ = let C1 x = cast2 a1 b1 (C1 f)
+ C2 y = cast2 a2 b2 (C2 x)
+ in y
+
+data Equal a b where
+ Equal :: Equal c c
+
+cmpTy :: Ty a -> Ty b -> Maybe (Equal a b)
+cmpTy Bool Bool = Just Equal
+cmpTy (Arr a1 a2) (Arr b1 b2)
+ = do { Equal <- cmpTy a1 b1
+ ; Equal <- cmpTy a2 b2
+ ; return Equal }
+
+-- Typechecking terms
+tc :: UTerm -> TyEnv g -> Typed (Term g)
+tc (UVar v) env = case lookupVar v env of
+ Typed ty v -> Typed ty (Var v)
+tc (UConBool b) env
+ = Typed Bool (ConBool b)
+tc (ULam s ty body) env
+ = case tcType ty of { ExType bndr_ty' ->
+ case tc body (Cons s bndr_ty' env) of { Typed body_ty' body' ->
+ Typed (Arr bndr_ty' body_ty')
+ (Lam bndr_ty' body') }}
+tc (UApp e1 e2) env
+ = case tc e1 env of { Typed (Arr bndr_ty body_ty) e1' ->
+ case tc e2 env of { Typed arg_ty e2' ->
+ case cmpTy arg_ty bndr_ty of
+ Nothing -> error "Type error"
+ Just Equal -> Typed body_ty (App e1' e2') }}
+tc (UIf e1 e2 e3) env
+ = case tc e1 env of { Typed Bool e1' ->
+ case tc e2 env of { Typed t2 e2' ->
+ case tc e3 env of { Typed t3 e3' ->
+ case cmpTy t2 t3 of
+ Nothing -> error "Type error"
+ Just Equal -> Typed t2 (If e1' e2' e3') }}}
+
+showType :: Ty a -> String
+showType Bool = "Bool"
+showType (Arr t1 t2) = "(" ++ showType t1 ++ ") -> (" ++ showType t2 ++ ")"
+
+uNot = ULam "x" UBool (UIf (UVar "x") (UConBool False) (UConBool True))
+
+test :: UTerm
+test = UApp uNot (UConBool True)
+
+main = putStrLn (case tc test Nil of
+ Typed ty _ -> showType ty
+ )
\ No newline at end of file diff --git a/testsuite/tests/gadt/tc.stdout b/testsuite/tests/gadt/tc.stdout new file mode 100644 index 0000000000..13b3e8786a --- /dev/null +++ b/testsuite/tests/gadt/tc.stdout @@ -0,0 +1 @@ +Bool diff --git a/testsuite/tests/gadt/tdpe.hs b/testsuite/tests/gadt/tdpe.hs new file mode 100644 index 0000000000..58a4b85094 --- /dev/null +++ b/testsuite/tests/gadt/tdpe.hs @@ -0,0 +1,24 @@ +{-# LANGUAGE GADTs #-} + +module Tdpe where + +data Type t where + TBase :: Type Base + TFun :: Type a -> Type b -> Type (a -> b) + +b :: Type Base +b = TBase + +newtype Base = In { out :: Term Base } + +data Term t where + App :: Term (a->b) -> Term a -> Term b + Fun :: (Term a -> Term b) -> Term (a->b) + +reify :: Type t -> t -> Term t +reify (TBase) v = out v +reify (TFun a b) v = Fun (\x -> reify b (v (reflect a x))) + +reflect :: Type t -> Term t -> t +reflect (TBase) e = In e +reflect (TFun a b) e = \x -> reflect b (App e (reify a x)) diff --git a/testsuite/tests/gadt/termination.hs b/testsuite/tests/gadt/termination.hs new file mode 100644 index 0000000000..be2431b812 --- /dev/null +++ b/testsuite/tests/gadt/termination.hs @@ -0,0 +1,183 @@ +{-# LANGUAGE GADTs, Rank2Types #-} + +module Termination where + +{- Message from Jim Apple to Haskell-Cafe, 7/1/07 + +To show how expressive GADTs are, the datatype Terminating can hold +any term in the untyped lambda calculus that terminates, and none that +don't. I don't think that an encoding of this is too surprising, but I +thought it might be a good demonstration of the power that GADTs +bring. + + + Using GADTs to encode normalizable and non-normalizable terms in + the lambda calculus. For definitions of normalizable and de Bruin + indices, I used: + + Christian Urban and Stefan Berghofer - A Head-to-Head Comparison of + de Bruijn Indices and Names. In Proceedings of the International + Workshop on Logical Frameworks and Meta-Languages: Theory and + Practice (LFMTP 2006). Seattle, USA. ENTCS. Pages 46-59 + + http://www4.in.tum.de/~urbanc/Publications/lfmtp-06.ps + + @incollection{ pierce97foundational, + author = "Benjamin Pierce", + title = "Foundational Calculi for Programming Languages", + booktitle = "The Computer Science and Engineering Handbook", + publisher = "CRC Press", + address = "Boca Raton, FL", + editor = "Allen B. Tucker", + year = "1997", + url = "citeseer.ist.psu.edu/pierce95foundational.html" + } + +> So it sounds to me like the (terminating) type checker solves the +> halting problem. Can you please explain which part of this I have +> misunderstood? + +The Terminating datatype takes three parameters: +1. A term in the untyped lambda calculus +2. A sequence of beta reductions +3. A proof that the result of the beta reductions is normalized. + +Number 2 is the hard part. For a term that calculated the factorial of +5, the list in part 2 would be at least 120 items long, and each one +is kind of a pain. + +GHC's type checker ends up doing exactly what it was doing before: +checking proofs. + +-} + + +-- Terms in the untyped lambda-calculus with the de Bruijn representation + +data Term t where + Var :: Nat n -> Term (Var n) + Lambda :: Term t -> Term (Lambda t) + Apply :: Term t1 -> Term t2 -> Term (Apply t1 t2) + +-- Natural numbers + +data Nat n where + Zero :: Nat Z + Succ :: Nat n -> Nat (S n) + +data Z +data S n + +data Var t +data Lambda t +data Apply t1 t2 + +data Less n m where + LessZero :: Less Z (S n) + LessSucc :: Less n m -> Less (S n) (S m) + +data Equal a b where + Equal :: Equal a a + +data Plus a b c where + PlusZero :: Plus Z b b + PlusSucc :: Plus a b c -> Plus (S a) b (S c) + +{- We can reduce a term by function application, reduction under the lambda, + or reduction of either side of an application. We don't need this full + power, since we could get by with normal-order evaluation, but that + required a more complicated datatype for Reduce. +-} +data Reduce t1 t2 where + ReduceSimple :: Replace Z t1 t2 t3 -> Reduce (Apply (Lambda t1) t2) t3 + ReduceLambda :: Reduce t1 t2 -> Reduce (Lambda t1) (Lambda t2) + ReduceApplyLeft :: Reduce t1 t2 -> Reduce (Apply t1 t3) (Apply t2 t3) + ReduceApplyRight :: Reduce t1 t2 -> Reduce (Apply t3 t1) (Apply t3 t2) + +{- Lift and Replace use the de Bruijn operations as expressed in the Urban + and Berghofer paper. -} +data Lift n k t1 t2 where + LiftVarLess :: Less i k -> Lift n k (Var i) (Var i) + LiftVarGTE :: Either (Equal i k) (Less k i) -> Plus i n r -> Lift n k (Var i) (Var r) + LiftApply :: Lift n k t1 t1' -> Lift n k t2 t2' -> Lift n k (Apply t1 t2) (Apply t1' t2') + LiftLambda :: Lift n (S k) t1 t2 -> Lift n k (Lambda t1) (Lambda t2) + +data Replace k t n r where + ReplaceVarLess :: Less i k -> Replace k (Var i) n (Var i) + ReplaceVarEq :: Equal i k -> Lift k Z n r -> Replace k (Var i) n r + ReplaceVarMore :: Less k (S i) -> Replace k (Var (S i)) n (Var i) + ReplaceApply :: Replace k t1 n r1 -> Replace k t2 n r2 -> Replace k (Apply t1 t2) n (Apply r1 r2) + ReplaceLambda :: Replace (S k) t n r -> Replace k (Lambda t) n (Lambda r) + +{- Reflexive transitive closure of the reduction relation. -} +data ReduceEventually t1 t2 where + ReduceZero :: ReduceEventually t1 t1 + ReduceSucc :: Reduce t1 t2 -> ReduceEventually t2 t3 -> ReduceEventually t1 t3 + +-- Definition of normal form: nothing with a lambda term applied to anything. +data Normal t where + NormalVar :: Normal (Var n) + NormalLambda :: Normal t -> Normal (Lambda t) + NormalApplyVar :: Normal t -> Normal (Apply (Var i) t) + NormalApplyApply :: Normal (Apply t1 t2) -> Normal t3 -> Normal (Apply (Apply t1 t2) t3) + +-- Something is terminating when it reduces to something normal +data Terminating where + Terminating :: Term t -> ReduceEventually t t' -> Normal t' -> Terminating + +{- We can encode terms that are non-terminating, even though this set is + only co-recursively enumerable, so we can't actually prove all of the + non-normalizable terms of the lambda calculus are non-normalizable. +-} + +data Reducible t1 where + Reducible :: Reduce t1 t2 -> Reducible t1 +-- A term is non-normalizable if, no matter how many reductions you have applied, +-- you can still apply one more. +type Infinite t1 = forall t2 . ReduceEventually t1 t2 -> Reducible t2 + +data NonTerminating where + NonTerminating :: Term t -> Infinite t -> NonTerminating + +-- x +test1 :: Terminating +test1 = Terminating (Var Zero) ReduceZero NormalVar + +-- (\x . x)@y +test2 :: Terminating +test2 = Terminating (Apply (Lambda (Var Zero))(Var Zero)) + (ReduceSucc (ReduceSimple (ReplaceVarEq Equal (LiftVarGTE (Left Equal) PlusZero))) ReduceZero) + NormalVar + +-- omega = \x.x@x +type Omega = Lambda (Apply (Var Z) (Var Z)) +omega = Lambda (Apply (Var Zero) (Var Zero)) + +-- (\x . \y . y)@(\z.z@z) +test3 :: Terminating +test3 = Terminating (Apply (Lambda (Lambda (Var Zero))) omega) + (ReduceSucc (ReduceSimple (ReplaceLambda (ReplaceVarLess LessZero))) ReduceZero) + (NormalLambda NormalVar) + +-- (\x.x@x)(\x.x@x) +test4 :: NonTerminating +test4 = NonTerminating (Apply omega omega) help3 + +help1 :: Reducible (Apply Omega Omega) +help1 = Reducible (ReduceSimple + (ReplaceApply (ReplaceVarEq Equal (LiftLambda + (LiftApply (LiftVarLess LessZero) (LiftVarLess LessZero)))) + (ReplaceVarEq Equal (LiftLambda (LiftApply + (LiftVarLess LessZero) (LiftVarLess LessZero)))))) + +help2 :: ReduceEventually (Apply Omega Omega) t -> Equal (Apply Omega Omega) t +help2 ReduceZero = Equal +help2 (ReduceSucc (ReduceSimple (ReplaceApply + (ReplaceVarEq _ (LiftLambda (LiftApply (LiftVarLess _) (LiftVarLess _)))) + (ReplaceVarEq _ (LiftLambda (LiftApply (LiftVarLess _) (LiftVarLess _)))))) y) + = case help2 y of + Equal -> Equal + +help3 :: Infinite (Apply Omega Omega) +help3 x = case help2 x of + Equal -> help1 diff --git a/testsuite/tests/gadt/type-rep.hs b/testsuite/tests/gadt/type-rep.hs new file mode 100644 index 0000000000..ed41c7a5cc --- /dev/null +++ b/testsuite/tests/gadt/type-rep.hs @@ -0,0 +1,38 @@ +{-# LANGUAGE GADTs #-} + +module Main where + +data Rep t where + Rint :: Rep Int + Rchar :: Rep Char + Runit :: Rep () + Rpair :: Rep a -> Rep b -> Rep (a,b) + Rsum :: Rep a -> Rep b -> Rep (Either a b) + Rcon :: String -> Rep t -> Rep t + Rdata :: Rep i -> (t -> i) -> (i -> t) -> Rep t + + +int :: Rep Int +int = Rint + +list :: Rep a -> Rep [a] +list x = Rdata (Rsum (Rcon "[]" Runit) (Rcon ":" (Rpair x (list x)))) h g + where + h [] = Left () + h (x:xs) = Right (x,xs) + + g (Left ()) = [] + g (Right (x,xs)) = x:xs + + +addUp :: Rep a -> a -> Int +addUp Rint n = n +addUp (Rpair r s) (x,y) = addUp r x + addUp s y +addUp (Rsum r s) (Left x) = addUp r x +addUp (Rsum r s) (Right x) = addUp s x +addUp (Rdata i f g) x = addUp i (f x) +addUp (Rcon s r) x = addUp r x +addUp v x = 0 + + +main = print (addUp (list int) [1,2,4]) diff --git a/testsuite/tests/gadt/type-rep.stdout b/testsuite/tests/gadt/type-rep.stdout new file mode 100644 index 0000000000..7f8f011eb7 --- /dev/null +++ b/testsuite/tests/gadt/type-rep.stdout @@ -0,0 +1 @@ +7 diff --git a/testsuite/tests/gadt/ubx-records.hs b/testsuite/tests/gadt/ubx-records.hs new file mode 100644 index 0000000000..ab21dc65fe --- /dev/null +++ b/testsuite/tests/gadt/ubx-records.hs @@ -0,0 +1,30 @@ +{-# LANGUAGE GADTs #-} +{-# OPTIONS_GHC -funbox-strict-fields #-} + +-- Tests record selectors with unboxed fields for GADTs + +module Main where + +data T a where + T1 :: { w :: !(Int, Int), x :: a, y :: b } -> T (a,b) + T2 :: { w :: !(Int, Int), x :: a } -> T (a,b) + T3 :: { z :: Int } -> T Bool + +-- T1 :: forall c a b. (c~(a,b)) => (Int,Int) -> a -> b -> T c + +f xv yv = T1 { w = (0,0), x = xv, y = yv } + +g :: T a -> T a +g (T1 {x=xv, y=yv}) = T2 { w = (0,0), x = xv } + +-- h :: Num a => T a any -> a +h v = x v + 1 + +i v = let (x,y) = w v in x + y + +main = do { let t1 = T1 { w = (0,0), y = "foo", x = 4 } + t2 = g t1 + ; print (h (f 8 undefined)) + ; print (h t2) + ; print (i t1) + } diff --git a/testsuite/tests/gadt/ubx-records.stdout b/testsuite/tests/gadt/ubx-records.stdout new file mode 100644 index 0000000000..bb9cc4d945 --- /dev/null +++ b/testsuite/tests/gadt/ubx-records.stdout @@ -0,0 +1,3 @@ +9 +5 +0 diff --git a/testsuite/tests/gadt/while.hs b/testsuite/tests/gadt/while.hs new file mode 100644 index 0000000000..2040511c0f --- /dev/null +++ b/testsuite/tests/gadt/while.hs @@ -0,0 +1,216 @@ +{-# LANGUAGE GADTs, ExistentialQuantification #-} + +module Main where + +succeed :: a -> Maybe a +succeed = return + +data V s t where + Z :: V (t,m) t + S :: V m t -> V (x,m) t + +data Exp s t where + IntC :: Int -> Exp s Int -- 5 + BoolC :: Bool -> Exp s Bool -- True + Plus :: Exp s Int -> Exp s Int -> Exp s Int -- x + 3 + Lteq :: Exp s Int -> Exp s Int -> Exp s Bool -- x <= 3 + Var :: V s t -> Exp s t -- x + +data Com s where + Set :: V s t -> Exp s t -> Com s -- x := e + Seq :: Com s -> Com s -> Com s -- { s1; s2; } + If :: Exp s Bool -> Com s -> Com s -> Com s -- if e then x else y + While :: Exp s Bool -> Com s -> Com s -- while e do s + Declare :: Exp s t -> Com (t,s) -> Com s -- { int x = 5; s } + +update :: (V s t) -> t -> s -> s +update Z n (x,y) = (n,y) +update (S v) n (x,y) = (x,update v n y) + +eval :: Exp s t -> s -> t +eval (IntC n) s = n +eval (BoolC b) s = b +eval (Plus x y) s = (eval x s) + (eval y s) +eval (Lteq x y) s = (eval x s) <= (eval y s) +eval (Var Z) (x,y) = x +eval (Var (S v)) (x,y) = eval (Var v) y + + +exec :: (Com st) -> st -> st +exec (Set v e) s = update v (eval e s) s +exec (Seq x y) s = exec y (exec x s) +exec (If test x1 x2) s = + if (eval test s) then exec x1 s else exec x2 s +exec (While test body) s = loop s + where loop s = if (eval test s) + then loop (exec body s) + else s +exec (Declare e body) s = store + where (_,store) = (exec body (eval e s,s)) + +v0 = Z +v1 = S Z +v2 = S (S Z) +v3 = S (S (S Z)) + +e2 = Lteq (Plus (Var v0)(Var v1)) (Plus (Var v0) (IntC 1)) + +sum_var = Z +x = S Z + +prog :: Com (Int,(Int,a)) +prog = + Seq (Set sum_var (IntC 0)) + (Seq (Set x (IntC 1)) + (While (Lteq (Var x) (IntC 5)) + (Seq (Set sum_var (Plus (Var sum_var)(Var x))) + (Set x (Plus (Var x) (IntC 1)))))) + +ans = exec prog (34,(12,1)) +main = print ans +{- +{ sum = 0 ; + x = 1; + while (x <= 5) + { sum = sum + x; + x = x + 1; + } +} +-} + + +--------------------------------------------------- +-- Untyped Annotated AST + +data TyAst = I | B | P TyAst TyAst + +data TypeR t where + IntR :: TypeR Int + BoolR :: TypeR Bool + PairR :: TypeR a -> TypeR b -> TypeR (a,b) + +-- Judgments for Types +data TJudgment = forall t . TJ (TypeR t) + +checkT :: TyAst -> TJudgment +checkT I = TJ IntR +checkT B = TJ BoolR +checkT (P x y) = + case (checkT x,checkT y) of + (TJ a, TJ b) -> TJ(PairR a b) + +---------------------------------------------------- +-- Equality Proofs and Type representations +data Equal a b where + EqProof :: Equal a a + +match :: TypeR a -> TypeR b -> Maybe (Equal a b) +match IntR IntR = succeed EqProof +match BoolR BoolR = succeed EqProof +match (PairR a b) (PairR c d) = + do { EqProof <- match a c + ; EqProof <- match b d + ; succeed EqProof } +match _ _ = fail "match fails" + + +---------------------------------------------- +-- checking Variables are consistent + +checkV :: Int -> TypeR t -> TypeR s -> Maybe(V s t) +checkV 0 t1 (PairR t2 p) = + do { EqProof <- match t1 t2 + ; return Z } +checkV n t1 (PairR ty p) = + do { v <- checkV (n-1) t1 p; return(S v)} +checkV n t1 sr = Nothing + + +----------------------------------------------------- +data ExpAst + = IntCA Int + | BoolCA Bool + | PlusA ExpAst ExpAst + | LteqA ExpAst ExpAst + | VarA Int TyAst + +-- Judgments for Expressions +data EJudgment s = forall t . EJ (TypeR t) (Exp s t) + +checkE :: ExpAst -> TypeR s -> Maybe (EJudgment s) +checkE (IntCA n) sr = succeed(EJ IntR (IntC n)) +checkE (BoolCA b) sr = succeed(EJ BoolR (BoolC b)) +checkE (PlusA x y) sr = + do { EJ t1 e1 <- checkE x sr + ; EqProof <- match t1 IntR + ; EJ t2 e2 <- checkE y sr + ; EqProof <- match t2 IntR + ; succeed(EJ IntR (Plus e1 e2))} +checkE (VarA n ty) sr = + do { TJ t <- succeed(checkT ty) + ; v <- checkV n t sr + ; return(EJ t (Var v)) } + +----------------------------------------------------- +data ComAst + = SetA Int TyAst ExpAst + | SeqA ComAst ComAst + | IfA ExpAst ComAst ComAst + | WhileA ExpAst ComAst + | DeclareA TyAst ExpAst ComAst + +data CJudgment s = EC (Com s) + +checkC :: ComAst -> TypeR s -> Maybe(CJudgment s) +checkC (SetA n ty e) sr = + do { TJ t1 <- succeed(checkT ty) + ; v <- checkV n t1 sr + ; EJ t2 e1 <- checkE e sr + ; EqProof <- match t1 t2 + ; return(EC (Set v e1))} +checkC (SeqA x y) sr = + do { EC c1 <- checkC x sr + ; EC c2 <- checkC y sr + ; return(EC (Seq c1 c2)) } +checkC (IfA e x y) sr = + do { EJ t1 e1 <- checkE e sr + ; EqProof <- match t1 BoolR + ; EC c1 <- checkC x sr + ; EC c2 <- checkC y sr + ; return(EC(If e1 c1 c2)) } +checkC (WhileA e x) sr = + do { EJ t1 e1 <- checkE e sr + ; EqProof <- match t1 BoolR + ; EC c1 <- checkC x sr + ; return(EC(While e1 c1)) } +checkC (DeclareA ty e c) sr = + do { TJ t1 <- succeed(checkT ty) + ; EJ t2 e2 <- checkE e sr + ; EqProof <- match t1 t2 + ; EC c2 <- checkC c (PairR t1 sr) + ; return(EC(Declare e2 c2)) } + +-------------------------------------------------------------- + +e1 = Lteq (Plus (Var sum_var)(Var x)) (Plus (Var x) (IntC 1)) + +{- +data Store s + = M (Code s) + | forall a b . N (Code a) (Store b) where s = (a,b) + +eval2 :: Exp s t -> Store s -> Code t +eval2 (IntC n) s = lift n +eval2 (BoolC b) s = lift b +eval2 (Plus x y) s = [| $(eval2 x s) + $(eval2 y s) |] +eval2 (Lteq x y) s = [| $(eval2 x s) <= $(eval2 y s) |] +eval2 (Var Z) (N a b) = a +eval2 (Var (S v)) (N a b) = eval2 (Var v) b +eval2 (Var Z) (M x) = [| fst $x |] +eval2 (Var (S v)) (M x) = eval2 (Var v) (M [| snd $x |]) + + +test e = [| \ (x,(y,z)) -> $(eval2 e (N [|x|] (N [|y|] (M [|z|])))) |] + +-- test e1 ---> [| \ (x,(y,z)) -> x + y <= y + 1 |] +-}
\ No newline at end of file diff --git a/testsuite/tests/gadt/while.stdout b/testsuite/tests/gadt/while.stdout new file mode 100644 index 0000000000..8237a9beac --- /dev/null +++ b/testsuite/tests/gadt/while.stdout @@ -0,0 +1 @@ +(15,(6,1)) |