ref: 2d0fe2526dcb98a40293f9c508dd22e33a7de27f
parent: 5f773c1e7ad514e2b9901eba55cc715a2d6ead32
author: Lennart Augustsson <lennart@augustsson.net>
date: Thu Nov 23 16:33:07 EST 2023
Clean up
--- a/src/MicroHs/paper/BasicTypes.hs
+++ /dev/null
@@ -1,256 +1,0 @@
-module BasicTypes where
-import Prelude hiding ((<>))
--- This module defines the basic types used by the type checker
--- Everything defined in here is exported
-import Text.PrettyPrint.HughesPJ
-import Data.IORef
-import Data.List( nub )
-import Data.Maybe( fromMaybe )
-
-infixr 4 --> -- The arrow type constructor
-infixl 4 `App` -- Application
-
------------------------------------
--- Ubiquitous types --
------------------------------------
-type Name = String -- Names are very simple
-
------------------------------------
--- Expressions --
------------------------------------
--- Examples below
-data Term = Var Name -- x
- | LitI Int -- 3
- | LitB Bool -- True
- | App Term Term -- f x
- | Lam Name Term -- \ x -> x
- | ALam Name Sigma Term -- \ x -> x
- | Let Name Term Term -- let x = f y in x+1
- | Ann Term Sigma -- (f x) :: Int
- | If Term Term Term
- | PLam Pat Term -- \ x -> x
-
-atomicTerm :: Term -> Bool
-atomicTerm (Var _) = True
-atomicTerm (LitI _) = True
-atomicTerm (LitB _) = True
-atomicTerm _ = False
-
-data Pat = PVar Name
- | PWild
- | PAnn Pat Sigma
- | PCon Name [Pat]
-
------------------------------------
--- Types --
------------------------------------
-type Sigma = Type
-type Rho = Type -- No top-level ForAll
-type Tau = Type -- No ForAlls anywhere
-
-data Type = ForAll [TyVar] Rho -- Forall type
- | Fun Type Type -- Function type
- | TyCon TyCon -- Type constants
- | TyVar TyVar -- Always bound by a ForAll
- | MetaTv MetaTv -- A meta type variable
- | TyApp Type Type
-
-data TyVar
- = BoundTv String -- A type variable bound by a ForAll
- | SkolemTv String Uniq -- A skolem constant; the String is
- -- just to improve error messages
-
-data MetaTv = Meta Uniq TyRef -- Can unify with any tau-type
-type TyRef = IORef (Maybe Tau)
- -- 'Nothing' means the type variable is not substituted
- -- 'Just ty' means it has been substituted by 'ty'
-
-instance Eq MetaTv where
- (Meta u1 _) == (Meta u2 _) = u1 == u2
-
-instance Eq TyVar where
- (BoundTv s1) == (BoundTv s2) = s1 == s2
- (SkolemTv _ u1) == (SkolemTv _ u2) = u1 == u2
- _ == _ = False
-
-type Uniq = Int
-
-type TyCon = String
-
----------------------------------
--- Constructors
-(-->) :: Sigma -> Sigma -> Sigma
-arg --> res = Fun arg res
-
-intType, boolType :: Tau
-intType = TyCon "Int"
-boolType = TyCon "Bool"
-
----------------------------------
--- Free and bound variables
-metaTvs :: [Type] -> [MetaTv]
--- Get the MetaTvs from a type; no duplicates in result
-metaTvs tys = foldr go [] tys
- where
- go (MetaTv tv) acc
- | tv `elem` acc = acc
- | otherwise = tv : acc
- go (TyVar _) acc = acc
- go (TyCon _) acc = acc
- go (Fun arg res) acc = go arg (go res acc)
- go (ForAll _ ty) acc = go ty acc -- ForAll binds TyVars only
- go (TyApp fun arg) acc = go fun (go arg acc)
-
-freeTyVars :: [Type] -> [TyVar]
--- Get the free TyVars from a type; no duplicates in result
-freeTyVars tys = foldr (go []) [] tys
- where
- go :: [TyVar] -- Ignore occurrences of bound type variables
- -> Type -- Type to look at
- -> [TyVar] -- Accumulates result
- -> [TyVar]
- go bound (TyVar tv) acc
- | tv `elem` bound = acc
- | tv `elem` acc = acc
- | otherwise = tv : acc
- go _bound (MetaTv _) acc = acc
- go _bound (TyCon _) acc = acc
- go bound (Fun arg res) acc = go bound arg (go bound res acc)
- go bound (ForAll tvs ty) acc = go (tvs ++ bound) ty acc
- go bound (TyApp fun arg) acc = go bound fun (go bound arg acc)
-
-tyVarBndrs :: Rho -> [TyVar]
--- Get all the binders used in ForAlls in the type, so that
--- when quantifying an outer for-all we can avoid these inner ones
-tyVarBndrs ty = nub (bndrs ty)
- where
- bndrs (ForAll tvs body) = tvs ++ bndrs body
- bndrs (Fun arg res) = bndrs arg ++ bndrs res
- bndrs _ = []
-
-tyVarName :: TyVar -> String
-tyVarName (BoundTv n) = n
-tyVarName (SkolemTv n _) = n
-
----------------------------------
--- Substitution
-type Env = [(TyVar, Tau)]
-
-substTy :: [TyVar] -> [Type] -> Type -> Type
-
--- Replace the specified quantified type variables by
--- given meta type variables
--- No worries about capture, because the two kinds of type
--- variable are distinct
-substTy tvs tys ty = subst_ty (tvs `zip` tys) ty
-subst_ty :: Env -> Type -> Type
-subst_ty env (Fun arg res) = Fun (subst_ty env arg) (subst_ty env res)
-subst_ty env (TyVar n) = fromMaybe (TyVar n) (lookup n env)
-subst_ty _env (MetaTv tv) = MetaTv tv
-subst_ty _env (TyCon tc) = TyCon tc
-subst_ty env (ForAll ns rho) = ForAll ns (subst_ty env' rho)
- where
- env' = [(n,ty') | (n,ty') <- env, not (n `elem` ns)]
-subst_ty env (TyApp fun arg) = TyApp (subst_ty env fun) (subst_ty env arg)
-
------------------------------------
--- Pretty printing class --
------------------------------------
-class Outputable a where
- ppr :: a -> Doc
-
-docToString :: Doc -> String
-docToString = render
-
-dcolon, dot :: Doc
-dcolon = text "::"
-dot = char '.'
-
--------------- Pretty-printing terms ---------------------
-instance Outputable Term where
- ppr (Var n) = pprName n
- ppr (LitI i) = int i
- ppr (LitB i) = text $ if i then "True" else "False"
- ppr (App e1 e2) = pprApp (App e1 e2)
- ppr (Lam v e) = sep [char '\\' <> pprName v <> text ".", ppr e]
- ppr (ALam v t e) = sep [char '\\' <> parens (pprName v <> dcolon <> ppr t)
- <> text ".", ppr e]
- ppr (Let v rhs b) = sep [text "let {",- nest 2 (pprName v <+> equals <+> ppr rhs <+> char '}') ,
- text "in",
- ppr b]
- ppr (Ann e ty) = pprParendTerm e <+> dcolon <+> pprParendType ty
- ppr (If e1 e2 e3) = parens $ text "if" <+> ppr e1 <+> text "then" <+> ppr e2 <+> text "else" <+> ppr e3
- ppr (PLam p e) = sep [char '\\' <> ppr p <> text ".", ppr e]
-
-instance Show Term where
- show t = docToString (ppr t)
-
-instance Outputable Pat where
- ppr (PVar n) = pprName n
- ppr PWild = text "_"
- ppr (PAnn p t) = parens $ ppr p <+> dcolon <+> ppr t
- ppr (PCon c ps) = parens $ pprName c <+> hsep (map ppr ps)
-
-pprParendTerm :: Term -> Doc
-pprParendTerm e | atomicTerm e = ppr e
- | otherwise = parens (ppr e)
-
-pprApp :: Term -> Doc
-pprApp e = go e []
- where
- go (App e1 e2) es = go e1 (e2:es)
- go e' es = pprParendTerm e' <+> sep (map pprParendTerm es)
-
-pprName :: Name -> Doc
-pprName n = text n
-
--------------- Pretty-printing types ---------------------
-instance Outputable Type where
- ppr ty = pprType topPrec ty
-
-instance Outputable MetaTv where
- ppr (Meta u _) = text "$" <> int u
-
-instance Outputable TyVar where
- ppr (BoundTv n) = text n
- ppr (SkolemTv n u) = text n <+> int u
-
-instance Show Type where
- show t = docToString (ppr t)
-
-type Precedence = Int
-
-topPrec, arrPrec, tcPrec, appPrec, atomicPrec :: Precedence
-topPrec = 0 -- Top-level precedence
-arrPrec = 1 -- Precedence of (a->b)
-tcPrec = 2 -- Precedence of (T a b)
-appPrec = 3
-atomicPrec = 4 -- Precedence of t
-
-precType :: Type -> Precedence
-precType (ForAll _ _) = topPrec
-precType (Fun _ _) = arrPrec
-precType _ = atomicPrec -- All the types are be atomic
-
-pprParendType :: Type -> Doc
-pprParendType ty = pprType tcPrec ty
-
-pprType :: Precedence -> Type -> Doc
--- Print with parens if precedence arg > precedence of type itself
-pprType p ty | p >= precType ty = parens (ppr_type ty)
- | otherwise = ppr_type ty
-
-ppr_type :: Type -> Doc -- No parens
-ppr_type (ForAll ns ty) = sep [text "forall" <+>
- hsep (map ppr ns) <> dot,
- ppr ty]
-ppr_type (Fun arg res) = sep [pprType arrPrec arg <+> text "->",
- pprType (arrPrec-1) res]
-ppr_type (TyCon tc) = ppr_tc tc
-ppr_type (TyVar n) = ppr n
-ppr_type (MetaTv tv) = ppr tv
-ppr_type (TyApp arg res) = pprType appPrec arg <+> pprType (appPrec-1) res
-
-ppr_tc :: TyCon -> Doc
-ppr_tc s = text s
--- a/src/MicroHs/paper/Main.hs
+++ /dev/null
@@ -1,55 +1,0 @@
-import BasicTypes
-import TcTerm
-import TcMonad
-
-env :: [(Name,Sigma)]
-env =
- [("not", boolType --> boolType)- ,("C", (ForAll [tvx] (tx --> tx)) --> TyCon "T")- ,("pair", ForAll [tvx,tvy] (tx --> ty --> TyApp (TyApp (TyCon "Pair") tx) ty))- ]
-
-tvx, tvy :: TyVar
-tvx = BoundTv "x"
-tvy = BoundTv "y"
-tx, ty :: Type
-tx = TyVar tvx
-ty = TyVar tvy
-
-tc :: Term -> IO Sigma
-tc e = do
- et <- runTc env (typecheck e)
- case et of
- Left msg -> error $ docToString msg
- Right t -> return t
-
-pp :: Outputable a => a -> IO ()
-pp = putStrLn . docToString . ppr
-
-tcpp :: Term -> IO ()
-tcpp e = do
- pp e
- t <- tc e
- pp t
-
-main :: IO ()
-main = do
- tcpp e1
- tcpp e2
- tcpp e3
- tcpp e4
-
-_tv :: String -> Type
-_tv = TyVar . BoundTv
-
-e1 :: Term
-e1 = Lam "x" $ Var "x"
-
-e2 :: Term
-e2 = Ann (Lam "x" $ Var "x") (ForAll [tvx] (tx --> tx))
-
-e3 :: Term
-e3 = Lam "b" $ If (App (Var "not") (Var "b")) e1 e2
-
-e4 :: Term
-e4 = PLam (PCon "C" [PVar "f"]) $ App (App (Var "pair") (App (Var "f") (LitI 1))) (App (Var "f") (LitB True))
--- a/src/MicroHs/paper/TcMonad.hs
+++ /dev/null
@@ -1,284 +1,0 @@
-module TcMonad(
- Tc, -- The monad type constructor
- runTc, ErrMsg, lift, check,
- -- Environment manipulation
- extendVarEnv, extendVarEnvList, lookupVar,
- getEnvTypes, getFreeTyVars, getMetaTyVars,
- -- Types and unification
- newTyVarTy,
- instantiate, skolemise, zonkType, quantify,
- unify, unifyFun,
- -- Ref cells
- newTcRef, readTcRef, writeTcRef
-) where
-import Control.Monad(ap)
-import BasicTypes
-import qualified Data.Map as Map
-import Text.PrettyPrint.HughesPJ
-import Data.IORef
-import Data.List( (\\) )
-------------------------------------------
--- The monad itself --
-------------------------------------------
-
-data TcEnv
- = TcEnv { uniqs :: IORef Uniq, -- Unique supply- var_env :: Map.Map Name Sigma -- Type environment for term variables
- }
-
-newtype Tc a = Tc (TcEnv -> IO (Either ErrMsg a))
-unTc :: Tc a -> (TcEnv -> IO (Either ErrMsg a))
-unTc (Tc a) = a
-
-type ErrMsg = Doc
-
-instance Functor Tc where
- fmap f t = t >>= return . f
-
-instance Applicative Tc where
- pure x = Tc (\_env -> return (Right x))
- (<*>) = ap
-
-instance Monad Tc where
- return = pure
- m >>= k = Tc (\env -> do { r1 <- unTc m env- ; case r1 of
- Left err -> return (Left err)
- Right v -> unTc (k v) env })
-
-instance MonadFail Tc where
- fail err = Tc (\_env -> return (Left (text err)))
-
-failTc :: Doc -> Tc a -- Fail unconditionally
-failTc d = fail (docToString d)
-
-check :: Bool -> Doc -> Tc ()
-check True _ = return ()
-check False d = failTc d
-
-runTc :: [(Name,Sigma)] -> Tc a -> IO (Either ErrMsg a)
--- Run type-check, given an initial environment
-runTc binds (Tc tc)
- = do { ref <- newIORef 0- ; let { env = TcEnv { uniqs = ref,- var_env = Map.fromList binds } }
- ; tc env }
-
-lift :: IO a -> Tc a
--- Lift a state transformer action into the typechecker monad
--- ignores the environment and always succeeds
-lift st = Tc (\_env -> do { r <- st; return (Right r) })-
-newTcRef :: a -> Tc (IORef a)
-newTcRef v = lift (newIORef v)
-
-readTcRef :: IORef a -> Tc a
-readTcRef r = lift (readIORef r)
-
-writeTcRef :: IORef a -> a -> Tc ()
-writeTcRef r v = lift (writeIORef r v)
-
---------------------------------------------------
--- Dealing with the type environment --
---------------------------------------------------
-extendVarEnv :: Name -> Sigma -> Tc a -> Tc a
-extendVarEnv var ty (Tc m)
- = Tc (\env -> m (extend env))
- where
- extend env = env { var_env = Map.insert var ty (var_env env) }-
-extendVarEnvList :: [(Name, Sigma)] -> Tc a -> Tc a
-extendVarEnvList varTys (Tc m)
- = Tc (\env -> m (extend env))
- where
- extend env = env { var_env = foldr (uncurry Map.insert) (var_env env) varTys }-
-getEnv :: Tc (Map.Map Name Sigma)
-getEnv = Tc (\ env -> return (Right (var_env env)))
-
-lookupVar :: Name -> Tc Sigma -- May fail
-lookupVar n = do { env <- getEnv- ; case Map.lookup n env of
- Just ty -> return ty
- Nothing -> failTc (text "Not in scope:" <+> quotes (pprName n)) }
-
---------------------------------------------------
--- Creating, reading, writing MetaTvs --
---------------------------------------------------
-newTyVarTy :: Tc Tau
-newTyVarTy = do { tv <- newMetaTyVar- ; return (MetaTv tv) }
-
-newMetaTyVar :: Tc MetaTv
-newMetaTyVar = do { uniq <- newUnique- ; tref <- newTcRef Nothing
- ; return (Meta uniq tref) }
-
-newSkolemTyVar :: TyVar -> Tc TyVar
-newSkolemTyVar tv = do { uniq <- newUnique- ; return (SkolemTv (tyVarName tv) uniq) }
-
-readTv :: MetaTv -> Tc (Maybe Tau)
-readTv (Meta _ ref) = readTcRef ref
-
-writeTv :: MetaTv -> Tau -> Tc ()
-writeTv (Meta _ ref) ty = writeTcRef ref (Just ty)
-
-newUnique :: Tc Uniq
-newUnique = Tc (\ (TcEnv {uniqs = ref}) ->- do { uniq <- readIORef ref- ; writeIORef ref (uniq + 1)
- ; return (Right uniq) })
-
-------------------------------------------
--- Instantiation --
-------------------------------------------
-instantiate :: Sigma -> Tc Rho
--- Instantiate the topmost for-alls of the argument type
--- with flexible type variables
-instantiate (ForAll tvs ty)
- = do { tvs' <- mapM (\_ -> newMetaTyVar) tvs- ; return (substTy tvs (map MetaTv tvs') ty) }
-instantiate ty
- = return ty
-
-skolemise :: Sigma -> Tc ([TyVar], Rho)
--- Performs deep skolemisation, retuning the
--- skolem constants and the skolemised type
-skolemise (ForAll tvs ty) -- Rule PRPOLY
- = do { sks1 <- mapM newSkolemTyVar tvs- ; (sks2, ty') <- skolemise (substTy tvs (map TyVar sks1) ty)
- ; return (sks1 ++ sks2, ty') }
-skolemise (Fun arg_ty res_ty) -- Rule PRFUN
- = do { (sks, res_ty') <- skolemise res_ty- ; return (sks, Fun arg_ty res_ty') }
-skolemise ty -- Rule PRMONO
- = return ([], ty)
-
-------------------------------------------
--- Quantification --
-------------------------------------------
-quantify :: [MetaTv] -> Rho -> Tc Sigma
--- Quantify over the specified type variables (all flexible)
-quantify tvs ty
- = do { mapM_ bind (tvs `zip` new_bndrs) -- 'bind' is just a cunning way- ; ty' <- zonkType ty -- of doing the substitution
- ; return (ForAll new_bndrs ty') }
- where
- used_bndrs = tyVarBndrs ty -- Avoid quantified type variables in use
- new_bndrs = take (length tvs) (allBinders \\ used_bndrs)
- bind (tv, name) = writeTv tv (TyVar name)
-
-allBinders :: [TyVar] -- a,b,..z, a1, b1,... z1, a2, b2,...
-allBinders = [ BoundTv [x] | x <- ['a'..'z'] ] ++
- [ BoundTv (x : show i) | i <- [1 :: Integer ..], x <- ['a'..'z']]
-
-------------------------------------------
--- Getting the free tyvars --
-------------------------------------------
-getEnvTypes :: Tc [Type]
--- Get the types mentioned in the environment
-getEnvTypes = do { env <- getEnv- ; return (Map.elems env) }
-getMetaTyVars :: [Type] -> Tc [MetaTv]
--- This function takes account of zonking, and returns a set
--- (no duplicates) of unbound meta-type variables
-getMetaTyVars tys = do { tys' <- mapM zonkType tys- ; return (metaTvs tys') }
-getFreeTyVars :: [Type] -> Tc [TyVar]
--- This function takes account of zonking, and returns a set
--- (no duplicates) of free type variables
-getFreeTyVars tys = do { tys' <- mapM zonkType tys- ; return (freeTyVars tys') }
-
-------------------------------------------
--- Zonking --
--- Eliminate any substitutions in the type
-------------------------------------------
-zonkType :: Type -> Tc Type
-zonkType (ForAll ns ty) = do { ty' <- zonkType ty- ; return (ForAll ns ty') }
-zonkType (Fun arg res) = do { arg' <- zonkType arg- ; res' <- zonkType res
- ; return (Fun arg' res') }
-zonkType (TyCon tc) = return (TyCon tc)
-zonkType (TyVar n) = return (TyVar n)
-zonkType (MetaTv tv) -- A mutable type variable
- = do { mb_ty <- readTv tv- ; case mb_ty of
- Nothing -> return (MetaTv tv)
- Just ty -> do { ty' <- zonkType ty- ; writeTv tv ty' -- "Short out" multiple hops
- ; return ty' } }
-zonkType (TyApp arg res) = do { arg' <- zonkType arg- ; res' <- zonkType res
- ; return (TyApp arg' res') }
-
-------------------------------------------
--- Unification --
-------------------------------------------
-unify :: Tau -> Tau -> Tc ()
-unify ty1 ty2
- | badType ty1 || badType ty2 -- Compiler error
- = failTc (text "Panic! Unexpected types in unification:" <+>
- vcat [ppr ty1, ppr ty2])
-unify (TyVar tv1) (TyVar tv2) | tv1 == tv2 = return ()
-unify (MetaTv tv1) (MetaTv tv2) | tv1 == tv2 = return ()
-unify (MetaTv tv) ty = unifyVar tv ty
-unify ty (MetaTv tv) = unifyVar tv ty
-unify (Fun arg1 res1)
- (Fun arg2 res2)
- = do { unify arg1 arg2; unify res1 res2 }-unify (TyCon tc1) (TyCon tc2)
- | tc1 == tc2
- = return ()
-unify (TyApp arg1 res1)
- (TyApp arg2 res2)
- = do { unify arg1 arg2; unify res1 res2 }-unify ty1 ty2 = failTc (text "Cannot unify types:" <+> vcat [ppr ty1, ppr ty2])
-
------------------------------------------
-
-unifyVar :: MetaTv -> Tau -> Tc ()
--- Invariant: tv1 is a flexible type variable
-unifyVar tv1 ty2 -- Check whether tv1 is bound
- = do { mb_ty1 <- readTv tv1- ; case mb_ty1 of
- Just ty1 -> unify ty1 ty2
- Nothing -> unifyUnboundVar tv1 ty2 }
-unifyUnboundVar :: MetaTv -> Tau -> Tc ()
--- Invariant: the flexible type variable tv1 is not bound
-unifyUnboundVar tv1 ty2@(MetaTv tv2)
- = do { -- We know that tv1 /= tv2 (else the- -- top case in unify would catch it)
- mb_ty2 <- readTv tv2
- ; case mb_ty2 of
- Just ty2' -> unify (MetaTv tv1) ty2'
- Nothing -> writeTv tv1 ty2 }
-unifyUnboundVar tv1 ty2
- = do { tvs2 <- getMetaTyVars [ty2]- ; if tv1 `elem` tvs2 then
- occursCheckErr tv1 ty2
- else
- writeTv tv1 ty2 }
-
------------------------------------------
-unifyFun :: Rho -> Tc (Sigma, Rho)
--- (arg,res) <- unifyFunTy fun
--- unifies 'fun' with '(arg -> res)'
-unifyFun (Fun arg res) = return (arg,res)
-unifyFun tau = do { arg_ty <- newTyVarTy- ; res_ty <- newTyVarTy
- ; unify tau (arg_ty --> res_ty)
- ; return (arg_ty, res_ty) }
------------------------------------------
-occursCheckErr :: MetaTv -> Tau -> Tc ()
--- Raise an occurs-check error
-occursCheckErr tv ty
- = failTc (text "Occurs check for" <+> quotes (ppr tv) <+>
- text "in:" <+> ppr ty)
-
-badType :: Tau -> Bool
--- Tells which types should never be encountered during unification
-badType (TyVar (BoundTv _)) = True
-badType _ = False
--- a/src/MicroHs/paper/TcTerm.hs
+++ /dev/null
@@ -1,191 +1,0 @@
-module TcTerm where
-import BasicTypes
-import Data.IORef
-import TcMonad
-import Data.List( (\\) )
-import Text.PrettyPrint.HughesPJ
-
-------------------------------------------
--- The top-level wrapper --
-------------------------------------------
-typecheck :: Term -> Tc Sigma
-typecheck e = do { ty <- inferSigma e- ; zonkType ty }
-
------------------------------------
--- The expected type --
------------------------------------
-data Expected a = Infer (IORef a) | Check a
-
-------------------------------------------
--- tcRho, and its variants --
-------------------------------------------
-checkRho :: Term -> Rho -> Tc ()
--- Invariant: the Rho is always in weak-prenex form
-checkRho expr ty = tcRho expr (Check ty)
-
-inferRho :: Term -> Tc Rho
-inferRho expr
- = do { ref <- newTcRef (error "inferRho: empty result")- ; tcRho expr (Infer ref)
- ; readTcRef ref }
-
-tcRho :: Term -> Expected Rho -> Tc ()
--- Invariant: if the second argument is (Check rho),
--- then rho is in weak-prenex form
-tcRho (LitI _) exp_ty
- = instSigma intType exp_ty
-tcRho (LitB _) exp_ty
- = instSigma boolType exp_ty
-tcRho (Var v) exp_ty
- = do { v_sigma <- lookupVar v- ; instSigma v_sigma exp_ty }
-tcRho (App fun arg) exp_ty
- = do { fun_ty <- inferRho fun- ; (arg_ty, res_ty) <- unifyFun fun_ty
- ; checkSigma arg arg_ty
- ; instSigma res_ty exp_ty }
-tcRho (Lam var body) (Check exp_ty)
- = do { (var_ty, body_ty) <- unifyFun exp_ty- ; extendVarEnv var var_ty (checkRho body body_ty) }
-tcRho (Lam var body) (Infer ref)
- = do { var_ty <- newTyVarTy- ; body_ty <- extendVarEnv var var_ty (inferRho body)
- ; writeTcRef ref (var_ty --> body_ty) }
-tcRho (ALam var var_ty body) (Check exp_ty)
- = do { (arg_ty, body_ty) <- unifyFun exp_ty- ; subsCheck arg_ty var_ty
- ; extendVarEnv var var_ty (checkRho body body_ty) }
-tcRho (ALam var var_ty body) (Infer ref)
- = do { body_ty <- extendVarEnv var var_ty (inferRho body)- ; writeTcRef ref (var_ty --> body_ty) }
-tcRho (Let var rhs body) exp_ty
- = do { var_ty <- inferSigma rhs- ; extendVarEnv var var_ty (tcRho body exp_ty) }
-tcRho (Ann body ann_ty) exp_ty
- = do { checkSigma body ann_ty- ; instSigma ann_ty exp_ty }
-tcRho (If e1 e2 e3) (Check exp_ty) -- This?
- = do { checkRho e1 boolType- ; checkSigma e2 exp_ty
- ; checkSigma e3 exp_ty }
-tcRho (If e1 e2 e3) (Infer ref)
- = do { checkRho e1 boolType- ; rho1 <- inferRho e2
- ; rho2 <- inferRho e3
- ; subsCheck rho1 rho2
- ; subsCheck rho2 rho1
- ; writeTcRef ref rho1 }
-tcRho (PLam pat body) (Infer ref)
- = do { (binds, pat_ty) <- inferPat pat- ; body_ty <- extendVarEnvList binds (inferRho body)
- ; writeTcRef ref (pat_ty --> body_ty) }
-tcRho (PLam pat body) (Check ty)
- = do { (arg_ty, res_ty) <- unifyFun ty- ; binds <- checkPat pat arg_ty
- ; extendVarEnvList binds (checkRho body res_ty) }
-
-tcPat :: Pat -> Expected Sigma -> Tc [(Name,Sigma)]
-tcPat PWild _exp_ty = return []
-tcPat (PVar v) (Infer ref) = do { ty <- newTyVarTy- ; writeTcRef ref ty
- ; return [(v,ty)] }
-tcPat (PVar v) (Check ty) = return [(v, ty)]
-tcPat (PAnn p pat_ty) exp_ty = do { binds <- checkPat p pat_ty- ; instPatSigma pat_ty exp_ty
- ; return binds }
-tcPat (PCon con ps) exp_ty
- = do { (arg_tys, res_ty) <- instDataCon con- ; envs <- mapM check_arg (ps `zip` arg_tys)
- ; instPatSigma res_ty exp_ty
- ; return (concat envs) }
- where
- check_arg (p,ty) = checkPat p ty
-
-instPatSigma :: Sigma -> Expected Sigma -> Tc ()
-instPatSigma pat_ty (Check exp_ty) = subsCheck exp_ty pat_ty
-instPatSigma pat_ty (Infer ref) = writeTcRef ref pat_ty
-
-checkPat :: Pat -> Sigma -> Tc [(Name, Sigma)]
-checkPat p exp_ty = tcPat p (Check exp_ty)
-
-inferPat :: Pat -> Tc ([(Name, Sigma)], Sigma)
-inferPat pat
- = do { ref <- newTcRef (error "inferPat: empty result")- ; binds <- tcPat pat (Infer ref)
- ; ty <- readTcRef ref
- ; return (binds, ty) }
-
-instDataCon :: Name -> Tc ([Sigma], Tau)
-instDataCon c = do
- v_sigma <- lookupVar c
- v_sigma' <- instantiate v_sigma
- return (argsAndRes v_sigma')
-
-argsAndRes :: Rho -> ([Sigma], Tau)
-argsAndRes (Fun arg_ty res_ty) = (arg_ty : arg_tys, res_ty') where (arg_tys, res_ty') = argsAndRes res_ty
-argsAndRes t = ([], t)
-
-------------------------------------------
--- inferSigma and checkSigma
-------------------------------------------
-
-inferSigma :: Term -> Tc Sigma
-inferSigma e
- = do { exp_ty <- inferRho e- ; env_tys <- getEnvTypes
- ; env_tvs <- getMetaTyVars env_tys
- ; res_tvs <- getMetaTyVars [exp_ty]
- ; let forall_tvs = res_tvs \\ env_tvs
- ; quantify forall_tvs exp_ty }
-
-checkSigma :: Term -> Sigma -> Tc ()
-checkSigma expr sigma
- = do { (skol_tvs, rho) <- skolemise sigma- ; checkRho expr rho
- ; env_tys <- getEnvTypes
- ; esc_tvs <- getFreeTyVars (sigma : env_tys)
- ; let bad_tvs = filter (`elem` esc_tvs) skol_tvs
- ; check (null bad_tvs)
- (text "Type not polymorphic enough") }
-
-------------------------------------------
--- Subsumption checking --
-------------------------------------------
-subsCheck :: Sigma -> Sigma -> Tc ()
--- (subsCheck args off exp) checks that
--- 'off' is at least as polymorphic as 'args -> exp'
-subsCheck sigma1 sigma2 -- Rule DEEP-SKOL
- = do { (skol_tvs, rho2) <- skolemise sigma2- ; subsCheckRho sigma1 rho2
- ; esc_tvs <- getFreeTyVars [sigma1,sigma2]
- ; let bad_tvs = filter (`elem` esc_tvs) skol_tvs
- ; check (null bad_tvs)
- (vcat [text "Subsumption check failed:",
- nest 2 (ppr sigma1),
- text "is not as polymorphic as",
- nest 2 (ppr sigma2)])
- }
-
-subsCheckRho :: Sigma -> Rho -> Tc ()
--- Invariant: the second argument is in weak-prenex form
-subsCheckRho sigma1@(ForAll _ _) rho2 -- Rule SPEC
- = do { rho1 <- instantiate sigma1- ; subsCheckRho rho1 rho2 }
-subsCheckRho rho1 (Fun a2 r2) -- Rule FUN
- = do { (a1,r1) <- unifyFun rho1; subsCheckFun a1 r1 a2 r2 }-subsCheckRho (Fun a1 r1) rho2 -- Rule FUN
- = do { (a2,r2) <- unifyFun rho2; subsCheckFun a1 r1 a2 r2 }-subsCheckRho tau1 tau2 -- Rule MONO
- = unify tau1 tau2 -- Revert to ordinary unification
-
-subsCheckFun :: Sigma -> Rho -> Sigma -> Rho -> Tc ()
-subsCheckFun a1 r1 a2 r2
- = do { subsCheck a2 a1 ; subsCheckRho r1 r2 }-
-instSigma :: Sigma -> Expected Rho -> Tc ()
--- Invariant: if the second argument is (Check rho),
--- then rho is in weak-prenex form
-instSigma t1 (Check t2) = subsCheckRho t1 t2
-instSigma t1 (Infer r) = do { t1' <- instantiate t1- ; writeTcRef r t1' }
--
⑨