Modify a couple of error messages slightly
[ghc.git] / testsuite / tests / gadt / tc.hs
1 {-# LANGUAGE GADTs, ExistentialQuantification #-}
2
3 -- This typechecker, written by Stephanie Weirich at Dagstuhl (Sept 04)
4 -- demonstrates that it's possible to write functions of type
5 -- tc :: String -> Term a
6 -- where Term a is our strongly-typed GADT.
7 -- That is, generate a typed term from an untyped source; Lennart
8 -- Augustsson set this as a challenge.
9 --
10 -- In fact the main function goes
11 -- tc :: UTerm -> exists ty. (Ty ty, Term ty)
12 -- so the type checker returns a pair of an expression and its type,
13 -- wrapped, of course, in an existential.
14
15 module Main where
16
17 -- Untyped world --------------------------------------------
18 data UTerm = UVar String
19 | ULam String UType UTerm
20 | UApp UTerm UTerm
21 | UConBool Bool
22 | UIf UTerm UTerm UTerm
23
24 data UType = UBool | UArr UType UType
25
26 -- Typed world -----------------------------------------------
27 data Ty t where
28 Bool :: Ty Bool
29 Arr :: Ty a -> Ty b -> Ty (a -> b)
30
31 data Term g t where
32 Var :: Var g t -> Term g t
33 Lam :: Ty a -> Term (g,a) b -> Term g (a->b)
34 App :: Term g (s -> t) -> Term g s -> Term g t
35 ConBool :: Bool -> Term g Bool
36 If :: Term g Bool -> Term g a -> Term g a -> Term g a
37
38 data Var g t where
39 ZVar :: Var (h,t) t
40 SVar :: Var h t -> Var (h,s) t
41
42 data Typed thing = forall ty. Typed (Ty ty) (thing ty)
43
44 -- Typechecking types
45 data ExType = forall t. ExType (Ty t)
46
47 tcType :: UType -> ExType
48 tcType UBool = ExType Bool
49 tcType (UArr t1 t2) = case tcType t1 of { ExType t1' ->
50 case tcType t2 of { ExType t2' ->
51 ExType (Arr t1' t2') }}
52
53 -- The type environment and lookup
54 data TyEnv g where
55 Nil :: TyEnv g
56 Cons :: String -> Ty t -> TyEnv h -> TyEnv (h,t)
57
58 lookupVar :: String -> TyEnv g -> Typed (Var g)
59 lookupVar _ Nil = error "Variable not found"
60 lookupVar v (Cons s ty e)
61 | v==s = Typed ty ZVar
62 | otherwise = case lookupVar v e of
63 Typed ty v -> Typed ty (SVar v)
64
65 -- Comparing types
66 newtype C1 c a2 d = C1 { unC1 :: c (d -> a2) }
67 newtype C2 c b1 d = C2 { unC2 :: c (b1 -> d) }
68
69 cast2 :: Ty a -> Ty b -> (c a -> c b)
70 cast2 Bool Bool x = x
71 cast2 (Arr a1 a2) (Arr b1 b2) f
72 = let C1 x = cast2 a1 b1 (C1 f)
73 C2 y = cast2 a2 b2 (C2 x)
74 in y
75
76 data Equal a b where
77 Equal :: Equal c c
78
79 cmpTy :: Ty a -> Ty b -> Maybe (Equal a b)
80 cmpTy Bool Bool = Just Equal
81 cmpTy (Arr a1 a2) (Arr b1 b2)
82 = do { Equal <- cmpTy a1 b1
83 ; Equal <- cmpTy a2 b2
84 ; return Equal }
85
86 -- Typechecking terms
87 tc :: UTerm -> TyEnv g -> Typed (Term g)
88 tc (UVar v) env = case lookupVar v env of
89 Typed ty v -> Typed ty (Var v)
90 tc (UConBool b) env
91 = Typed Bool (ConBool b)
92 tc (ULam s ty body) env
93 = case tcType ty of { ExType bndr_ty' ->
94 case tc body (Cons s bndr_ty' env) of { Typed body_ty' body' ->
95 Typed (Arr bndr_ty' body_ty')
96 (Lam bndr_ty' body') }}
97 tc (UApp e1 e2) env
98 = case tc e1 env of { Typed (Arr bndr_ty body_ty) e1' ->
99 case tc e2 env of { Typed arg_ty e2' ->
100 case cmpTy arg_ty bndr_ty of
101 Nothing -> error "Type error"
102 Just Equal -> Typed body_ty (App e1' e2') }}
103 tc (UIf e1 e2 e3) env
104 = case tc e1 env of { Typed Bool e1' ->
105 case tc e2 env of { Typed t2 e2' ->
106 case tc e3 env of { Typed t3 e3' ->
107 case cmpTy t2 t3 of
108 Nothing -> error "Type error"
109 Just Equal -> Typed t2 (If e1' e2' e3') }}}
110
111 showType :: Ty a -> String
112 showType Bool = "Bool"
113 showType (Arr t1 t2) = "(" ++ showType t1 ++ ") -> (" ++ showType t2 ++ ")"
114
115 uNot = ULam "x" UBool (UIf (UVar "x") (UConBool False) (UConBool True))
116
117 test :: UTerm
118 test = UApp uNot (UConBool True)
119
120 main = putStrLn (case tc test Nil of
121 Typed ty _ -> showType ty
122 )