alms-0.5.0: src/Statics.hs
-- | The type checker
{-# LANGUAGE
DeriveDataTypeable,
FlexibleContexts,
FlexibleInstances,
ImplicitParams,
MultiParamTypeClasses,
ParallelListComp,
PatternGuards,
QuasiQuotes,
ScopedTypeVariables,
TemplateHaskell,
TypeSynonymInstances,
UndecidableInstances,
ViewPatterns #-}
{-# OPTIONS_GHC -fno-warn-unused-imports #-}
module Statics (
-- * The type checking monad
TC, runTC, tcMapM,
-- * Static environments
S, env0,
-- ** Environment construction
addVal, addType, addMod, addDecl,
-- * Type checking
tcProg, tcDecls,
-- * Type checking results for the REPL
runTCNew, Module(..), getExnParam, tyConToDec,
getVarInfo, getTypeInfo, getConInfo,
staticsEnterScope,
) where
import Meta.Quasi
import Util
import qualified Syntax
import qualified Syntax.Decl
import qualified Syntax.Expr
import qualified Syntax.Notable
import qualified Syntax.Patt
import Syntax hiding (Type, Type'(..), tyAll, tyEx, tyUn, tyAf,
tyTuple, tyUnit, tyArr, tyApp,
TyPat, TyPat'(..))
import Loc
import Env as Env
import Ppr (Ppr, TyNames)
import Type
import TypeRel
import Coercion (coerceExpression)
import ErrorMessage
import Message.AST
import Control.Monad.RWS as RWS
import Control.Monad.Error as Error
import System.IO (hPutStrLn, stderr)
import Data.Data (Typeable, Data)
import Data.Generics (everywhere, mkT)
import Data.List (transpose, tails)
import Data.Monoid
import qualified Data.Map as M
import qualified Data.Set as S
import System.IO.Unsafe (unsafePerformIO)
pP :: Show a => a -> b -> b
pP a b = unsafePerformIO (print a) `seq` b
pM :: (Show a, Monad m) => a -> m ()
pM a = if pP a True then return () else fail "wibble"
ioM :: Monad m => IO a -> m ()
ioM a = if unsafePerformIO a `seq` True then return () else fail "wibble"
-- The kind of names we're using.
type R = Renamed
---
--- Type checking environment
---
-- | Mapping from identifiers to value types (includes datacons)
type VE = Env (BIdent R) Type
-- | Mapping from type constructor names to tycon info
type TE = Env (Lid R) TyCon
-- | Mapping from module names to modules
type ME = Env (Uid R) (Module, E)
-- | Mapping from module type names to signatures
type SE = Env SIGVAR (Module, E)
-- | An environment
data E = E {
vlevel :: VE, -- values
tlevel :: TE, -- types
mlevel :: ME, -- modules
slevel :: SE -- module types
}
deriving (Typeable, Data)
-- | To distinguish signature variables from module variables
-- in overloaded situations
newtype SIGVAR = SIGVAR { unSIGVAR :: Uid R }
deriving (Eq, Ord, Typeable, Data)
instance Show SIGVAR where
showsPrec p (SIGVAR u) = showsPrec p u
-- | A module item is empty, a pair of modules, a value entry (variable
-- or data constructor), a type constructor, or a module.
data Module
= MdNil
| MdApp !Module !Module
| MdValue !(BIdent R) !Type
| MdTycon !(Lid R) !TyCon
| MdModule !(Uid R) !Module
| MdSig !(Uid R) !Module
deriving (Typeable, Data, Show)
-- | Convert an ordered module into an un-ordered environment
envify :: Module -> E
envify MdNil = genEmpty
envify (MdApp md1 md2) = envify md1 =+= envify md2
envify (MdValue x t) = genEmpty =+= x =:= t
envify (MdTycon l tc) = genEmpty =+= l =:= tc
envify (MdModule u md) = genEmpty =+= u =:= (md, envify md)
envify (MdSig u md) = genEmpty =+= SIGVAR u =:= (md, envify md)
instance Monoid Module where
mempty = MdNil
mappend = MdApp
instance Monoid E where
mempty = E empty empty empty empty
mappend (E a1 a2 a3 a4) (E b1 b2 b3 b4)
= E (a1 =+= b1) (a2 =+= b2) (a3 =+= b3) (a4 =+= b4)
-- Instances for generalizing environment operations over
-- the whole environment structure
instance GenEmpty E where
genEmpty = mempty
instance GenExtend E E where
(=+=) = mappend
instance GenExtend E VE where
e =+= ve' = e =+= E ve' empty empty empty
instance GenExtend E TE where
e =+= te' = e =+= E empty te' empty empty
instance GenExtend E ME where
e =+= me' = e =+= E empty empty me' empty
instance GenExtend E SE where
e =+= se' = e =+= E empty empty empty se'
instance GenLookup E (BIdent R) Type where
e =..= k = vlevel e =..= k
instance GenLookup E (Lid R) TyCon where
e =..= k = tlevel e =..= k
instance GenLookup E (Uid R) (Module, E) where
e =..= k = mlevel e =..= k
instance GenLookup E SIGVAR (Module, E) where
e =..= k = slevel e =..= k
instance GenLookup E k v =>
GenLookup E (Path (Uid R) k) v where
e =..= J [] k = e =..= k
e =..= J (p:ps) k = do
(_, e') <- e =..= p
e' =..= J ps k
---
--- Type checking context and state
---
-- | The type checking context
data Context = Context {
environment :: !E,
modulePath :: ![Uid R]
}
-- | The packaged-up state of the type-checker, which needs to be
-- threaded from one interaction to the next by the REPL
data S = S {
-- | The environment
sEnv :: E,
-- | Index for gensyms
currIx :: !Int
}
instance GenLookup E k v =>
GenLookup Context (Path (Uid R) k) v where
cxt =..= k = environment cxt =..= k
instance GenExtend Context E where
cxt =+= e = cxt { environment = environment cxt =+= e }
instance GenExtend Context VE where
cxt =+= venv = cxt =+= E venv empty empty empty
instance GenExtend Context TE where
cxt =+= tenv = cxt =+= E empty tenv empty empty
instance GenExtend Context ME where
cxt =+= menv = cxt =+= E empty empty menv empty
instance GenExtend Context SE where
cxt =+= senv = cxt =+= E empty empty empty senv
---
--- The type-checking monad
---
-- | The type checking monad reads an environment, writes a module,
-- and keeps track of a gensym counter (currently unused).
newtype TC m a = TC {
unTC :: RWST Context Module Int (ErrorT AlmsException m) a
}
instance Monad m => Monad (TC m) where
return = TC . return
m >>= k = TC (unTC m >>= unTC . k)
fail = let ?loc = bogus in typeError . [$msg| $words:1 |]
instance Monad m => Functor (TC m) where
fmap = liftM
instance Monad m => Applicative (TC m) where
pure = return
(<*>) = ap
instance Monad m => MonadWriter Module (TC m) where
tell = TC . tell
listen = TC . listen . unTC
pass = TC . pass . unTC
instance Monad m => MonadReader Context (TC m) where
ask = TC ask
local f = TC . local f . unTC
instance Monad m => MonadError AlmsException (TC m) where
throwError = TC . throwError
catchError body handler =
TC (catchError (unTC body) (unTC . handler))
instance Monad m => AlmsMonad (TC m) where
throwAlms = throwError
catchAlms = catchError
-- | Generate a type error.
typeError :: (AlmsMonad m, ?loc :: Loc) => Message V -> m a
typeError msg0 = throwAlms (AlmsException StaticsPhase ?loc msg0)
-- | Indicate a type checker bug.
typeBug :: AlmsMonad m => String -> String -> m a
typeBug culprit msg0 = throwAlms (almsBug StaticsPhase bogus culprit msg0)
-- | Like 'ask', but monadic
asksM :: MonadReader r m => (r -> m a) -> m a
asksM = (ask >>=)
-- | Run a type checking computation with the given initial state,
-- returning the result and the updated state
runTC :: AlmsMonad m => S -> TC m a -> m (a, S)
runTC = liftM prj <$$> runTCNew where
prj (a, _, s) = (a, s)
-- | Run a type checking computation with the given initial state,
-- returning the result and the updated state
runTCNew :: AlmsMonad m => S -> TC m a -> m (a, Module, S)
runTCNew s action = unTryAlms . runErrorT $ do
let cxt = Context (sEnv s) []
ix = currIx s
(a, ix', md) <- runRWST (unTC action) cxt ix
let e' = sEnv s =+= envify md
return (a, md, S e' ix')
-- | Generate a fresh integer for use as a 'TyCon' id
newIndex :: Monad m => TC m Int
newIndex = TC $ do
i <- get
put (i + 1)
return i
-- | Add a module to the current module path
enterModule :: Monad m => Uid R -> TC m a -> TC m a
enterModule u = local $ \cxt ->
cxt { modulePath = u : modulePath cxt }
-- | Forget the module path (for type checking signatures)
forgetModulePath :: Monad m => TC m a -> TC m a
forgetModulePath = local $ \cxt -> cxt { modulePath = [] }
-- | Find out the current module path
currentModulePath :: Monad m => TC m [Uid R]
currentModulePath = asks (reverse . modulePath)
-- | Add a variable binding to the generated module
bindVar :: Monad m => Lid R -> Type -> TC m ()
bindVar l t = tell (MdValue (Var l) t)
-- | Add a data constructor binding to the generated module
bindCon :: Monad m => Uid R -> Type -> TC m ()
bindCon u t = tell (MdValue (Con u) t)
-- | Add a type constructor binding to the generated module
bindTycon :: Monad m => Lid R -> TyCon -> TC m ()
bindTycon l tc = tell (MdTycon l tc)
-- | Add a module binding to the generated module
bindModule :: Monad m => Uid R -> Module -> TC m ()
bindModule u md = tell (MdModule u md)
-- | Add a module type binding to the generated module
bindSig :: Monad m => Uid R -> Module -> TC m ()
bindSig u md = tell (MdSig u md)
-- | Run some computation with the context extended by a module
inModule :: Monad m => Module -> TC m a -> TC m a
inModule md = local (=+= envify md)
-- | Run in the environment consisting of only the given module
onlyInModule :: Monad m => Module -> TC m a -> TC m a
onlyInModule = local (\cxt -> cxt { environment = mempty }) <$$> inModule
-- | Grab the module generated by a computate, and generate the empty
-- module in turn
steal :: Monad m => TC m a -> TC m (a, Module)
steal = censor (const mempty) . listen
-- | Map a function over a list, allowing the exports of each item
-- to be in scope for the rest
tcMapM :: Monad m => (a -> TC m b) -> [a] -> TC m [b]
tcMapM _ [] = return []
tcMapM f (x:xs) = do
(x', md) <- listen (f x)
xs' <- inModule md $ tcMapM f xs
return (x':xs')
{- -- deprecated?
-- | Abstract the given type by removing its datacon or synonym info
withoutConstructors :: Monad m =>
TyCon -> TC m a -> TC m a
withoutConstructors tc = TC . M.R.local clean . unTC where
-- Note: only filters immediate scope -- should be right.
clean (TCEnv env) = TCEnv (map eachScope env)
eachScope :: Scope -> Scope
eachScope scope = genModify scope emptyPath flevel
flevel :: Level -> Level
flevel level = level { vlevel = eachVe (vlevel level) }
eachVe :: VE -> VE
eachVe = fromList . filter keep . toList
keep :: (BIdent R, Type) -> Bool
keep (Con _, TyFun _ _ (TyApp tc' _ _)) = tc' /= tc
keep (Con _, TyApp tc' _ _) = tc' /= tc
keep _ = True
-}
-- | Try to look up any environment binding (value, tycon, ...)
find :: (Monad m, GenLookup Context k v, Show k) =>
k -> TC m v
find k = asksM $ \cxt -> case cxt =..= k of
Just v -> return v
Nothing -> typeBug "find" ("got unbound identifier: " ++ show k)
-- | Try to look up any environment binding (value, tycon, ...)
tryFind :: (Monad m, GenLookup Context k v, Show k) =>
k -> TC m (Maybe v)
tryFind k = asks (=..= k)
---
--- Type errors
---
-- | A type checking "assertion" raises a type error if the
-- asserted condition is false.
tassert :: (?loc :: Loc, AlmsMonad m) =>
Bool -> Message V -> m ()
tassert True _ = return ()
tassert False m = typeError m
-- | A common form of type error: A got B where C expected
terrgot :: (?loc :: Loc, AlmsMonad m) =>
String -> Type -> String -> m a
terrgot who got expected = typeError
[$msg| $words:who got $q:got where $words:expected expected. |]
-- | Combination of 'tassert and 'terrgot'
tassgot :: (?loc :: Loc, AlmsMonad m) =>
Bool -> String -> Type -> String -> m ()
tassgot False = terrgot
tassgot True = \_ _ _ -> return ()
-- | Common message pattern, actual vs. expected
terrexp :: (?loc :: Loc, AlmsMonad m) =>
Message V -> Message V -> Message V -> m a
terrexp = typeError <$$$> [$msg|
$msg:1
<dl>
<dt>actual: <dd>$msg:2
<dt>expected: <dd>$msg:3
</dl>
|]
-- | Common message pattern, actual vs. expected
tassexp :: (?loc :: Loc, AlmsMonad m) =>
Bool -> Message V -> Message V -> Message V -> m ()
tassexp False = terrexp
tassexp True = \_ _ _ -> return ()
-- | Conveniently weak-head normalize a type
hnT :: Monad m => Type -> m Type
hnT = headNormalizeTypeM 100
-- | Check type for closed-ness and and defined-ness, and add info
tcType :: (?loc :: Loc, Monad m) =>
Syntax.Type R -> TC m Type
tcType stxtype0 = do
t <- tc iaeInit stxtype0
return t
where
tc :: Monad m => CurrentImpArrRule -> Syntax.Type R -> TC m Type
tc iae [$ty| '$tv |] = do
return (TyVar tv)
tc iae [$ty| $t1 -[$opt:mq]> $t2 |] = do
qd <- iaeInterpret iae mq
t1' <- tc (iaeLeft iae) t1
t2' <- tc (iaeRight iae qd t1') t2
return (TyFun qd t1' t2')
tc iae [$ty| ($list:ts) $qlid:n |] = do
tc' <- find n
ts' <- zipWithM (tc . iaeUnder iae) (tcArity tc') ts
checkLength (length (tcArity tc'))
checkBound (tcBounds tc') ts'
return (tyApp tc' ts')
where
actualLen = length ts
checkLength len =
tassexp (actualLen == len)
[$msg| Type constructor $q:n got wrong number of parameters: |]
[$msg| $actualLen |]
[$msg| $len |]
checkBound quals ts' =
tassexp (all2 (\qlit t -> qualConst t <: qlit) quals ts')
[$msg| Type constructor $q:n used on higher
qualifiers than permitted: |]
([$msg| $1 |] (map (qRepresent . qualifier) ts'))
[$msg| $quals (or less) |]
tc iae [$ty| $quant:u '$tv . $t |] =
TyQu u tv <$> tc iae t
tc iae t0@[$ty| mu '$tv . $t |] = do
case unfoldTyMu t of
(_, N _ (Syntax.TyVar tv')) | tv == tv' ->
typeError [$msg| Recursive type is not contractive: $t0 |]
_ -> return ()
t' <- tc iae t
let actqual = qualConst t'
expqual = tvqual tv
tassert (actqual == expqual)
[$msg| Recursive type has qualifier that does
not match its own bound type variable:
<dl>
<dt>actual qualifier: <dd>$actqual
<dt>expected qualifier: <dd>$expqual
<dt>in type: <dd>$5:t0
</dl> |]
return (TyMu tv t')
tc _ [$ty| $anti:a |] = $antifail
-- | Type check an A expression
tcExpr :: Monad m => Expr R -> TC m (Type, Expr R)
tcExpr = tc where
tc :: Monad m => Expr R -> TC m (Type, Expr R)
tc e0 = let ?loc = getLoc e0 in case e0 of
[$ex| $id:x |] -> do
tx <- find x
x' <- case view x of
Left _ -> return x
Right qu -> return (fmap Con qu)
return (tx, [$ex|+ $id:x' |])
[$ex| $str:s |] -> return (tyString, [$ex|+ $str:s |])
[$ex| $int:z |] -> return (tyInt, [$ex|+ $int:z |])
[$ex| $flo:f |] -> return (tyFloat, [$ex|+ $flo:f |])
[$ex| match $e with $list:clauses |] -> do
(t0, e') <- tc e
(t1:ts, clauses') <- liftM unzip . forM clauses $ \(N note ca) -> do
(xi', md) <- steal $ tcPatt t0 (capatt ca)
(ti, ei') <- inModule md $ tc (caexpr ca)
checkSharing "match or let" (caexpr ca) md
return (ti, caClause xi' ei' <<@ note)
tr <- foldM (\ti' ti -> case ti' \/? ti of
Right tr' -> return tr'
Left (_ :: String) -> typeError [$msg|
Mismatch in branches of match or let. Cannot unify:
<ul>
<li>$ti
<li>$ti'
</ul>
|]) t1 ts
return (tr, [$ex|+ match $e' with $list:clauses' |])
[$ex| let rec $list:bsN in $e2 |] -> do
let bs = map dataOf bsN
(tfs, md) <- steal $ forM bs $ \b -> do
t' <- tcType (bntype b)
tassert (syntacticValue (bnexpr b)) $
"Not a syntactic value in let rec:" !:: bnexpr b
tassgot (qualConst t' <: Qu)
"Let rec binding" t' "unlimited type"
bindVar (bnvar b) t'
return t'
(tas, e's) <- liftM unzip $ inModule md $ mapM (tc . bnexpr) bs
zipWithM_ (\tf ta ->
tassexp (ta <: tf)
[$msg| In let rec, actual type does not
agree with declared type: |]
[$msg| $ta |]
[$msg| $tf |])
tfs tas
(t2, e2') <- inModule md $ tc e2
let b's =
zipWith3
(\b tf e' -> newBinding b { bntype = typeToStx' tf,
bnexpr = e' })
bs tfs e's
return (t2, [$ex|+ let rec $list:b's in $e2' |])
[$ex| let $decl:d in $e2 |] -> do
(d', md) <- steal $ tcDecl d
(t2, e2') <- inModule md $ tc e2
return (t2, [$ex|+ let $decl:d' in $e2' |])
[$ex| ($e1, $e2) |] -> do
(t1, e1') <- tc e1
(t2, e2') <- tc e2
return (t1 .*. t2, [$ex|+ ($e1', $e2') |])
[$ex| fun ($x : $t) -> $e |] -> do
t' <- tcType t
(x', md) <- steal $ tcPatt t' x
checkSharing "function body" e md
(te, e') <- inModule md $ tc e
q <- getWorthiness e0
let stxt' = typeToStx' t'
return (TyFun q t' te, [$ex|+ fun ($x' : $stxt') -> $e' |])
[$ex| $_ $_ |] -> do
tcExApp tc e0
[$ex| fun '$tv -> $e |] -> do
tassert (syntacticValue e) $
"Not a syntactic value under type abstraction:" !:: show e0
(t, e') <- tc e
return (tyAll tv t, [$ex|+ fun '$tv -> $e' |])
[$ex| $e1 [$t2] |] -> do
(t1, e1') <- tc e1
t2' <- tcType t2
t1' <- tapply t1 t2'
let stxt2' = typeToStx' t2'
return (t1', [$ex|+ $e1' [$stxt2'] |])
[$ex| Pack[$opt:mt1]($t2, $e) |] -> do
t2' <- tcType t2
(te, e') <- tc e
t1' <- case mt1 of
Just t1 -> tcType t1
Nothing -> return (makeExType te t2')
case t1' of
TyQu Exists tv t11' -> do
te' <- tapply (tyAll tv t11') t2'
tassert (te <: te')
[$msg| Could not pack existential:
<dl>
<dt>concrete type: <dd>$te
<dt>hiding: <dd>$t2
<dt>to get: <dd>$t1'
</dl> |]
let stxt1' = typeToStx' t1'
stxt2' = typeToStx' t2'
return (t1', [$ex| Pack[$stxt1']($stxt2', $e') |])
_ -> terrgot "Pack[-]" t1' "existential type"
[$ex| ( $e1 : $t2 ) |] -> do
(t1, e1') <- tc e1
t2' <- tcType t2
tassexp (t1 <: t2')
[$msg| Type ascription mismatch: |]
[$msg| $t1 |]
[$msg| $t2' |]
return (t2', e1')
[$ex| ( $e1 :> $t2 ) |] -> do
(t1, e1') <- tc e1
t2' <- tcType t2
tassgot (castableType t2')
"Coercion (:>)" t1 "function type"
e1'' <- coerceExpression (e1' <<@ e0) t1 t2'
`catchAlms` \AlmsException { exnMessage = m } ->
typeError [$msg|
Cannot constructor coercion
<dl>
<dt>from type: <dd>$t1
<dt>to type: <dd>$t2',
</dl>
because there is no coercion available
$vmsg:m
|]
-- tcExpr e1'' -- re-type check the coerced expression
return (t2', e1'')
[$ex| $anti:a |] -> $antifail
[$ex| $antiL:a |] -> $antifail
--
-- | Assert that type given to a name is allowed by its usage
checkSharing :: (Monad m, ?loc :: Loc) =>
String -> Expr R -> Module -> TC m ()
checkSharing name e = loop where
loop md0 = case md0 of
MdApp md1 md2 -> do loop md1; loop md2
MdValue (Var l) t ->
tassert (qualConst t <: usage (J [] l) e)
[$msg| Affine variable $q:l of type $q:t
duplicated in $words:name. |]
_ -> return ()
--
-- | What is the join of the qualifiers of all free variables
-- of the given expression?
getWorthiness e =
liftM bigVee . forM (M.keys (fv e)) $ \x -> do
mtx <- tryFind (fmap Var x)
return $ case mtx of
Just tx -> qualifier tx
_ -> minBound
-- | Remove all instances of t2 from t1, replacing with
-- a new type variable
makeExType :: Type -> Type -> Type
makeExType t1 t2 = TyQu Exists tv $ everywhere (mkT erase) t1 where
tv = fastFreshTyVar (TV (lid "a") (qualConst t2)) (maxtv (t1, t2))
erase t' = if t' == t2 then TyVar tv else t'
-- Get the usage (sharing) of a variable in an expression:
usage :: QLid R -> Expr R -> QLit
usage x e = case M.lookup x (fv e) of
Just u | u > 1 -> Qu
_ -> Qa
-- | Type check an application, given the type subsumption
-- relation, the appropriate type checking function, and the
-- expression to check.
--
-- This is highly ad-hoc, as it does significant local type inference.
-- Ick.
tcExApp :: (?loc :: Loc, Monad m) =>
(Expr R -> TC m (Type, Expr R)) ->
Expr R -> TC m (Type, Expr R)
tcExApp tc e0 = do
let foralls t1 ts = do
let (tvs, t1f) = vtQus Forall t1 -- peel off quantification
(tas, _) = vtFuns t1f -- peel off arg types
nargs = min (length tas) (length ts)
tup ps = foldl tyTuple tyUnit (take nargs ps)
-- try to find types to unify formals and actuals, and apply
t1' <- tryUnify tvs (tup tas) (tup ts) >>= foldM tapply t1
arrows t1' ts
arrows tr [] = return tr
arrows t'@(view -> TyQu Forall _ _) ts = foralls t' ts
arrows (view -> TyFun _ ta tr) (t:ts) = do
b <- unifies [] t ta
tassexp b
[$msg| In application, operand type not in operator’s domain: |]
[$msg| $t |]
[$msg| $ta |]
arrows tr ts
arrows (view -> TyMu tv t') ts = arrows (tysubst tv (TyMu tv t') t') ts
arrows t' (t:_) =
terrexp
[$msg| In application, operator is not a function: |]
[$msg| $t' |]
[$msg| $t -[...]> ... |]
unifies tvs ta tf = do
ts <- tryUnify tvs ta tf
ta' <- foldM tapply (foldr tyAll ta tvs) ts
if (ta' <: tf)
then return True
else deeper
`catchAlms` \_ -> deeper
where
deeper = case ta of
TyQu Forall tv ta1 -> unifies (tvs++[tv]) ta1 tf
_ -> return False
let (es, e1) = unfoldExApp e0 -- get operator and args
(t1, e1') <- tc e1 -- check operator
(ts, es') <- unzip `liftM` mapM tc es -- check args
tr <- foralls t1 ts
return (tr, foldl exApp e1' es')
-- | Figure out the result type of a type application, given
-- the type of the function and the argument type
tapply :: (?loc :: Loc, AlmsMonad m) =>
Type -> Type -> m Type
tapply (view -> TyQu Forall tv t1') t2 = do
tassert (qualConst t2 <: tvqual tv) $
[$msg| Type application cannot instantiate type variable:
<dl>
<dt>type variable: <dd>$tv
<dt>expected qualifier:<dd>$1
<dt>type given: <dd>$t2
<dt>actual qualifier: <dd>$2
</dl> |] (tvqual tv) (qRepresent (qualifier t2))
return (tysubst tv t2 t1')
tapply t1 _ = terrgot "Type application" t1 "forall type"
-- Given the type of thing to match and a pattern, return
-- the type environment bound by that pattern.
tcPatt :: (?loc :: Loc, Monad m) =>
Type -> Patt R -> TC m (Patt R)
tcPatt t x0 = case x0 of
[$pa| _ |] -> return x0
[$pa| $lid:x |] -> x0 <$ bindVar x t
[$pa| $quid:u $opt:mx |] -> do
t' <- hnT t
case t' of
TyApp _ ts _ -> do
tu <- find (fmap Con u)
(params, mt, res) <- case vtQus Forall tu of
(params, TyFun _ arg res)
-> return (params, Just arg, res)
(params, res)
-> return (params, Nothing, res)
let te = tysubsts params ts res
tassert (t' <: te)
[$msg| Pattern got wrong type:
<dl>
<dt>actual: <dd>$t'
<dt>expected: <dd>$te
<dt>in pattern: <dd>$x0
</dl> |]
case (mt, mx) of
(Nothing, Nothing) ->
return [$pa|+ $quid:u |]
(Just t1, Just x1) -> do
let t1' = tysubsts params ts t1
x1' <- tcPatt t1' x1
return [$pa|+ $quid:u $x1' |]
(Nothing, Just _) -> typeError $
"Pattern has parameter where none expected:" !:: x0
(Just _, Nothing) -> typeError $
"Pattern has no parameter but expects one of type" !:: t
_ | isBotType t' -> case mx of
Nothing -> return x0
Just x -> tcPatt tyBot x
| otherwise ->
typeError [$msg| Pattern got wrong type:
<dl>
<dt>type: <dd>$t'
<dt>pattern: <dd>$x0
</dl> |]
[$pa| ($x, $y) |] -> do
t' <- hnT t >>! mapBottom (tyApp tcTuple . replicate 2)
case t' of
TyApp tc [xt, yt] _ | tc == tcTuple -> do
x' <- tcPatt xt x
y' <- tcPatt yt y
return [$pa| ($x', $y') |]
_ -> terrgot "Pattern " t' "pair type"
[$pa| $str:_ |] -> do
tassgot (t <: tyString)
"Pattern" t "string"
return x0
[$pa| $int:_ |] -> do
tassgot (t <: tyInt)
"Pattern" t "int"
return x0
[$pa| $flo:_ |] -> do
tassgot (t <: tyFloat)
"Pattern" t "float"
return x0
[$pa| $x as $lid:y |] -> do
x' <- tcPatt t x
bindVar y t
return [$pa| $x' as $lid:y |]
[$pa| Pack('$tv, $x) |] -> do
t' <- hnT t >>! mapBottom (tyEx tv)
case t' of
TyQu Exists tve te -> do
let qexp = tvqual tv
qact = tvqual tve
tassert (qact <: qexp)
[$msg| Existential unpacking pattern cannot
instantiate type variable:
<dl>
<dt>pattern type variable: <dd>$tv
<dt>expected qualifier: <dd>$qexp
<dt>actual type variable: <dd>$tve
<dt>actual qualifier: <dd>$qact
</dl> |]
let te' = tysubst tve (TyVar tv) te
x' <- tcPatt te' x
return [$pa| Pack('$tv, $x') |]
_ -> terrgot "Pattern" t' "existential type"
[$pa| $antiL:a |] -> $antifail
[$pa| $anti:a |] -> $antifail
-- | Check if type is bottom, and if so, apply the given function
-- to it
mapBottom :: (Type -> Type) -> Type -> Type
mapBottom ft t
| isBotType t = ft t
| otherwise = t
-- Given a list of type variables tvs, a type t in which tvs
-- may be free, and a type t', tries to substitute for tvs in t
-- to produce a type that *might* unify with t'
tryUnify :: (?loc :: Loc, AlmsMonad m) =>
[TyVarR] -> Type -> Type -> m [Type]
tryUnify [] _ _ = return []
tryUnify tvs t t' =
case subtype 100 [] t' tvs t of
Left s -> giveUp (s :: String)
Right (_, ts) -> return ts
where
giveUp _ = typeError $
[$msg| In application, cannot find substitution for type
$msg:1 to unify types:
<dl>
<dt>actual: <dd>$t'
<dt>expected:<dd>$t
</dl> |] $
case tvs of
[tv] -> [$msg| variable $tv |]
[tv1,tv2] -> [$msg| variables $tv1 and $tv2 |]
_ -> [$msg| variables $flow:1 |]
(map [$msg| $1 |] tvs)
-- | Convert qualset representations from a list of all tyvars and
-- list of qualifier-significant tyvars to a set of type parameter
-- indices
indexQuals :: (?loc :: Loc, Monad m) =>
Lid R -> [TyVarR] -> QExp R -> TC m (QDen Int)
indexQuals name tvs qexp = do
qden <- qInterpretM qexp
numberQDenM unbound tvs qden where
unbound tv = typeError
[$msg| Unbound type variable $tv in qualifier list
for type $q:name. |]
-- BEGIN type decl checking
-- | Run a computation in the context of type declarations
tcTyDecs :: (?loc :: Loc, Monad m) =>
[TyDec R] -> TC m [TyDec R]
tcTyDecs tds0 = do
let (atds, stds, dtds) = foldr partition ([], [], []) tds0
-- stds <- topSort getEdge stds0
(_, stub) <- steal $ forM (atds ++ dtds ++ stds) $ \td0 ->
case dataOf td0 of
TdDat name params _ -> allocStub name (map tvqual params)
TdSyn name ((ps,_):_) -> allocStub name (map (const Qa) ps)
TdAbs name params variances quals -> do
quals' <- indexQuals name params quals
ix <- newIndex
us <- currentModulePath
let tc' = mkTC ix (J us name) quals'
[ (tvqual parm, var)
| var <- variances
| parm <- params ]
bindTycon name tc'
_ -> return ()
let loop md = do
((changed, tcs), md') <-
steal $
inModule md $
liftM unzip $
mapM tcTyDec (atds ++ dtds ++ stds)
if or changed
then loop md'
else return (tcs, md')
(tcs, md') <- loop stub
forM_ tcs $ \tc -> do
case tcNext tc of
Nothing -> return ()
Just clauses -> forM_ clauses $ \(tps, rhs) -> do
tassert (rhs /= tyPatToType (TpApp tc {tcNext = Nothing} tps)) $
"Recursive type synonym is not contractive:" !:: tc
tell (replaceTyCons tcs md')
return tds0
where
allocStub name params = do
ix <- newIndex
us <- currentModulePath
let tc = mkTC ix (J us name)
[ (q, Omnivariant) | q <- params ]
bindTycon name tc
--
getEdge td0 = case dataOf td0 of
TdSyn name cs -> (name, S.unions (map (tyConsOfType . snd) cs))
TdAbs name _ _ _ -> (name, S.empty)
TdDat name _ alts -> (name, names) where
names = S.unions [ tyConsOfType t | (_, Just t) <- alts ]
TdAnti a -> $antierror
--
partition td (atds, stds, dtds) =
case dataOf td of
TdAbs _ _ _ _ -> (td : atds, stds, dtds)
TdSyn _ _ -> (atds, td : stds, dtds)
TdDat _ _ _ -> (atds, stds, td : dtds)
TdAnti a -> $antierror
-- tcTyDec types a type declaration, but in addition to
-- returnng a declaration, it returns a boolean that indicates
-- whether the type metadata has changed, which allows for iterating
-- to a fixpoint.
tcTyDec :: (?loc :: Loc, Monad m) =>
TyDec R -> TC m (Bool, TyCon)
tcTyDec td0 = case dataOf td0 of
TdAbs name _ _ _ -> do
tc <- find (J [] name :: QLid R)
bindTycon name tc
return (False, tc)
TdSyn name cs -> do
tc <- find (J [] name :: QLid R)
let nparams = length (fst (head cs))
tassert (all ((==) nparams . length . fst) cs) $
[$msg| In definition of type operator $q:name, not all
clauses have the same number of parameters. |]
(cs', quals, vqs) <- liftM unzip3 $ forM cs $ \(tps, rhs) -> do
rhs' <- tcType rhs
let vs1 = ftvVs rhs'
(tps', tvses, vqs) <- liftM unzip3 $ forM tps $ \tp -> do
tp' <- tcTyPat tp
let tpt = tyPatToType tp'
vs2 = ftvVs tpt
vs' = M.intersectionWith (*) vs1 vs2
var = bigVee (M.elems vs')
qp = qualConst tpt
tvs = qDenFtv (qualifier tpt)
return (tp', tvs, (var, qp))
let tvmap = M.unions [ M.fromDistinctAscList
[ (tv, i) | tv <- S.toAscList tvs ]
| tvs <- tvses
| i <- [ 0 .. ] ]
qual = numberQDenMap tvqual tvmap (qualifier rhs')
return ((tps', rhs'), qual, vqs)
let (arity, bounds) = unzip (map bigVee (transpose vqs))
qual = bigVee quals
changed = arity /= tcArity tc
|| qual /= tcQual tc
tc' = tc { tcArity = arity, tcQual = qual,
tcNext = Just cs', tcBounds = bounds }
bindTycon name tc'
return (changed, tc')
TdDat name params alts -> do
tc <- find (J [] name :: QLid R)
alts' <- sequence
[ case mt of
Nothing -> return (cons, Nothing)
Just t -> do
t' <- tcType t
return (cons, Just t')
| (cons, mt) <- alts ]
let t' = foldl tyTuple tyUnit [ t | (_, Just t) <- alts' ]
qual = numberQDen params (qualifier t')
arity = typeVariances params t'
changed = arity /= tcArity tc
|| qual /= tcQual tc
tc' = tc { tcArity = arity, tcQual = qual,
tcCons = (params, fromList alts') }
bindTycon name tc'
bindAlts params tc' alts'
return (changed, tc')
TdAnti a -> $antifail
-- | Build a module of datacon types from a datatype's
-- alternatives
bindAlts :: Monad m => [TyVarR] -> TyCon -> [(Uid R, Maybe Type)] -> TC m ()
bindAlts params tc = mapM_ each where
each (u, Nothing) = bindCon u (alls result)
each (u, Just t) = bindCon u (alls (t .->. result))
alls t = foldr tyAll t params
result = tyApp tc (map TyVar params)
-- | Compute the variances at which some type variables occur
-- in an open type expression
typeVariances :: [TyVarR] -> Type -> [Variance]
typeVariances d0 = finish . ftvVs where
finish m = [ maybe 0 id (M.lookup tv m)
| tv <- d0 ]
-- | Generic topological sort
--
-- Uses an adjacency-list graph representation. Given a
-- function from abstract node values to comparable nodes,
-- and a list of node values, returns a list of node values (or
-- fails if there's a cycle).
topSort :: forall node m a.
(?loc :: Loc, AlmsMonad m, Ord node, Ppr node) =>
(a -> (node, S.Set node)) -> [a] -> m [a]
topSort getEdge edges = do
(_, w) <- RWS.execRWST visitAll S.empty S.empty
return w
where
visitAll = mapM_ visit (M.keys graph)
--
visit :: node -> RWS.RWST (S.Set node) [a] (S.Set node) m ()
visit node = do
stack <- RWS.ask
lift $
tassert (not (node `S.member` stack)) $
"Unproductive cycle in type definitions via type" !:: node
seen <- RWS.get
if node `S.member` seen
then return ()
else do
RWS.put (S.insert node seen)
case M.lookup node graph of
Just (succs, info) -> do
RWS.local (S.insert node) $
mapM_ visit succs
RWS.tell [info]
Nothing ->
return ()
--
graph :: M.Map node ([node], a)
graph = M.fromList [ let (node, succs) = getEdge info
in (node, (S.toList succs, info))
| info <- edges ]
-- | The (unqualified) tycons that appear in a syntactic type
tyConsOfType :: Syntax.Type R -> S.Set (Lid R)
tyConsOfType [$ty| ($list:ts) $qlid:n |] =
case n of
J [] l -> S.singleton l
_ -> S.empty
`S.union` S.unions (map tyConsOfType ts)
tyConsOfType [$ty| '$_ |] = S.empty
tyConsOfType [$ty| $t1 -[$opt:_]> $t2 |] =
tyConsOfType t1 `S.union` tyConsOfType t2
tyConsOfType [$ty| $quant:_ '$_. $t |] = tyConsOfType t
tyConsOfType [$ty| mu '$_. $t |] = tyConsOfType t
tyConsOfType [$ty| $anti:a |] = $antierror
tcTyPat :: Monad m => Syntax.TyPat R -> TC m TyPat
tcTyPat (N note (Syntax.TpVar tv var)) = do
let ?loc = getLoc note
tassert (var == Invariant)
[$msg| Type pattern variable $tv has a variance annotation
$q:var. Variances may not be specified for parameters
of type operators, but are inferred. |]
return (TpVar tv)
tcTyPat tp@[$tpQ| ($list:tps) $qlid:qu |] = do
let ?loc = _loc
tc <- find qu
tassert (isNothing (tcNext tc)) $
"Type operator pattern is also a type operator:" !:: tp
TpApp tc <$> mapM tcTyPat tps
tcTyPat [$tpQ| $antiP:a |] = $antifail
-- END type decl checking
-- | Type check a signature
tcSigExp :: (?loc :: Loc, Monad m) =>
SigExp R -> TC m (SigExp R)
tcSigExp [$seQ| sig $list:ds end |] = do
ds' <- forgetModulePath $ tcMapM tcSigItem ds
return [$seQ| sig $list:ds' end |]
tcSigExp [$seQ| $quid:n $list:qls |] = do
(md, _) <- find (fmap SIGVAR n)
tell md
return [$seQ| $quid:n $list:qls |]
tcSigExp [$seQ| $se1 with type $list:tvs $qlid:tc = $t |] = do
(se1', md) <- steal $ tcSigExp se1
t' <- tcType t
fibrate tvs tc t' md
return [$seQ| $se1' with type $list:tvs $qlid:tc = $t |]
tcSigExp [$seQ| $anti:a |] = $antifail
fibrate :: (?loc :: Loc, Monad m) =>
[TyVar R] -> QLid R -> Type -> Module -> TC m ()
fibrate tvs ql t md = do
let Just tc = findTycon ql md
tassert (isAbstractTyCon tc) $
"Signature fibration (with-type) cannot update concrete" ++
"type constructor:" !:: ql
let actlen = length tvs
explen = length (tcArity tc)
tassert (actlen == explen)
[$msg| In signature fibration (with type), wrong number of
parameters to type:
<dl>
<dt>actual count: <dd>$actlen
<dt>expected count: <dd>$explen
<dt>for type: <dd>$ql
</dl> |]
let amap = ftvVs t
arity = map (\tv -> fromJust (M.lookup tv amap)) tvs
bounds = map tvqual tvs
qual = numberQDen tvs (qualifier t)
next = Just [(map TpVar tvs, t)]
tc' = tc {
tcArity = arity,
tcBounds = bounds,
tcQual = qual,
tcNext = next
}
tell (replaceTyCon tc' md)
where
findTycon ql0 md0 = case md0 of
MdNil -> mzero
MdApp md1 md2 -> findTycon ql0 md1 `mplus` findTycon ql0 md2
MdTycon l tc -> if J [] l == ql0 then return tc else mzero
MdModule u md1 -> case ql0 of
J (u':us) l | u == u' -> findTycon (J us l) md1
_ -> mzero
MdSig _ _ -> mzero
MdValue _ _ -> mzero
tcSigItem :: (?loc :: Loc, Monad m) =>
SigItem R -> TC m (SigItem R)
tcSigItem sg0 = case sg0 of
[$sgQ| val $lid:l : $t |] -> do
t' <- tcType t
bindVar l t'
return [$sgQ| val $lid:l : $t |]
[$sgQ| type $list:tds |] -> do
tds' <- tcTyDecs tds
return [$sgQ| type $list:tds' |]
[$sgQ| module $uid:u : $se1 |] -> do
(se', md) <- steal $ tcSigExp se1
bindModule u md
return [$sgQ| module $uid:u : $se' |]
[$sgQ| module type $uid:u = $se1 |] -> do
se' <- tcSig u se1
return [$sgQ| module type $uid:u = $se' |]
[$sgQ| include $se1 |] -> do
se' <- tcSigExp se1
return [$sgQ| include $se' |]
[$sgQ| exception $uid:u of $opt:mt |] -> do
mt' <- tcException u mt
return [$sgQ| exception $uid:u of $opt:mt' |]
[$sgQ| $anti:a |] -> $antifail
-- | Run a computation in the context of a let declaration
tcLet :: (?loc :: Loc, Monad m) =>
Patt R -> Maybe (Syntax.Type R) -> Expr R ->
TC m (Patt R, Maybe (Syntax.Type R), Expr R)
tcLet x mt e = do
tassert (S.null (dtv x)) $
"Attempt to unpack existential in top-level binding:" !:: x
(te, e') <- tcExpr e
t' <- case mt of
Just t -> do
t' <- tcType t
tassert (qualConst t' == Qu) $
[$msg| Declared type of let declaration of $q:x is not unlimited |]
tassert (te <: t')
[$msg| Mismatch in declared type for let declaration:
<dl>
<dt>actual: <dd>$te
<dt>expected: <dd>$t'
<dt>in pattern: <dd>$x
</dl> |]
return t'
Nothing -> do
tassert (qualConst te == Qu) $
[$msg| Type of let declaration binding is not unlimited:
<dl>
<dt>type: <dd>$te
<dt>qualifier: <dd>$1
<dt>in pattern: <dd>$x
</dl> |] (qRepresent (qualifier te))
return te
x' <- tcPatt t' x
-- ioM (hPutStrLn stderr (show te))
return (x', Just (typeToStx' t'), e')
-- | Run a computation in the context of a module open declaration
tcOpen :: (?loc :: Loc, Monad m) =>
ModExp R -> TC m (ModExp R)
tcOpen b = tcModExp b
-- | Run a computation in the context of a local block (that is, after
-- the block)
tcLocal :: (?loc :: Loc, Monad m) =>
[Decl R] -> [Decl R] ->
TC m ([Decl R], [Decl R])
tcLocal ds1 ds2 = do
(ds1', md1) <- steal $ tcDecls ds1
ds2' <- inModule md1 $ tcDecls ds2
return (ds1', ds2')
-- | Run a computation in the context of a new exception variant
tcException :: (?loc :: Loc, Monad m) =>
Uid R -> Maybe (Syntax.Type R) ->
TC m (Maybe (Syntax.Type R))
tcException n mt = do
mt' <- gmapM tcType mt
bindCon n (maybe tyExn (`tyArr` tyExn) mt')
return (fmap typeToStx' mt')
-- | Type check and bind a module
tcMod :: (?loc :: Loc, Monad m) =>
Uid R -> ModExp R -> TC m (ModExp R)
tcMod u me0 = do
(me', md) <- steal $ enterModule u $ tcModExp me0
bindModule u md
return me'
-- | Type check and bind a signature
tcSig :: (?loc :: Loc, Monad m) =>
Uid R -> SigExp R -> TC m (SigExp R)
tcSig u se0 = do
(se', md) <- steal $ tcSigExp se0
bindSig u md
return se'
-- | Type check a module body
tcModExp :: (?loc :: Loc, Monad m) =>
ModExp R -> TC m (ModExp R)
tcModExp [$me| struct $list:ds end |] = do
ds' <- tcDecls ds
return [$me| struct $list:ds' end |]
tcModExp [$me| $quid:n $list:qls |] = do
(md, _) <- find n
tell md
return [$me| $quid:n $list:qls |]
tcModExp [$me| $me1 : $se2 |] = do
(me1', md1) <- steal $ tcModExp me1
(se2', md2) <- steal $ tcSigExp se2
ascribeSignature md1 md2
return [$me| $me1' : $se2' |]
tcModExp [$me| $anti:a |] = $antifail
-- | Run a computation in the context of an abstype block
tcAbsTy :: (?loc :: Loc, Monad m) =>
[AbsTy R] -> [Decl R] ->
TC m ([AbsTy R], [Decl R])
tcAbsTy atds ds = do
(_, md1) <- steal $ tcTyDecs (map (atdecl . dataOf) atds)
(ds', md2) <- steal $ inModule md1 $ tcDecls ds
tcs <- forM atds $ \at0 -> case view at0 of
AbsTy arity quals (N _ (TdDat name params _)) -> do
let env = envify md1
tc = fromJust (env =..= name)
qualSet <- indexQuals name params quals
if length params == length (tcArity tc)
then return ()
else typeBug "tcAbsTy" $
"in abstype declaration " ++ show (length params) ++
" parameters given for type " ++ show name ++
" which has " ++ show (length (tcArity tc))
let actualArity = tcArity tc
actualQual = tcQual tc
tassexp (all2 (<:) actualArity arity)
[$msg| In abstype declaration, declared parameter variance for
type $q:name is more permissive than actual variance: |]
(pprMsg actualArity)
(pprMsg arity)
tassexp (actualQual <: qualSet)
[$msg| In abstype declaration, declared qualifier for
type $q:name is more permissive than actual qualifier: |]
(showMsg actualQual)
(showMsg qualSet)
return $ abstractTyCon tc {
tcQual = qualSet,
tcArity = arity,
tcCons = ([], empty)
}
_ -> typeBug "tcAbsTy" "Can’t do abstype with non-datatypes"
tell (replaceTyCons tcs (md1 `mappend` md2))
return (atds, ds')
-- | Type check a declaration
tcDecl :: Monad m => Decl R -> TC m (Decl R)
tcDecl decl =
let ?loc = getLoc decl in
case decl of
[$dc| let $x : $opt:t = $e |] -> do
(x', t', e') <- tcLet x t e
return [$dc| let $x' : $opt:t' = $e' |]
[$dc| type $list:tds |] -> do
tds' <- tcTyDecs tds
return [$dc| type $list:tds' |]
[$dc| abstype $list:at with $list:ds end |] -> do
(at', ds') <- tcAbsTy at ds
return [$dc| abstype $list:at' with $list:ds' end |]
[$dc| module $uid:x = $b |] -> do
b' <- tcMod x b
return [$dc| module $uid:x = $b' |]
[$dc| module type $uid:x = $b |] -> do
b' <- tcSig x b
return [$dc| module type $uid:x = $b' |]
[$dc| open $b |] -> do
b' <- tcOpen b
return [$dc| open $b' |]
[$dc| local $list:ds0 with $list:ds1 end |] -> do
(ds0', ds1') <- tcLocal ds0 ds1
return [$dc| local $list:ds0' with $list:ds1' end |]
[$dc| exception $uid:n of $opt:mt |] -> do
mt' <- tcException n mt
return [$dc| exception $uid:n of $opt:mt' |]
[$dc| $anti:a |] -> $antifail
-- | Type check a sequence of declarations
tcDecls :: Monad m => [Decl R] -> TC m [Decl R]
tcDecls = tcMapM tcDecl
---
--- Module sealing
---
-- | For mapping renamed names (from structures) into unrenamed names
-- (in signatures)
data NameMap
= NameMap {
nmValues :: Env (BIdent R) (BIdent R),
nmTycons :: Env (Lid R) (Lid R),
nmModules :: Env (Uid R) (Uid R, NameMap),
nmSigs :: Env (Uid R) (Uid R)
}
instance Monoid NameMap where
mempty = NameMap empty empty empty empty
mappend (NameMap a1 a2 a3 a4) (NameMap b1 b2 b3 b4) =
NameMap (a1 =+= b1) (a2 =+= b2) (a3 =+= b3) (a4 =+= b4) where
instance GenEmpty NameMap where
genEmpty = mempty
instance GenExtend NameMap NameMap where
(=+=) = mappend
instance GenLookup NameMap (BIdent R) (BIdent R) where
e =..= k = nmValues e =..= k
instance GenLookup NameMap (Lid R) (Lid R) where
e =..= k = nmTycons e =..= k
instance GenLookup NameMap (Uid R) (Uid R, NameMap) where
e =..= k = nmModules e =..= k
instance GenLookup NameMap SIGVAR (Uid R) where
e =..= k = nmSigs e =..= unSIGVAR k
-- | Given a module, construct a 'NameMap' mapping raw versions of its
-- names to the actual renamed version.
makeNameMap :: Module -> NameMap
makeNameMap md0 = case md0 of
MdNil -> mempty
MdApp md1 md2 -> makeNameMap md1 =+= makeNameMap md2
MdValue x _ -> mempty { nmValues = unnameBIdent x =:= x }
MdTycon x _ -> mempty { nmTycons = unnameLid x =:= x }
MdModule x md1 -> mempty { nmModules = unnameUid x =:= (x, makeNameMap md1) }
MdSig x _ -> mempty { nmSigs = unnameUid x =:= x }
where
unnameLid :: Lid R -> Lid R
unnameLid = lid . unLid
unnameUid :: Uid R -> Uid R
unnameUid = uid . unUid
unnameBIdent :: BIdent R -> BIdent R
unnameBIdent (Var l) = Var (unnameLid l)
unnameBIdent (Con u) = Con (unnameUid u)
-- | Given a module and a signature, ascribe the signature to the module
-- and write the result.
ascribeSignature :: (?loc :: Loc, Monad m) =>
Module -> Module -> TC m ()
ascribeSignature md1 md2 = do
us <- currentModulePath
let md2' = renameSig (makeNameMap md1) us md2
onlyInModule md1 $ do
subst <- matchSigTycons md2'
subsumeSig (applyTyConSubstInSig subst md2')
let tcs = getGenTycons md2' []
tcs' <- forM tcs $ \tc -> do
ix <- newIndex
return tc { tcId = ix }
tell (substTyCons tcs tcs' md2')
-- | Make the names in a signature match the names from the module it's
-- being applied to.
renameSig :: NameMap -> [Uid Renamed] -> Module -> Module
renameSig nm0 us = loop where
loop md0 = case md0 of
MdNil -> MdNil
MdApp md1 md2 -> MdApp (loop md1) (loop md2)
MdValue x t -> MdValue (fromJust (nm0 =..= x)) t
MdTycon x tc -> MdTycon (fromJust (nm0 =..= x)) tc'
where tc' = tc { tcName = J us (jname (tcName tc)) }
MdModule x md1 ->
let Just (x', nm1) = nm0 =..= x
in MdModule x' (renameSig nm1 (us++[x']) md1)
MdSig x md1 -> MdSig (fromJust (nm0 =..= SIGVAR x)) md1
-- | Given a signature, find the tycon substitutions necessary to
-- unify it with the module in the environment.
matchSigTycons :: Monad m => Module -> TC m TyConSubst
matchSigTycons = loop [] where
loop path md0 = case md0 of
MdNil -> return mempty
MdApp md1 md2 -> mappend <$> loop path md1 <*> loop path md2
MdValue _ _ -> return mempty
MdTycon x tc -> do
tc' <- find (J path x)
return (makeTyConSubst [tc] [tc'])
MdModule x md1 -> loop (path++[x]) md1
MdSig _ _ -> return mempty
-- | Given a tycon substitution, apply it to all the values and
-- RIGHT-HAND-SIDES of type definitions in a signature. In
-- particular, don't replace any tycon bindings directly, but do
-- replace any references to other types in their definitions.
applyTyConSubstInSig :: TyConSubst -> Module -> Module
applyTyConSubstInSig subst = loop where
loop md0 = case md0 of
MdNil -> MdNil
MdApp md1 md2 -> MdApp (loop md1) (loop md2)
MdValue x t -> MdValue x (applyTyConSubst subst t)
MdTycon x tc -> MdTycon x (applyTyConSubstInTyCon subst tc)
MdModule x md1 -> MdModule x (loop md1)
MdSig x md1 -> MdSig x (loop md1)
-- | Get a list of all the tycons that need a new index allocated
-- because they're generative.
getGenTycons :: Module -> [TyCon] -> [TyCon]
getGenTycons = loop where
loop MdNil = id
loop (MdApp md1 md2) = loop md1 . loop md2
loop (MdValue _ _) = id
loop (MdTycon _ tc) = if varietyOf tc == OperatorType
then id
else (tc:)
loop (MdModule _ md1) = loop md1
loop (MdSig _ _) = id
-- | Check whether the given signature subsumes the signature
-- implicit in the environment.
subsumeSig :: (?loc :: Loc, Monad m) =>
Module -> TC m ()
subsumeSig = loop where
loop md0 = case md0 of
MdNil -> return ()
MdApp md1 md2 -> do loop md1; loop md2
MdValue x t -> do
t' <- find (J [] x :: Ident R)
tassexp (t' <: t)
[$msg| In signature matching, type mismatch for $q:x: |]
[$msg| $t' |]
[$msg| $t |]
MdTycon x tc -> do
tc' <- find (J [] x :: QLid R)
case varietyOf tc of
AbstractType -> do
let sigass assertion thing getter =
tassexp assertion
([$msg| In signature matching, cannot match the
definition for type $q:1 because the
$words:thing does not match: |] (tcName tc))
(showMsg (getter tc'))
(showMsg (getter tc))
sigass (length (tcArity tc') == length (tcArity tc))
"number of type parameters" (length . tcArity)
sigass (all2 (<:) (tcArity tc') (tcArity tc))
"variance" tcArity
sigass (all2 (<:) (tcBounds tc') (tcBounds tc))
"parameter bounds" tcBounds
sigass (tcQual tc' <: tcQual tc)
"qualifier" tcQual
OperatorType -> matchTycons tc' tc
DataType -> matchTycons tc' tc
MdModule x md1 -> do
(md2, _) <- find (J [] x :: QUid R)
onlyInModule md2 $ subsumeSig md1
MdSig x md1 -> do
(md2, _) <- find (J [] (SIGVAR x) :: Path (Uid R) SIGVAR)
matchSigs md2 md1
-- | Check that two signatures match EXACTLY.
-- First signature is what we have, and second is what we want.
matchSigs :: (?loc :: Loc, Monad m) =>
Module -> Module -> TC m ()
matchSigs md10 md20 = loop (linearize md10 []) (linearize md20 []) where
loop [] [] = return ()
loop (MdValue x1 t1 : sgs1) (MdValue x2 t2 : sgs2)
| x1 == x2 && t1 == t2 = loop sgs1 sgs2
loop (MdTycon x1 tc1 : sgs1) (MdTycon x2 tc2 : sgs2)
| x1 == x2 = do
matchTycons tc1 tc2
loop (substTyCon tc1 tc2 sgs1) sgs2
loop (MdModule x1 md1 : sgs1) (MdModule x2 md2 : sgs2)
| x1 == x2 = do
matchSigs md1 md2
loop sgs1 sgs2
loop (MdSig x1 md1 : sgs1) (MdSig x2 md2 : sgs2)
| x1 == x2 = do
matchSigs md1 md2
loop sgs1 sgs2
loop [] (sg : _) = do
(x, what) <- whatIs sg
typeError [$msg|
In exact signature matching, missing expected $what $qmsg:x.
|]
loop (sg : _) [] = do
(x, what) <- whatIs sg
typeError [$msg|
In exact signature matching, found unexpected $what $qmsg:x.
|]
loop (sg1 : _) (sg2 : _) = do
(x1, what1) <- whatIs sg1
(x2, what2) <- whatIs sg2
typeError [$msg|
In exact signature matching (for signatures as entries in
signatures being matched), got signature items didn’t match:
<dl>
<dt>actual: <dd>$what1 $qmsg:x1
<dt>expected: <dd>$what2 $qmsg:x2
</dl>
|]
--
whatIs (MdValue x _) = return (pprMsg x, "value")
whatIs (MdTycon x _) = return (pprMsg x, "type")
whatIs (MdModule x _) = return (pprMsg x, "module")
whatIs (MdSig x _) = return (pprMsg x, "module type")
whatIs _ = typeBug "matchSigs" "weird signature item"
-- | Extensional equality for type constructors
tyconExtEq :: TyCon -> TyCon -> Bool
tyconExtEq tc1 tc2 | tcBounds tc1 == tcBounds tc2 =
let tvs = zipWith (TyVar .) tvalphabet (tcBounds tc1)
in tyApp tc1 tvs == tyApp tc2 tvs
tyconExtEq _ _ = False
-- | Check that two type constructors match exactly.
matchTycons :: (?loc :: Loc, Monad m) =>
TyCon -> TyCon -> TC m ()
matchTycons tc1 tc2 = case (varietyOf tc1, varietyOf tc2) of
(AbstractType, AbstractType) -> do
tassert (tcArity tc1 == tcArity tc2) $
estr "the arity or variance"
(show (tcArity tc1)) (show (tcArity tc2))
tassert (tcBounds tc1 == tcBounds tc2) $
estr "parameter bound" (show (tcBounds tc1)) (show (tcBounds tc2))
tassert (tcQual tc1 == tcQual tc2) $
estr "qualifier" (show (tcQual tc1)) (show (tcQual tc2))
(DataType, DataType) -> do
let (tvs1, rhs1) = tcCons tc1
(tvs2, rhs2) = tcCons tc2
tassert (length tvs1 == length tvs2) $
estr "number of parameters" (show (length tvs1)) (show (length tvs2))
let mtv = maxtv (tvs1, tvs2, Env.range rhs1, Env.range rhs2)
tvs' = fastFreshTyVars tvs1 mtv
rhs1' = Env.mapVals (fmap (tysubsts tvs1 (map TyVar tvs'))) rhs1
rhs2' = Env.mapVals (fmap (tysubsts tvs2 (map TyVar tvs'))) rhs2
forM_ (Env.toList rhs1') $ \(k, t1) ->
let Just t2 = rhs2' =..= k
in tassert (t1 == t2) $ estr
("constructor ‘" ++ show k ++ "’")
(maybe "nothing" show t1)
(maybe "nothing" show t2)
(OperatorType, _) | tyconExtEq tc1 tc2 -> return ()
(_, OperatorType) | tyconExtEq tc1 tc2 -> return ()
(OperatorType, OperatorType) -> do
let next1 = fromJust (tcNext tc1)
next2 = fromJust (tcNext tc2)
tassert (length next1 == length next2) $
estr "number of clauses" (show (length next1)) (show (length next2))
forM_ (zip3 next1 next2 [1 :: Int .. ]) $
\((tp1, t1), (tp2, t2), ix) -> do
tassert (length tp1 == length tp2) $
estr ("number of parameters in clause " ++ show ix)
(show (length tp1)) (show (length tp2))
(tvs1, tvs2) <- mconcat `liftM` zipWithM matchTypats tp1 tp2
let mtv = maxtv (tvs1, tvs2, t1, t2)
tvs' = fastFreshTyVars tvs1 mtv
t1' = tysubsts tvs1 (map TyVar tvs') t1
t2' = tysubsts tvs2 (map TyVar tvs') t2
tassert (t1' == t2') $
estr ("type operator right-hand sides in clause " ++ show ix)
(show t1') (show t2')
(v1, v2) -> typeError $ estr "kind of definition" (show v1) (show v2)
where
estr what which1 which2 =
[$msg|
In signature matching, cannot match definition for type
$q:tc1 because the $words:what does not match:
<dl>
<dt>actual: <dd>$which1
<dt>expected: <dd>$which2
</dl>
|]
-- | To check that two type patterns match, and return the pairs of
-- type variables that line up and thus need renaming.
matchTypats :: (?loc :: Loc, Monad m) =>
TyPat -> TyPat -> TC m ([TyVar R], [TyVar R])
matchTypats (TpVar tv1) (TpVar tv2)
= return ([tv1], [tv2])
matchTypats (TpApp tc1 tvs1) (TpApp tc2 tvs2)
| tc1 == tc2
= mconcat `liftM` zipWithM matchTypats tvs1 tvs2
matchTypats tp1 tp2
= terrexp
[$msg| In signature matching, cannot match type patterns: |]
(pprMsg tp1) (pprMsg tp2)
-- | To flatten all the 'MdNil' and 'MdApp' constructors in a module
-- into an ordinary list.
linearize :: Module -> [Module] -> [Module]
linearize MdNil = id
linearize (MdApp md1 md2) = linearize md1 . linearize md2
linearize md1 = (md1 :)
---
--- END Module Sealing
---
-- | Add the type of a value binding
addVal :: Monad m => Lid R -> Syntax.Type R -> TC m ()
addVal x t = do
let ?loc = mkBogus "<addVal>"
t' <- tcType t
bindVar x t'
-- | Add an arbitrary declaration
addDecl :: Monad m => Decl R -> TC m ()
addDecl d = () <$ tcDecl d
-- | Add a type constructor binding
addType :: Monad m => Lid R -> TyCon -> TC m ()
addType n tc = () <$ bindTycon n tc
-- | Add a nested submodule
addMod :: Monad m => Uid R -> TC m a -> TC m ()
addMod u action = do
(_, md) <- steal $ enterModule u $ action
bindModule u md
-- | Type check a program
tcProg :: Monad m => Prog R -> TC m (Type, Prog R)
tcProg [$prQ| $list:ds in $opt:e0 |] = do
(ds', md) <- steal $ tcDecls ds
(t, e0') <- case e0 of
Just e -> liftM (second Just) $ inModule md $ tcExpr e
Nothing -> return (tyUnit, Nothing)
return (t, [$prQ|+ $list:ds' in $opt:e0' |])
-- | The initial type-checking state
env0 :: S
env0 = S e0 0 where
e0 :: E
e0 = genEmpty =+= (Con (uid "()") -:- tyUnit :: VE)
-- | Find out the parameter type of an exception
getExnParam :: Type -> Maybe (Maybe Type)
getExnParam (TyApp tc _ _)
| tc == tcExn = Just Nothing
getExnParam (TyFun _ t1 (TyApp tc _ _))
| tc == tcExn = Just (Just t1)
getExnParam _ = Nothing
-- | Reconstruct the declaration from a tycon binding, for printing
tyConToDec :: TyNames -> TyCon -> TyDec R
tyConToDec tn tc = case tc of
_ | tc == tcExn
-> tdAbs (lid "exn") [] [] maxBound
TyCon { tcName = n, tcNext = Just clauses }
-> tdSyn (jname n) [ (map (tyPatToStx tn) ps, typeToStx tn rhs)
| (ps, rhs) <- clauses ]
TyCon { tcName = n, tcCons = (ps, alts) }
| not (isEmpty alts)
-> tdDat (jname n) ps [ (u, fmap (typeToStx tn) mt)
| (u, mt) <- toList alts ]
TyCon { tcName = n }
->
let tyvars = zipWith ($) tvalphabet (tcBounds tc)
in tdAbs (jname n)
(zipWith const tyvars (tcArity tc))
(tcArity tc)
(qRepresent
(denumberQDen
(map (qInterpret . qeVar) tyvars)
(tcQual tc)))
getVarInfo :: QLid R -> S -> Maybe Type
getVarInfo ql (S e _) = e =..= fmap Var ql
getTypeInfo :: QLid R -> S -> Maybe TyCon
getTypeInfo ql (S e _) = e =..= ql
-- Find out about a data constructor. If it's an exception constructor,
-- return 'Left' with its paramter, otherwise return the type construtor
-- of the result type
getConInfo :: QUid R -> S -> Maybe (Either (Maybe Type) TyCon)
getConInfo qu (S e _) = do
t <- e =..= fmap Con qu
case getExnParam t of
Just mt -> Just (Left mt)
Nothing ->
let loop (TyFun _ _ t2) = loop t2
loop (TyQu _ _ t1) = loop t1
loop (TyApp tc _ _) = Just (Right tc)
loop _ = Nothing
in loop t
-- Open the given module, if it exists.
staticsEnterScope :: Uid R -> S -> S
staticsEnterScope u s =
let e = sEnv s in
case e =..= u of
Just (_, e') -> s { sEnv = e =+= e' }
Nothing -> s