ref: dd4eadf2c105c53baed21ae3e800721c502f98d7
parent: 25a4ef8b3bbfd898fa1e029a1228b863cac8c434
author: Lennart Augustsson <lennart.augustsson@epicgames.com>
date: Sun Sep 24 13:42:03 EDT 2023
Code from the paper Practical type inference for arbitrary-rank types Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, Mark Shields
--- a/src/MicroHs/TypeCheck2.hs
+++ /dev/null
@@ -1,93 +1,0 @@
-module MicroHs.TypeCheck2(module MicroHs.TypeCheck2) where
-import Data.IORef
-import qualified Data.Map as M
-type Name = String
-
-type ErrMsg = String
-type TcEnv = M.Map Name Sigma
-
-newtype Tc a = Tc (TcEnv -> IO (Either ErrMsg a))
-
--- Control flow
-check :: Bool -> String -> Tc () -- Type inference can fail
-check = undefined
-
--- The type environment
-lookupVar :: Name -> Tc Sigma -- Look up in the envt (may fail)
-lookupVar = undefined
-extendVarEnv :: Name -> Sigma -- Extend the envt
- -> Tc a -> Tc a
-extendVarEnv = undefined
-getEnvTypes :: Tc [Sigma] -- Get all types in the envt
-
--- Instantiation, skolemisation, quantification
-instantiate :: Sigma -> Tc Rho
-instantiate = undefined
-skolemise :: Sigma -> Tc ([TyVar], Rho)
-skolemise = undefined
-quantify :: [MetaTv] -> Rho -> Tc Sigma
-quantify = undefined
-
--- Unification and fresh type variables
-newMetaTyVar :: Tc Tau -- Make (MetaTv tv), where tv is fresh
-newMetaTyVar = undefined
-newSkolemTyVar :: Tc TyVar -- Make a fresh skolem TyVar
-newSkolemTyVar = undefined
-unify :: Tau -> Tau -> Tc () -- Unification (may fail)
-unify = undefined
-
--- Free type variables
-getMetaTyVars :: [Type] -> Tc [MetaTv]
-getMetaTyVars = undefined
-getFreeTyVars :: [Type] -> Tc [TyVar]
-getFreeTyVars = undefined
-
-newTcRef :: a -> Tc (IORef a)
-newTcRef = undefined
-readTcRef :: IORef a -> Tc a
-readTcRef = undefined
-writeTcRef :: IORef a -> a -> Tc ()
-writeTcRef = undefined
-
----------------- Terms -------------------
-data Term
- = Var Name -- x
- | Lit Int -- 3
- | App Term Term -- f x
- | Lam Name Term -- \x. x
- | Let Name Term Term -- let x = f y in x+1
- | Ann Term Sigma -- f x :: Int
-
----------------- 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
-
-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 TyCon = IntT | BoolT
-
-(-->) :: Type -> Type-> Type -- Build a function type
-arg --> res = Fun arg res
-
-intType :: Tau
-intType = TyCon IntT
-
---------------------------------------------
-
-data MetaTv = Meta Uniq TyRef
-type TyRef = IORef (Maybe Tau)
- -- 'Nothing' means the type variable is not substituted
- -- 'Just ty' means it has been substituted by ty
-type Uniq = Int
-
---------------------------------------------
--- /dev/null
+++ b/src/MicroHs/paper/BasicTypes.hs
@@ -1,0 +1,233 @@
+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
+ | Lit Int -- 3
+ | 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
+
+atomicTerm :: Term -> Bool
+atomicTerm (Var _) = True
+atomicTerm (Lit _) = True
+atomicTerm _ = False
+
+-----------------------------------
+-- 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
+
+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
+
+data TyCon = IntT | BoolT
+ deriving( Eq )
+
+---------------------------------
+-- Constructors
+(-->) :: Sigma -> Sigma -> Sigma
+arg --> res = Fun arg res
+intType, boolType :: Tau
+intType = TyCon IntT
+boolType = TyCon BoolT
+
+---------------------------------
+-- 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
+
+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
+
+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)]
+
+-----------------------------------
+-- 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 (Lit i) = int i
+ 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
+
+instance Show Term where
+ show t = docToString (ppr t)
+
+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, atomicPrec :: Precedence
+topPrec = 0 -- Top-level precedence
+arrPrec = 1 -- Precedence of (a->b)
+tcPrec = 2 -- Precedence of (T a b)
+atomicPrec = 3 -- 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_tc :: TyCon -> Doc
+ppr_tc IntT = text "Int"
+ppr_tc BoolT = text "Bool"
--- /dev/null
+++ b/src/MicroHs/paper/TcMonad.hs
@@ -1,0 +1,272 @@
+module TcMonad(
+ Tc, -- The monad type constructor
+ runTc, ErrMsg, lift, check,
+ -- Environment manipulation
+ extendVarEnv, 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( nub, (\\) )
+------------------------------------------
+-- 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) }+
+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' } }
+
+------------------------------------------
+-- 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 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
--- /dev/null
+++ b/src/MicroHs/paper/TcTerm.hs
@@ -1,0 +1,127 @@
+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 (Lit _) exp_ty
+ = instSigma intType 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 }
+
+------------------------------------------
+-- 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' }
--
⑨