sem.icl

   1 implementation module sem
   2
   3 import qualified Data.Map as Map
   4
   5 from Data.Func import $
   6 from StdFunc import o, flip, const, id
   7
   8 import Control.Applicative
   9 import Control.Monad
  10 import Control.Monad.Trans
  11 import Control.Monad.State
  12 import Data.Either
  13 import Data.Maybe
  14 import Data.Monoid
  15 import Data.List
  16 import Data.Functor
  17 import Data.Tuple
  18
  19 import StdString
  20 import StdTuple
  21 import StdList
  22 import StdMisc
  23 import StdEnum
  24 import GenEq
  25
  26 from Text import class Text(concat), instance Text String
  27
  28 import AST
  29
  30 :: Scheme = Forall [TVar] Type
  31 :: Gamma :== 'Map'.Map String Scheme //map from Variables! to types
  32 :: Typing a :== StateT (Gamma, [TVar]) (Either SemError) a
  33 :: Substitution :== 'Map'.Map TVar Type
  34 :: Constraints :== [(Type, Type)]
  35 :: SemError
  36         = ParseError Pos String
  37         | UnifyError Pos Type Type
  38     | InfiniteTypeError Pos Type
  39     | FieldSelectorError Pos Type FieldSelector
  40         | OperatorError Pos Op2 Type
  41     | UndeclaredVariableError Pos String
  42     | ArgumentMisMatchError Pos String
  43         | SanityError Pos String
  44         | Error String
  45
  46 instance zero Gamma where
  47         zero = 'Map'.newMap
  48
  49 variableStream :: [TVar]
  50 variableStream = map toString [1..]
  51
  52 defaultGamma :: Gamma //includes all default functions
  53 defaultGamma = extend "print" (Forall ["a"] ((IdType "a") ->> VoidType))
  54                 $ extend "isEmpty" (Forall ["a"] ((ListType (IdType "a")) ->> BoolType))
  55                 $ extend "read" (Forall [] (FuncType CharType))
  56                 $ extend "1printchar" (Forall [] (CharType ->> VoidType))
  57                 $ extend "1printint" (Forall [] (IntType ->> VoidType))
  58                 $ extend "1printbool" (Forall [] (BoolType ->> VoidType))
  59                 zero
  60
  61 sem :: AST -> Either [SemError] (AST, Gamma)
  62 sem (AST fd) = case foldM (const $ hasNoDups fd) () fd
  63                         >>| foldM (const isNiceMain) () fd
  64                         >>| hasMain fd
  65                     >>| runStateT (unfoldLambda fd >>= type) (defaultGamma, variableStream) of
  66         Left e = Left [e]
  67     Right ((_,fds),(gam,_)) = Right (AST fds, gam)
  68 where
  69                 hasNoDups :: [FunDecl] FunDecl -> Either SemError ()
  70                 hasNoDups fds (FunDecl p n _ _ _ _)
  71                 # mbs = map (\(FunDecl p` n` _ _ _ _)->if (n == n`) (Just p`) Nothing) fds
  72                 = case catMaybes mbs of
  73                         [] = Left $ SanityError p "HUH THIS SHOULDN'T HAPPEN"
  74                         [x] = pure ()
  75                         [_:x] = Left $ SanityError p (concat
  76                                 [n, " multiply defined at ", toString p])
  77
  78                 hasMain :: [FunDecl] -> Either SemError ()
  79                 hasMain [(FunDecl _ "main" _ _ _ _):fd] = pure ()
  80                 hasMain [_:fd] = hasMain fd
  81                 hasMain [] = Left $ SanityError zero "no main function defined"
  82
  83                 isNiceMain :: FunDecl -> Either SemError ()
  84                 isNiceMain (FunDecl p "main" as mt _ _) = case (as, mt) of
  85                         ([_:_], _) = Left $ SanityError p "main must have arity 0"
  86                         ([], t) = (case t of
  87                                 Nothing = pure ()
  88                                 Just VoidType = pure ()
  89                                 _ = Left $ SanityError p "main has to return Void")
  90                 isNiceMain _ = pure ()
  91
  92
  93 //------------------
  94 // LAMBDA UNFOLDING
  95 //------------------
  96 unfoldLambda :: [FunDecl] -> Typing [FunDecl]
  97 unfoldLambda [] = pure []
  98 unfoldLambda [fd:fds] = unfoldL_ fd >>= \(gen1, fs_)->
  99                         unfoldLambda fds >>= \gen2->
 100                         pure $ gen1 ++ [fs_] ++ gen2
 101
 102 flattenT :: [([a],b)] -> ([a],[b])
 103 flattenT ts = (flatten $ map fst ts, map snd ts)
 104
 105 class unfoldL_ a :: a -> Typing ([FunDecl], a)
 106
 107 instance unfoldL_ FunDecl where
 108     unfoldL_ (FunDecl p f args mt vds stmts) =
 109         flattenT <$> mapM unfoldL_ vds >>= \(fds1,vds_) ->
 110         flattenT <$> mapM unfoldL_ stmts >>= \(fds2,stmts_)->
 111         pure (fds1 ++ fds2, FunDecl p f args mt vds_ stmts_)
 112
 113 instance unfoldL_ VarDecl where
 114     unfoldL_ (VarDecl p mt v e) = unfoldL_ e >>= \(fds, e_)->pure (fds, VarDecl p mt v e_)
 115
 116 instance unfoldL_ Stmt where
 117     unfoldL_ (IfStmt e th el) = unfoldL_ e >>= \(fds, e_)->pure (fds, IfStmt e_ th el)
 118     unfoldL_ (WhileStmt e c) = unfoldL_ e >>= \(fds, e_)->pure (fds, WhileStmt e_ c)
 119     unfoldL_ (AssStmt vd e) = unfoldL_ e >>= \(fds, e_)->pure (fds, AssStmt vd e_)
 120     unfoldL_ (FunStmt f es fs) = flattenT <$> mapM unfoldL_ es >>= \(fds, es_)->
 121         pure (fds, FunStmt f es_ fs)
 122     unfoldL_ (ReturnStmt (Just e)) = unfoldL_ e >>= \(fds, e_) ->
 123         pure (fds, ReturnStmt (Just e_))
 124     unfoldL_ (ReturnStmt Nothing) = pure ([], ReturnStmt Nothing)
 125
 126 instance unfoldL_ Expr where
 127     unfoldL_ (LambdaExpr p args e) =
 128         fresh >>= \(IdType n) ->
 129         let f = ("2lambda_"+++n) in
 130         let fd = FunDecl p f args Nothing [] [ReturnStmt $ Just e] in
 131         let fe = VarExpr p (VarDef f []) in
 132         pure ([fd], fe)
 133     unfoldL_ (FunExpr p f es fs) = flattenT <$> mapM unfoldL_ es >>= \(fds, es_)->
 134         pure (fds, FunExpr p f es_ fs)
 135     unfoldL_ (Op2Expr p e1 op e2) = unfoldL_ e1 >>= \(fds1, e1_)->
 136         unfoldL_ e2 >>= \(fds2, e2_)->
 137         pure (fds1++fds2, Op2Expr p e1_ op e2_)
 138     unfoldL_ (Op1Expr p op e1) = unfoldL_ e1 >>= \(fds, e1_)->pure (fds, Op1Expr p op e1_)
 139     unfoldL_ (TupleExpr p (e1, e2)) = unfoldL_ e1 >>= \(fds1, e1_)->
 140         unfoldL_ e2 >>= \(fds2, e2_)->
 141         pure (fds1++fds2, TupleExpr p (e1_, e2_))
 142     unfoldL_ e = pure ([], e)
 143
 144 //------------
 145 //------------
 146 //      TYPING
 147 //------------
 148 //------------
 149
 150 class Typeable a where
 151     ftv :: a -> [TVar]
 152     subst :: Substitution a -> a
 153
 154 instance Typeable Scheme where
 155     ftv (Forall bound t) = difference (ftv t) bound
 156     subst s (Forall bound t) = Forall bound $ subst s_ t
 157         where s_ = 'Map'.filterWithKey (\k _ -> not (elem k bound)) s
 158
 159 instance Typeable [a] | Typeable a where
 160     ftv types   = foldr (\t ts-> ftv t ++ ts) [] types
 161     subst s ts  = map (\t->subst s t) ts
 162
 163 instance Typeable Type where
 164     ftv (TupleType (t1, t2))    = ftv t1 ++ ftv t2
 165     ftv (ListType t)            = ftv t
 166     ftv (IdType tvar)           = [tvar]
 167     ftv (FuncType t)            = ftv t
 168     ftv (t1 ->> t2)             = ftv t1 ++ ftv t2
 169     ftv _                       = []
 170     subst s (TupleType (t1, t2))= TupleType (subst s t1, subst s t2)
 171     subst s (ListType t1)       = ListType (subst s t1)
 172     subst s (FuncType t)        = FuncType (subst s t)
 173     subst s (t1 ->> t2)         = (subst s t1) ->> (subst s t2)
 174     subst s t1=:(IdType tvar)   = 'Map'.findWithDefault t1 tvar s
 175     subst s t                   = t
 176
 177 instance Typeable Gamma where
 178     ftv gamma       = concatMap id $ map ftv ('Map'.elems gamma)
 179     subst s gamma   = Mapmap (subst s) gamma
 180
 181 extend :: String Scheme Gamma -> Gamma
 182 extend k t g = 'Map'.put k t g
 183
 184 //// ------------------------
 185 //// algorithm U, Unification
 186 //// ------------------------
 187 instance zero Substitution where zero = 'Map'.newMap
 188
 189 compose :: Substitution Substitution -> Substitution
 190 compose s1 s2 = 'Map'.union (Mapmap (subst s1) s2) s1
 191 //Note: just like function compositon compose does snd first
 192
 193 occurs :: TVar a -> Bool | Typeable a
 194 occurs tvar a = elem tvar (ftv a)
 195
 196 unify :: Type Type -> Either SemError Substitution
 197 unify t1 t2=:(IdType tv)    | t1 == (IdType tv) = Right zero
 198                             | occurs tv t1 = Left $ InfiniteTypeError zero t1
 199                             | otherwise = Right $ 'Map'.singleton tv t1
 200 unify t1=:(IdType tv) t2 = unify t2 t1
 201 unify (ta1->>ta2) (tb1->>tb2) = unify ta1 tb1 >>= \s1->
 202                                 unify ta2 tb2 >>= \s2->
 203                                 Right $ compose s1 s2
 204 unify (TupleType (ta1,ta2)) (TupleType (tb1,tb2)) = unify ta1 tb1 >>= \s1->
 205                                                     unify ta2 tb2 >>= \s2->
 206                                                     Right $ compose s1 s2
 207 unify (ListType t1) (ListType t2) = unify t1 t2
 208 unify (FuncType t1) (FuncType t2) = unify t1 t2
 209 unify t1 t2 | t1 == t2  = Right zero
 210             | otherwise = Left $ UnifyError zero t1 t2
 211
 212 //// ------------------------
 213 //// Algorithm M, Inference and Solving
 214 //// ------------------------
 215 gamma :: Typing Gamma
 216 gamma = gets fst
 217 putGamma :: Gamma -> Typing ()
 218 putGamma g = modify (appFst $ const g) >>| pure ()
 219 changeGamma :: (Gamma -> Gamma) -> Typing Gamma
 220 changeGamma f = modify (appFst f) >>| gamma
 221 withGamma :: (Gamma -> a) -> Typing a
 222 withGamma f = f <$> gamma
 223 fresh :: Typing Type
 224 fresh = gets snd >>= \vars->
 225         modify (appSnd $ const $ tail vars) >>|
 226         pure (IdType (head vars))
 227
 228 lift :: (Either SemError a) -> Typing a
 229 lift (Left e) = liftT $ Left e
 230 lift (Right v) = pure v
 231
 232 //instantiate maps a schemes type variables to variables with fresh names
 233 //and drops the quantification: i.e. forall a,b.a->[b] becomes c->[d]
 234 instantiate :: Scheme -> Typing Type
 235 instantiate (Forall bound t) =
 236     mapM (const fresh) bound >>= \newVars->
 237     let s = 'Map'.fromList (zip (bound,newVars)) in
 238     pure (subst s t)
 239
 240 //generalize quentifies all free type variables in a type which are not
 241 //in the gamma
 242 generalize :: Type -> Typing Scheme
 243 generalize t = gamma >>= \g-> pure $ Forall (difference (ftv t) (ftv g)) t
 244
 245 lookup :: String -> Typing Type
 246 lookup k = gamma >>= \g-> case 'Map'.member k g of
 247     False = liftT (Left $ UndeclaredVariableError zero k)
 248     True = instantiate $ 'Map'.find k g
 249
 250 //The inference class
 251 //When tying it all together we will treat the program is a big
 252 //let x=e1 in let y=e2 in ....
 253 class infer a :: a -> Typing (Substitution, Type, a)
 254
 255 ////---- Inference for Expressions ----
 256
 257 instance infer Expr where
 258  infer e = case e of
 259     VarExpr _ (VarDef k fs) = lookup k >>= \t ->
 260         foldM foldFieldSelectors t fs >>= \finalT ->
 261         pure (zero, finalT, e)
 262
 263     Op2Expr p e1 op e2 =
 264         infer e1 >>= \(s1, t1, e1_) ->
 265         applySubst s1 >>|
 266         infer e2 >>= \(s2, t2, e2_) ->
 267         applySubst s2 >>|
 268         fresh >>= \tv ->
 269         let given = t1 ->> t2 ->> tv in
 270         op2Type op >>= \expected ->
 271         lift (unify expected given) >>= \s3 ->
 272         pure ((compose s3 $ compose s2 s1), subst s3 tv, Op2Expr p e1_ op e2_)
 273
 274     Op1Expr p op e1 =
 275         infer e1 >>= \(s1, t1, e1_) ->
 276         fresh >>= \tv ->
 277         let given = t1 ->> tv in
 278         op1Type op >>= \expected ->
 279         lift (unify expected given) >>= \s2 ->
 280         pure (compose s2 s1, subst s2 tv, Op1Expr p op e1)
 281
 282     EmptyListExpr _ = (\tv->(zero,tv,e)) <$> fresh
 283
 284     TupleExpr p (e1, e2) =
 285         infer e1 >>= \(s1, t1, e1_) ->
 286         infer e2 >>= \(s2, t2, e2_) ->
 287         pure (compose s2 s1, TupleType (t1,t2), TupleExpr p (e1_,e2_))
 288
 289     LambdaExpr _ _ _ = liftT $ Left $ Error "PANIC: lambdas should be Unfolded"
 290
 291     FunExpr p f args fs =
 292         lookup f >>= \expected ->
 293         let accST = (\(s,ts,es) e->infer e >>= \(s_,et,e_)-> pure (compose s_ s,ts++[et],es++[e_])) in
 294         foldM accST (zero,[],[]) args >>= \(s1, argTs, args_)->
 295         (case f of
 296             "print" = case head argTs of
 297                 IntType = pure "1printint"
 298                 CharType = pure "1printchar"
 299                 BoolType = pure "1printbool"
 300                 ListType (CharType) = pure "1printstr"
 301                 t = liftT $ Left $ SanityError p ("can not print " +++ toString t)
 302             _ = pure f
 303         ) >>= \newF->
 304         fresh >>= \tv->case expected of
 305             FuncType t = pure (s1, t, (FunExpr p newF args fs))
 306                 //TODO: Fieldselectors!
 307             _ = (let given = foldr (->>) tv argTs in
 308                 lift (unify expected given) >>= \s2->
 309                 let fReturnType = subst s2 tv in
 310                 foldM foldFieldSelectors fReturnType fs >>= \returnType ->
 311                 pure (compose s2 s1, returnType, FunExpr p newF args_ fs))
 312
 313     IntExpr _ _ = pure $ (zero, IntType, e)
 314     BoolExpr _ _ = pure $ (zero, BoolType, e)
 315     CharExpr _ _ = pure $ (zero, CharType, e)
 316
 317 foldFieldSelectors :: Type FieldSelector -> Typing Type
 318 foldFieldSelectors (ListType t) (FieldHd) = pure t
 319 foldFieldSelectors t=:(ListType _) (FieldTl) = pure t
 320 foldFieldSelectors (TupleType (t1, _)) (FieldFst) = pure t1
 321 foldFieldSelectors (TupleType (_, t2)) (FieldSnd) = pure t2
 322 foldFieldSelectors t fs = liftT $ Left $ FieldSelectorError zero t fs
 323
 324 op2Type :: Op2 -> Typing Type
 325 op2Type op
 326 | elem op [BiPlus, BiMinus, BiTimes, BiDivide, BiMod]
 327   = pure (IntType ->> IntType ->> IntType)
 328 | elem op [BiEquals, BiUnEqual]
 329   = fresh >>= \t1-> fresh >>= \t2-> pure (t1 ->> t2 ->> BoolType)
 330 | elem op [BiLesser, BiGreater, BiLesserEq, BiGreaterEq]
 331   = pure (IntType ->> IntType ->> BoolType)
 332 | elem op [BiAnd, BiOr]
 333   = pure (BoolType ->> BoolType ->> BoolType)
 334 | op == BiCons
 335   = fresh >>= \t1-> pure (t1 ->> ListType t1 ->> ListType t1)
 336
 337 op1Type :: Op1 -> Typing Type
 338 op1Type UnNegation = pure $ (BoolType ->> BoolType)
 339 op1Type UnMinus = pure $ (IntType ->> IntType)
 340
 341 ////----- Inference for Statements -----
 342 applySubst :: Substitution -> Typing Gamma
 343 applySubst s = changeGamma (subst s)
 344
 345 instance infer Stmt where
 346  infer s = case s of
 347     IfStmt e th el =
 348         infer e >>= \(s1, et, e_)->
 349         lift (unify et BoolType) >>= \s2 ->
 350         applySubst (compose s2 s1) >>|
 351         infer th >>= \(s3, tht, th_)->
 352         applySubst s3 >>|
 353         infer el >>= \(s4, elt, el_)->
 354         applySubst s4 >>|
 355         lift (unify tht elt) >>= \s5->
 356         let sub = compose s5 $ compose s4 $ compose s3 $ compose s2 s1 in
 357         pure (sub, subst s5 tht, IfStmt e_ th_ el_)
 358
 359     WhileStmt e wh =
 360         infer e >>= \(s1, et, e_)->
 361         lift (unify et BoolType) >>= \s2 ->
 362         applySubst (compose s2 s1) >>|
 363         infer wh >>= \(s3, wht, wh_)->
 364         pure (compose s3 $ compose s2 s1, subst s3 wht, WhileStmt e_ wh_)
 365
 366     AssStmt vd=:(VarDef k fs) e =
 367         lookup k >>= \expected ->
 368         infer e >>= \(s1, given, e_)->
 369         foldM reverseFs given (reverse fs) >>= \varType->
 370         lift (unify expected varType) >>= \s2->
 371         let s = compose s2 s1 in
 372         applySubst s >>|
 373         changeGamma (extend k (Forall [] (subst s varType))) >>|
 374         pure (s, VoidType, AssStmt vd e_)
 375
 376     FunStmt f args fs =
 377         lookup f >>= \expected ->
 378         let accST = (\(s,ts,es) e->infer e >>= \(s_,et,e_)-> pure (compose s_ s,ts++[et],es++[e_])) in
 379         foldM accST (zero,[],[]) args >>= \(s1, argTs, args_)->
 380         fresh >>= \tv->
 381         let given = foldr (->>) tv argTs in
 382         lift (unify expected given) >>= \s2->
 383         let fReturnType = subst s2 tv in
 384         foldM foldFieldSelectors fReturnType fs >>= \returnType ->
 385         (case f of
 386             "print" = case head argTs of
 387                 IntType = pure "1printint"
 388                 CharType = pure "1printchar"
 389                 BoolType = pure "1printbool"
 390                 ListType (CharType) = pure "1printstr"
 391                 t = liftT $ Left $ SanityError zero ("can not print " +++ toString t)
 392             _ = pure f) >>= \newF->
 393         pure (compose s2 s1, VoidType, FunStmt newF args_ fs)
 394
 395     ReturnStmt Nothing = pure (zero, VoidType, s)
 396     //hier ook sub applyen
 397     ReturnStmt (Just e) = infer e >>= \(sub, t, e_)-> pure (sub, t, ReturnStmt (Just e_))
 398
 399 reverseFs :: Type FieldSelector -> Typing Type
 400 reverseFs t FieldHd = pure $ ListType t
 401 reverseFs t FieldTl = pure $ ListType t
 402 reverseFs t FieldFst = fresh >>= \tv -> pure $ TupleType (t, tv)
 403 reverseFs t FieldSnd = fresh >>= \tv -> pure $ TupleType (tv, t)
 404
 405 //The type of a list of statements is either an encountered
 406 //return, or VoidType
 407 instance infer [a] | infer a where
 408     infer []        = pure (zero, VoidType, [])
 409     infer [stmt:ss] =
 410         infer stmt >>= \(s1, t1, s_) ->
 411         applySubst s1 >>|
 412         infer ss >>= \(s2, t2, ss_) ->
 413         applySubst s2 >>|
 414         case t1 of
 415             VoidType = pure (compose s2 s1, t2, [s_:ss_])
 416             _ = case t2 of
 417                 VoidType = pure (compose s2 s1, t1, [s_:ss_])
 418                 _ = lift (unify t1 t2) >>= \s3 ->
 419                     pure (compose s3 $ compose s2 s1, t1, [s_:ss_])
 420
 421 //the type class inferes the type of an AST element (VarDecl or FunDecl)
 422 //and adds it to the AST element
 423 class type a :: a -> Typing (Substitution, a)
 424
 425 instance type VarDecl where
 426     type (VarDecl p expected k e) =
 427         infer e >>= \(s1, given, e_) ->
 428         applySubst s1 >>|
 429         case expected of
 430             Nothing = pure zero
 431             Just expected_ = lift (unify expected_ given)
 432         >>= \s2->
 433         applySubst s2 >>|
 434         let vtype = subst (compose s2 s1) given in
 435         generalize vtype >>= \t ->
 436         changeGamma (extend k t) >>|
 437         pure (compose s2 s1, VarDecl p (Just vtype) k e_)
 438
 439 instance type FunDecl where
 440     type fd=:(FunDecl p f args expected vds stmts) =
 441         gamma >>= \outerScope-> //functions are infered in their own scopde
 442         introduce f >>|
 443         mapM introduce args >>= \argTs->
 444         fresh >>= \tempTv ->
 445         let temp = foldr (->>) tempTv argTs in
 446         (case expected of
 447             Just expected_ = lift (unify expected_ temp)
 448             _   = pure zero
 449         ) >>= \s0->
 450         applySubst s0 >>|
 451         type vds >>= \(s1, tVds)->
 452         applySubst s1 >>|
 453         infer stmts >>= \(s2, result, stmts_)->
 454         applySubst s1 >>|
 455         let argTs_ = map (subst $ compose s2 $ compose s1 s0) argTs in
 456         let given = foldr (->>) result argTs_ in
 457         (case expected of
 458             Nothing = pure zero
 459             Just (FuncType expected_) = lift (unify expected_ given)
 460             Just expected_ = lift (unify expected_ given)
 461         ) >>= \s3 ->
 462         let ftype = subst (compose s3 $ compose s2 $ compose s1 s0) given in
 463         (case ftype of
 464             _ ->> _ = pure ftype
 465             _       = pure $ FuncType ftype
 466         ) >>= \ftype_->
 467         generalize ftype_ >>= \t->
 468         putGamma outerScope >>|
 469         changeGamma (extend f t) >>|
 470         pure (compose s3 $ compose s2 $ compose s1 s0,
 471                 FunDecl p f args (Just ftype_) tVds stmts_)
 472
 473 instance type [a] | type a where
 474     type []     = pure (zero, [])
 475     type [v:vs] =
 476         type v >>= \(s1, v_)->
 477         applySubst s1 >>|
 478         type vs >>= \(s2, vs_)->
 479         applySubst (compose s2 s1) >>|
 480         pure (compose s2 s1, [v_:vs_])
 481
 482 introduce :: String -> Typing Type
 483 introduce k =
 484     fresh >>= \tv ->
 485     changeGamma (extend k (Forall [] tv)) >>|
 486     pure tv
 487
 488 instance toString Scheme where
 489     toString (Forall x t) =
 490         concat ["Forall ": intersperse "," x] +++ concat [". ", toString t];
 491
 492 instance toString Gamma where
 493     toString mp =
 494         concat [concat [k, ": ", toString v, "\n"]\\(k, v)<-'Map'.toList mp]
 495
 496 instance toString Substitution where
 497     toString subs =
 498         concat [concat [k, ": ", toString t, "\n"]\\(k, t)<-'Map'.toList subs]
 499
 500 instance toString SemError where
 501     toString (SanityError p e) = concat [toString p,
 502         "SemError: SanityError: ", e]
 503     toString (ParseError p s) = concat [toString p,
 504         "ParseError: ", s]
 505     toString (UnifyError p t1 t2) = concat [toString p,
 506         "Can not unify types, expected|given:\n", toString t1,
 507         "\n", toString t2]
 508     toString (InfiniteTypeError p t) = concat [toString p,
 509         "Infinite type: ", toString t]
 510     toString (FieldSelectorError p t fs) = concat [toString p,
 511         "Can not run fieldselector '", toString fs, "' on type: ",
 512         toString t]
 513     toString (OperatorError p op t) = concat [toString p,
 514         "Operator error, operator '", toString op, "' can not be",
 515         "used on type: ", toString t]
 516     toString (UndeclaredVariableError p k) = concat [toString p,
 517         "Undeclared identifier: ", k]
 518     toString (ArgumentMisMatchError p str) = concat [toString p,
 519         "Argument mismatch: ", str]
 520     toString (Error e) = concat ["Unknown error during semantical",
 521         "analysis: ", e]
 522
 523 instance toString (Maybe a) | toString a where
 524     toString Nothing = "Nothing"
 525     toString (Just e) = concat ["Just ", toString e]
 526
 527 instance MonadTrans (StateT (Gamma, [TVar])) where
 528     liftT m = StateT \s-> m >>= \a-> return (a, s)
 529
 530 Mapmap :: (a->b) ('Map'.Map k a) -> ('Map'.Map k b)
 531 Mapmap _ 'Map'.Tip = 'Map'.Tip
 532 Mapmap f ('Map'.Bin sz k v ml mr) = 'Map'.Bin sz k (f v)
 533                                         (Mapmap f ml)
 534                                         (Mapmap f mr)