Commit 0763bae0 authored by Björn Peemöller 's avatar Björn Peemöller
Browse files

Checks improved

parent 6bef7507
...@@ -13,8 +13,9 @@ ...@@ -13,8 +13,9 @@
-} -}
module Checks where module Checks where
import Curry.Base.MessageMonad (Message) import Curry.Syntax (Module (..))
import Curry.Syntax
import Base.Messages
import qualified Checks.KindCheck as KC (kindCheck) import qualified Checks.KindCheck as KC (kindCheck)
import qualified Checks.PrecCheck as PC (precCheck) import qualified Checks.PrecCheck as PC (precCheck)
...@@ -25,36 +26,51 @@ import qualified Checks.WarnCheck as WC (warnCheck) ...@@ -25,36 +26,51 @@ import qualified Checks.WarnCheck as WC (warnCheck)
import CompilerEnv import CompilerEnv
import CompilerOpts import CompilerOpts
data CheckStatus a
= CheckFailed [Message]
| CheckSuccess a
instance Monad CheckStatus where
return = CheckSuccess
m >>= f = case m of
CheckFailed errs -> CheckFailed errs
CheckSuccess a -> f a
-- TODO: More documentation -- TODO: More documentation
-- |Check the kinds of type definitions and signatures. -- |Check the kinds of type definitions and signatures.
-- In addition, nullary type constructors and type variables are dinstiguished -- In addition, nullary type constructors and type variables are dinstiguished
kindCheck :: Module -> CompilerEnv -> (Module, CompilerEnv) kindCheck :: CompilerEnv -> Module -> (CompilerEnv, Module)
kindCheck (Module m es is ds) env = (Module m es is ds', env) kindCheck env (Module m es is ds)
where ds' = KC.kindCheck (moduleIdent env) (tyConsEnv env) ds | null msgs = (env, Module m es is ds')
| otherwise = errorMessages msgs
where (ds', msgs) = KC.kindCheck (moduleIdent env) (tyConsEnv env) ds
-- |Apply the precendences of infix operators. -- |Apply the precendences of infix operators.
-- This function reanrranges the AST. -- This function reanrranges the AST.
precCheck :: Module -> CompilerEnv -> (Module, CompilerEnv) precCheck :: CompilerEnv -> Module -> (CompilerEnv, Module)
precCheck (Module m es is ds) env = (Module m es is ds', env { opPrecEnv = pEnv' }) precCheck env (Module m es is ds)
where (pEnv', ds') = PC.precCheck (moduleIdent env) (opPrecEnv env) ds | null msgs = (env { opPrecEnv = pEnv' }, Module m es is ds')
| otherwise = errorMessages msgs
where (ds', pEnv', msgs) = PC.precCheck (moduleIdent env) (opPrecEnv env) ds
-- |Apply the syntax check. -- |Apply the syntax check.
syntaxCheck :: Options -> Module -> CompilerEnv -> (Module, CompilerEnv) syntaxCheck :: Options -> CompilerEnv -> Module -> (CompilerEnv, Module)
syntaxCheck opts (Module m es is ds) env = (Module m es is ds', env) syntaxCheck opts env (Module m es is ds)
where ds' = SC.syntaxCheck withExt (moduleIdent env) (aliasEnv env) | null msgs = (env, Module m es is ds')
| otherwise = errorMessages msgs
where (ds', msgs) = SC.syntaxCheck opts (moduleIdent env) (aliasEnv env)
(arityEnv env) (valueEnv env) (tyConsEnv env) ds (arityEnv env) (valueEnv env) (tyConsEnv env) ds
withExt = BerndExtension `elem` optExtensions opts
-- |Apply the type check. -- |Apply the type check.
typeCheck :: Module -> CompilerEnv -> (Module, CompilerEnv) typeCheck :: CompilerEnv -> Module -> (CompilerEnv, Module)
typeCheck mdl@(Module _ _ _ ds) env = (mdl, env { tyConsEnv = tcEnv', valueEnv = tyEnv' }) typeCheck env mdl@(Module _ _ _ ds) = (env { tyConsEnv = tcEnv', valueEnv = tyEnv' }, mdl)
where (tcEnv', tyEnv') = TC.typeCheck (moduleIdent env) where (tcEnv', tyEnv') = TC.typeCheck (moduleIdent env)
(tyConsEnv env) (valueEnv env) ds (tyConsEnv env) (valueEnv env) ds
-- TODO: Which kind of warnings? -- TODO: Which kind of warnings?
-- |Check for warnings. -- |Check for warnings.
warnCheck :: Module -> CompilerEnv -> [Message] warnCheck :: CompilerEnv -> Module -> [Message]
warnCheck (Module _ _ is ds) env warnCheck env (Module _ _ is ds)
= WC.warnCheck (moduleIdent env) (valueEnv env) is ds = WC.warnCheck (moduleIdent env) (valueEnv env) is ds
...@@ -4,6 +4,7 @@ ...@@ -4,6 +4,7 @@
% See LICENSE for the full license. % See LICENSE for the full license.
% %
% Modified by Martin Engelke (men@informatik.uni-kiel.de) % Modified by Martin Engelke (men@informatik.uni-kiel.de)
% Modified by Björn Peemöller (bjp@informatik.uni-kiel.de)
% %
\nwfilename{KindCheck.lhs} \nwfilename{KindCheck.lhs}
\section{Checking Type Definitions} \section{Checking Type Definitions}
...@@ -14,7 +15,7 @@ type classes, kind checking is rather trivial. All types must be of ...@@ -14,7 +15,7 @@ type classes, kind checking is rather trivial. All types must be of
first order kind ($\star$), i.e., all type constructor applications first order kind ($\star$), i.e., all type constructor applications
must be saturated. must be saturated.
During kind checking, this module will also disambiguate nullary During kind checking, this module will also disambiguate nullary type
constructors and type variables which -- in contrast to Haskell -- is constructors and type variables which -- in contrast to Haskell -- is
not possible on purely syntactic criteria. In addition it is checked not possible on purely syntactic criteria. In addition it is checked
that all type constructors and type variables occurring on the right that all type constructors and type variables occurring on the right
...@@ -24,17 +25,17 @@ is defined more than once. ...@@ -24,17 +25,17 @@ is defined more than once.
> module Checks.KindCheck (kindCheck) where > module Checks.KindCheck (kindCheck) where
> import Control.Monad.State > import Control.Monad (forM, liftM, liftM2, liftM3, when)
> import qualified Control.Monad.State as S (State, runState, gets, modify)
> import Curry.Base.Position > import Curry.Base.Position
> import Curry.Base.Ident > import Curry.Base.Ident
> import Curry.Base.MessageMonad (Message (..), showError)
> import Curry.Syntax > import Curry.Syntax
> import Base.Messages (errorAt', internalError) > import Base.Messages (Message, posErr, qposErr, internalError)
> import Base.Utils (findDouble) > import Base.TopEnv
> import Base.Utils (findMultiples)
> import Env.TopEnv
> import Env.TypeConstructors (TCEnv, tcArity) > import Env.TypeConstructors (TCEnv, tcArity)
\end{verbatim} \end{verbatim}
...@@ -47,32 +48,37 @@ defined type constructors are inserted into the environment, and, ...@@ -47,32 +48,37 @@ defined type constructors are inserted into the environment, and,
finally, the declarations are checked within this environment. finally, the declarations are checked within this environment.
\begin{verbatim} \begin{verbatim}
TODO: Propagate errors > kindCheck :: ModuleIdent -> TCEnv -> [Decl] -> ([Decl], [Message])
> kindCheck m tcEnv decls = case findMultiples $ map typeConstr tds of
> [] -> runKCM (mapM checkDecl decls) initState
> ms -> (decls, map errMultipleDeclaration ms)
> where tds = filter isTypeDecl decls
> kEnv = foldr (bindKind m) (fmap tcArity tcEnv) tds
> initState = KCState m kEnv []
> kindCheck :: ModuleIdent -> TCEnv -> [Decl] -> [Decl] \end{verbatim}
> kindCheck m tcEnv decls = case findDouble $ map typeConstr typeDecls of The kind check monad.
> Just tc -> errorAt' $ errDuplicateType tc \begin{verbatim}
> Nothing -> case errors s' of
> [] -> decls'
> errs -> errorAt' $ last errs
> where typeDecls = filter isTypeDecl decls
> kEnv = foldr (bindKind m) (fmap tcArity tcEnv) typeDecls
> initState = CheckState m kEnv []
> (decls',s') = runKcM (mapM checkDecl decls) initState
> data CheckState = CheckState > data KCState = KCState
> { moduleIdent :: ModuleIdent > { moduleIdent :: ModuleIdent
> , kindEnv :: KindEnv > , kindEnv :: KindEnv
> , errors :: [(Position, String)] > , errors :: [Message]
> } > }
> type KcM = State CheckState > type KCM = S.State KCState -- the Kind Check Monad
> runKCM :: KCM a -> KCState -> (a, [Message])
> runKCM kcm s = let (a, s') = S.runState kcm s in (a, reverse $ errors s')
> getModuleIdent :: KCM ModuleIdent
> getModuleIdent = S.gets moduleIdent
> runKcM :: KcM a -> CheckState -> (a, CheckState) > getKindEnv :: KCM KindEnv
> runKcM = runState > getKindEnv = S.gets kindEnv
> reportError :: (Position, String) -> KcM () > report :: Message -> KCM ()
> reportError err = modify (\ s -> s { errors = err : errors s }) > report err = S.modify (\ s -> s { errors = err : errors s })
\end{verbatim} \end{verbatim}
The kind environment only needs to record the arity of each type constructor. The kind environment only needs to record the arity of each type constructor.
...@@ -87,10 +93,10 @@ The kind environment only needs to record the arity of each type constructor. ...@@ -87,10 +93,10 @@ The kind environment only needs to record the arity of each type constructor.
> bindKind _ _ = id > bindKind _ _ = id
> bindKind' :: ModuleIdent -> Ident -> [Ident] -> KindEnv -> KindEnv > bindKind' :: ModuleIdent -> Ident -> [Ident] -> KindEnv -> KindEnv
> bindKind' m tc tvs = bindTopEnv "KindCheck.bindKind'" tc n > bindKind' m tc tvs = bindTopEnv "KindCheck.bindKind'" tc arity
> . qualBindTopEnv "KindCheck.bindKind'" qtc n > . qualBindTopEnv "KindCheck.bindKind'" qtc arity
> where n = length tvs > where arity = length tvs
> qtc = qualifyWith m tc > qtc = qualifyWith m tc
> lookupKind :: Ident -> KindEnv -> [Int] > lookupKind :: Ident -> KindEnv -> [Int]
> lookupKind = lookupTopEnv > lookupKind = lookupTopEnv
...@@ -105,7 +111,7 @@ the right hand side. Function and pattern declarations must be ...@@ -105,7 +111,7 @@ the right hand side. Function and pattern declarations must be
traversed because they can contain local type signatures. traversed because they can contain local type signatures.
\begin{verbatim} \begin{verbatim}
> checkDecl :: Decl -> KcM Decl > checkDecl :: Decl -> KCM Decl
> checkDecl (DataDecl p tc tvs cs) = do > checkDecl (DataDecl p tc tvs cs) = do
> tvs' <- checkTypeLhs tvs > tvs' <- checkTypeLhs tvs
> cs' <- mapM (checkConstrDecl tvs') cs > cs' <- mapM (checkConstrDecl tvs') cs
...@@ -118,21 +124,17 @@ traversed because they can contain local type signatures. ...@@ -118,21 +124,17 @@ traversed because they can contain local type signatures.
> tvs' <- checkTypeLhs tvs > tvs' <- checkTypeLhs tvs
> ty' <- checkClosedType tvs' ty > ty' <- checkClosedType tvs' ty
> return $ TypeDecl p tc tvs' ty' > return $ TypeDecl p tc tvs' ty'
> checkDecl (TypeSig p vs ty) = do > checkDecl (TypeSig p vs ty) =
> ty' <- checkType ty > TypeSig p vs `liftM` checkType ty
> return $ TypeSig p vs ty' > checkDecl (FunctionDecl p f eqs) =
> checkDecl (FunctionDecl p f eqs) = do > FunctionDecl p f `liftM` mapM checkEquation eqs
> eqs' <- mapM checkEquation eqs > checkDecl (PatternDecl p t rhs) =
> return $ FunctionDecl p f eqs' > PatternDecl p t `liftM` checkRhs rhs
> checkDecl (PatternDecl p t rhs) = do > checkDecl (ExternalDecl p cc ie f ty) =
> rhs' <- checkRhs rhs > ExternalDecl p cc ie f `liftM` checkType ty
> return $ PatternDecl p t rhs'
> checkDecl (ExternalDecl p cc ie f ty) = do
> ty' <- checkType ty
> return $ ExternalDecl p cc ie f ty'
> checkDecl d = return d > checkDecl d = return d
> checkConstrDecl :: [Ident] -> ConstrDecl -> KcM ConstrDecl > checkConstrDecl :: [Ident] -> ConstrDecl -> KCM ConstrDecl
> checkConstrDecl tvs (ConstrDecl p evs c tys) = do > checkConstrDecl tvs (ConstrDecl p evs c tys) = do
> evs' <- checkTypeLhs evs > evs' <- checkTypeLhs evs
> tys' <- mapM (checkClosedType (evs' ++ tvs)) tys > tys' <- mapM (checkClosedType (evs' ++ tvs)) tys
...@@ -144,7 +146,7 @@ traversed because they can contain local type signatures. ...@@ -144,7 +146,7 @@ traversed because they can contain local type signatures.
> ty2' <- checkClosedType tvs' ty2 > ty2' <- checkClosedType tvs' ty2
> return $ ConOpDecl p evs' ty1' op ty2' > return $ ConOpDecl p evs' ty1' op ty2'
> checkNewConstrDecl :: [Ident] -> NewConstrDecl -> KcM NewConstrDecl > checkNewConstrDecl :: [Ident] -> NewConstrDecl -> KCM NewConstrDecl
> checkNewConstrDecl tvs (NewConstrDecl p evs c ty) = do > checkNewConstrDecl tvs (NewConstrDecl p evs c ty) = do
> evs' <- checkTypeLhs evs > evs' <- checkTypeLhs evs
> ty' <- checkClosedType (evs' ++ tvs) ty > ty' <- checkClosedType (evs' ++ tvs) ty
...@@ -154,15 +156,14 @@ traversed because they can contain local type signatures. ...@@ -154,15 +156,14 @@ traversed because they can contain local type signatures.
> -- * Anonymous type variables are allowed > -- * Anonymous type variables are allowed
> -- * only type variables (no type constructors) > -- * only type variables (no type constructors)
> -- * linearity > -- * linearity
> checkTypeLhs :: [Ident] -> KcM [Ident] > checkTypeLhs :: [Ident] -> KCM [Ident]
> checkTypeLhs [] = return [] > checkTypeLhs [] = return []
> checkTypeLhs (tv : tvs) = do > checkTypeLhs (tv : tvs) = do
> when (tv /= anonId) $ do > when (tv /= anonId) $ do
> isTyCons <- gets (not . null . lookupKind tv . kindEnv) > isTyCons <- (not . null . lookupKind tv) `liftM` getKindEnv
> when isTyCons $ reportError $ errNoVariable tv > when isTyCons $ report $ errNoVariable tv
> when (tv `elem` tvs) $ reportError $ errNonLinear tv > when (tv `elem` tvs) $ report $ errNonLinear tv
> tvs' <- checkTypeLhs tvs > (tv :) `liftM` checkTypeLhs tvs
> return $ tv : tvs'
\end{verbatim} \end{verbatim}
Checking expressions is rather straight forward. The compiler must Checking expressions is rather straight forward. The compiler must
...@@ -170,132 +171,68 @@ only traverse the structure of expressions in order to find local ...@@ -170,132 +171,68 @@ only traverse the structure of expressions in order to find local
declaration groups. declaration groups.
\begin{verbatim} \begin{verbatim}
> checkEquation :: Equation -> KcM Equation > checkEquation :: Equation -> KCM Equation
> checkEquation (Equation p lhs rhs) = do > checkEquation (Equation p lhs rhs) = Equation p lhs `liftM` checkRhs rhs
> rhs' <- checkRhs rhs
> return $ Equation p lhs rhs' > checkRhs :: Rhs -> KCM Rhs
> checkRhs (SimpleRhs p e ds) =
> checkRhs :: Rhs -> KcM Rhs > liftM2 (SimpleRhs p) (checkExpr e) (mapM checkDecl ds)
> checkRhs (SimpleRhs p e ds) = do > checkRhs (GuardedRhs es ds) =
> e' <- checkExpr e > liftM2 GuardedRhs (mapM checkCondExpr es) (mapM checkDecl ds)
> ds' <- mapM checkDecl ds
> return $ SimpleRhs p e' ds' > checkCondExpr :: CondExpr -> KCM CondExpr
> checkRhs (GuardedRhs es ds) = do > checkCondExpr (CondExpr p g e) =
> es' <- mapM checkCondExpr es > liftM2 (CondExpr p) (checkExpr g) (checkExpr e)
> ds' <- mapM checkDecl ds
> return $ GuardedRhs es' ds' > checkExpr :: Expression -> KCM Expression
> checkExpr l@(Literal _) = return l
> checkCondExpr :: CondExpr -> KcM CondExpr > checkExpr v@(Variable _) = return v
> checkCondExpr (CondExpr p g e) = do > checkExpr c@(Constructor _) = return c
> g' <- checkExpr g > checkExpr (Paren e) = Paren `liftM` checkExpr e
> e' <- checkExpr e > checkExpr (Typed e ty) = liftM2 Typed (checkExpr e) (checkType ty)
> return $ CondExpr p g' e' > checkExpr (Tuple p es) = Tuple p `liftM` mapM checkExpr es
> checkExpr (List p es) = List p `liftM` mapM checkExpr es
> checkExpr :: Expression -> KcM Expression > checkExpr (ListCompr p e qs) =
> checkExpr (Literal l) = return $ Literal l > liftM2 (ListCompr p) (checkExpr e) (mapM checkStmt qs)
> checkExpr (Variable v) = return $ Variable v > checkExpr (EnumFrom e) = EnumFrom `liftM` checkExpr e
> checkExpr (Constructor c) = return $ Constructor c > checkExpr (EnumFromThen e1 e2) =
> checkExpr (Paren e) = do > liftM2 EnumFromThen (checkExpr e1) (checkExpr e2)
> e' <- checkExpr e > checkExpr (EnumFromTo e1 e2) =
> return $ Paren e' > liftM2 EnumFromTo (checkExpr e1) (checkExpr e2)
> checkExpr (Typed e ty) = do > checkExpr (EnumFromThenTo e1 e2 e3) =
> e' <- checkExpr e > liftM3 EnumFromThenTo (checkExpr e1) (checkExpr e2) (checkExpr e3)
> ty' <- checkType ty > checkExpr (UnaryMinus op e) = UnaryMinus op `liftM` checkExpr e
> return $ Typed e' ty' > checkExpr (Apply e1 e2) = liftM2 Apply (checkExpr e1) (checkExpr e2)
> checkExpr (Tuple p es) = do > checkExpr (InfixApply e1 op e2) =
> es' <- mapM checkExpr es > liftM2 (\f1 f2 -> InfixApply f1 op f2) (checkExpr e1) (checkExpr e2)
> return $ Tuple p es' > checkExpr (LeftSection e op) = flip LeftSection op `liftM` checkExpr e
> checkExpr (List p es) = do > checkExpr (RightSection op e) = RightSection op `liftM` checkExpr e
> es' <- mapM checkExpr es > checkExpr (Lambda r ts e) = Lambda r ts `liftM` checkExpr e
> return $ List p es' > checkExpr (Let ds e) =
> checkExpr (ListCompr p e qs) = do > liftM2 Let (mapM checkDecl ds) (checkExpr e)
> e' <- checkExpr e > checkExpr (Do sts e) =
> qs' <- mapM checkStmt qs > liftM2 Do (mapM checkStmt sts) (checkExpr e)
> return $ ListCompr p e' qs' > checkExpr (IfThenElse r e1 e2 e3) =
> checkExpr (EnumFrom e) = do > liftM3 (IfThenElse r) (checkExpr e1) (checkExpr e2) (checkExpr e3)
> e' <- checkExpr e > checkExpr (Case r e alts) =
> return $ EnumFrom e' > liftM2 (Case r) (checkExpr e) (mapM checkAlt alts)
> checkExpr (EnumFromThen e1 e2) = do > checkExpr (RecordConstr fs) =
> e1' <- checkExpr e1 > RecordConstr `liftM` mapM checkFieldExpr fs
> e2' <- checkExpr e2 > checkExpr (RecordSelection e l) =
> return $ EnumFromThen e1' e2' > flip RecordSelection l `liftM` checkExpr e
> checkExpr (EnumFromTo e1 e2) = do > checkExpr (RecordUpdate fs e) =
> e1' <- checkExpr e1 > liftM2 RecordUpdate (mapM checkFieldExpr fs) (checkExpr e)
> e2' <- checkExpr e2
> return $ EnumFromTo e1' e2' > checkStmt :: Statement -> KCM Statement
> checkExpr (EnumFromThenTo e1 e2 e3) = do > checkStmt (StmtExpr p e) = StmtExpr p `liftM` checkExpr e
> e1' <- checkExpr e1 > checkStmt (StmtBind p t e) = StmtBind p t `liftM` checkExpr e
> e2' <- checkExpr e2 > checkStmt (StmtDecl ds) = StmtDecl `liftM` mapM checkDecl ds
> e3' <- checkExpr e3
> return $ EnumFromThenTo e1' e2' e3' > checkAlt :: Alt -> KCM Alt
> checkExpr (UnaryMinus op e) = do > checkAlt (Alt p t rhs) = Alt p t `liftM` checkRhs rhs
> e' <- checkExpr e
> return $ UnaryMinus op e' > checkFieldExpr :: Field Expression -> KCM (Field Expression)
> checkExpr (Apply e1 e2) = do > checkFieldExpr (Field p l e) = Field p l `liftM` checkExpr e
> e1' <- checkExpr e1
> e2' <- checkExpr e2
> return $ Apply e1' e2'
> checkExpr (InfixApply e1 op e2) = do
> e1' <- checkExpr e1
> e2' <- checkExpr e2
> return $ InfixApply e1' op e2'
> checkExpr (LeftSection e op) = do
> e' <- checkExpr e
> return $ LeftSection e' op
> checkExpr (RightSection op e) = do
> e' <- checkExpr e
> return $ RightSection op e'
> checkExpr (Lambda r ts e) = do
> e' <- checkExpr e
> return $ Lambda r ts e'
> checkExpr (Let ds e) = do
> ds' <- mapM checkDecl ds
> e' <- checkExpr e
> return $ Let ds' e'
> checkExpr (Do sts e) = do
> sts' <- mapM checkStmt sts
> e' <- checkExpr e
> return $ Do sts' e'
> checkExpr (IfThenElse r e1 e2 e3) = do
> e1' <- checkExpr e1
> e2' <- checkExpr e2
> e3' <- checkExpr e3
> return $ IfThenElse r e1' e2' e3'
> checkExpr (Case r e alts) = do
> e' <- checkExpr e
> alts' <- mapM checkAlt alts
> return $ Case r e' alts'
> checkExpr (RecordConstr fs) = do
> fs' <- mapM checkFieldExpr fs
> return $ RecordConstr fs'
> checkExpr (RecordSelection e l) = do
> e' <- checkExpr e
> return $ RecordSelection e' l
> checkExpr (RecordUpdate fs e) = do
> fs' <- mapM checkFieldExpr fs
> e' <- checkExpr e
> return $ RecordUpdate fs' e'
> checkStmt :: Statement -> KcM Statement
> checkStmt (StmtExpr p e) = do
> e' <- checkExpr e
> return $ StmtExpr p e'
> checkStmt (StmtBind p t e) = do
> e' <- checkExpr e
> return $ StmtBind p t e'
> checkStmt (StmtDecl ds) = do
> ds' <- mapM checkDecl ds
> return $ StmtDecl ds'
> checkAlt :: Alt -> KcM Alt
> checkAlt (Alt p t rhs) = do
> rhs' <- checkRhs rhs
> return $ Alt p t rhs'
> checkFieldExpr :: Field Expression -> KcM (Field Expression)
> checkFieldExpr (Field p l e) = do
> e' <- checkExpr e
> return $ Field p l e'
\end{verbatim} \end{verbatim}
The parser cannot distinguish unqualified nullary type constructors The parser cannot distinguish unqualified nullary type constructors
...@@ -304,69 +241,59 @@ identifier in a position where a type variable is admissible, it will ...@@ -304,69 +241,59 @@ identifier in a position where a type variable is admissible, it will
interpret the identifier as such. interpret the identifier as such.
\begin{verbatim} \begin{verbatim}
> checkClosedType :: [Ident] -> TypeExpr -> KcM TypeExpr > checkClosedType :: [Ident] -> TypeExpr -> KCM TypeExpr
> checkClosedType tvs ty = checkType ty >>= checkClosed tvs > checkClosedType tvs ty = checkType ty >>= checkClosed tvs
> checkType :: TypeExpr -> KcM TypeExpr > checkType :: TypeExpr -> KCM TypeExpr
> checkType c@(ConstructorType tc tys) = do > checkType c@(ConstructorType tc tys) = do
> m <- gets moduleIdent > m <- getModuleIdent
> kEnv <- gets kindEnv > kEnv <- getKindEnv
> case qualLookupKind tc kEnv of > case qualLookupKind tc kEnv of
> [] > []
> | not (isQualified tc) && null tys -> return $ VariableType $ unqualify tc > | not (isQualified tc) && null tys ->
> | otherwise -> reportError (errUndefinedType tc) >> return c > return $ VariableType $ unqualify tc
> | otherwise -> report (errUndefinedType tc) >> return c
> [n] > [n]
> | n == n' -> do > | n == n' -> ConstructorType tc `liftM` mapM checkType tys
> tys' <- mapM checkType tys > | otherwise -> report (errWrongArity tc n n') >> return c
> return $ ConstructorType tc tys'
> | otherwise -> reportError (errWrongArity tc n n') >> return c
> _ -> case qualLookupKind (qualQualify m tc) kEnv of > _ -> case qualLookupKind (qualQualify m tc) kEnv of
> [n] > [n]
> | n == n' -> do > | n == n' -> ConstructorType tc `liftM` mapM checkType tys
> tys' <- mapM checkType tys > | otherwise -> report (errWrongArity tc n n') >> return c
> return $ ConstructorType tc tys' > _ -> report (errAmbiguousType tc) >> return c
> | otherwise -> reportError (errWrongArity tc n n') >> return c
> _ -> reportError (errAmbiguousType tc) >> return c
> where n' = length tys > where n' = length tys
> checkType (VariableType tv) > checkType v@(VariableType tv)
> | tv == anonId = return $ VariableType tv > | tv == anonId = return v
> | otherwise = checkType (ConstructorType (qualify tv) []) > | otherwise = checkType $ ConstructorType (qualify tv) []
> checkType (TupleType tys) = do > checkType (TupleType tys) = TupleType `liftM` mapM checkType tys
> tys' <- mapM checkType tys > checkType (ListType ty) = ListType `liftM` checkType ty
> return $ TupleType tys' > checkType (ArrowType ty1 ty2) =
> checkType (ListType ty) = do > liftM2 ArrowType (checkType ty1) (checkType ty2)
> ty' <- checkType ty > checkType (RecordType fs r) = do
> return $ ListType ty' > fs' <- forM fs $ \ (l, ty) -> do
> checkType (ArrowType ty1 ty2) = do > ty' <- checkType ty
> ty1' <- checkType ty1 > return (l, ty')
> ty2' <- checkType ty2
> return $ ArrowType ty1' ty2'
> checkType (RecordType fs r) = do
> fs' <- mapM (\ (l, ty) -> do { ty' <- checkType ty; return (l, ty') }) fs
> r' <- case r of > r' <- case r of
> Nothing -> return Nothing > Nothing -> return Nothing