ref: 84d5753303938265b4a2083772122117903a9c66
parent: 8b3176b9565fd6773e4ad5c040278bd99e3c9480
author: Lennart Augustsson <lennart.augustsson@epicgames.com>
date: Fri Sep 29 16:58:29 EDT 2023
Temp
--- a/comb/mhs.comb
+++ b/comb/mhs.comb
@@ -1,3 +1,3 @@
v3.5
-929
-(($A :0 _813) (($A :1 (($B _859) _0)) (($A :2 ((($S' _859) _0) $I)) (($A :3 _783) (($A :4 (_3 "undefined")) (($A :5 $I) (($A :6 ((($C' $B) _812) (($C _73) _5))) (($A :7 ((($C' _6) (_830 _70)) ((_73 _828) _69))) (($A :8 (($B (($S _859) _828)) _3)) (($A :9 $T) (($A :10 ($T $I)) (($A :11 (($B (_73 _185)) _10)) (($A :12 (($B ($B (_72 _9))) ((($C' $B) (($B $C) _10)) ($B _10)))) (($A :13 (($B ($B (_72 _9))) ((($C' $B) (($B $C) _10)) ($BK _10)))) (($A :14 (($B (_72 _9)) $P)) (($A :15 (($B ($B (_72 _9))) (($B (($C' $C) _10)) ($B $P)))) (($A :16 _15) (($A :17 (($B (_72 _9)) ($B ($P _741)))) (($A :18 (($B (_72 _9)) ($BK ($P _741)))) (($A :19 ((_72 _9) (($S $P) $I))) (($A :20 (($B (_72 _9)) (($C ($S' $P)) $I))) (($A :21 (($B $Y) (($B ($B ($P (_14 _113)))) ((($C' $B) (($B ($C' $B)) ($B _12))) ((($C' ($C' $B)) ($B _12)) (($B ($B _14)) _114)))))) (($A :22 (($B $Y) (($B ($B ($P (_14 _741)))) (($B ($C' $B)) ($B _13))))) (($A :23 _3) (($A :24 ($T (_14 _741))) (($A :25 (($C $C) _32)) (($A :26 ($T _31)) (($A :27 (($P _32) _31)) (($A :28 _32) (($A :29 (($C (($C $S') _27)) $I)) (($A :30 (($C $S) _27)) (($A :31 $K) (($A :32 $A) (($A :33 _788) (($A :34 _789) (($A :35 ((($S' _26) (_780 97)) (($C _780) 122))) (($A :36 ((($S' _26) (_780 65)) (($C _780) 90))) (($A :37 ((($S' _25) _35) _36)) (($A :38 ((($S' _26) (_780 48)) (($C _780) 57))) (($A :39 ((($S' _26) (_780 32)) (($C _780) 126))) (($A :40 _777) (($A :41 _778) (($A :42 _780) (($A :43 _779) (($A :44 ((($S' _25) (($C _40) 32)) ((($S' _25) (($C _40) 9)) (($C _40) 10)))) (($A :45 (($S (($S ((($S' _26) (_42 65)) (($C _42) 90))) (_32 (((_740 "lib/Data/Char.hs") 3) 8)))) (($B _33) ((($C' _80) ((($C' _81) _34) (_34 65))) (_34 97))))) (($A :46 (($S (($S ((($S' _26) (_42 97)) (($C _42) 97))) (_32 (((_740 "lib/Data/Char.hs") 3) 8)))) (($B _33) ((($C' _80) ((($C' _81) _34) (_34 97))) (_34 65))))) (($A :47 _748) (($A :48 _749) (($A :49 _750) (($A :50 _751) (($A :51 (_48 %0.0)) (($A :52 _47) (($A :53 _48) (($A :54 _49) (($A :55 _50) (($A :56 _752) (($A :57 _753) (($A :58 _56) (($A :59 _57) (($A :60 _754) (($A :61 _755) (($A :62 _756) (($A :63 _757) (($A :64 _60) (($A :65 _61) (($A :66 _62) (($A :67 _63) (($A :68 _758) (($A :69 (($B $BK) $T)) (($A :70 ($BK $T)) (($A :71 $P) (($A :72 $I) (($A :73 $B) (($A :74 $I) (($A :75 $K) (($A :76 $C) (($A :77 _784) (($A :78 (($C (($C $S') _185)) _186)) (($A :79 ((($C' ($S' ($C' $B))) $B) $I)) (($A :80 _742) (($A :81 _743) (($A :82 _744) (($A :83 _745) (($A :84 _746) (($A :85 _747) (($A :86 (_81 0)) (($A :87 _765) (($A :88 _766) (($A :89 _767) (($A :90 _768) (($A :91 _769) (($A :92 _770) (($A :93 _87) (($A :94 ($BK $K)) (($A :95 (($B $BK) (($B ($B $BK)) $P))) (($A :96 (($B ($B ($B $BK))) (($B ($B ($B $BK))) (($B ($B ($B $C))) (($B ($B $C)) $P))))) (($A :97 ((($S' $S) ((($S' ($S' $C)) ((($C' ($C' $S)) ((($C' $B) (($B ($S' $S')) ((($C' $B) (($B _25) (_90 0))) (_87 0)))) (($B ($B (($C' $P) (_85 1)))) _80))) ($C $P))) _83)) _84)) (($A :98 _94) (($A :99 ((($S' $C) (($B ($P _174)) ((($C' ($C' $B)) ((($C' $C) _87) _174)) _175))) (($B (($C' ($C' ($C' $C))) ((($C' ($C' ($C' $C))) ((($C' ($C' ($C' ($C' $S')))) (($B ($B ($B ($B $C)))) (($B (($C' ($C' ($C' $C))) (($B ($B ($B (($S' $S') (_87 0))))) (($B (($C' ($C' $C)) (($B ($B (($S' $S') (_87 1)))) (($B (($C' $C) (($B (($C' $S') (_87 2))) ($C _99)))) ($C _99))))) ($C _99))))) ($C _99)))) ($T $K))) ($T $A)))) (($C _97) 4)))) (($A :100 (_106 _75)) (($A :101 ((_121 (_78 _100)) _98)) (($A :102 (($C ((($C' $B) (($P _113) ((($C' ($C' $O)) $P) $K))) ((($S' ($C' ($C' ($C' $B)))) (($B ($B ($B ($B _103)))) ((($S' ($C' ($C' $B))) (($B ($B ($B _103))) ((($S' ($C' $B)) (($B ($B _103)) ((($C' $B) (($B _119) ($T 0))) _102))) ((($C' $B) (($B _119) ($T 1))) _102)))) ((($C' $B) (($B _119) ($T 2))) _102)))) ((($C' $B) (($B _119) ($T 3))) _102)))) (($B $T) (($B ($B $P)) (($C' _80) (_82 4)))))) (($A :103 (($S $S) (($B $BK) (($B $BK) ((($S' $S) $T) (($B $BK) (($B $BK) (($C ((($S' $C') $S) (($B ($B ($B ($S $B)))) (($B ($B ($B ($B ($B $BK))))) (($B (($S' ($C' $B)) (($B $B') $B'))) (($B ($B ($B ($B ($B ($S $B)))))) (($B ($B ($B ($B ($B ($B ($B $BK)))))))
\ No newline at end of file
+931
+(($A :0 _815) (($A :1 (($B _861) _0)) (($A :2 ((($S' _861) _0) $I)) (($A :3 _785) (($A :4 (_3 "undefined")) (($A :5 $I) (($A :6 ((($C' $B) _814) (($C _73) _5))) (($A :7 ((($C' _6) (_832 _70)) ((_73 _830) _69))) (($A :8 (($B (($S _861) _830)) _3)) (($A :9 $T) (($A :10 ($T $I)) (($A :11 (($B (_73 _185)) _10)) (($A :12 (($B ($B (_72 _9))) ((($C' $B) (($B $C) _10)) ($B _10)))) (($A :13 (($B ($B (_72 _9))) ((($C' $B) (($B $C) _10)) ($BK _10)))) (($A :14 (($B (_72 _9)) $P)) (($A :15 (($B ($B (_72 _9))) (($B (($C' $C) _10)) ($B $P)))) (($A :16 _15) (($A :17 (($B (_72 _9)) ($B ($P _743)))) (($A :18 (($B (_72 _9)) ($BK ($P _743)))) (($A :19 ((_72 _9) (($S $P) $I))) (($A :20 (($B (_72 _9)) (($C ($S' $P)) $I))) (($A :21 (($B $Y) (($B ($B ($P (_14 _113)))) ((($C' $B) (($B ($C' $B)) ($B _12))) ((($C' ($C' $B)) ($B _12)) (($B ($B _14)) _114)))))) (($A :22 (($B $Y) (($B ($B ($P (_14 _743)))) (($B ($C' $B)) ($B _13))))) (($A :23 _3) (($A :24 ($T (_14 _743))) (($A :25 (($C $C) _32)) (($A :26 ($T _31)) (($A :27 (($P _32) _31)) (($A :28 _32) (($A :29 (($C (($C $S') _27)) $I)) (($A :30 (($C $S) _27)) (($A :31 $K) (($A :32 $A) (($A :33 _790) (($A :34 _791) (($A :35 ((($S' _26) (_782 97)) (($C _782) 122))) (($A :36 ((($S' _26) (_782 65)) (($C _782) 90))) (($A :37 ((($S' _25) _35) _36)) (($A :38 ((($S' _26) (_782 48)) (($C _782) 57))) (($A :39 ((($S' _26) (_782 32)) (($C _782) 126))) (($A :40 _779) (($A :41 _780) (($A :42 _782) (($A :43 _781) (($A :44 ((($S' _25) (($C _40) 32)) ((($S' _25) (($C _40) 9)) (($C _40) 10)))) (($A :45 (($S (($S ((($S' _26) (_42 65)) (($C _42) 90))) (_32 (((_742 "lib/Data/Char.hs") 3) 8)))) (($B _33) ((($C' _80) ((($C' _81) _34) (_34 65))) (_34 97))))) (($A :46 (($S (($S ((($S' _26) (_42 97)) (($C _42) 97))) (_32 (((_742 "lib/Data/Char.hs") 3) 8)))) (($B _33) ((($C' _80) ((($C' _81) _34) (_34 97))) (_34 65))))) (($A :47 _750) (($A :48 _751) (($A :49 _752) (($A :50 _753) (($A :51 (_48 %0.0)) (($A :52 _47) (($A :53 _48) (($A :54 _49) (($A :55 _50) (($A :56 _754) (($A :57 _755) (($A :58 _56) (($A :59 _57) (($A :60 _756) (($A :61 _757) (($A :62 _758) (($A :63 _759) (($A :64 _60) (($A :65 _61) (($A :66 _62) (($A :67 _63) (($A :68 _760) (($A :69 (($B $BK) $T)) (($A :70 ($BK $T)) (($A :71 $P) (($A :72 $I) (($A :73 $B) (($A :74 $I) (($A :75 $K) (($A :76 $C) (($A :77 _786) (($A :78 (($C (($C $S') _185)) _186)) (($A :79 ((($C' ($S' ($C' $B))) $B) $I)) (($A :80 _744) (($A :81 _745) (($A :82 _746) (($A :83 _747) (($A :84 _748) (($A :85 _749) (($A :86 (_81 0)) (($A :87 _767) (($A :88 _768) (($A :89 _769) (($A :90 _770) (($A :91 _771) (($A :92 _772) (($A :93 _87) (($A :94 ($BK $K)) (($A :95 (($B $BK) (($B ($B $BK)) $P))) (($A :96 (($B ($B ($B $BK))) (($B ($B ($B $BK))) (($B ($B ($B $C))) (($B ($B $C)) $P))))) (($A :97 ((($S' $S) ((($S' ($S' $C)) ((($C' ($C' $S)) ((($C' $B) (($B ($S' $S')) ((($C' $B) (($B _25) (_90 0))) (_87 0)))) (($B ($B (($C' $P) (_85 1)))) _80))) ($C $P))) _83)) _84)) (($A :98 _94) (($A :99 ((($S' $C) (($B ($P _174)) ((($C' ($C' $B)) ((($C' $C) _87) _174)) _175))) (($B (($C' ($C' ($C' $C))) ((($C' ($C' ($C' $C))) ((($C' ($C' ($C' ($C' $S')))) (($B ($B ($B ($B $C)))) (($B (($C' ($C' ($C' $C))) (($B ($B ($B (($S' $S') (_87 0))))) (($B (($C' ($C' $C)) (($B ($B (($S' $S') (_87 1)))) (($B (($C' $C) (($B (($C' $S') (_87 2))) ($C _99)))) ($C _99))))) ($C _99))))) ($C _99)))) ($T $K))) ($T $A)))) (($C _97) 4)))) (($A :100 (_106 _75)) (($A :101 ((_121 (_78 _100)) _98)) (($A :102 (($C ((($C' $B) (($P _113) ((($C' ($C' $O)) $P) $K))) ((($S' ($C' ($C' ($C' $B)))) (($B ($B ($B ($B _103)))) ((($S' ($C' ($C' $B))) (($B ($B ($B _103))) ((($S' ($C' $B)) (($B ($B _103)) ((($C' $B) (($B _119) ($T 0))) _102))) ((($C' $B) (($B _119) ($T 1))) _102)))) ((($C' $B) (($B _119) ($T 2))) _102)))) ((($C' $B) (($B _119) ($T 3))) _102)))) (($B $T) (($B ($B $P)) (($C' _80) (_82 4)))))) (($A :103 (($S $S) (($B $BK) (($B $BK) ((($S' $S) $T) (($B $BK) (($B $BK) (($C ((($S' $C') $S) (($B ($B ($B ($S $B)))) (($B ($B ($B ($B ($B $BK))))) (($B (($S' ($C' $B)) (($B $B') $B'))) (($B ($B ($B ($B ($B ($S $B)))))) (($B ($B ($B ($B ($B ($B ($B $BK)))))))
\ No newline at end of file
--- a/src/MicroHs/TypeCheck.hs
+++ b/src/MicroHs/TypeCheck.hs
@@ -4,7 +4,7 @@
module MicroHs.TypeCheck(
typeCheck,
TModule(..), showTModule,
- impossible
+ impossible,
) where
import Prelude
import Data.List
@@ -33,6 +33,9 @@
data Entry = Entry Expr ETypeScheme
--Xderiving(Show)
+--entryType :: Entry -> ETypeScheme
+--entryType (Entry _ t) = t
+
type ValueTable = M.Map [Entry]
type TypeTable = M.Map [Entry]
type KindTable = M.Map [Entry]
@@ -378,6 +381,9 @@
EUVar j -> if i == j then T.return () else add
_ -> add
+getUVar :: Int -> T (Maybe EType)
+getUVar i = gets (IM.lookup i . uvarSubst)
+
munify :: --XHasCallStack =>
SLoc -> Maybe EType -> EType -> T ()
munify _ Nothing _ = T.return ()
@@ -420,8 +426,8 @@
ax <- derefUVar a
T.return $ EApp fx ax
EUVar i -> T.do
- sub <- gets uvarSubst
- case IM.lookup i sub of
+ mt <- getUVar i
+ case mt of
Nothing -> T.return at
Just t -> derefUVar t
EVar _ -> T.return at
@@ -475,10 +481,13 @@
put (TC mn 0 fx tenv senv venv IM.empty)
newUVar :: T EType
-newUVar = T.do
+newUVar = EUVar <$> newUniq
+
+newUniq :: T Int
+newUniq = T.do
TC mn n fx tenv senv venv sub <- get
put (TC mn (n+1) fx tenv senv venv sub)
- T.return (EUVar n)
+ T.return n
tLookupInst :: --XHasCallStack =>
String -> Ident -> T (Expr, EType)
@@ -1104,4 +1113,301 @@
showValueTable :: ValueTable -> String
showValueTable vt =
unlines $ take 5 [showIdent i ++ " : " ++ showExpr t | (i, [Entry _ t]) <- M.toList vt]
+-}
+
+-----------------------------------------------------
+{-+
+type Sigma = EType
+type Tau = EType
+type Rho = EType
+type TyVar = Ident
+
+type TcRef = Int
+data Expected = Infer TcRef | Check EType
+type MetaTv = TcRef
+
+type Tc a = T a
+
+newTcRef :: EType -> Tc TcRef
+newTcRef t = T.do
+ r <- newUniq
+ addUVar r t
+ T.return r
+readTcRef :: TcRef -> Tc EType
+readTcRef r = T.do
+ mt <- getUVar r
+ case mt of
+ Just t -> T.return t
+ Nothing -> error "readTcRef"
+writeTcRef :: TcRef -> EType -> Tc ()
+writeTcRef r t = addUVar r t
+
+getFreeTyVars :: [EType] -> Tc [TyVar]
+getFreeTyVars tys = do
+ tys' <- mapM zonkType tys
+ return (freeTyVars tys')
+
+getMetaTyVars :: [EType] -> Tc [MetaTv]
+getMetaTyVars tys = T.do
+ tys' <- mapM zonkType tys
+ return (metaTvs tys')
+
+getEnvTypes :: Tc [EType]
+getEnvTypes = gets (map entryType . concat . M.elems . valueTable)
+
+zonkType :: EType -> Tc EType
+zonkType (EForall ns ty) = T.do
+ ty' <- zonkType ty
+ T.return (EForall ns ty')
+zonkType t@(EVar n) = return t
+zonkType t@(EUVar tv) = T.do -- A mutable type variable
+ mb_ty <- getUVar tv
+ case mb_ty of
+ Nothing -> return t
+ Just ty -> T.do
+ ty' <- zonkType ty
+ writeTcRef tv ty' -- "Short out" multiple hops
+ T.return ty'
+zonkType (EApp arg res) = T.do
+ arg' <- zonkType arg
+ res' <- zonkType res
+ T.return (EApp arg' res')
+zonkType t = undefined
+
+quantify :: [MetaTv] -> Rho -> Tc Sigma
+-- Quantify over the specified type variables (all flexible)
+quantify tvs ty = T.do
+ mapM_ bind (tvs `zip` new_bndrs) -- 'bind' is just a cunning way
+ ty' <- zonkType ty -- of doing the substitution
+ T.return (EForall new_bndrs_kind ty')
+ where
+ used_bndrs = tyVarBndrs ty -- Avoid quantified type variables in use
+ new_bndrs = deleteFirstsBy eqIdent allBinders used_bndrs
+ bind (tv, name) = writeTcRef tv (EVar name)
+ new_bndrs_kind = map (\ i -> IdKind i undefined) new_bndrs
+
+allBinders :: [Ident] -- a,b,..z, a1, b1,... z1, a2, b2,...
+allBinders = [ mkIdent [x] | x <- ['a'..'z'] ] ++
+ [ mkIdent (x : show i) | i <- [1 ..], x <- ['a'..'z']]
+
+skolemise :: Sigma -> Tc ([TyVar], Rho)
+-- Performs deep skolemisation, retuning the
+-- skolem constants and the skolemised type
+skolemise (EForall tvs ty) = T.do -- Rule PRPOLY
+ sks1 <- mapM (newSkolemTyVar . idKindIdent) tvs
+ (sks2, ty') <- skolemise (substTy (map idKindIdent tvs) (map EVar sks1) ty)
+ T.return (sks1 ++ sks2, ty')
+skolemise (EApp arg_ty res_ty) = T.do -- Rule PRFUN
+ (sks, res_ty') <- skolemise res_ty
+ T.return (sks, EApp arg_ty res_ty')
+skolemise ty@(EVar _) = T.return ([], ty) -- Rule PRMONO
+skolemise ty = undefined
+
+-- Skolem tyvars are just identifiers that start with a uniq
+newSkolemTyVar :: Ident -> Tc Ident
+newSkolemTyVar tv = T.do
+ uniq <- newUniq
+ return (mkIdentSLoc (getSLocIdent tv) (show uniq ++ unIdent tv))
+
+------------------
+
+freeTyVars :: [EType] -> [TyVar]
+-- Get the free TyVars from a type; no duplicates in result
+freeTyVars = foldr (go []) []
+ where
+ go :: [TyVar] -- Ignore occurrences of bound type variables
+ -> EType -- Type to look at
+ -> [TyVar] -- Accumulates result
+ -> [TyVar]
+ go bound (EVar tv) acc
+ | elemBy eqIdent tv bound = acc
+ | elemBy eqIdent tv acc = acc
+ | otherwise = tv : acc
+ go bound (EForall tvs ty) acc = go (map idKindIdent tvs ++ bound) ty acc
+ go bound (EApp fun arg) acc = go bound fun (go bound arg acc)
+ go _bound (EUVar _) acc = acc
+ go _ _ _ = undefined
+
+metaTvs :: [EType] -> [MetaTv]
+-- Get the MetaTvs from a type; no duplicates in result
+metaTvs tys = foldr go [] tys
+ where
+ go (EUVar tv) acc
+ | elemBy eqInt tv acc = acc
+ | otherwise = tv : acc
+ go (EVar _) acc = acc
+ go (EForall _ ty) acc = go ty acc -- ForAll binds TyVars only
+ go (EApp fun arg) acc = go fun (go arg acc)
+ go _ _ = undefined
+
+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 (EForall tvs body) = map idKindIdent tvs ++ bndrs body
+ bndrs (EApp arg res) = bndrs arg ++ bndrs res
+ bndrs (EVar _) = []
+ bndrs _ = undefined
+
+substTy :: [Ident] -> [EType] -> EType -> EType
+
+-- 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 :: [(TyVar, Tau)] -> EType -> EType
+subst_ty env (EApp arg res) = EApp (subst_ty env arg) (subst_ty env res)
+subst_ty env ty@(EVar n) = fromMaybe ty (lookupBy eqIdent n env)
+subst_ty _env (EUVar tv) = EUVar tv
+subst_ty env (EForall nks rho) = EForall nks (subst_ty env' rho)
+ where
+ env' = [(n, ty') | (n, ty') <- env, not (elemBy eqIdent n ns)]
+ ns = map idKindIdent nks
+subst_ty _ _ = undefined
+
+-----------------------
+
+check :: Bool -> String -> Tc ()
+check False msg = error msg
+check True _ = return ()
+
+inferSigma :: Expr -> Tc (Expr, Sigma)
+inferSigma e = T.do
+ (e', exp_ty) <- inferRho e
+ env_tys <- getEnvTypes
+ env_tvs <- getMetaTyVars env_tys
+ res_tvs <- getMetaTyVars [exp_ty]
+ let forall_tvs = deleteFirstsBy eqInt res_tvs env_tvs
+ (e',) <$> quantify forall_tvs exp_ty
+
+checkSigma :: Expr -> Sigma -> Tc Expr
+checkSigma expr sigma = T.do
+ (skol_tvs, rho) <- skolemise sigma
+ expr' <- checkRho expr rho
+ env_tys <- getEnvTypes
+ esc_tvs <- getFreeTyVars (sigma : env_tys)
+ let bad_tvs = filter (\ i -> elemBy eqIdent i esc_tvs) skol_tvs
+ check (null bad_tvs) $
+ "Type not polymorphic enough"
+ T.return expr'
+
+checkRho :: Expr -> Rho -> Tc Expr
+checkRho expr ty =
+ tcRho expr (Check ty)
+
+inferRho :: Expr -> Tc (Expr, Rho)
+inferRho expr = T.do
+ ref <- newTcRef (error "inferRho: empty result")
+ expr' <- tcRho expr (Infer ref)
+ (expr',) <$> readTcRef ref
+
+tcRho :: Expr -> Expected -> Tc Expr
+tcRho (EVar v) exp_ty = T.do
+ (expr', v_sigma) <- tLookup "variable" v
+ instSigma v_sigma exp_ty
+ T.return expr'
+tcRho (EApp fun arg) exp_ty = T.do
+ (fun', fun_ty) <- inferRho fun
+ (arg_ty, res_ty) <- unifyFun fun_ty
+ arg' <- checkSigma arg arg_ty
+ instSigma res_ty exp_ty
+ T.return (EApp fun' arg')
+tcRho (EOper e ies) _ = undefined
+tcRho (ELam [] body) exp_ty = tcRho body exp_ty
+tcRho (ELam (pat:pats) body) exp_ty = tcLamRho pat (ELam pats body) exp_ty
+tcRho expr@(ELit loc l) exp_ty = T.do
+ tcLitRho loc l exp_ty
+ T.return expr
+tcRho (ECase a arms) _ = undefined
+tcRho (ELet bs a) _ = undefined
+tcRho (ETuple es) _ = undefined
+tcRho (EDo mmn ass) _ = undefined
+tcRho (ESectL e i) _ = undefined
+tcRho (ESectR i e) _ = undefined
+tcRho (EIf e1 e2 e3) _ = undefined
+tcRho (EListish _) _ = undefined
+tcRho (ESign e t) _ = undefined
+tcRho (EAt i e) _ = undefined
+tcRho (EForall vks t) _ = undefined
+
+tcLitRho :: SLoc -> Lit -> Expected -> Tc ()
+tcLitRho loc l exp_ty = T.do
+ let
+ lit t = instSigma t exp_ty
+ case l of
+ LInt _ -> lit (tConI loc "Primitives.Int")
+ LDouble _ -> lit (tConI loc "Primitives.Double")
+ LChar _ -> lit (tConI loc "Primitives.Char")
+ LStr _ -> lit (tApp (tConI loc "Data.List.[]") (tConI loc "Primitives.Char"))
+ LPrim _ -> newUVar >>= lit
+ LForImp _ -> impossible
+
+tcLamRho :: EPat -> Expr -> Expected -> Tc Expr
+tcLamRho pat body (Infer ref) = T.do
+ (binds, pat_ty) <- inferPat pat
+ body_ty <- extendVarEnvList binds (inferRho body)
+ writeTcRef ref (pat_ty `tArrow` body_ty)
+
+unifyFun :: Rho -> Tc (Sigma, Rho)
+-- (arg,res) <- unifyFunTy fun
+-- unifies 'fun' with '(arg -> res)'
+unifyFun tau =
+ case getArrow tau of
+ Just tt -> return tt
+ Nothing -> T.do
+ arg_ty <- newUVar
+ res_ty <- newUVar
+ unify noSLoc tau (arg_ty `tArrow` res_ty)
+ return (arg_ty, res_ty)
+
+subsCheck :: Sigma -> Sigma -> Tc ()
+-- (subsCheck args off exp) checks that
+-- 'off' is at least as polymorphic as 'args -> exp'
+subsCheck sigma1 sigma2 = T.do -- Rule DEEP-SKOL
+ (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)
+ "Subsumption check failed"
+
+subsCheckRho :: Sigma -> Rho -> Tc ()
+-- Invariant: the second argument is in weak-prenex form
+subsCheckRho sigma1@(EForall _ _) rho2 = T.do -- Rule SPEC
+ rho1 <- instantiate sigma1
+ subsCheckRho rho1 rho2
+subsCheckRho rho1 rho2 | Just (a2, r2) <- getArrow rho2 = T.do -- Rule FUN
+ (a1, r1) <- unifyFun rho1
+ subsCheckFun a1 r1 a2 r2
+subsCheckRho rho1 rho2 | Just (a1, r1) <- getArrow rho1 = T.do -- Rule FUN
+ (a2,r2) <- unifyFun rho2
+ subsCheckFun a1 r1 a2 r2
+subsCheckRho tau1 tau2 -- Rule MONO
+ = unify noSLoc tau1 tau2 -- Revert to ordinary unification
+
+subsCheckFun :: Sigma -> Rho -> Sigma -> Rho -> Tc ()
+subsCheckFun a1 r1 a2 r2
+ = do { subsCheck a2 a1 ; subsCheckRho r1 r2 }+
+instantiate :: Sigma -> Tc Rho
+-- Instantiate the topmost for-alls of the argument type
+-- with flexible type variables
+instantiate (EForall tvs ty) = T.do
+ tvs' <- mapM (\_ -> newUVar) tvs
+ return (substTy (map idKindIdent tvs) tvs' ty)
+instantiate ty =
+ return ty
+
+instSigma :: Sigma -> Expected -> 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) = T.do
+ t1' <- instantiate t1
+ writeTcRef r t1'
+
-}
--- a/src/MicroHs/paper/TcTerm.hs
+++ b/src/MicroHs/paper/TcTerm.hs
@@ -178,9 +178,11 @@
= 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
--
⑨