cryptol-3.2.0: src/Cryptol/TypeCheck/Sanity.hs
-- |
-- Module : Cryptol.TypeCheck.Sanity
-- Copyright : (c) 2015-2016 Galois, Inc.
-- License : BSD3
-- Maintainer : cryptol@galois.com
-- Stability : provisional
-- Portability : portable
{-# Language OverloadedStrings #-}
module Cryptol.TypeCheck.Sanity
( tcExpr
, tcDecls
, tcModule
, ProofObligation
, onlyNonTrivial
, Error(..)
, AreSame(..)
, same
) where
import Data.Maybe(maybeToList)
import Data.List (sort)
import qualified Data.Set as Set
import MonadLib
import qualified Control.Applicative as A
import Data.Map ( Map )
import qualified Data.Map as Map
import Cryptol.Parser.Position(thing,Range,emptyRange)
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.Subst (apSubst, singleTParamSubst, mergeDistinctSubst)
import Cryptol.TypeCheck.Monad(InferInput(..))
import Cryptol.ModuleSystem.Name(nameLoc,nameIdent)
import Cryptol.Utils.Ident
import Cryptol.Utils.RecordMap
import Cryptol.Utils.PP
tcExpr :: InferInput -> Expr -> Either (Range, Error) (Schema, [ ProofObligation ])
tcExpr env e = runTcM env (exprSchema e)
tcDecls :: InferInput -> [DeclGroup] -> Either (Range, Error) [ ProofObligation ]
tcDecls env ds0 = case runTcM env (checkDecls ds0) of
Left err -> Left err
Right (_,ps) -> Right ps
tcModule :: InferInput -> Module -> Either (Range, Error) [ ProofObligation ]
tcModule env m = case runTcM env check of
Left err -> Left err
Right (_,ps) -> Right ps
where check = foldr withTVar k1 (map mtpParam (Map.elems (mParamTypes m)))
k1 = foldr withAsmp k2 (map thing (mParamConstraints m))
k2 = withVars (Map.toList (fmap mvpType (mParamFuns m)))
$ withVars (concatMap nominalTypeConTypes
(Map.elems (mNominalTypes m)))
$ checkDecls (mDecls m)
onlyNonTrivial :: [ProofObligation] -> [ProofObligation]
onlyNonTrivial = filter (not . trivialProofObligation)
-- | Identify proof obligations that are obviously true.
-- We can filter these to avoid clutter
trivialProofObligation :: ProofObligation -> Bool
trivialProofObligation oblig = pIsTrue goal || simpleEq || goal `elem` asmps
where
goal = sType oblig
asmps = sProps oblig
simpleEq = case pIsEqual goal of
Just (t1,t2) -> t1 == t2
Nothing -> False
--------------------------------------------------------------------------------
checkDecls :: [DeclGroup] -> TcM ()
checkDecls decls =
case decls of
[] -> return ()
d : ds -> do xs <- checkDeclGroup d
withVars xs (checkDecls ds)
-- | Validate a type, returning its kind.
checkType :: Type -> TcM Kind
checkType ty =
case ty of
TUser _ _ t -> checkType t -- Maybe check synonym too?
TCon tc ts ->
do ks <- mapM checkType ts
checkKind (kindOf tc) ks
TNominal nt ts ->
do ks <- mapM checkType ts
checkKind (kindOf nt) ks
TVar tv -> lookupTVar tv
TRec fs ->
do forM_ fs $ \t ->
do k <- checkType t
unless (k == KType) $ reportError $ KindMismatch KType k
return KType
where
checkKind k [] = case k of
_ :-> _ -> reportError $ NotEnoughArgumentsInKind k
KProp -> return k
KNum -> return k
KType -> return k
checkKind (k1 :-> k2) (k : ks)
| k == k1 = checkKind k2 ks
| otherwise = reportError $ KindMismatch k1 k
checkKind k ks = reportError $ BadTypeApplication k ks
-- | Check that the type is valid, and it has the given kind.
checkTypeIs :: Kind -> Type -> TcM ()
checkTypeIs k ty =
do k1 <- checkType ty
unless (k == k1) $ reportError $ KindMismatch k k1
-- | Check that this is a valid schema.
checkSchema :: Schema -> TcM ()
checkSchema (Forall as ps t) = foldr withTVar check as
where check = do mapM_ (checkTypeIs KProp) ps
checkTypeIs KType t
data AreSame = SameIf [Prop]
| NotSame
areSame :: AreSame
areSame = SameIf []
sameAnd :: AreSame -> AreSame -> AreSame
sameAnd x y =
case (x,y) of
(SameIf xs, SameIf ys) -> SameIf (xs ++ ys)
_ -> NotSame
sameBool :: Bool -> AreSame
sameBool b = if b then areSame else NotSame
sameTypes :: String -> Type -> Type -> TcM ()
sameTypes msg x y = sameSchemas msg (tMono x) (tMono y)
sameSchemas :: String -> Schema -> Schema -> TcM ()
sameSchemas msg x y =
case same x y of
NotSame -> reportError (TypeMismatch msg x y)
SameIf ps -> mapM_ proofObligation ps
class Same a where
same :: a -> a -> AreSame
instance Same a => Same [a] where
same [] [] = areSame
same (x : xs) (y : ys) = same x y `sameAnd` same xs ys
same _ _ = NotSame
data Field a b = Field a b
instance (Eq a, Same b) => Same (Field a b) where
same (Field x a) (Field y b) = sameBool (x == y) `sameAnd` same a b
instance Same Type where
same t1 t2
| k1 /= k2 = NotSame
| k1 == KNum = if t1 == t2 then SameIf [] else SameIf [ t1 =#= t2 ]
| otherwise =
case (tNoUser t1, tNoUser t2) of
(TVar x, TVar y) -> sameBool (x == y)
(TRec x, TRec y) -> same (mkRec x) (mkRec y)
(TNominal x xs, TNominal y ys) -> same (Field x xs) (Field y ys)
(TCon x xs, TCon y ys) -> same (Field x xs) (Field y ys)
_ -> NotSame
where
k1 = kindOf t1
k2 = kindOf t2
mkRec r = [ Field x y | (x,y) <- canonicalFields r ]
instance Same Schema where
same (Forall xs ps s) (Forall ys qs t) =
same xs ys `sameAnd` same ps qs `sameAnd` same s t
instance Same TParam where
same x y = sameBool (tpName x == tpName y && tpKind x == tpKind y)
--------------------------------------------------------------------------------
-- | Check that the expression is well-formed, and compute its type.
-- Reports an error if the expression is not of a mono type.
exprType :: Expr -> TcM Type
exprType expr =
do s <- exprSchema expr
case isMono s of
Just t -> return t
Nothing -> reportError (ExpectedMono s)
-- | Check that the expression is well-formed, and compute its schema.
exprSchema :: Expr -> TcM Schema
exprSchema expr =
case expr of
ELocated rng t -> withRange rng (exprSchema t)
EList es t ->
do checkTypeIs KType t
forM_ es $ \e ->
do t1 <- exprType e
sameTypes "EList" t1 t
return $ tMono $ tSeq (tNum (length es)) t
ETuple es ->
fmap (tMono . tTuple) (mapM exprType es)
ERec fs ->
do fs1 <- traverse exprType fs
return $ tMono $ TRec fs1
ESet _ e x v ->
do ty <- exprType e
expe <- checkHas ty x
has <- exprType v
sameTypes "ESet" expe has
return (tMono ty)
ESel e sel -> do ty <- exprType e
ty1 <- checkHas ty sel
return (tMono ty1)
EIf e1 e2 e3 ->
do ty <- exprType e1
sameTypes "EIf_condition" tBit ty
t1 <- exprType e2
t2 <- exprType e3
sameTypes "EIf_arms" t1 t2
return $ tMono t1
ECase e as d ->
do ty <- exprType e
case tNoUser ty of
TNominal nt targs
| Enum cons <- ntDef nt ->
do alts <- traverse checkCaseAlt as
dflt <- traverse checkCaseAlt d
let resTypes = map snd (maybeToList dflt ++ Map.elems alts)
resT <- case resTypes of
[] -> reportError (BadCase Nothing)
t : ts ->
do mapM_ (sameTypes "ECase_alt_result" t) ts
pure t
let su = mergeDistinctSubst
(zipWith singleTParamSubst (ntParams nt) targs)
conMap = Map.fromList [ (nameIdent (ecName c)
, apSubst su <$> ecFields c)
| c <- cons ]
checkCon (c,(ts,_)) =
case Map.lookup c conMap of
Just ts1 | length ts == length ts1 ->
zipWithM_ (sameTypes "ECase_alt_field") ts ts1
_ -> reportError (BadCaseAlt (Just c))
mapM_ checkCon (Map.toList alts)
case dflt of
Nothing -> pure ()
Just ([t],_) -> sameTypes "ECase_default_arg" t ty
_ -> reportError (BadCaseAlt Nothing)
pure (tMono resT)
_ -> reportError (BadCase (Just ty))
EComp len t e mss ->
do checkTypeIs KNum len
checkTypeIs KType t
(xs,ls) <- unzip `fmap` mapM checkArm mss
-- XXX: check no duplicates
elT <- withVars (concat xs) $ exprType e
case ls of
[] -> return ()
_ -> convertible (tSeq len t) (tSeq (foldr1 tMin ls) elT)
return (tMono (tSeq len t))
EVar x -> lookupVar x
ETAbs a e ->
do Forall as p t <- withTVar a (exprSchema e)
when (any (== a) as) $
reportError $ RepeatedVariableInForall a
return (Forall (a : as) p t)
ETApp e t ->
do k <- checkType t
s <- exprSchema e
case s of
Forall (a : as) ps t1 ->
do let vs = fvs t
forM_ (map tpVar as) $ \b ->
when (b `Set.member` vs) $ reportError $ Captured b
let k' = kindOf a
unless (k == k') $ reportError $ KindMismatch k' k
let su = singleTParamSubst a t
return $ Forall as (apSubst su ps) (apSubst su t1)
Forall [] _ _ -> reportError BadInstantiation
EApp e1 e2 ->
do t1 <- exprType e1
t2 <- exprType e2
case tNoUser t1 of
TCon (TC TCFun) [ a, b ]
| SameIf ps <- same a t2 ->
do mapM_ proofObligation ps
return (tMono b)
tf -> reportError (BadApplication tf t1)
EAbs x t e ->
do checkTypeIs KType t
res <- withVar x t (exprType e)
return $ tMono $ tFun t res
EProofAbs p e ->
do checkTypeIs KProp p
withAsmp p $ do Forall as ps t <- exprSchema e
return $ Forall as (p : ps) t
EProofApp e ->
do Forall as ps t <- exprSchema e
case (as,ps) of
([], p:qs) -> do proofObligation p
return (Forall [] qs t)
([], _) -> reportError BadProofNoAbs
(_,_) -> reportError (BadProofTyVars as)
-- XXX: Check that defined things are distinct?
EWhere e dgs ->
let go [] = exprSchema e
go (d : ds) = do xs <- checkDeclGroup d
withVars xs (go ds)
in go dgs
EPropGuards guards typ ->
do forM_ guards $ \(prop, e) ->
do mapM_ (checkTypeIs KProp) prop
eTyp <- exprType e
sameTypes "EPropGuards" typ eTyp
pure (tMono typ)
checkCaseAlt :: CaseAlt -> TcM ([Type], Type)
checkCaseAlt (CaseAlt xs e) =
do ty <- foldr addVar (exprType e) xs
pure (map snd xs, ty)
where
addVar (x,t) = withVar x t
checkHas :: Type -> Selector -> TcM Type
checkHas t sel =
case sel of
TupleSel n mb ->
case tNoUser t of
TCon (TC (TCTuple sz)) ts ->
do case mb of
Just sz1 ->
when (sz /= sz1) (reportError (UnexpectedTupleShape sz1 sz))
Nothing -> return ()
unless (n < sz) $ reportError (TupleSelectorOutOfRange n sz)
return $ ts !! n
TCon (TC TCSeq) [s,elT] ->
do res <- checkHas elT sel
return (TCon (TC TCSeq) [s,res])
TCon (TC TCFun) [a,b] ->
do res <- checkHas b sel
return (TCon (TC TCFun) [a,res])
_ -> reportError $ BadSelector sel t
RecordSel f mb ->
case tNoUser t of
TRec fs ->
do case mb of
Nothing -> return ()
Just fs1 ->
do let ns = Set.toList (fieldSet fs)
ns1 = sort fs1
unless (ns == ns1) $
reportError $ UnexpectedRecordShape ns1 ns
case lookupField f fs of
Nothing -> reportError $ MissingField f $ displayOrder fs
Just ft -> return ft
TCon (TC TCSeq) [s,elT] -> do res <- checkHas elT sel
return (TCon (TC TCSeq) [s,res])
TCon (TC TCFun) [a,b] -> do res <- checkHas b sel
return (TCon (TC TCFun) [a,res])
_ -> reportError $ BadSelector sel t
-- XXX: Remove this?
ListSel _ mb ->
case tNoUser t of
TCon (TC TCSeq) [ n, elT ] ->
do case mb of
Nothing -> return ()
Just len ->
case tNoUser n of
TCon (TC (TCNum m)) []
| m == toInteger len -> return ()
_ -> reportError $ UnexpectedSequenceShape len n
return elT
_ -> reportError $ BadSelector sel t
-- | Check if the one type is convertible to the other.
convertible :: Type -> Type -> TcM ()
convertible t1 t2
| k1 /= k2 = reportError (KindMismatch k1 k2)
| k1 == KNum = proofObligation (t1 =#= t2)
where
k1 = kindOf t1
k2 = kindOf t2
convertible t1 t2 = go t1 t2
where
go ty1 ty2 =
let err = reportError $ TypeMismatch "convertible" (tMono ty1) (tMono ty2)
other = tNoUser ty2
goMany [] [] = return ()
goMany (x : xs) (y : ys) = convertible x y >> goMany xs ys
goMany _ _ = err
in case ty1 of
TUser _ _ s -> go s ty2
TVar x -> case other of
TVar y | x == y -> return ()
_ -> err
TCon tc1 ts1 -> case other of
TCon tc2 ts2
| tc1 == tc2 -> goMany ts1 ts2
_ -> err
TNominal nt1 ts1 ->
case other of
TNominal nt2 ts2
| nt1 == nt2 -> goMany ts1 ts2
_ -> err
TRec fs ->
case other of
TRec gs ->
do unless (fieldSet fs == fieldSet gs) err
goMany (recordElements fs) (recordElements gs)
_ -> err
--------------------------------------------------------------------------------
-- | Check a declaration. The boolean indicates if we should check the siganture
checkDecl :: Bool -> Decl -> TcM (Name, Schema)
checkDecl checkSig d =
case dDefinition d of
DPrim ->
do when checkSig $ checkSchema $ dSignature d
return (dName d, dSignature d)
DForeign _ me ->
do when checkSig $ checkSchema $ dSignature d
mapM_ checkExpr me
return (dName d, dSignature d)
DExpr e ->
do let s = dSignature d
when checkSig $ checkSchema s
checkExpr e
return (dName d, s)
where
checkExpr e =
do let s = dSignature d
s1 <- exprSchema e
let nm = dName d
loc = "definition of " ++ show (pp nm) ++
", at " ++ show (pp (nameLoc nm))
sameSchemas loc s s1
checkDeclGroup :: DeclGroup -> TcM [(Name, Schema)]
checkDeclGroup dg =
case dg of
NonRecursive d -> do x <- checkDecl True d
return [x]
Recursive ds ->
do xs <- forM ds $ \d ->
do checkSchema (dSignature d)
return (dName d, dSignature d)
withVars xs $ mapM (checkDecl False) ds
checkMatch :: Match -> TcM ((Name, Schema), Type)
checkMatch ma =
case ma of
From x len elt e ->
do checkTypeIs KNum len
checkTypeIs KType elt
t1 <- exprType e
case tNoUser t1 of
TCon (TC TCSeq) [ l, el ]
| SameIf ps <- same elt el ->
do mapM_ proofObligation ps
return ((x, tMono elt), l)
| otherwise -> reportError $ TypeMismatch "From" (tMono elt) (tMono el)
_ -> reportError $ BadMatch t1
Let d -> do x <- checkDecl True d
return (x, tNum (1 :: Int))
checkArm :: [Match] -> TcM ([(Name, Schema)], Type)
checkArm [] = reportError EmptyArm
checkArm [m] = do (x,l) <- checkMatch m
return ([x], l)
checkArm (m : ms) =
do (x, l) <- checkMatch m
(xs, l1) <- withVars [x] $ checkArm ms
let newLen = tMul l l1
return $ if fst x `elem` map fst xs
then (xs, newLen)
else (x : xs, newLen)
--------------------------------------------------------------------------------
data RO = RO
{ roTVars :: Map Int TParam
, roAsmps :: [Prop]
, roRange :: Range
, roVars :: Map Name Schema
}
type ProofObligation = Schema -- but the type is of kind Prop
data RW = RW
{ woProofObligations :: [ProofObligation]
}
newtype TcM a = TcM (ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a)
instance Functor TcM where
fmap = liftM
instance A.Applicative TcM where
pure a = TcM (pure a)
(<*>) = ap
instance Monad TcM where
return = pure
TcM m >>= f = TcM (do a <- m
let TcM m1 = f a
m1)
runTcM :: InferInput -> TcM a -> Either (Range, Error) (a, [ProofObligation])
runTcM env (TcM m) =
case runM m ro rw of
(Left err, _) -> Left err
(Right a, s) -> Right (a, woProofObligations s)
where
allPs = inpParams env
ro = RO { roTVars = Map.fromList [ (tpUnique x, x)
| tp <- Map.elems (mpnTypes allPs)
, let x = mtpParam tp ]
, roAsmps = map thing (mpnConstraints allPs)
, roRange = emptyRange
, roVars = Map.unions
[ fmap mvpType (mpnFuns allPs)
, inpVars env
, Map.fromList
[ c
| nt <- Map.elems (inpNominalTypes env)
, c <- nominalTypeConTypes nt
]
]
}
rw = RW { woProofObligations = [] }
data Error =
TypeMismatch String Schema Schema -- ^ expected, actual
| ExpectedMono Schema -- ^ expected a mono type, got this
| TupleSelectorOutOfRange Int Int
| MissingField Ident [Ident]
| UnexpectedTupleShape Int Int
| UnexpectedRecordShape [Ident] [Ident]
| UnexpectedSequenceShape Int Type
| BadSelector Selector Type
| BadInstantiation
| Captured TVar
| BadProofNoAbs
| BadProofTyVars [TParam]
| KindMismatch Kind Kind
| NotEnoughArgumentsInKind Kind
| BadApplication Type Type
| FreeTypeVariable TVar
| BadTypeApplication Kind [Kind]
| RepeatedVariableInForall TParam
| BadMatch Type
| EmptyArm
| UndefinedTypeVaraible TVar
| UndefinedVariable Name
| BadCase (Maybe Type)
| BadCaseAlt (Maybe Ident)
deriving Show
reportError :: Error -> TcM a
reportError e = TcM $
do ro <- ask
raise (roRange ro, e)
withTVar :: TParam -> TcM a -> TcM a
withTVar a (TcM m) = TcM $
do ro <- ask
local ro { roTVars = Map.insert (tpUnique a) a (roTVars ro) } m
withRange :: Range -> TcM a -> TcM a
withRange rng (TcM m) = TcM $
do ro <- ask
local ro { roRange = rng } m
withAsmp :: Prop -> TcM a -> TcM a
withAsmp p (TcM m) = TcM $
do ro <- ask
local ro { roAsmps = p : roAsmps ro } m
withVar :: Name -> Type -> TcM a -> TcM a
withVar x t = withVars [(x,tMono t)]
withVars :: [(Name, Schema)] -> TcM a -> TcM a
withVars xs (TcM m) = TcM $
do ro <- ask
local ro { roVars = Map.union (Map.fromList xs) (roVars ro) } m
proofObligation :: Prop -> TcM ()
proofObligation p = TcM $
do ro <- ask
sets_ $ \rw -> rw { woProofObligations =
Forall (Map.elems (roTVars ro)) (roAsmps ro) p
: woProofObligations rw }
lookupTVar :: TVar -> TcM Kind
lookupTVar x =
case x of
TVFree {} -> reportError (FreeTypeVariable x)
TVBound tpv ->
do let u = tpUnique tpv
k = tpKind tpv
ro <- TcM ask
case Map.lookup u (roTVars ro) of
Just tp
| kindOf tp == k -> return k
| otherwise -> reportError $ KindMismatch (kindOf tp) k
Nothing -> reportError $ UndefinedTypeVaraible x
lookupVar :: Name -> TcM Schema
lookupVar x =
do ro <- TcM ask
case Map.lookup x (roVars ro) of
Just s -> return s
Nothing -> reportError $ UndefinedVariable x
instance PP Error where
ppPrec _ err =
case err of
TypeMismatch what expected actual ->
ppErr ("Type mismatch in" <+> text what)
[ "Expected:" <+> pp expected
, "Actual :" <+> pp actual
]
ExpectedMono s ->
ppErr "Not a monomorphic type"
[ pp s ]
TupleSelectorOutOfRange sel sz ->
ppErr "Tuple selector out of range"
[ "Selector:" <+> int sel
, "Size :" <+> int sz
]
MissingField f fs ->
ppErr "Invalid record selector"
[ "Field: " <+> pp f
, "Fields:" <+> commaSep (map pp fs)
]
UnexpectedTupleShape expected actual ->
ppErr "Unexpected tuple shape"
[ "Expected:" <+> int expected
, "Actual :" <+> int actual
]
UnexpectedRecordShape expected actual ->
ppErr "Unexpected record shape"
[ "Expected:" <+> commaSep (map pp expected)
, "Actual :" <+> commaSep (map pp actual)
]
UnexpectedSequenceShape n t ->
ppErr "Unexpected sequence shape"
[ "Expected:" <+> int n
, "Actual :" <+> pp t
]
BadSelector sel t ->
ppErr "Bad selector"
[ "Selector:" <+> pp sel
, "Type :" <+> pp t
]
BadInstantiation ->
ppErr "Bad instantiation" []
Captured x ->
ppErr "Captured type variable"
[ "Variable:" <+> pp x ]
BadProofNoAbs ->
ppErr "Proof application without a proof abstraction" []
BadProofTyVars xs ->
ppErr "Proof application with type abstraction"
[ "Type parameter:" <+> pp x | x <- xs ]
KindMismatch expected actual ->
ppErr "Kind mismatch"
[ "Expected:" <+> pp expected
, "Actual :" <+> pp actual
]
NotEnoughArgumentsInKind k ->
ppErr "Not enough arguments in kind" [ pp k ]
BadApplication t1 t2 ->
ppErr "Bad application"
[ "Function:" <+> pp t1
, "Argument:" <+> pp t2
]
FreeTypeVariable x ->
ppErr "Free type variable"
[ "Variable:" <+> pp x ]
BadTypeApplication kf ka ->
ppErr "Bad type application"
[ "Function :" <+> pp kf
, "Arguments:" <+> commaSep (map pp ka)
]
RepeatedVariableInForall x ->
ppErr "Repeated variable in forall"
[ "Variable:" <+> pp x ]
BadMatch t ->
ppErr "Bad match"
[ "Type:" <+> pp t ]
EmptyArm -> ppErr "Empty comprehension arm" []
UndefinedTypeVaraible x ->
ppErr "Undefined type variable"
[ "Variable:" <+> pp x ]
UndefinedVariable x ->
ppErr "Undefined variable"
[ "Variable:" <+> pp x ]
BadCase mbt ->
ppErr "Malformed cased expression" $
case mbt of
Just t -> [ "Expected: `enum` type", "Actual:" <+> pp t ]
Nothing -> [ "Empty alternatives" ]
BadCaseAlt mbCon ->
ppErr "Malformed case alternative" $
[ case mbCon of
Just c -> "Alternative for constructor" <+> pp c
Nothing -> "Default alternative"
]
where
ppErr x ys = hang x 2 (vcat [ "•" <+> y | y <- ys ])