{-# LANGUAGE CPP #-}
module Checks.TypeSyntaxCheck (typeSyntaxCheck) where
#if __GLASGOW_HASKELL__ < 710
import Control.Applicative ((<$>), (<*>), pure)
#endif
import Control.Monad (unless, when)
import qualified Control.Monad.State as S (State, runState, gets, modify)
import Data.List (nub)
import Data.Maybe (isNothing)
import Curry.Base.Ident
import Curry.Base.Position
import Curry.Base.SpanInfo
import Curry.Base.Pretty
import Curry.Syntax
import Curry.Syntax.Pretty
import Base.Expr (Expr (fv))
import Base.Messages (Message, spanInfoMessage, internalError)
import Base.TopEnv
import Base.Utils (findMultiples, findDouble)
import Env.TypeConstructor (TCEnv)
import Env.Type
typeSyntaxCheck :: TCEnv -> Module a -> (Module a, [Message])
typeSyntaxCheck tcEnv mdl@(Module _ _ _ m _ _ ds) =
case findMultiples $ map getIdent tcds of
[] -> if length dfds <= 1
then runTSCM (checkModule mdl) state
else (mdl, [errMultipleDefaultDeclarations dfps])
tss -> (mdl, map errMultipleDeclarations tss)
where
tcds = filter isTypeOrClassDecl ds
dfds = filter isDefaultDecl ds
dfps = map (\(DefaultDecl p _) -> p) dfds
tEnv = foldr (bindType m) (fmap toTypeKind tcEnv) tcds
state = TSCState m tEnv 1 []
type TSCM = S.State TSCState
data TSCState = TSCState
{ moduleIdent :: ModuleIdent
, typeEnv :: TypeEnv
, nextId :: Integer
, errors :: [Message]
}
runTSCM :: TSCM a -> TSCState -> (a, [Message])
runTSCM tscm s = let (a, s') = S.runState tscm s in (a, reverse $ errors s')
getModuleIdent :: TSCM ModuleIdent
getModuleIdent = S.gets moduleIdent
getTypeEnv :: TSCM TypeEnv
getTypeEnv = S.gets typeEnv
newId :: TSCM Integer
newId = do
curId <- S.gets nextId
S.modify $ \s -> s { nextId = succ curId }
return curId
report :: Message -> TSCM ()
report err = S.modify (\s -> s { errors = err : errors s })
ok :: TSCM ()
ok = return ()
bindType :: ModuleIdent -> Decl a -> TypeEnv -> TypeEnv
bindType m (DataDecl _ tc _ cs _) = bindTypeKind m tc (Data qtc ids)
where
qtc = qualifyWith m tc
ids = map constrId cs ++ nub (concatMap recordLabels cs)
bindType m (ExternalDataDecl _ tc _) = bindTypeKind m tc (Data qtc [])
where
qtc = qualifyWith m tc
bindType m (NewtypeDecl _ tc _ nc _) = bindTypeKind m tc (Data qtc ids)
where
qtc = qualifyWith m tc
ids = nconstrId nc : nrecordLabels nc
bindType m (TypeDecl _ tc _ _) = bindTypeKind m tc (Alias qtc)
where
qtc = qualifyWith m tc
bindType m (ClassDecl _ _ _ cls _ ds) = bindTypeKind m cls (Class qcls ms)
where
qcls = qualifyWith m cls
ms = concatMap methods ds
bindType _ _ = id
checkModule :: Module a -> TSCM (Module a)
checkModule (Module spi li ps m es is ds) = do
ds' <- mapM checkDecl ds
return $ Module spi li ps m es is ds'
checkDecl :: Decl a -> TSCM (Decl a)
checkDecl (DataDecl p tc tvs cs clss) = do
checkTypeLhs tvs
cs' <- mapM (checkConstrDecl tvs) cs
mapM_ (checkClass False) clss
return $ DataDecl p tc tvs cs' clss
checkDecl (NewtypeDecl p tc tvs nc clss) = do
checkTypeLhs tvs
nc' <- checkNewConstrDecl tvs nc
mapM_ (checkClass False) clss
return $ NewtypeDecl p tc tvs nc' clss
checkDecl (TypeDecl p tc tvs ty) = do
checkTypeLhs tvs
ty' <- checkClosedType tvs ty
return $ TypeDecl p tc tvs ty'
checkDecl (TypeSig p vs qty) =
TypeSig p vs <$> checkQualType qty
checkDecl (FunctionDecl a p f eqs) = FunctionDecl a p f <$>
mapM checkEquation eqs
checkDecl (PatternDecl p t rhs) = PatternDecl p t <$> checkRhs rhs
checkDecl (DefaultDecl p tys) = DefaultDecl p <$>
mapM (checkClosedType []) tys
checkDecl (ClassDecl p li cx cls clsvar ds) = do
checkTypeVars "class declaration" [clsvar]
cx' <- checkClosedContext [clsvar] cx
checkSimpleContext cx'
ds' <- mapM checkDecl ds
mapM_ (checkClassMethod clsvar) ds'
return $ ClassDecl p li cx' cls clsvar ds'
checkDecl (InstanceDecl p li cx qcls inst ds) = do
checkClass True qcls
QualTypeExpr _ cx' inst' <- checkQualType $ QualTypeExpr NoSpanInfo cx inst
checkSimpleContext cx'
checkInstanceType p inst'
InstanceDecl p li cx' qcls inst' <$> mapM checkDecl ds
checkDecl d = return d
checkConstrDecl :: [Ident] -> ConstrDecl -> TSCM ConstrDecl
checkConstrDecl tvs (ConstrDecl p c tys) = do
tys' <- mapM (checkClosedType tvs) tys
return $ ConstrDecl p c tys'
checkConstrDecl tvs (ConOpDecl p ty1 op ty2) = do
tys' <- mapM (checkClosedType tvs) [ty1, ty2]
let [ty1', ty2'] = tys'
return $ ConOpDecl p ty1' op ty2'
checkConstrDecl tvs (RecordDecl p c fs) = do
fs' <- mapM (checkFieldDecl tvs) fs
return $ RecordDecl p c fs'
checkFieldDecl :: [Ident] -> FieldDecl -> TSCM FieldDecl
checkFieldDecl tvs (FieldDecl p ls ty) =
FieldDecl p ls <$> checkClosedType tvs ty
checkNewConstrDecl :: [Ident] -> NewConstrDecl -> TSCM NewConstrDecl
checkNewConstrDecl tvs (NewConstrDecl p c ty) = do
ty' <- checkClosedType tvs ty
return $ NewConstrDecl p c ty'
checkNewConstrDecl tvs (NewRecordDecl p c (l, ty)) = do
ty' <- checkClosedType tvs ty
return $ NewRecordDecl p c (l, ty')
checkSimpleContext :: Context -> TSCM ()
checkSimpleContext = mapM_ checkSimpleConstraint
checkSimpleConstraint :: Constraint -> TSCM ()
checkSimpleConstraint c@(Constraint _ _ ty) =
unless (isVariableType ty) $ report $ errIllegalSimpleConstraint c
checkClassMethod :: Ident -> Decl a -> TSCM ()
checkClassMethod tv (TypeSig spi _ qty) = do
unless (tv `elem` fv qty) $ report $ errAmbiguousType spi tv
let QualTypeExpr _ cx _ = qty
when (tv `elem` fv cx) $ report $ errConstrainedClassVariable spi tv
checkClassMethod _ _ = ok
checkInstanceType :: SpanInfo -> InstanceType -> TSCM ()
checkInstanceType p inst = do
tEnv <- getTypeEnv
unless (isSimpleType inst &&
not (isTypeSyn (typeConstr inst) tEnv) &&
not (any isAnonId $ typeVariables inst) &&
isNothing (findDouble $ fv inst)) $
report $ errIllegalInstanceType p inst
checkTypeLhs :: [Ident] -> TSCM ()
checkTypeLhs = checkTypeVars "left hand side of type declaration"
checkTypeVars :: String -> [Ident] -> TSCM ()
checkTypeVars _ [] = ok
checkTypeVars what (tv : tvs) = do
unless (isAnonId tv) $ do
isTypeConstrOrClass <- not . null . lookupTypeKind tv <$> getTypeEnv
when isTypeConstrOrClass $ report $ errNoVariable tv what
when (tv `elem` tvs) $ report $ errNonLinear tv what
checkTypeVars what tvs
checkEquation :: Equation a -> TSCM (Equation a)
checkEquation (Equation p lhs rhs) = Equation p lhs <$> checkRhs rhs
checkRhs :: Rhs a -> TSCM (Rhs a)
checkRhs (SimpleRhs spi li e ds) =
SimpleRhs spi li <$> checkExpr e <*> mapM checkDecl ds
checkRhs (GuardedRhs spi li es ds) =
GuardedRhs spi li <$> mapM checkCondExpr es <*> mapM checkDecl ds
checkCondExpr :: CondExpr a -> TSCM (CondExpr a)
checkCondExpr (CondExpr spi g e) = CondExpr spi <$> checkExpr g <*> checkExpr e
checkExpr :: Expression a -> TSCM (Expression a)
checkExpr l@(Literal _ _ _) = return l
checkExpr v@(Variable _ _ _) = return v
checkExpr c@(Constructor _ _ _) = return c
checkExpr (Paren spi e) = Paren spi <$> checkExpr e
checkExpr (Typed spi e qty) = Typed spi <$> checkExpr e
<*> checkQualType qty
checkExpr (Record spi a c fs) =
Record spi a c <$> mapM checkFieldExpr fs
checkExpr (RecordUpdate spi e fs) =
RecordUpdate spi <$> checkExpr e <*> mapM checkFieldExpr fs
checkExpr (Tuple spi es) = Tuple spi <$> mapM checkExpr es
checkExpr (List spi a es) = List spi a <$> mapM checkExpr es
checkExpr (ListCompr spi e qs) = ListCompr spi <$> checkExpr e
<*> mapM checkStmt qs
checkExpr (EnumFrom spi e) = EnumFrom spi <$> checkExpr e
checkExpr (EnumFromThen spi e1 e2) = EnumFromThen spi <$> checkExpr e1
<*> checkExpr e2
checkExpr (EnumFromTo spi e1 e2) = EnumFromTo spi <$> checkExpr e1
<*> checkExpr e2
checkExpr (EnumFromThenTo spi e1 e2 e3) = EnumFromThenTo spi <$> checkExpr e1
<*> checkExpr e2
<*> checkExpr e3
checkExpr (UnaryMinus spi e) = UnaryMinus spi <$> checkExpr e
checkExpr (Apply spi e1 e2) = Apply spi <$> checkExpr e1
<*> checkExpr e2
checkExpr (InfixApply spi e1 op e2) = InfixApply spi <$> checkExpr e1
<*> return op
<*> checkExpr e2
checkExpr (LeftSection spi e op) = flip (LeftSection spi) op <$>
checkExpr e
checkExpr (RightSection spi op e) = RightSection spi op <$> checkExpr e
checkExpr (Lambda spi ts e) = Lambda spi ts <$> checkExpr e
checkExpr (Let spi li ds e) = Let spi li <$> mapM checkDecl ds
<*> checkExpr e
checkExpr (Do spi li sts e) = Do spi li <$> mapM checkStmt sts
<*> checkExpr e
checkExpr (IfThenElse spi e1 e2 e3) = IfThenElse spi <$> checkExpr e1
<*> checkExpr e2
<*> checkExpr e3
checkExpr (Case spi li ct e alts) = Case spi li ct <$> checkExpr e
<*> mapM checkAlt alts
checkStmt :: Statement a -> TSCM (Statement a)
checkStmt (StmtExpr spi e) = StmtExpr spi <$> checkExpr e
checkStmt (StmtBind spi t e) = StmtBind spi t <$> checkExpr e
checkStmt (StmtDecl spi li ds) = StmtDecl spi li <$> mapM checkDecl ds
checkAlt :: Alt a -> TSCM (Alt a)
checkAlt (Alt spi t rhs) = Alt spi t <$> checkRhs rhs
checkFieldExpr :: Field (Expression a) -> TSCM (Field (Expression a))
checkFieldExpr (Field spi l e) = Field spi l <$> checkExpr e
checkQualType :: QualTypeExpr -> TSCM QualTypeExpr
checkQualType (QualTypeExpr spi cx ty) = do
ty' <- checkType ty
cx' <- checkClosedContext (fv ty') cx
return $ QualTypeExpr spi cx' ty'
checkClosedContext :: [Ident] -> Context -> TSCM Context
checkClosedContext tvs cx = do
cx' <- checkContext cx
mapM_ (\(Constraint _ _ ty) -> checkClosed tvs ty) cx'
return cx'
checkContext :: Context -> TSCM Context
checkContext = mapM checkConstraint
checkConstraint :: Constraint -> TSCM Constraint
checkConstraint c@(Constraint spi qcls ty) = do
checkClass False qcls
ty' <- checkType ty
unless (isVariableType $ rootType ty') $ report $ errIllegalConstraint c
return $ Constraint spi qcls ty'
where
rootType (ApplyType _ ty' _) = ty'
rootType ty' = ty'
checkClass :: Bool -> QualIdent -> TSCM ()
checkClass isInstDecl qcls = do
m <- getModuleIdent
tEnv <- getTypeEnv
case qualLookupTypeKind qcls tEnv of
[] -> report $ errUndefinedClass qcls
[Class c _]
| c == qDataId -> when (isInstDecl && m /= preludeMIdent) $ report $
errIllegalDataInstance qcls
| otherwise -> ok
[_] -> report $ errUndefinedClass qcls
tks -> case qualLookupTypeKind (qualQualify m qcls) tEnv of
[Class c _]
| c == qDataId -> when (isInstDecl && m /= preludeMIdent) $ report $
errIllegalDataInstance qcls
| otherwise -> ok
[_] -> report $ errUndefinedClass qcls
_ -> report $ errAmbiguousIdent qcls $ map origName tks
checkClosedType :: [Ident] -> TypeExpr -> TSCM TypeExpr
checkClosedType tvs ty = do
ty' <- checkType ty
checkClosed tvs ty'
return ty'
checkType :: TypeExpr -> TSCM TypeExpr
checkType c@(ConstructorType spi tc) = do
m <- getModuleIdent
tEnv <- getTypeEnv
case qualLookupTypeKind tc tEnv of
[]
| isQTupleId tc -> return c
| not (isQualified tc) -> return $ VariableType spi $ unqualify tc
| otherwise -> report (errUndefinedType tc) >> return c
[Class _ _] -> report (errUndefinedType tc) >> return c
[_] -> return c
tks -> case qualLookupTypeKind (qualQualify m tc) tEnv of
[Class _ _] -> report (errUndefinedType tc) >> return c
[_] -> return c
_ -> report (errAmbiguousIdent tc $ map origName tks) >> return c
checkType (ApplyType spi ty1 ty2) = ApplyType spi <$> checkType ty1
<*> checkType ty2
checkType (VariableType spi tv)
| isAnonId tv = (VariableType spi . renameIdent tv) <$> newId
| otherwise = checkType $ ConstructorType spi (qualify tv)
checkType (TupleType spi tys) = TupleType spi <$> mapM checkType tys
checkType (ListType spi ty) = ListType spi <$> checkType ty
checkType (ArrowType spi ty1 ty2) = ArrowType spi <$> checkType ty1
<*> checkType ty2
checkType (ParenType spi ty) = ParenType spi <$> checkType ty
checkType (ForallType spi vs ty) = ForallType spi vs <$> checkType ty
checkClosed :: [Ident] -> TypeExpr -> TSCM ()
checkClosed _ (ConstructorType _ _) = ok
checkClosed tvs (ApplyType _ ty1 ty2) = mapM_ (checkClosed tvs) [ty1, ty2]
checkClosed tvs (VariableType _ tv) =
when (isAnonId tv || tv `notElem` tvs) $ report $ errUnboundVariable tv
checkClosed tvs (TupleType _ tys) = mapM_ (checkClosed tvs) tys
checkClosed tvs (ListType _ ty) = checkClosed tvs ty
checkClosed tvs (ArrowType _ ty1 ty2) = mapM_ (checkClosed tvs) [ty1, ty2]
checkClosed tvs (ParenType _ ty) = checkClosed tvs ty
checkClosed tvs (ForallType _ vs ty) = checkClosed (tvs ++ vs) ty
getIdent :: Decl a -> Ident
getIdent (DataDecl _ tc _ _ _) = tc
getIdent (ExternalDataDecl _ tc _) = tc
getIdent (NewtypeDecl _ tc _ _ _) = tc
getIdent (TypeDecl _ tc _ _) = tc
getIdent (ClassDecl _ _ _ cls _ _) = cls
getIdent _ = internalError
"Checks.TypeSyntaxCheck.getIdent: no type or class declaration"
isTypeSyn :: QualIdent -> TypeEnv -> Bool
isTypeSyn tc tEnv = case qualLookupTypeKind tc tEnv of
[Alias _] -> True
_ -> False
errMultipleDefaultDeclarations :: [SpanInfo] -> Message
errMultipleDefaultDeclarations spis = spanInfoMessage (head spis) $
text "More than one default declaration:" $+$
nest 2 (vcat $ map showPos spis)
where showPos = text . showLine . getPosition
errMultipleDeclarations :: [Ident] -> Message
errMultipleDeclarations is = spanInfoMessage i $
text "Multiple declarations of" <+> text (escName i) <+> text "at:" $+$
nest 2 (vcat $ map showPos is)
where i = head is
showPos = text . showLine . getPosition
errUndefined :: String -> QualIdent -> Message
errUndefined what qident = spanInfoMessage qident $ hsep $ map text
["Undefined", what, qualName qident]
errUndefinedClass :: QualIdent -> Message
errUndefinedClass = errUndefined "class"
errUndefinedType :: QualIdent -> Message
errUndefinedType = errUndefined "type"
errAmbiguousIdent :: QualIdent -> [QualIdent] -> Message
errAmbiguousIdent qident qidents = spanInfoMessage qident $
text "Ambiguous identifier" <+> text (escQualName qident) $+$
text "It could refer to:" $+$ nest 2 (vcat (map (text . qualName) qidents))
errAmbiguousType :: SpanInfo -> Ident -> Message
errAmbiguousType spi ident = spanInfoMessage spi $ hsep $ map text
[ "Method type does not mention class variable", idName ident ]
errConstrainedClassVariable :: SpanInfo -> Ident -> Message
errConstrainedClassVariable spi ident = spanInfoMessage spi $ hsep $ map text
[ "Method context must not constrain class variable", idName ident ]
errNonLinear :: Ident -> String -> Message
errNonLinear tv what = spanInfoMessage tv $ hsep $ map text
[ "Type variable", idName tv, "occurs more than once in", what ]
errNoVariable :: Ident -> String -> Message
errNoVariable tv what = spanInfoMessage tv $ hsep $ map text
["Type constructor or type class identifier", idName tv, "used in", what]
errUnboundVariable :: Ident -> Message
errUnboundVariable tv = spanInfoMessage tv $ hsep $ map text
[ "Unbound type variable", idName tv ]
errIllegalConstraint :: Constraint -> Message
errIllegalConstraint c@(Constraint _ qcls _) = spanInfoMessage qcls $ vcat
[ text "Illegal class constraint" <+> pPrint c
, text "Constraints must be of the form C u or C (u t1 ... tn),"
, text "where C is a type class, u is a type variable and t1, ..., tn are types."
]
errIllegalSimpleConstraint :: Constraint -> Message
errIllegalSimpleConstraint c@(Constraint _ qcls _) = spanInfoMessage qcls $ vcat
[ text "Illegal class constraint" <+> pPrint c
, text "Constraints in class and instance declarations must be of"
, text "the form C u, where C is a type class and u is a type variable."
]
errIllegalInstanceType :: SpanInfo -> InstanceType -> Message
errIllegalInstanceType spi inst = spanInfoMessage spi $ vcat
[ text "Illegal instance type" <+> ppInstanceType inst
, text "The instance type must be of the form (T u_1 ... u_n),"
, text "where T is not a type synonym and u_1, ..., u_n are"
, text "mutually distinct, non-anonymous type variables."
]
errIllegalDataInstance :: QualIdent -> Message
errIllegalDataInstance qcls = spanInfoMessage qcls $ vcat
[ text "Illegal instance of" <+> ppQIdent qcls
, text "Instances of this class cannot be defined."
, text "Instead, they are automatically derived if possible."
]