{- PiForall language -} {-# LANGUAGE ViewPatterns, TypeSynonymInstances, ExistentialQuantification, NamedFieldPuns, ParallelListComp, FlexibleContexts, ScopedTypeVariables, TupleSections, FlexibleInstances, CPP #-} {-# OPTIONS_GHC -Wall -fno-warn-unused-matches #-} -- | The main routines for type-checking module TypeCheck(tcModules, inferType, checkType) where import Syntax import Environment import PrettyPrint import Equal import Unbound.Generics.LocallyNameless import Unbound.Generics.LocallyNameless.Internal.Fold (toListOf) #ifdef MIN_VERSION_GLASGOW_HASKELL #if MIN_VERSION_GLASGOW_HASKELL(7,10,3,0) -- ghc >= 7.10.3 #else -- older ghc versions, but MIN_VERSION_GLASGOW_HASKELL defined #endif #else -- MIN_VERSION_GLASGOW_HASKELL not even defined yet (ghc <= 7.8.x) import Control.Applicative #endif import Control.Monad.Except import Text.PrettyPrint.HughesPJ import Data.Maybe import Data.List(nub) import Unbound.Generics.LocallyNameless.Unsafe (unsafeUnbind) -- | Infer the type of a term, producing an annotated version of the -- term (whose type can *always* be inferred). inferType :: Term -> TcMonad (Term,Type) inferType t = tcTerm t Nothing -- | Check that the given term has the expected type. -- The provided type does not necessarily need to be in whnf, but it should be -- elaborated (i.e. already checked to be a good type). checkType :: Term -> Type -> TcMonad (Term, Type) checkType tm expectedTy = do nf <- whnf expectedTy tcTerm tm (Just nf) -- | check a term, producing an elaborated term -- where all of the type annotations have been filled in -- The second argument is 'Nothing' in inference mode and -- an expected type (must be in whnf) in checking mode tcTerm :: Term -> Maybe Type -> TcMonad (Term,Type) tcTerm t@(Var x) Nothing = do ty <- lookupTy x return (t,ty) tcTerm t@(Type) Nothing = return (t,Type) tcTerm (Pi bnd) Nothing = do ((x, unembed -> tyA), tyB) <- unbind bnd atyA <- tcType tyA atyB <- extendCtx (Sig x atyA) $ tcType tyB return (Pi (bind (x, embed atyA) atyB), Type) -- Check the type of a function tcTerm (Lam bnd) (Just (Pi bnd2)) = do -- unbind the variables in the lambda expression and pi type ((x,unembed -> Annot ma), body, (_, unembed -> tyA), tyB) <- unbind2Plus bnd bnd2 -- check tyA matches type annotation on binder, if present maybe (return ()) (equate tyA) ma -- check the type of the body of the lambda expression (ebody, etyB) <- extendCtx (Sig x tyA) (checkType body tyB) return (Lam (bind (x, embed (Annot (Just tyA))) ebody), Pi bnd2) tcTerm (Lam _) (Just nf) = err [DS "Lambda expression has a function type, not", DD nf] -- infer the type of a lambda expression, when an annotation -- on the binder is present tcTerm (Lam bnd) Nothing = do ((x,(unembed -> Annot annot)), body) <- unbind bnd tyA <- maybe (err [DS "Must annotate lambda"]) (return) annot -- check that the type annotation is well-formed atyA <- tcType tyA -- infer the type of the body of the lambda expression (ebody, atyB) <- extendCtx (Sig x atyA) (inferType body) return (Lam (bind (x, embed (Annot (Just atyA))) ebody), Pi (bind (x, embed atyA) atyB)) tcTerm (App t1 t2) Nothing = do (at1, ty1) <- inferType t1 (x, tyA, tyB) <- ensurePi ty1 (at2, ty2) <- checkType t2 tyA let result = (App at1 at2, subst x at2 tyB) return result -- Check the type of a function tcTerm (ErasedLam bnd) (Just (ErasedPi bnd2)) = do -- unbind the variables in the lambda expression and pi type ((x,unembed -> Annot ma), body, (_, unembed -> tyA), tyB) <- unbind2Plus bnd bnd2 -- check tyA matches type annotation on binder, if present maybe (return ()) (equate tyA) ma -- check the type of the body of the lambda expression (ebody, etyB) <- extendCtx (Sig x tyA) (checkType body tyB) -- make sure that an 'erased' variable isn't used when (x `elem` toListOf fv (erase ebody)) $ err [DS "Erased variable", DD x, DS "used in body"] return (ErasedLam (bind (x, embed (Annot (Just tyA))) ebody), ErasedPi bnd2) tcTerm (ErasedLam _) (Just nf) = err [DS "Lambda expression has a function type, not", DD nf] -- infer the type of a lambda expression, when an annotation -- on the binder is present tcTerm (ErasedLam bnd) Nothing = do ((x,(unembed -> Annot annot)), body) <- unbind bnd tyA <- maybe (err [DS "Must annotate lambda"]) (return) annot -- check that the type annotation is well-formed atyA <- tcType tyA -- infer the type of the body of the lambda expression (ebody, atyB) <- extendCtx (Sig x atyA) (inferType body) -- make sure that an 'erased' variable isn't used when (x `elem` toListOf fv (erase ebody)) $ err [DS "Erased variable", DD x, DS "used in body"] return (ErasedLam (bind (x, embed (Annot (Just atyA))) ebody), ErasedPi (bind (x, embed atyA) atyB)) tcTerm (ErasedApp t1 t2) Nothing = do (at1, ty1) <- inferType t1 (x, tyA, tyB) <- ensureErasedPi ty1 (at2, ty2) <- checkType t2 tyA let result = (ErasedApp at1 at2, subst x at2 tyB) return result tcTerm (ErasedPi bnd) Nothing = do ((x, unembed -> tyA), tyB) <- unbind bnd atyA <- tcType tyA atyB <- extendCtx (Sig x atyA) $ tcType tyB return (ErasedPi (bind (x, embed atyA) atyB), Type) tcTerm (Ann tm ty) Nothing = do ty' <- tcType ty (tm', ty'') <- checkType tm ty' return (tm', ty'') tcTerm (Pos p tm) mTy = extendSourceLocation p tm $ tcTerm tm mTy tcTerm (Paren tm) mTy = tcTerm tm mTy tcTerm t@(TrustMe ann1) ann2 = do expectedTy <- matchAnnots t ann1 ann2 return (TrustMe (Annot (Just expectedTy)), expectedTy) tcTerm (TyUnit) Nothing = return (TyUnit, Type) tcTerm (LitUnit) Nothing = return (LitUnit, TyUnit) tcTerm (TyBool) Nothing = return (TyBool,Type) tcTerm (LitBool b) Nothing = do return (LitBool b, TyBool) tcTerm t@(If t1 t2 t3 ann1) ann2 = do ty <- matchAnnots t ann1 ann2 (at1,_) <- checkType t1 TyBool nf <- whnf at1 let ctx b = case nf of Var x -> [Def x (LitBool b)] _ -> [] (at2, _) <- extendCtxs (ctx True) $ checkType t2 ty (at3, _) <- extendCtxs (ctx False) $ checkType t3 ty return (If at1 at2 at3 (Annot (Just ty)), ty) tcTerm (Let bnd) ann = do ((x,unembed->rhs),body) <- unbind bnd (arhs,aty) <- inferType rhs (abody,ty) <- extendCtxs [Sig x aty, Def x arhs] $ tcTerm body ann when (x `elem` toListOf fv ty) $ err [DS "Let bound variable", DD x, DS "escapes in type", DD ty] return (Let (bind (x,embed arhs) abody), ty) -- Type constructor application tcTerm (TCon c params) Nothing = do (delta, _) <- lookupTCon c unless (length params == teleLength delta) $ err [DS "Datatype constructor", DD c, DS $ "should have " ++ show (teleLength delta) ++ "parameters, but was given", DD (length params)] eparams <- tsTele params delta return (TCon c eparams, Type) -- Data constructor application -- we don't know the expected type, so see if there -- is only one datacon of that name that takes no -- parameters tcTerm t@(DCon c args (Annot Nothing)) Nothing = do matches <- lookupDConAll c case matches of [(tname,(Empty,ConstructorDef _ _ deltai))] -> do let numArgs = teleLength deltai unless (length args == numArgs) $ err [DS "Constructor", DS c, DS "should have", DD numArgs, DS "data arguments, but was given", DD (length args), DS "arguments."] eargs <- tcArgTele args deltai let ty = TCon tname [] return (DCon c eargs (Annot (Just ty)),ty) [_] -> err [DS "Cannot infer the parameters to data constructors.", DS "Add an annotation."] _ -> err [DS "Ambiguous data constructor", DS c] -- we know the expected type of the data constructor -- so look up its type in the context tcTerm t@(DCon c args ann1) ann2 = do ty <- matchAnnots t ann1 ann2 case ty of (TCon tname params) -> do (delta, deltai) <- lookupDCon c tname let numArgs = teleLength deltai unless (length args == numArgs) $ err [DS "Constructor", DS c, DS "should have", DD numArgs, DS "data arguments, but was given", DD (length args), DS "arguments."] newTele <- substTele delta params deltai eargs <- tcArgTele args newTele return (DCon c eargs (Annot (Just ty)), ty) _ -> err [DS "Unexpected type", DD ty, DS "for data constructor", DD t] -- If we are in inference mode, then -- we do not use refinement -- otherwise, we must have a typing annotation tcTerm t@(Case scrut alts ann1) ann2 = do ty <- matchAnnots t ann1 ann2 (ascrut, sty) <- inferType scrut scrut' <- whnf ascrut (n, params) <- ensureTCon sty let checkAlt (Match bnd) = do (pat, body) <- unbind bnd -- add variables from pattern to context -- could fail if branch is in-accessible (decls, evars) <- declarePat pat Runtime (TCon n params) -- add defs to the contents from scrut = pat -- could fail if branch is in-accessible decls' <- equateWithPat scrut' pat (TCon n params) (ebody, _) <- extendCtxs (decls ++ decls') $ checkType body ty -- make sure 'erased' components aren't used when (any (`elem` (toListOf fv (erase ebody))) evars) $ err [DS "Erased variable bound in match used"] return (Match (bind pat ebody)) let pats = map (\(Match bnd) -> fst (unsafeUnbind bnd)) alts aalts <- mapM checkAlt alts exhaustivityCheck scrut' sty pats return (Case ascrut aalts (Annot (Just ty)), ty) tcTerm (TyEq a b) Nothing = do (aa,aTy) <- inferType a (ab,bTy) <- checkType b aTy return (TyEq aa ab, Type) tcTerm t@(Refl ann1) ann2 = do ty <- matchAnnots t ann1 ann2 case ty of (TyEq a b) -> do equate a b return (Refl (Annot (Just ty)), ty) _ -> err [DS "refl annotated with", DD ty] tcTerm t@(Subst tm p ann1) ann2 = do ty <- matchAnnots t ann1 ann2 -- infer the type of the proof p (apf, tp) <- inferType p -- make sure that it is an equality between m and n (m,n) <- ensureTyEq tp -- if either side is a variable, add a definition to the context edecl <- do m' <- whnf m n' <- whnf n case (m',n') of (Var x, _) -> return [Def x n'] (_, Var y) -> return [Def y m'] (_,_) -> return [] pdecl <- do p' <- whnf apf case p' of (Var x) -> return [Def x (Refl (Annot (Just tp)))] _ -> return [] let refined = extendCtxs (edecl ++ pdecl) (atm, _) <- refined $ checkType tm ty return (Subst atm apf (Annot (Just ty)), ty) tcTerm t@(Contra p ann1) ann2 = do ty <- matchAnnots t ann1 ann2 (apf, ty') <- inferType p (a,b) <- ensureTyEq ty' a' <- whnf a b' <- whnf b case (a',b') of (DCon da _ _, DCon db _ _) | da /= db -> return (Contra apf (Annot (Just ty)), ty) (LitBool b1, LitBool b2) | b1 /= b2 -> return (Contra apf (Annot (Just ty)), ty) (_,_) -> err [DS "I can't tell that", DD a, DS "and", DD b, DS "are contradictory"] tcTerm t@(Sigma bnd) Nothing = do ((x,unembed->tyA),tyB) <- unbind bnd aa <- tcType tyA ba <- extendCtx (Sig x aa) $ tcType tyB return (Sigma (bind (x,embed aa) ba), Type) tcTerm t@(Prod a b ann1) ann2 = do ty <- matchAnnots t ann1 ann2 case ty of (Sigma bnd) -> do ((x, unembed-> tyA), tyB) <- unbind bnd (aa,_) <- checkType a tyA (ba,_) <- extendCtxs [Sig x tyA, Def x aa] $ checkType b tyB return (Prod aa ba (Annot (Just ty)), ty) _ -> err [DS "Products must have Sigma Type", DD ty, DS "found instead"] tcTerm t@(Pcase p bnd ann1) ann2 = do ty <- matchAnnots t ann1 ann2 (apr, pty) <- inferType p pty' <- whnf pty case pty' of Sigma bnd' -> do ((x,unembed->tyA),tyB) <- unbind bnd' ((x',y'),body) <- unbind bnd let tyB' = subst x (Var x') tyB nfp <- whnf apr let ctx = case nfp of Var x0 -> [Def x0 (Prod (Var x') (Var y') (Annot (Just pty')))] _ -> [] (abody, bTy) <- extendCtxs ([Sig x' tyA, Sig y' tyB'] ++ ctx) $ checkType body ty return (Pcase apr (bind (x',y') abody) (Annot (Just ty)), bTy) _ -> err [DS "Scrutinee of pcase must have Sigma type"] tcTerm tm (Just ty) = do (atm, ty') <- inferType tm equate ty' ty return (atm, ty) --------------------------------------------------------------------- -- helper functions for type checking -- | Merge together two sources of type information -- The first annotation is assumed to come from an annotation on -- the syntax of the term itself, the second as an argument to -- 'checkType'. matchAnnots :: Term -> Annot -> Maybe Type -> TcMonad Type matchAnnots e (Annot Nothing) Nothing = err [DD e, DS "requires annotation"] matchAnnots e (Annot Nothing) (Just t) = return t matchAnnots e (Annot (Just t)) Nothing = do at <- tcType t return at matchAnnots e (Annot (Just t1)) (Just t2) = do at1 <- tcType t1 equate at1 t2 return at1 -- | Make sure that the term is a type (i.e. has type 'Type') tcType :: Term -> TcMonad Term tcType tm = do (atm, _) <- checkType tm Type return atm --------------------------------------------------------------------- -- helper functions for type constructor creation -- | type check a list of type constructor arguments against a telescope tsTele :: [Term] -> Telescope -> TcMonad [Term] tsTele tms tele = do args <- tcArgTele (map (Arg Runtime) tms) tele return (map unArg args) --------------------------------------------------------------------- -- helper functions for data constructor creation -- | calculate the length of a telescope teleLength :: Telescope -> Int teleLength Empty = 0 teleLength (Constraint _ _ tele) = teleLength tele teleLength (Cons _ _ _ tele) = 1 + teleLength tele -- | type check a list of data constructor arguments against a telescope tcArgTele :: [Arg] -> Telescope -> TcMonad [Arg] tcArgTele [] Empty = return [] tcArgTele args (Constraint tx ty tele) = do equate tx ty tcArgTele args tele tcArgTele (Arg ep1 tm:terms) (Cons ep2 x ty tele') | ep1 == ep2 = do (etm, ety) <- checkType tm ty tele'' <- doSubst [(x,etm)] tele' eterms <- tcArgTele terms tele'' return $ Arg ep1 etm:eterms tcArgTele (Arg ep1 _ : _) (Cons ep2 _ _ _) = err [DD ep1, DS "argument provided when", DD ep2, DS "argument was expected"] tcArgTele [] _ = err [DD "Too few arguments provided."] tcArgTele _ Empty = err [DD "Too many arguments provided."] -- | Substitute a list of terms for the variables bound in a telescope -- This is used to instantiate the parameters of a data constructor -- to find the types of its arguments. -- The first argument should only contain 'Runtime' type declarations. substTele :: Telescope -> [ Term ] -> Telescope -> TcMonad Telescope substTele tele args delta = doSubst (mkSubst tele args) delta where mkSubst Empty [] = [] mkSubst (Cons Runtime x _ tele') (tm : tms) = (x, tm) : mkSubst tele' tms mkSubst _ _ = error "Internal error: substTele given illegal arguments" -- From a constraint, fetch all declarations -- derived from unifying the two terms -- If the terms are not unifiable, throw an error -- Note: we could do better with our unification amb :: Term -> Bool amb (App t1 t2) = True amb (Pi _) = True amb (If _ _ _ _) = True amb (Sigma _) = True amb (Pcase _ _ _ ) = True amb (Let _ ) = True amb (ErasedLam _) = True amb (ErasedPi _) = True amb (ErasedApp _ _) = True amb (Case _ _ _) = True amb _ = False constraintToDecls :: Term -> Term -> TcMonad [Decl] constraintToDecls tx ty = do txnf <- whnf tx tynf <- whnf ty if (aeq txnf tynf) then return [] else case (txnf, tynf) of (Var y, yty) -> return [Def y yty] (yty, Var y) -> return [Def y yty] (TCon s1 tms1, TCon s2 tms2) | s1 == s2 -> matchTerms tms1 tms2 (Prod a1 a2 _, Prod b1 b2 _) -> matchTerms [a1,a2] [b1,b2] (TyEq a1 a2, TyEq b1 b2) -> matchTerms [a1,a2] [b1,b2] (DCon s1 a1s _, DCon s2 a2s _) | s1 == s2 -> matchArgs a1s a2s _ -> if amb txnf || amb tynf then return [] else err [DS "Cannot equate", DD txnf, DS "and", DD tynf] where matchTerms ts1 ts2 = matchArgs (map (Arg Runtime) ts1) (map (Arg Runtime) ts2) matchArgs (Arg _ t1 : a1s) (Arg _ t2 : a2s) = do ds <- constraintToDecls t1 t2 ds' <- matchArgs a1s a2s return $ ds ++ ds' matchArgs [] [] = return [] matchArgs _ _ = err [DS "internal error (constraintToDecls)"] -- Propagate the given substitution through the telescope, potentially -- reworking the constraints. doSubst :: [(TName,Term)] -> Telescope -> TcMonad Telescope doSubst ss Empty = return Empty doSubst ss (Constraint tx ty tele') = do let tx' = substs ss tx let ty' = substs ss ty -- (_decls, tsf) <- match tx' ty' decls <- constraintToDecls tx' ty' tele <- extendCtxs decls $ (doSubst ss tele') return $ (Constraint tx' ty' tele) doSubst ss (Cons ep x ty tele') = do tynf <- whnf (substs ss ty) tele'' <- doSubst ss tele' return $ Cons ep x tynf tele'' ----------------------------------------------------------- -- helper functions for checking pattern matching -- | Create a binding in the context for each of the variables in -- the pattern. -- Also returns the erased variables so that they can be checked declarePat :: Pattern -> Epsilon -> Type -> TcMonad ([Decl], [TName]) declarePat (PatVar x) Runtime y = return ([Sig x y],[]) declarePat (PatVar x) Erased y = return ([Sig x y],[x]) declarePat (PatCon d pats) Runtime (TCon c params) = do (delta, deltai) <- lookupDCon d c tele <- substTele delta params deltai declarePats d pats tele declarePat (PatCon d pats) Erased (TCon c params) = err [DS "Cannot pattern match erased arguments"] declarePat pat ep ty = err [DS "Cannot match pattern", DD pat, DS "with type", DD ty] declarePats :: DCName -> [(Pattern,Epsilon)] -> Telescope -> TcMonad ([Decl],[TName]) declarePats dc [] Empty = return ([],[]) declarePats dc pats (Constraint tx ty tele) = do new_decls <- constraintToDecls tx ty (decls, names) <- extendCtxs new_decls $ declarePats dc pats tele return (new_decls ++ decls, names) declarePats dc ((pat,_):pats) (Cons ep x ty tele) = do (ds1,v1) <- declarePat pat ep ty tm <- pat2Term pat ty (ds2,v2) <- declarePats dc pats (subst x tm tele) return ((ds1 ++ ds2),(v1 ++ v2)) declarePats dc [] _ = err [DS "Not enough patterns in match for data constructor", DD dc] declarePats dc pats Empty = err [DS "Too many patterns in match for data constructor", DD dc] -- | Convert a pattern to an (annotated) term so that we can substitute it for -- variables in telescopes. Because data constructors must be annotated with -- their types, we need to have the expected type of the pattern available. pat2Term :: Pattern -> Type -> TcMonad Term pat2Term (PatCon dc pats) ty@(TCon n params) = do (delta, deltai) <- lookupDCon dc n tele <- substTele delta params deltai args <- pats2Terms pats tele return (DCon dc args (Annot (Just ty))) where pats2Terms :: [(Pattern,Epsilon)] -> Telescope -> TcMonad [Arg] pats2Terms [] Empty = return [] pats2Terms ps (Constraint tx' ty' tele') = do decls <- constraintToDecls tx' ty' extendCtxs decls $ pats2Terms ps tele' pats2Terms ((p,_) : ps) (Cons ep x ty1 d) = do ty' <- whnf ty1 t <- pat2Term p ty' ts <- pats2Terms ps (subst x t d) return (Arg ep t : ts) pats2Terms _ _ = err [DS "Invalid number of args to pattern", DD dc] pat2Term (PatCon _ _) ty = error "Internal error: should be a tcon" pat2Term (PatVar x) ty = return (Var x) -- | Create a list of variable definitions from the scrutinee -- of a case expression and the pattern in a branch. Scrutinees -- that are not variables or constructors applied to vars may not -- produce any equations. equateWithPat :: Term -> Pattern -> Type -> TcMonad [Decl] equateWithPat (Var x) pat ty = do tm <- pat2Term pat ty return [Def x tm] equateWithPat (DCon dc args _) (PatCon dc' pats) (TCon n params) | dc == dc' = do (delta, deltai) <- lookupDCon dc n tele <- substTele delta params deltai let eqWithPats :: [Term] -> [(Pattern,Epsilon)] -> Telescope -> TcMonad [Decl] eqWithPats [] [] Empty = return [] eqWithPats ts ps (Constraint tx ty tl) = do decls <- constraintToDecls tx ty extendCtxs decls $ eqWithPats ts ps tl eqWithPats (t : ts) ((p,_) : ps) (Cons _ x ty tl) = do t' <- whnf t decls <- equateWithPat t' p ty decls' <- eqWithPats ts ps (subst x t' tl) return (decls ++ decls') eqWithPats _ _ _ = err [DS "Invalid number of args to pattern", DD dc] eqWithPats (map unArg args) pats tele equateWithPat (DCon dc args _) (PatCon dc' pats) (TCon n params) = do warn [DS "The case for", DD dc', DS "is unreachable.", DS "However, this implementation cannot yet allow it", DS "to be omitted."] >> return [] equateWithPat _ _ _ = return [] -- | Check all of the types contained within a telescope -- returns a telescope where all of the types have been annotated tcTypeTele :: Telescope -> TcMonad Telescope tcTypeTele Empty = return Empty tcTypeTele (Constraint tm1 tm2 tl) = do (tm1', ty1) <- inferType tm1 (tm2',_) <- checkType tm2 ty1 decls <- constraintToDecls tm1' tm2' tele' <- extendCtxs decls $ tcTypeTele tl return (Constraint tm1' tm2' tele') tcTypeTele (Cons ep x ty tl) = do ty' <- tcType ty tele' <- extendCtx (Sig x ty') $ tcTypeTele tl return (Cons ep x ty' tele') -------------------------------------------------------- -- Using the typechecker for decls and modules and stuff -------------------------------------------------------- -- | Typecheck a collection of modules. Assumes that each module -- appears after its dependencies. Returns the same list of modules -- with each definition typechecked tcModules :: [Module] -> TcMonad [Module] tcModules mods = foldM tcM [] mods -- Check module m against modules in defs, then add m to the list. where defs `tcM` m = do -- "M" is for "Module" not "monad" let name = moduleName m liftIO $ putStrLn $ "Checking module " ++ show name m' <- defs `tcModule` m return $ defs++[m'] -- | Typecheck an entire module. tcModule :: [Module] -- ^ List of already checked modules (including their Decls). -> Module -- ^ Module to check. -> TcMonad Module -- ^ The same module with all Decls checked and elaborated. tcModule defs m' = do checkedEntries <- extendCtxMods importedModules $ foldr tcE (return []) (moduleEntries m') return $ m' { moduleEntries = checkedEntries } where d `tcE` m = do -- Extend the Env per the current Decl before checking -- subsequent Decls. x <- tcEntry d case x of AddHint hint -> extendHints hint m -- Add decls to the Decls to be returned AddCtx decls -> (decls++) <$> (extendCtxsGlobal decls m) -- Get all of the defs from imported modules (this is the env to check current module in) importedModules = filter (\x -> (ModuleImport (moduleName x)) `elem` moduleImports m') defs -- | The Env-delta returned when type-checking a top-level Decl. data HintOrCtx = AddHint Hint | AddCtx [Decl] -- | Check each sort of declaration in a module tcEntry :: Decl -> TcMonad HintOrCtx tcEntry (Def n term) = do oldDef <- lookupDef n case oldDef of Nothing -> tc Just term' -> die term' where tc = do lkup <- lookupHint n case lkup of Nothing -> do (aterm, ty) <- inferType term return $ AddCtx [Sig n ty, Def n aterm] Just ty -> let handler (Err ps msg) = throwError $ Err (ps) (msg $$ msg') msg' = disp [DS "When checking the term ", DD term, DS "against the signature", DD ty] in do (eterm, ety) <- extendCtx (Sig n ty) $ checkType term ty `catchError` handler -- Put the elaborated version of term into the context. if (n `elem` toListOf fv eterm) then return $ AddCtx [Sig n ety, RecDef n eterm] else return $ AddCtx [Sig n ety, Def n eterm] die term' = extendSourceLocation (unPosFlaky term) term $ err [DS "Multiple definitions of", DD n, DS "Previous definition was", DD term'] tcEntry (Sig n ty) = do duplicateTypeBindingCheck n ty ety <- tcType ty return $ AddHint (Hint n ety) -- rule Decl_data tcEntry (Data t delta cs) = do -- Check that the telescope for the datatype definition is well-formed edelta <- tcTypeTele delta ---- check that the telescope provided --- for each data constructor is wellfomed, and elaborate them let elabConstructorDef defn@(ConstructorDef pos d tele) = extendSourceLocation pos defn $ extendCtx (DataSig t edelta) $ extendCtxTele edelta $ do etele <- tcTypeTele tele return (ConstructorDef pos d etele) ecs <- mapM elabConstructorDef cs -- Implicitly, we expect the constructors to actually be different... let cnames = map (\(ConstructorDef _ c _) -> c) cs unless (length cnames == length (nub cnames)) $ err [DS "Datatype definition", DD t, DS "contains duplicated constructors" ] -- finally, add the datatype to the env and perform action m return $ AddCtx [Data t edelta ecs] tcEntry (DataSig _ _ ) = err [DS "internal construct"] tcEntry (RecDef _ _ ) = err [DS "internal construct"] -- | Make sure that we don't have the same name twice in the -- environment. (We don't rename top-level module definitions.) duplicateTypeBindingCheck :: TName -> Term -> TcMonad () duplicateTypeBindingCheck n ty = do -- Look for existing type bindings ... l <- lookupTyMaybe n l' <- lookupHint n -- ... we don't care which, if either are Just. case catMaybes [l,l'] of [] -> return () -- We already have a type in the environment so fail. ty':_ -> let (Pos p _) = ty msg = [DS "Duplicate type signature ", DD ty, DS "for name ", DD n, DS "Previous typing was", DD ty'] in extendSourceLocation p ty $ err msg ----------------------------------------------------------- -- Checking that pattern matching is exhaustive ----------------------------------------------------------- -- | Given a particular type and a list of patterns, make -- sure that the patterns cover all potential cases for that -- type. -- If the list of patterns starts with a variable, then it doesn't -- matter what the type is, the variable is exhaustive. (This code -- does not report unreachable patterns.) -- Otherwise, the scrutinee type must be a type constructor, so the -- code looks up the data constructors for that type and makes sure that -- there are patterns for each one. exhaustivityCheck :: Term -> Type -> [Pattern] -> TcMonad () exhaustivityCheck scrut ty (PatVar x:_) = return () exhaustivityCheck scrut ty pats = do (tcon, tys) <- ensureTCon ty (delta,mdefs) <- lookupTCon tcon case mdefs of Just datacons -> loop pats datacons where loop [] [] = return () loop [] dcons = do l <- checkImpossible dcons if null l then return () else err $ [DS "Missing case for "] ++ map DD l loop ((PatVar x):_) dcons = return () loop ((PatCon dc args):pats') dcons = do (cd@(ConstructorDef _ _ tele, dcons')) <- removeDcon dc dcons tele' <- substTele delta tys tele let (aargs, pats'') = relatedPats dc pats' checkSubPats dc tele' (args:aargs) loop pats'' dcons' -- make sure that the given list of constructors is impossible -- in the current environment checkImpossible :: [ConstructorDef] -> TcMonad [DCName] checkImpossible [] = return [] checkImpossible cd@(ConstructorDef _ dc tele : rest) = do this <- (do tele' <- substTele delta tys tele _ <- tcTypeTele tele' return [dc]) `catchError` (\_ -> return []) others <- checkImpossible rest return (this ++ others) Nothing -> err [DS "Cannot determine constructors of", DD ty] -- this could be because the scrutinee is not unifiable with the pattern -- or because the constraints on the pattern are not satisfiable -- | Given a particular data constructor name and a list of data -- constructor definitions, pull the definition out of the list and -- return it paired with the remainder of the list. removeDcon :: DCName -> [ConstructorDef] -> TcMonad (ConstructorDef, [ConstructorDef]) removeDcon dc (cd@(ConstructorDef _ dc' _):rest) | dc == dc' = return (cd, rest) removeDcon dc (cd1:rest) = do (cd2, rr) <- removeDcon dc rest return (cd2, cd1:rr) removeDcon dc [] = err [DS $ "Internal error: Can't find" ++ show dc] -- | Given a particular data constructor name and a list of patterns, -- pull out the subpatterns that occur as arguments to that data -- constructor and return them paired with the remaining patterns. relatedPats :: DCName -> [Pattern] -> ([[(Pattern,Epsilon)]], [Pattern]) relatedPats dc [] = ([],[]) relatedPats dc ((PatCon dc' args):pats) | dc == dc' = let (aargs, rest) = relatedPats dc pats in (args:aargs, rest) relatedPats dc (pc@(PatCon _ _):pats) = let (aargs, rest) = relatedPats dc pats in (aargs, pc:rest) relatedPats dc (pc@(PatVar _):pats) = ([], pc:pats) -- | Occurs check for the subpatterns of a data constructor. Given -- the telescope specifying the types of the arguments, plus the -- subpatterns identified by relatedPats, check that they are each -- exhaustive. -- for simplicity, this function requires that all subpatterns -- are pattern variables. checkSubPats :: DCName -> Telescope -> [[(Pattern,Epsilon)]] -> TcMonad () checkSubPats dc Empty _ = return () checkSubPats dc (Constraint _ _ tele) patss = checkSubPats dc tele patss checkSubPats dc (Cons _ name tyP tele) patss | length patss > 0 && (all ((> 0) . length) patss) = do let hds = map (fst . head) patss let tls = map tail patss case hds of (PatVar _ : []) -> checkSubPats dc tele tls _ -> err [DS "All subpatterns must be variables in this version."] checkSubPats dc t ps = err [DS "Internal error in checkSubPats", DD dc, DD t, DS (show ps)]