futhark-0.22.2: src/Language/Futhark/TypeChecker/Terms.hs
-- | Facilities for type-checking Futhark terms. Checking a term
-- requires a little more context to track uniqueness and such.
--
-- Type inference is implemented through a variation of
-- Hindley-Milner. The main complication is supporting the rich
-- number of built-in language constructs, as well as uniqueness
-- types. This is mostly done in an ad hoc way, and many programs
-- will require the programmer to fall back on type annotations.
module Language.Futhark.TypeChecker.Terms
( checkOneExp,
checkFunDef,
)
where
import Control.Monad.Except
import Control.Monad.Reader
import Control.Monad.State
import Data.Either
import Data.List (find, foldl', partition)
import Data.List.NonEmpty qualified as NE
import Data.Map.Strict qualified as M
import Data.Maybe
import Data.Set qualified as S
import Futhark.Util.Pretty hiding (space)
import Language.Futhark
import Language.Futhark.Primitive (intByteSize)
import Language.Futhark.Traversals
import Language.Futhark.TypeChecker.Match
import Language.Futhark.TypeChecker.Monad hiding (BoundV)
import Language.Futhark.TypeChecker.Terms.DoLoop
import Language.Futhark.TypeChecker.Terms.Monad
import Language.Futhark.TypeChecker.Terms.Pat
import Language.Futhark.TypeChecker.Types
import Language.Futhark.TypeChecker.Unify
import Prelude hiding (mod)
overloadedTypeVars :: Constraints -> Names
overloadedTypeVars = mconcat . map f . M.elems
where
f (_, HasFields fs _) = mconcat $ map typeVars $ M.elems fs
f _ = mempty
--- Basic checking
-- | Determine if the two types are identical, ignoring uniqueness.
-- Mismatched dimensions are turned into fresh rigid type variables.
-- Causes a 'TypeError' if they fail to match, and otherwise returns
-- one of them.
unifyBranchTypes :: SrcLoc -> PatType -> PatType -> TermTypeM (PatType, [VName])
unifyBranchTypes loc t1 t2 =
onFailure (CheckingBranches (toStruct t1) (toStruct t2)) $
unifyMostCommon (mkUsage loc "unification of branch results") t1 t2
unifyBranches :: SrcLoc -> Exp -> Exp -> TermTypeM (PatType, [VName])
unifyBranches loc e1 e2 = do
e1_t <- expTypeFully e1
e2_t <- expTypeFully e2
unifyBranchTypes loc e1_t e2_t
sliceShape ::
Maybe (SrcLoc, Rigidity) ->
Slice ->
TypeBase Size as ->
TermTypeM (TypeBase Size as, [VName])
sliceShape r slice t@(Array als u (Shape orig_dims) et) =
runStateT (setDims <$> adjustDims slice orig_dims) []
where
setDims [] = stripArray (length orig_dims) t
setDims dims' = Array als u (Shape dims') et
-- If the result is supposed to be a nonrigid size variable, then
-- don't bother trying to create non-existential sizes. This is
-- necessary to make programs type-check without too much
-- ceremony; see e.g. tests/inplace5.fut.
isRigid Rigid {} = True
isRigid _ = False
refine_sizes = maybe False (isRigid . snd) r
sliceSize orig_d i j stride =
case r of
Just (loc, Rigid _) -> do
(d, ext) <-
lift . extSize loc $
SourceSlice orig_d' (bareExp <$> i) (bareExp <$> j) (bareExp <$> stride)
modify (maybeToList ext ++)
pure d
Just (loc, Nonrigid) ->
lift $ NamedSize . qualName <$> newDimVar loc Nonrigid "slice_dim"
Nothing -> do
v <- lift $ newID "slice_anydim"
modify (v :)
pure $ NamedSize $ qualName v
where
-- The original size does not matter if the slice is fully specified.
orig_d'
| isJust i, isJust j = Nothing
| otherwise = Just orig_d
adjustDims (DimFix {} : idxes') (_ : dims) =
adjustDims idxes' dims
-- Pat match some known slices to be non-existential.
adjustDims (DimSlice i j stride : idxes') (_ : dims)
| refine_sizes,
maybe True ((== Just 0) . isInt64) i,
Just j' <- maybeDimFromExp =<< j,
maybe True ((== Just 1) . isInt64) stride =
(j' :) <$> adjustDims idxes' dims
adjustDims (DimSlice Nothing Nothing stride : idxes') (d : dims)
| refine_sizes,
maybe True (maybe False ((== 1) . abs) . isInt64) stride =
(d :) <$> adjustDims idxes' dims
adjustDims (DimSlice i j stride : idxes') (d : dims) =
(:) <$> sliceSize d i j stride <*> adjustDims idxes' dims
adjustDims _ dims =
pure dims
sliceShape _ _ t = pure (t, [])
--- Main checkers
-- The closure of a lambda or local function are those variables that
-- it references, and which local to the current top-level function.
lexicalClosure :: [Pat] -> Occurrences -> TermTypeM Aliasing
lexicalClosure params closure = do
vtable <- asks $ scopeVtable . termScope
let isGlobal v = case v `M.lookup` vtable of
Just (BoundV Global _ _) -> True
Just EqualityF {} -> True
Just OverloadedF {} -> True
Just (BoundV Local _ _) -> False
Just (BoundV Nonlocal _ _) -> False
Just WasConsumed {} -> False
Nothing -> False
pure . S.map AliasBound . S.filter (not . isGlobal) $
allOccurring closure S.\\ mconcat (map patNames params)
noAliasesIfOverloaded :: PatType -> TermTypeM PatType
noAliasesIfOverloaded t@(Scalar (TypeVar _ u tn [])) = do
subst <- fmap snd . M.lookup (qualLeaf tn) <$> getConstraints
case subst of
Just Overloaded {} -> pure $ Scalar $ TypeVar mempty u tn []
_ -> pure t
noAliasesIfOverloaded t =
pure t
checkAscript ::
SrcLoc ->
UncheckedTypeExp ->
UncheckedExp ->
TermTypeM (TypeExp VName, Exp)
checkAscript loc te e = do
(te', decl_t, _) <- checkTypeExpNonrigid te
e' <- checkExp e
e_t <- toStruct <$> expTypeFully e'
onFailure (CheckingAscription decl_t e_t) $
unify (mkUsage loc "type ascription") decl_t e_t
pure (te', e')
checkCoerce ::
SrcLoc ->
UncheckedTypeExp ->
UncheckedExp ->
TermTypeM (TypeExp VName, StructType, Exp, [VName])
checkCoerce loc te e = do
(te', te_t, ext) <- checkTypeExpRigid te RigidCoerce
e' <- checkExp e
e_t <- toStruct <$> expTypeFully e'
(e_t_nonrigid, _) <-
allDimsFreshInType loc Nonrigid "coerce_d" e_t
onFailure (CheckingAscription te_t e_t) $
unify (mkUsage loc "type ascription") te_t e_t_nonrigid
te_t' <- normTypeFully te_t
pure (te', te_t', e', ext)
unscopeType ::
SrcLoc ->
M.Map VName Ident ->
PatType ->
TermTypeM (PatType, [VName])
unscopeType tloc unscoped t = do
(t', m) <- runStateT (traverseDims onDim t) mempty
pure (t' `addAliases` S.map unAlias, M.elems m)
where
onDim bound _ (NamedSize d)
| Just loc <- srclocOf <$> M.lookup (qualLeaf d) unscoped,
not $ qualLeaf d `S.member` bound =
inst loc $ qualLeaf d
onDim _ _ d = pure d
inst loc d = do
prev <- gets $ M.lookup d
case prev of
Just d' -> pure $ NamedSize $ qualName d'
Nothing -> do
d' <- lift $ newDimVar tloc (Rigid $ RigidOutOfScope loc d) "d"
modify $ M.insert d d'
pure $ NamedSize $ qualName d'
unAlias (AliasBound v) | v `M.member` unscoped = AliasFree v
unAlias a = a
-- 'checkApplyExp' is like 'checkExp', but tries to find the "root
-- function", for better error messages.
checkApplyExp :: UncheckedExp -> TermTypeM (Exp, ApplyOp)
checkApplyExp (AppExp (Apply e1 e2 _ loc) _) = do
arg <- checkArg e2
(e1', (fname, i)) <- checkApplyExp e1
t <- expType e1'
(t1, rt, argext, exts) <- checkApply loc (fname, i) t arg
pure
( AppExp
(Apply e1' (argExp arg) (Info (diet t1, argext)) loc)
(Info $ AppRes rt exts),
(fname, i + 1)
)
checkApplyExp e = do
e' <- checkExp e
pure
( e',
( case e' of
Var qn _ _ -> Just qn
_ -> Nothing,
0
)
)
checkExp :: UncheckedExp -> TermTypeM Exp
checkExp (Literal val loc) =
pure $ Literal val loc
checkExp (Hole _ loc) = do
t <- newTypeVar loc "t"
pure $ Hole (Info $ t `setUniqueness` Unique) loc
checkExp (StringLit vs loc) =
pure $ StringLit vs loc
checkExp (IntLit val NoInfo loc) = do
t <- newTypeVar loc "t"
mustBeOneOf anyNumberType (mkUsage loc "integer literal") t
pure $ IntLit val (Info $ fromStruct t) loc
checkExp (FloatLit val NoInfo loc) = do
t <- newTypeVar loc "t"
mustBeOneOf anyFloatType (mkUsage loc "float literal") t
pure $ FloatLit val (Info $ fromStruct t) loc
checkExp (TupLit es loc) =
TupLit <$> mapM checkExp es <*> pure loc
checkExp (RecordLit fs loc) = do
fs' <- evalStateT (mapM checkField fs) mempty
pure $ RecordLit fs' loc
where
checkField (RecordFieldExplicit f e rloc) = do
errIfAlreadySet f rloc
modify $ M.insert f rloc
RecordFieldExplicit f <$> lift (checkExp e) <*> pure rloc
checkField (RecordFieldImplicit name NoInfo rloc) = do
errIfAlreadySet name rloc
(QualName _ name', t) <- lift $ lookupVar rloc $ qualName name
modify $ M.insert name rloc
pure $ RecordFieldImplicit name' (Info t) rloc
errIfAlreadySet f rloc = do
maybe_sloc <- gets $ M.lookup f
case maybe_sloc of
Just sloc ->
lift . typeError rloc mempty $
"Field"
<+> dquotes (pretty f)
<+> "previously defined at"
<+> pretty (locStrRel rloc sloc) <> "."
Nothing -> pure ()
checkExp (ArrayLit all_es _ loc) =
-- Construct the result type and unify all elements with it. We
-- only create a type variable for empty arrays; otherwise we use
-- the type of the first element. This significantly cuts down on
-- the number of type variables generated for pathologically large
-- multidimensional array literals.
case all_es of
[] -> do
et <- newTypeVar loc "t"
t <- arrayOfM loc et (Shape [ConstSize 0]) Unique
pure $ ArrayLit [] (Info t) loc
e : es -> do
e' <- checkExp e
et <- expType e'
es' <- mapM (unifies "type of first array element" (toStruct et) <=< checkExp) es
et' <- normTypeFully et
t <- arrayOfM loc et' (Shape [ConstSize $ length all_es]) Unique
pure $ ArrayLit (e' : es') (Info t) loc
checkExp (AppExp (Range start maybe_step end loc) _) = do
start' <- require "use in range expression" anySignedType =<< checkExp start
start_t <- toStruct <$> expTypeFully start'
maybe_step' <- case maybe_step of
Nothing -> pure Nothing
Just step -> do
let warning = warn loc "First and second element of range are identical, this will produce an empty array."
case (start, step) of
(Literal x _, Literal y _) -> when (x == y) warning
(Var x_name _ _, Var y_name _ _) -> when (x_name == y_name) warning
_ -> pure ()
Just <$> (unifies "use in range expression" start_t =<< checkExp step)
let unifyRange e = unifies "use in range expression" start_t =<< checkExp e
end' <- traverse unifyRange end
end_t <- case end' of
DownToExclusive e -> expType e
ToInclusive e -> expType e
UpToExclusive e -> expType e
-- Special case some ranges to give them a known size.
let dimFromBound = dimFromExp (SourceBound . bareExp)
(dim, retext) <-
case (isInt64 start', isInt64 <$> maybe_step', end') of
(Just 0, Just (Just 1), UpToExclusive end'')
| Scalar (Prim (Signed Int64)) <- end_t ->
dimFromBound end''
(Just 0, Nothing, UpToExclusive end'')
| Scalar (Prim (Signed Int64)) <- end_t ->
dimFromBound end''
(Just 1, Just (Just 2), ToInclusive end'')
| Scalar (Prim (Signed Int64)) <- end_t ->
dimFromBound end''
_ -> do
d <- newDimVar loc (Rigid RigidRange) "range_dim"
pure (NamedSize $ qualName d, Just d)
t <- arrayOfM loc start_t (Shape [dim]) Unique
let res = AppRes (t `setAliases` mempty) (maybeToList retext)
pure $ AppExp (Range start' maybe_step' end' loc) (Info res)
checkExp (Ascript e te loc) = do
(te', e') <- checkAscript loc te e
pure $ Ascript e' te' loc
checkExp (AppExp (Coerce e te loc) _) = do
(te', te_t, e', ext) <- checkCoerce loc te e
t <- expTypeFully e'
t' <- matchDims (const . const pure) t $ fromStruct te_t
pure $ AppExp (Coerce e' te' loc) (Info $ AppRes t' ext)
checkExp (AppExp (BinOp (op, oploc) NoInfo (e1, _) (e2, _) loc) NoInfo) = do
(op', ftype) <- lookupVar oploc op
e1_arg <- checkArg e1
e2_arg <- checkArg e2
-- Note that the application to the first operand cannot fix any
-- existential sizes, because it must by necessity be a function.
(p1_t, rt, p1_ext, _) <- checkApply loc (Just op', 0) ftype e1_arg
(p2_t, rt', p2_ext, retext) <- checkApply loc (Just op', 1) rt e2_arg
pure $
AppExp
( BinOp
(op', oploc)
(Info ftype)
(argExp e1_arg, Info (toStruct p1_t, p1_ext))
(argExp e2_arg, Info (toStruct p2_t, p2_ext))
loc
)
(Info (AppRes rt' retext))
checkExp (Project k e NoInfo loc) = do
e' <- checkExp e
t <- expType e'
kt <- mustHaveField (mkUsage loc $ docText $ "projection of field " <> dquotes (pretty k)) k t
pure $ Project k e' (Info kt) loc
checkExp (AppExp (If e1 e2 e3 loc) _) =
sequentially checkCond $ \e1' _ -> do
((e2', e3'), dflow) <- tapOccurrences $ checkExp e2 `alternative` checkExp e3
(brancht, retext) <- unifyBranches loc e2' e3'
let t' = addAliases brancht $ S.filter $ (`S.notMember` allConsumed dflow) . aliasVar
zeroOrderType
(mkUsage loc "returning value of this type from 'if' expression")
"type returned from branch"
t'
pure $ AppExp (If e1' e2' e3' loc) (Info $ AppRes t' retext)
where
checkCond = do
e1' <- checkExp e1
let bool = Scalar $ Prim Bool
e1_t <- toStruct <$> expType e1'
onFailure (CheckingRequired [bool] e1_t) $
unify (mkUsage (srclocOf e1') "use as 'if' condition") bool e1_t
pure e1'
checkExp (Parens e loc) =
Parens <$> checkExp e <*> pure loc
checkExp (QualParens (modname, modnameloc) e loc) = do
(modname', mod) <- lookupMod loc modname
case mod of
ModEnv env -> local (`withEnv` qualifyEnv modname' env) $ do
e' <- checkExp e
pure $ QualParens (modname', modnameloc) e' loc
ModFun {} ->
typeError loc mempty . withIndexLink "module-is-parametric" $
"Module" <+> pretty modname <+> " is a parametric module."
where
qualifyEnv modname' env =
env {envNameMap = M.map (qualify' modname') $ envNameMap env}
qualify' modname' (QualName qs name) =
QualName (qualQuals modname' ++ [qualLeaf modname'] ++ qs) name
checkExp (Var qn NoInfo loc) = do
-- The qualifiers of a variable is divided into two parts: first a
-- possibly-empty sequence of module qualifiers, followed by a
-- possible-empty sequence of record field accesses. We use scope
-- information to perform the split, by taking qualifiers off the
-- end until we find a module.
(qn', t, fields) <- findRootVar (qualQuals qn) (qualLeaf qn)
foldM checkField (Var qn' (Info t) loc) fields
where
findRootVar qs name =
(whenFound <$> lookupVar loc (QualName qs name)) `catchError` notFound qs name
whenFound (qn', t) = (qn', t, [])
notFound qs name err
| null qs = throwError err
| otherwise = do
(qn', t, fields) <-
findRootVar (init qs) (last qs)
`catchError` const (throwError err)
pure (qn', t, fields ++ [name])
checkField e k = do
t <- expType e
let usage = mkUsage loc $ docText $ "projection of field " <> dquotes (pretty k)
kt <- mustHaveField usage k t
pure $ Project k e (Info kt) loc
checkExp (Negate arg loc) = do
arg' <- require "numeric negation" anyNumberType =<< checkExp arg
pure $ Negate arg' loc
checkExp (Not arg loc) = do
arg' <- require "logical negation" (Bool : anyIntType) =<< checkExp arg
pure $ Not arg' loc
checkExp e@(AppExp Apply {} _) = fst <$> checkApplyExp e
checkExp (AppExp (LetPat sizes pat e body loc) _) =
sequentially (checkExp e) $ \e' e_occs -> do
-- Not technically an ascription, but we want the pattern to have
-- exactly the type of 'e'.
t <- expType e'
case anyConsumption e_occs of
Just c ->
let msg = "type computed with consumption at " <> locText (location c)
in zeroOrderType (mkUsage loc "consumption in right-hand side of 'let'-binding") msg t
_ -> pure ()
incLevel . bindingSizes sizes $ \sizes' ->
bindingPat sizes' pat (Ascribed t) $ \pat' -> do
body' <- checkExp body
(body_t, retext) <-
unscopeType loc (sizesMap sizes' <> patternMap pat') =<< expTypeFully body'
pure $ AppExp (LetPat sizes' pat' e' body' loc) (Info $ AppRes body_t retext)
where
sizesMap = foldMap onSize
onSize size =
M.singleton (sizeName size) $
Ident (sizeName size) (Info (Scalar $ Prim $ Signed Int64)) (srclocOf size)
checkExp (AppExp (LetFun name (tparams, params, maybe_retdecl, NoInfo, e) body loc) _) =
sequentially (checkBinding (name, maybe_retdecl, tparams, params, e, loc)) $
\(tparams', params', maybe_retdecl', rettype, e') closure -> do
closure' <- lexicalClosure params' closure
bindSpaced [(Term, name)] $ do
name' <- checkName Term name loc
let arrow (xp, xt) yt = RetType [] $ Scalar $ Arrow () xp xt yt
RetType _ ftype = foldr (arrow . patternParam) rettype params'
entry = BoundV Local tparams' $ ftype `setAliases` closure'
bindF scope =
scope
{ scopeVtable =
M.insert name' entry $ scopeVtable scope,
scopeNameMap =
M.insert (Term, name) (qualName name') $
scopeNameMap scope
}
body' <- localScope bindF $ checkExp body
-- We fake an ident here, but it's OK as it can't be a size
-- anyway.
let fake_ident = Ident name' (Info $ fromStruct ftype) mempty
(body_t, ext) <-
unscopeType loc (M.singleton name' fake_ident)
=<< expTypeFully body'
pure $
AppExp
( LetFun
name'
(tparams', params', maybe_retdecl', Info rettype, e')
body'
loc
)
(Info $ AppRes body_t ext)
checkExp (AppExp (LetWith dest src slice ve body loc) _) =
sequentially (checkIdent src) $ \src' _ -> do
slice' <- checkSlice slice
(t, _) <- newArrayType (srclocOf src) "src" $ sliceDims slice'
unify (mkUsage loc "type of target array") t $ toStruct $ unInfo $ identType src'
-- Need the fully normalised type here to get the proper aliasing information.
src_t <- normTypeFully $ unInfo $ identType src'
(elemt, _) <- sliceShape (Just (loc, Nonrigid)) slice' =<< normTypeFully t
sequentially (unifies "type of target array" (toStruct elemt) =<< checkExp ve) $ \ve' _ -> do
ve_t <- expTypeFully ve'
when (AliasBound (identName src') `S.member` aliases ve_t) $
badLetWithValue src ve loc
bindingIdent dest (src_t `setAliases` S.empty) $ \dest' -> do
body' <- consuming src' $ checkExp body
(body_t, ext) <-
unscopeType loc (M.singleton (identName dest') dest')
=<< expTypeFully body'
pure $ AppExp (LetWith dest' src' slice' ve' body' loc) (Info $ AppRes body_t ext)
checkExp (Update src slice ve loc) = do
slice' <- checkSlice slice
(t, _) <- newArrayType (srclocOf src) "src" $ sliceDims slice'
(elemt, _) <- sliceShape (Just (loc, Nonrigid)) slice' =<< normTypeFully t
sequentially (checkExp ve >>= unifies "type of target array" elemt) $ \ve' _ ->
sequentially (checkExp src >>= unifies "type of target array" t) $ \src' _ -> do
src_t <- expTypeFully src'
let src_als = aliases src_t
ve_t <- expTypeFully ve'
unless (S.null $ src_als `S.intersection` aliases ve_t) $ badLetWithValue src ve loc
consume loc src_als
pure $ Update src' slice' ve' loc
-- Record updates are a bit hacky, because we do not have row typing
-- (yet?). For now, we only permit record updates where we know the
-- full type up to the field we are updating.
checkExp (RecordUpdate src fields ve NoInfo loc) = do
src' <- checkExp src
ve' <- checkExp ve
a <- expTypeFully src'
foldM_ (flip $ mustHaveField usage) a fields
ve_t <- expType ve'
updated_t <- updateField fields ve_t =<< expTypeFully src'
pure $ RecordUpdate src' fields ve' (Info updated_t) loc
where
usage = mkUsage loc "record update"
updateField [] ve_t src_t = do
(src_t', _) <- allDimsFreshInType loc Nonrigid "any" src_t
onFailure (CheckingRecordUpdate fields (toStruct src_t') (toStruct ve_t)) $
unify usage (toStruct src_t') (toStruct ve_t)
-- Important that we return ve_t so that we get the right aliases.
pure ve_t
updateField (f : fs) ve_t (Scalar (Record m))
| Just f_t <- M.lookup f m = do
f_t' <- updateField fs ve_t f_t
pure $ Scalar $ Record $ M.insert f f_t' m
updateField _ _ _ =
typeError loc mempty . withIndexLink "record-type-not-known" $
"Full type of"
</> indent 2 (pretty src)
</> textwrap " is not known at this point. Add a type annotation to the original record to disambiguate."
--
checkExp (AppExp (Index e slice loc) _) = do
slice' <- checkSlice slice
(t, _) <- newArrayType loc "e" $ sliceDims slice'
e' <- unifies "being indexed at" t =<< checkExp e
-- XXX, the RigidSlice here will be overridden in sliceShape with a proper value.
(t', retext) <-
sliceShape (Just (loc, Rigid (RigidSlice Nothing ""))) slice'
=<< expTypeFully e'
-- Remove aliases if the result is an overloaded type, because that
-- will certainly not be aliased.
t'' <- noAliasesIfOverloaded t'
pure $ AppExp (Index e' slice' loc) (Info $ AppRes t'' retext)
checkExp (Assert e1 e2 NoInfo loc) = do
e1' <- require "being asserted" [Bool] =<< checkExp e1
e2' <- checkExp e2
pure $ Assert e1' e2' (Info (prettyText e1)) loc
checkExp (Lambda params body rettype_te NoInfo loc) = do
(params', body', body_t, rettype', info) <-
removeSeminullOccurrences . noUnique . incLevel . bindingParams [] params $ \_ params' -> do
rettype_checked <- traverse checkTypeExpNonrigid rettype_te
let declared_rettype =
case rettype_checked of
Just (_, st, _) -> Just st
Nothing -> Nothing
(body', closure) <-
tapOccurrences $ checkFunBody params' body declared_rettype loc
body_t <- expTypeFully body'
params'' <- mapM updateTypes params'
(rettype', rettype_st) <-
case rettype_checked of
Just (te, st, ext) -> do
let st_structural = toStructural st
checkReturnAlias loc st_structural params'' body_t
pure (Just te, RetType ext st)
Nothing -> do
ret <-
inferReturnSizes params'' . toStruct $
inferReturnUniqueness params'' body_t
pure (Nothing, ret)
closure' <- lexicalClosure params'' closure
pure (params'', body', body_t, rettype', Info (closure', rettype_st))
checkGlobalAliases params' body_t loc
verifyFunctionParams Nothing params'
pure $ Lambda params' body' rettype' info loc
where
-- Inferring the sizes of the return type of a lambda is a lot
-- like let-generalisation. We wish to remove any rigid sizes
-- that were created when checking the body, except for those that
-- are visible in types that existed before we entered the body,
-- are parameters, or are used in parameters.
inferReturnSizes params' ret = do
cur_lvl <- curLevel
let named (Named x, _) = Just x
named (Unnamed, _) = Nothing
param_names = mapMaybe (named . patternParam) params'
pos_sizes =
sizeNamesPos . foldFunType (map patternStructType params') $
RetType [] ret
hide k (lvl, _) =
lvl >= cur_lvl && k `notElem` param_names && k `S.notMember` pos_sizes
hidden_sizes <-
S.fromList . M.keys . M.filterWithKey hide <$> getConstraints
let onDim name
| name `S.member` hidden_sizes = S.singleton name
onDim _ = mempty
pure $ RetType (S.toList $ foldMap onDim $ freeInType ret) ret
checkExp (OpSection op _ loc) = do
(op', ftype) <- lookupVar loc op
pure $ OpSection op' (Info ftype) loc
checkExp (OpSectionLeft op _ e _ _ loc) = do
(op', ftype) <- lookupVar loc op
e_arg <- checkArg e
(t1, rt, argext, retext) <- checkApply loc (Just op', 0) ftype e_arg
case (ftype, rt) of
(Scalar (Arrow _ m1 _ _), Scalar (Arrow _ m2 t2 rettype)) ->
pure $
OpSectionLeft
op'
(Info ftype)
(argExp e_arg)
(Info (m1, toStruct t1, argext), Info (m2, toStruct t2))
(Info rettype, Info retext)
loc
_ ->
typeError loc mempty $
"Operator section with invalid operator of type" <+> pretty ftype
checkExp (OpSectionRight op _ e _ NoInfo loc) = do
(op', ftype) <- lookupVar loc op
e_arg <- checkArg e
case ftype of
Scalar (Arrow as1 m1 t1 (RetType [] (Scalar (Arrow as2 m2 t2 (RetType dims2 ret))))) -> do
(t2', ret', argext, _) <-
checkApply
loc
(Just op', 1)
(Scalar $ Arrow as2 m2 t2 $ RetType [] $ Scalar $ Arrow as1 m1 t1 $ RetType [] ret)
e_arg
pure $
OpSectionRight
op'
(Info ftype)
(argExp e_arg)
(Info (m1, toStruct t1), Info (m2, toStruct t2', argext))
(Info $ RetType dims2 $ addAliases ret (<> aliases ret'))
loc
_ ->
typeError loc mempty $
"Operator section with invalid operator of type" <+> pretty ftype
checkExp (ProjectSection fields NoInfo loc) = do
a <- newTypeVar loc "a"
let usage = mkUsage loc "projection at"
b <- foldM (flip $ mustHaveField usage) a fields
let ft = Scalar $ Arrow mempty Unnamed (toStruct a) $ RetType [] b
pure $ ProjectSection fields (Info ft) loc
checkExp (IndexSection slice NoInfo loc) = do
slice' <- checkSlice slice
(t, _) <- newArrayType loc "e" $ sliceDims slice'
(t', retext) <- sliceShape Nothing slice' t
let ft = Scalar $ Arrow mempty Unnamed t $ RetType retext $ fromStruct t'
pure $ IndexSection slice' (Info ft) loc
checkExp (AppExp (DoLoop _ mergepat mergeexp form loopbody loc) _) = do
((sparams, mergepat', mergeexp', form', loopbody'), appres) <-
checkDoLoop checkExp (mergepat, mergeexp, form, loopbody) loc
pure $
AppExp
(DoLoop sparams mergepat' mergeexp' form' loopbody' loc)
(Info appres)
checkExp (Constr name es NoInfo loc) = do
t <- newTypeVar loc "t"
es' <- mapM checkExp es
ets <- mapM expTypeFully es'
mustHaveConstr (mkUsage loc "use of constructor") name t (toStruct <$> ets)
-- A sum value aliases *anything* that went into its construction.
let als = foldMap aliases ets
pure $ Constr name es' (Info $ fromStruct t `addAliases` (<> als)) loc
checkExp (AppExp (Match e cs loc) _) =
sequentially (checkExp e) $ \e' _ -> do
mt <- expTypeFully e'
(cs', t, retext) <- checkCases mt cs
zeroOrderType
(mkUsage loc "being returned 'match'")
"type returned from pattern match"
t
pure $ AppExp (Match e' cs' loc) (Info $ AppRes t retext)
checkExp (Attr info e loc) =
Attr <$> checkAttr info <*> checkExp e <*> pure loc
checkCases ::
PatType ->
NE.NonEmpty (CaseBase NoInfo Name) ->
TermTypeM (NE.NonEmpty (CaseBase Info VName), PatType, [VName])
checkCases mt rest_cs =
case NE.uncons rest_cs of
(c, Nothing) -> do
(c', t, retext) <- checkCase mt c
pure (NE.singleton c', t, retext)
(c, Just cs) -> do
(((c', c_t, _), (cs', cs_t, _)), dflow) <-
tapOccurrences $ checkCase mt c `alternative` checkCases mt cs
(brancht, retext) <- unifyBranchTypes (srclocOf c) c_t cs_t
let t =
addAliases
brancht
(`S.difference` S.map AliasBound (allConsumed dflow))
pure (NE.cons c' cs', t, retext)
checkCase ::
PatType ->
CaseBase NoInfo Name ->
TermTypeM (CaseBase Info VName, PatType, [VName])
checkCase mt (CasePat p e loc) =
bindingPat [] p (Ascribed mt) $ \p' -> do
e' <- checkExp e
(t, retext) <- unscopeType loc (patternMap p') =<< expTypeFully e'
pure (CasePat p' e' loc, t, retext)
-- | An unmatched pattern. Used in in the generation of
-- unmatched pattern warnings by the type checker.
data Unmatched p
= UnmatchedNum p [PatLit]
| UnmatchedBool p
| UnmatchedConstr p
| Unmatched p
deriving (Functor, Show)
instance Pretty (Unmatched (PatBase Info VName)) where
pretty um = case um of
(UnmatchedNum p nums) -> pretty' p <+> "where p is not one of" <+> pretty nums
(UnmatchedBool p) -> pretty' p
(UnmatchedConstr p) -> pretty' p
(Unmatched p) -> pretty' p
where
pretty' (PatAscription p t _) = pretty p <> ":" <+> pretty t
pretty' (PatParens p _) = parens $ pretty' p
pretty' (PatAttr _ p _) = parens $ pretty' p
pretty' (Id v _ _) = prettyName v
pretty' (TuplePat pats _) = parens $ commasep $ map pretty' pats
pretty' (RecordPat fs _) = braces $ commasep $ map ppField fs
where
ppField (name, t) = pretty (nameToString name) <> equals <> pretty' t
pretty' Wildcard {} = "_"
pretty' (PatLit e _ _) = pretty e
pretty' (PatConstr n _ ps _) = "#" <> pretty n <+> sep (map pretty' ps)
checkIdent :: IdentBase NoInfo Name -> TermTypeM Ident
checkIdent (Ident name _ loc) = do
(QualName _ name', vt) <- lookupVar loc (qualName name)
pure $ Ident name' (Info vt) loc
checkSlice :: UncheckedSlice -> TermTypeM Slice
checkSlice = mapM checkDimIndex
where
checkDimIndex (DimFix i) =
DimFix <$> (require "use as index" anySignedType =<< checkExp i)
checkDimIndex (DimSlice i j s) =
DimSlice <$> check i <*> check j <*> check s
check =
maybe (pure Nothing) $
fmap Just . unifies "use as index" (Scalar $ Prim $ Signed Int64) <=< checkExp
-- The number of dimensions affected by this slice (so the minimum
-- rank of the array we are slicing).
sliceDims :: Slice -> Int
sliceDims = length
type Arg = (Exp, PatType, Occurrences, SrcLoc)
argExp :: Arg -> Exp
argExp (e, _, _, _) = e
argType :: Arg -> PatType
argType (_, t, _, _) = t
checkArg :: UncheckedExp -> TermTypeM Arg
checkArg arg = do
(arg', dflow) <- collectOccurrences $ checkExp arg
arg_t <- expType arg'
pure (arg', arg_t, dflow, srclocOf arg')
instantiateDimsInReturnType ::
SrcLoc ->
Maybe (QualName VName) ->
RetTypeBase Size als ->
TermTypeM (TypeBase Size als, [VName])
instantiateDimsInReturnType tloc fname =
instantiateEmptyArrayDims tloc $ Rigid $ RigidRet fname
-- Some information about the function/operator we are trying to
-- apply, and how many arguments it has previously accepted. Used for
-- generating nicer type errors.
type ApplyOp = (Maybe (QualName VName), Int)
-- | Extract all those names that are bound inside the type.
boundInsideType :: TypeBase Size as -> S.Set VName
boundInsideType (Array _ _ _ t) = boundInsideType (Scalar t)
boundInsideType (Scalar Prim {}) = mempty
boundInsideType (Scalar (TypeVar _ _ _ targs)) = foldMap f targs
where
f (TypeArgType t _) = boundInsideType t
f TypeArgDim {} = mempty
boundInsideType (Scalar (Record fs)) = foldMap boundInsideType fs
boundInsideType (Scalar (Sum cs)) = foldMap (foldMap boundInsideType) cs
boundInsideType (Scalar (Arrow _ pn t1 (RetType dims t2))) =
pn' <> boundInsideType t1 <> S.fromList dims <> boundInsideType t2
where
pn' = case pn of
Unnamed -> mempty
Named v -> S.singleton v
-- Returns the sizes of the immediate type produced,
-- the sizes of parameter types, and the sizes of return types.
dimUses :: StructType -> (Names, Names)
dimUses = flip execState mempty . traverseDims f
where
f bound _ (NamedSize v) | qualLeaf v `S.member` bound = pure ()
f _ PosImmediate (NamedSize v) = modify ((S.singleton (qualLeaf v), mempty) <>)
f _ PosParam (NamedSize v) = modify ((mempty, S.singleton (qualLeaf v)) <>)
f _ _ _ = pure ()
checkApply ::
SrcLoc ->
ApplyOp ->
PatType ->
Arg ->
TermTypeM (StructType, PatType, Maybe VName, [VName])
checkApply
loc
(fname, _)
(Scalar (Arrow as pname tp1 tp2))
(argexp, argtype, dflow, argloc) =
onFailure (CheckingApply fname argexp tp1 (toStruct argtype)) $ do
expect (mkUsage argloc "use as function argument") (toStruct tp1) (toStruct argtype)
-- Perform substitutions of instantiated variables in the types.
tp1' <- normTypeFully tp1
(tp2', ext) <- instantiateDimsInReturnType loc fname =<< normTypeFully tp2
argtype' <- normTypeFully argtype
-- Check whether this would produce an impossible return type.
let (tp2_produced_dims, tp2_paramdims) = dimUses $ toStruct tp2'
problematic = S.fromList ext <> boundInsideType argtype'
when (any (`S.member` problematic) (tp2_paramdims `S.difference` tp2_produced_dims)) $ do
typeError loc mempty . withIndexLink "existential-param-ret" $
"Existential size would appear in function parameter of return type:"
</> indent 2 (pretty (RetType ext tp2'))
</> textwrap "This is usually because a higher-order function is used with functional arguments that return existential sizes or locally named sizes, which are then used as parameters of other function arguments."
occur [observation as loc]
checkOccurrences dflow
case anyConsumption dflow of
Just c ->
let msg = "type of expression with consumption at " <> locText (location c)
in zeroOrderType (mkUsage argloc "potential consumption in expression") msg tp1
_ -> pure ()
occurs <- (dflow `seqOccurrences`) <$> consumeArg argloc argtype' (diet tp1')
checkIfConsumable loc $ S.map AliasBound $ allConsumed occurs
occur occurs
-- Unification ignores uniqueness in higher-order arguments, so
-- we check for that here.
unless (toStructural argtype' `subtypeOf` setUniqueness (toStructural tp1') Nonunique) $
typeError loc mempty "Consumption/aliasing does not match."
(argext, parsubst) <-
case pname of
Named pname'
| (Scalar (Prim (Signed Int64))) <- tp1' -> do
(d, argext) <- sizeFromArg fname argexp
pure
( argext,
(`M.lookup` M.singleton pname' (SizeSubst d))
)
_ -> pure (Nothing, const Nothing)
-- In case a function result is not immediately bound to a name,
-- we need to invent a name for it so we can track it during
-- aliasing (uniqueness-error54.fut, uniqueness-error55.fut,
-- uniqueness-error60.fut).
v <- newID "internal_app_result"
modify $ \s -> s {stateNames = M.insert v (NameAppRes fname loc) $ stateNames s}
let appres = S.singleton $ AliasFree v
let tp2'' = applySubst parsubst $ returnType appres tp2' (diet tp1') argtype'
pure (tp1', tp2'', argext, ext)
checkApply loc fname tfun@(Scalar TypeVar {}) arg = do
tv <- newTypeVar loc "b"
-- Change the uniqueness of the argument type because we never want
-- to infer that a function is consuming.
let argt_nonunique = toStruct (argType arg) `setUniqueness` Nonunique
unify (mkUsage loc "use as function") (toStruct tfun) $
Scalar $
Arrow mempty Unnamed argt_nonunique $
RetType [] tv
tfun' <- normPatType tfun
checkApply loc fname tfun' arg
checkApply loc (fname, prev_applied) ftype (argexp, _, _, _) = do
let fname' = maybe "expression" (dquotes . pretty) fname
typeError loc mempty $
if prev_applied == 0
then
"Cannot apply"
<+> fname'
<+> "as function, as it has type:"
</> indent 2 (pretty ftype)
else
"Cannot apply"
<+> fname'
<+> "to argument #" <> pretty (prev_applied + 1)
<+> dquotes (shorten $ group $ pretty argexp) <> ","
</> "as"
<+> fname'
<+> "only takes"
<+> pretty prev_applied
<+> arguments <> "."
where
arguments
| prev_applied == 1 = "argument"
| otherwise = "arguments"
-- | @returnType appres ret_type arg_diet arg_type@ gives result of applying
-- an argument the given types to a function with the given return
-- type, consuming the argument with the given diet.
returnType ::
Aliasing ->
PatType ->
Diet ->
PatType ->
PatType
returnType _ (Array _ Unique et shape) _ _ =
Array mempty Nonunique et shape -- Intentional!
returnType appres (Array als Nonunique et shape) d arg =
Array (appres <> als <> arg_als) Nonunique et shape
where
arg_als = aliases $ maskAliases arg d
returnType appres (Scalar (Record fs)) d arg =
Scalar $ Record $ fmap (\et -> returnType appres et d arg) fs
returnType _ (Scalar (Prim t)) _ _ =
Scalar $ Prim t
returnType _ (Scalar (TypeVar _ Unique t targs)) _ _ =
Scalar $ TypeVar mempty Nonunique t targs -- Intentional!
returnType appres (Scalar (TypeVar als Nonunique t targs)) d arg =
Scalar $ TypeVar (appres <> als <> arg_als) Unique t targs
where
arg_als = aliases $ maskAliases arg d
returnType _ (Scalar (Arrow old_als v t1 (RetType dims t2))) d arg =
Scalar $ Arrow als v (t1 `setAliases` mempty) $ RetType dims $ t2 `setAliases` als
where
-- Make sure to propagate the aliases of an existing closure.
als = old_als <> aliases (maskAliases arg d)
returnType appres (Scalar (Sum cs)) d arg =
Scalar $ Sum $ (fmap . fmap) (\et -> returnType appres et d arg) cs
-- @t `maskAliases` d@ removes aliases (sets them to 'mempty') from
-- the parts of @t@ that are denoted as consumed by the 'Diet' @d@.
maskAliases ::
Monoid as =>
TypeBase shape as ->
Diet ->
TypeBase shape as
maskAliases t Consume = t `setAliases` mempty
maskAliases t Observe = t
maskAliases (Scalar (Record ets)) (RecordDiet ds) =
Scalar $ Record $ M.intersectionWith maskAliases ets ds
maskAliases (Scalar (Sum ets)) (SumDiet ds) =
Scalar $ Sum $ M.intersectionWith (zipWith maskAliases) ets ds
maskAliases t FuncDiet {} = t
maskAliases _ _ = error "Invalid arguments passed to maskAliases."
consumeArg :: SrcLoc -> PatType -> Diet -> TermTypeM [Occurrence]
consumeArg loc (Scalar (Record ets)) (RecordDiet ds) =
concat . M.elems <$> traverse (uncurry $ consumeArg loc) (M.intersectionWith (,) ets ds)
consumeArg loc (Scalar (Sum ets)) (SumDiet ds) =
concat <$> traverse (uncurry $ consumeArg loc) (concat $ M.elems $ M.intersectionWith zip ets ds)
consumeArg loc (Scalar (Arrow _ _ t1 _)) (FuncDiet d _)
| not $ contravariantArg t1 d =
typeError loc mempty . withIndexLink "consuming-argument" $
"Non-consuming higher-order parameter passed consuming argument."
where
contravariantArg (Array _ Unique _ _) Observe =
False
contravariantArg (Scalar (TypeVar _ Unique _ _)) Observe =
False
contravariantArg (Scalar (Record ets)) (RecordDiet ds) =
and (M.intersectionWith contravariantArg ets ds)
contravariantArg (Scalar (Arrow _ _ tp (RetType _ tr))) (FuncDiet dp dr) =
contravariantArg tp dp && contravariantArg tr dr
contravariantArg _ _ =
True
consumeArg loc at Consume = pure [consumption (aliases at) loc]
consumeArg loc at _ = pure [observation (aliases at) loc]
-- | Type-check a single expression in isolation. This expression may
-- turn out to be polymorphic, in which case the list of type
-- parameters will be non-empty.
checkOneExp :: UncheckedExp -> TypeM ([TypeParam], Exp)
checkOneExp e = fmap fst . runTermTypeM $ do
e' <- checkExp e
let t = toStruct $ typeOf e'
(tparams, _, _) <-
letGeneralise (nameFromString "<exp>") (srclocOf e) [] [] t
fixOverloadedTypes $ typeVars t
e'' <- updateTypes e'
localChecks e''
causalityCheck e''
pure (tparams, e'')
-- Verify that all sum type constructors and empty array literals have
-- a size that is known (rigid or a type parameter). This is to
-- ensure that we can actually determine their shape at run-time.
causalityCheck :: Exp -> TermTypeM ()
causalityCheck binding_body = do
constraints <- getConstraints
let checkCausality what known t loc
| (d, dloc) : _ <-
mapMaybe (unknown constraints known) $
S.toList $
freeInType $
toStruct t =
Just $ lift $ causality what (locOf loc) d dloc t
| otherwise = Nothing
checkParamCausality known p =
checkCausality (pretty p) known (patternType p) (locOf p)
onExp ::
S.Set VName ->
Exp ->
StateT (S.Set VName) (Either TypeError) Exp
onExp known (Var v (Info t) loc)
| Just bad <- checkCausality (dquotes (pretty v)) known t loc =
bad
onExp known (ProjectSection _ (Info t) loc)
| Just bad <- checkCausality "projection section" known t loc =
bad
onExp known (IndexSection _ (Info t) loc)
| Just bad <- checkCausality "projection section" known t loc =
bad
onExp known (OpSectionRight _ (Info t) _ _ _ loc)
| Just bad <- checkCausality "operator section" known t loc =
bad
onExp known (OpSectionLeft _ (Info t) _ _ _ loc)
| Just bad <- checkCausality "operator section" known t loc =
bad
onExp known (ArrayLit [] (Info t) loc)
| Just bad <- checkCausality "empty array" known t loc =
bad
onExp known (Hole (Info t) loc)
| Just bad <- checkCausality "hole" known t loc =
bad
onExp known (Lambda params _ _ _ _)
| bad : _ <- mapMaybe (checkParamCausality known) params =
bad
onExp known e@(AppExp (LetPat _ _ bindee_e body_e _) (Info res)) = do
sequencePoint known bindee_e body_e $ appResExt res
pure e
onExp known e@(AppExp (Apply f arg (Info (_, p)) _) (Info res)) = do
sequencePoint known arg f $ maybeToList p ++ appResExt res
pure e
onExp
known
e@(AppExp (BinOp (f, floc) ft (x, Info (_, xp)) (y, Info (_, yp)) _) (Info res)) = do
args_known <-
lift $
execStateT (sequencePoint known x y $ catMaybes [xp, yp]) mempty
void $ onExp (args_known <> known) (Var f ft floc)
modify ((args_known <> S.fromList (appResExt res)) <>)
pure e
onExp known e@(AppExp e' (Info res)) = do
recurse known e'
modify (<> S.fromList (appResExt res))
pure e
onExp known e = do
recurse known e
pure e
recurse known = void . astMap mapper
where
mapper = identityMapper {mapOnExp = onExp known}
sequencePoint known x y ext = do
new_known <- lift $ execStateT (onExp known x) mempty
void $ onExp (new_known <> known) y
modify ((new_known <> S.fromList ext) <>)
either throwError (const $ pure ()) $
evalStateT (onExp mempty binding_body) mempty
where
unknown constraints known v = do
guard $ v `S.notMember` known
loc <- unknowable constraints v
pure (v, loc)
unknowable constraints v =
case snd <$> M.lookup v constraints of
Just (UnknowableSize loc _) -> Just loc
_ -> Nothing
causality what loc d dloc t =
Left . TypeError loc mempty . withIndexLink "causality-check" $
"Causality check: size"
</> dquotes (prettyName d)
</> "needed for type of"
<+> what <> colon
</> indent 2 (pretty t)
</> "But"
<+> dquotes (prettyName d)
<+> "is computed at"
</> pretty (locStrRel loc dloc) <> "."
</> ""
</> "Hint:"
<+> align
( textwrap "Bind the expression producing"
<+> dquotes (prettyName d)
<+> "with 'let' beforehand."
)
-- | Traverse the expression, emitting warnings and errors for various
-- problems:
--
-- * Unmatched cases.
--
-- * If any of the literals overflow their inferred types. Note:
-- currently unable to detect float underflow (such as 1e-400 -> 0)
localChecks :: Exp -> TermTypeM ()
localChecks = void . check
where
check e@(AppExp (Match _ cs loc) _) = do
let ps = fmap (\(CasePat p _ _) -> p) cs
case unmatched $ NE.toList ps of
[] -> recurse e
ps' ->
typeError loc mempty . withIndexLink "unmatched-cases" $
"Unmatched cases in match expression:"
</> indent 2 (stack (map pretty ps'))
check e@(IntLit x ty loc) =
e <$ case ty of
Info (Scalar (Prim t)) -> errorBounds (inBoundsI x t) x t loc
_ -> error "Inferred type of int literal is not a number"
check e@(FloatLit x ty loc) =
e <$ case ty of
Info (Scalar (Prim (FloatType t))) -> errorBounds (inBoundsF x t) x t loc
_ -> error "Inferred type of float literal is not a float"
check e@(Negate (IntLit x ty loc1) loc2) =
e <$ case ty of
Info (Scalar (Prim t)) -> errorBounds (inBoundsI (-x) t) (-x) t (loc1 <> loc2)
_ -> error "Inferred type of int literal is not a number"
check e@(AppExp (BinOp (QualName [] v, _) _ (_, Info (Array {}, _)) _ loc) _)
| baseName v == "==",
baseTag v <= maxIntrinsicTag = do
warn loc $
textwrap
"Comparing arrays with \"==\" is deprecated and will stop working in a future revision of the language."
recurse e
check e = recurse e
recurse = astMap identityMapper {mapOnExp = check}
bitWidth ty = 8 * intByteSize ty :: Int
inBoundsI x (Signed t) = x >= -2 ^ (bitWidth t - 1) && x < 2 ^ (bitWidth t - 1)
inBoundsI x (Unsigned t) = x >= 0 && x < 2 ^ bitWidth t
inBoundsI x (FloatType Float16) = not $ isInfinite (fromIntegral x :: Half)
inBoundsI x (FloatType Float32) = not $ isInfinite (fromIntegral x :: Float)
inBoundsI x (FloatType Float64) = not $ isInfinite (fromIntegral x :: Double)
inBoundsI _ Bool = error "Inferred type of int literal is not a number"
inBoundsF x Float16 = not $ isInfinite (realToFrac x :: Float)
inBoundsF x Float32 = not $ isInfinite (realToFrac x :: Float)
inBoundsF x Float64 = not $ isInfinite x
errorBounds inBounds x ty loc =
unless inBounds $
typeError loc mempty . withIndexLink "literal-out-of-bounds" $
"Literal "
<> pretty x
<> " out of bounds for inferred type "
<> pretty ty
<> "."
-- | Type-check a top-level (or module-level) function definition.
-- Despite the name, this is also used for checking constant
-- definitions, by treating them as 0-ary functions.
checkFunDef ::
( Name,
Maybe UncheckedTypeExp,
[UncheckedTypeParam],
[UncheckedPat],
UncheckedExp,
SrcLoc
) ->
TypeM
( VName,
[TypeParam],
[Pat],
Maybe (TypeExp VName),
StructRetType,
Exp
)
checkFunDef (fname, maybe_retdecl, tparams, params, body, loc) =
fmap fst . runTermTypeM $ do
(tparams', params', maybe_retdecl', RetType dims rettype', body') <-
checkBinding (fname, maybe_retdecl, tparams, params, body, loc)
-- Since this is a top-level function, we also resolve overloaded
-- types, using either defaults or complaining about ambiguities.
fixOverloadedTypes $
typeVars rettype' <> foldMap (typeVars . patternType) params'
-- Then replace all inferred types in the body and parameters.
body'' <- updateTypes body'
params'' <- updateTypes params'
maybe_retdecl'' <- traverse updateTypes maybe_retdecl'
rettype'' <- normTypeFully rettype'
-- Check if the function body can actually be evaluated.
causalityCheck body''
-- Check for various problems.
localChecks body''
bindSpaced [(Term, fname)] $ do
fname' <- checkName Term fname loc
when (nameToString fname `elem` doNotShadow) $
typeError loc mempty . withIndexLink "may-not-be-redefined" $
"The" <+> prettyName fname <+> "operator may not be redefined."
pure (fname', tparams', params'', maybe_retdecl'', RetType dims rettype'', body'')
-- | This is "fixing" as in "setting them", not "correcting them". We
-- only make very conservative fixing.
fixOverloadedTypes :: Names -> TermTypeM ()
fixOverloadedTypes tyvars_at_toplevel =
getConstraints >>= mapM_ fixOverloaded . M.toList . M.map snd
where
fixOverloaded (v, Overloaded ots usage)
| Signed Int32 `elem` ots = do
unify usage (Scalar (TypeVar () Nonunique (qualName v) [])) $
Scalar $
Prim $
Signed Int32
when (v `S.member` tyvars_at_toplevel) $
warn usage "Defaulting ambiguous type to i32."
| FloatType Float64 `elem` ots = do
unify usage (Scalar (TypeVar () Nonunique (qualName v) [])) $
Scalar $
Prim $
FloatType Float64
when (v `S.member` tyvars_at_toplevel) $
warn usage "Defaulting ambiguous type to f64."
| otherwise =
typeError usage mempty . withIndexLink "ambiguous-type" $
"Type is ambiguous (could be one of"
<+> commasep (map pretty ots) <> ")."
</> "Add a type annotation to disambiguate the type."
fixOverloaded (v, NoConstraint _ usage) = do
-- See #1552.
unify usage (Scalar (TypeVar () Nonunique (qualName v) [])) $
Scalar $
tupleRecord []
when (v `S.member` tyvars_at_toplevel) $
warn usage "Defaulting ambiguous type to ()."
fixOverloaded (_, Equality usage) =
typeError usage mempty . withIndexLink "ambiguous-type" $
"Type is ambiguous (must be equality type)."
</> "Add a type annotation to disambiguate the type."
fixOverloaded (_, HasFields fs usage) =
typeError usage mempty . withIndexLink "ambiguous-type" $
"Type is ambiguous. Must be record with fields:"
</> indent 2 (stack $ map field $ M.toList fs)
</> "Add a type annotation to disambiguate the type."
where
field (l, t) = pretty l <> colon <+> align (pretty t)
fixOverloaded (_, HasConstrs cs usage) =
typeError usage mempty . withIndexLink "ambiguous-type" $
"Type is ambiguous (must be a sum type with constructors:"
<+> pretty (Sum cs) <> ")."
</> "Add a type annotation to disambiguate the type."
fixOverloaded (v, Size Nothing (Usage Nothing loc)) =
typeError loc mempty . withIndexLink "ambiguous-size" $
"Ambiguous size" <+> dquotes (prettyName v) <> "."
fixOverloaded (v, Size Nothing (Usage (Just u) loc)) =
typeError loc mempty . withIndexLink "ambiguous-size" $
"Ambiguous size" <+> dquotes (prettyName v) <+> "arising from" <+> pretty u <> "."
fixOverloaded _ = pure ()
hiddenParamNames :: [Pat] -> Names
hiddenParamNames params = hidden
where
param_all_names = mconcat $ map patNames params
named (Named x, _) = Just x
named (Unnamed, _) = Nothing
param_names =
S.fromList $ mapMaybe (named . patternParam) params
hidden = param_all_names `S.difference` param_names
inferredReturnType :: SrcLoc -> [Pat] -> PatType -> TermTypeM StructType
inferredReturnType loc params t = do
-- The inferred type may refer to names that are bound by the
-- parameter patterns, but which will not be visible in the type.
-- These we must turn into fresh type variables, which will be
-- existential in the return type.
fmap (toStruct . fst) $
unscopeType loc hidden_params $
inferReturnUniqueness params t
where
hidden_params = M.filterWithKey (const . (`S.member` hidden)) $ foldMap patternMap params
hidden = hiddenParamNames params
checkReturnAlias :: SrcLoc -> TypeBase () () -> [Pat] -> PatType -> TermTypeM ()
checkReturnAlias loc rettp params =
foldM_ (checkReturnAlias' params) S.empty . returnAliasing rettp
where
checkReturnAlias' params' seen (Unique, names)
| any (`S.member` S.map snd seen) $ S.toList names =
uniqueReturnAliased loc
| otherwise = do
notAliasingParam params' names
pure $ seen `S.union` tag Unique names
checkReturnAlias' _ seen (Nonunique, names)
| any (`S.member` seen) $ S.toList $ tag Unique names =
uniqueReturnAliased loc
| otherwise = pure $ seen `S.union` tag Nonunique names
notAliasingParam params' names =
forM_ params' $ \p ->
let consumedNonunique p' =
not (unique $ unInfo $ identType p') && (identName p' `S.member` names)
in case find consumedNonunique $ S.toList $ patIdents p of
Just p' ->
returnAliased (baseName $ identName p') loc
Nothing ->
pure ()
tag u = S.map (u,)
returnAliasing (Scalar (Record ets1)) (Scalar (Record ets2)) =
concat $ M.elems $ M.intersectionWith returnAliasing ets1 ets2
returnAliasing expected got =
[(uniqueness expected, S.map aliasVar $ aliases got)]
checkBinding ::
( Name,
Maybe UncheckedTypeExp,
[UncheckedTypeParam],
[UncheckedPat],
UncheckedExp,
SrcLoc
) ->
TermTypeM
( [TypeParam],
[Pat],
Maybe (TypeExp VName),
StructRetType,
Exp
)
checkBinding (fname, maybe_retdecl, tparams, params, body, loc) =
noUnique . incLevel . bindingParams tparams params $ \tparams' params' -> do
maybe_retdecl' <- traverse checkTypeExpNonrigid maybe_retdecl
body' <-
checkFunBody
params'
body
((\(_, x, _) -> x) <$> maybe_retdecl')
(maybe loc srclocOf maybe_retdecl)
params'' <- mapM updateTypes params'
body_t <- expTypeFully body'
(maybe_retdecl'', rettype) <- case maybe_retdecl' of
Just (retdecl', ret, _) -> do
let rettype_structural = toStructural ret
checkReturnAlias loc rettype_structural params'' body_t
when (null params) $ nothingMustBeUnique loc rettype_structural
ret' <- normTypeFully ret
pure (Just retdecl', ret')
Nothing
| null params ->
pure (Nothing, toStruct $ body_t `setUniqueness` Nonunique)
| otherwise -> do
body_t' <- inferredReturnType loc params'' body_t
pure (Nothing, body_t')
verifyFunctionParams (Just fname) params''
(tparams'', params''', rettype') <-
letGeneralise fname loc tparams' params'' rettype
checkGlobalAliases params'' body_t loc
pure (tparams'', params''', maybe_retdecl'', rettype', body')
-- | Extract all the shape names that occur in positive position
-- (roughly, left side of an arrow) in a given type.
sizeNamesPos :: TypeBase Size als -> S.Set VName
sizeNamesPos (Scalar (Arrow _ _ t1 (RetType _ t2))) = onParam t1 <> sizeNamesPos t2
where
onParam :: TypeBase Size als -> S.Set VName
onParam (Scalar Arrow {}) = mempty
onParam (Scalar (Record fs)) = mconcat $ map onParam $ M.elems fs
onParam (Scalar (TypeVar _ _ _ targs)) = mconcat $ map onTypeArg targs
onParam t = freeInType t
onTypeArg (TypeArgDim (NamedSize d) _) = S.singleton $ qualLeaf d
onTypeArg (TypeArgDim _ _) = mempty
onTypeArg (TypeArgType t _) = onParam t
sizeNamesPos _ = mempty
checkGlobalAliases :: [Pat] -> PatType -> SrcLoc -> TermTypeM ()
checkGlobalAliases params body_t loc = do
vtable <- asks $ scopeVtable . termScope
let isGlobal v = case v `M.lookup` vtable of
Just (BoundV Global _ _) -> True
_ -> False
let als =
filter isGlobal . S.toList $
boundArrayAliases body_t `S.difference` foldMap patNames params
unless (null params) $ case als of
v : _ ->
typeError loc mempty . withIndexLink "alias-free-variable" $
"Function result aliases the free variable "
<> dquotes (prettyName v)
<> "."
</> "Use"
<+> dquotes "copy"
<+> "to break the aliasing."
_ ->
pure ()
inferReturnUniqueness :: [Pat] -> PatType -> PatType
inferReturnUniqueness params t =
let forbidden = aliasesMultipleTimes t
uniques = uniqueParamNames params
delve (Scalar (Record fs)) =
Scalar $ Record $ M.map delve fs
delve t'
| all (`S.member` uniques) (boundArrayAliases t'),
not $ any ((`S.member` forbidden) . aliasVar) (aliases t') =
t' `setUniqueness` Unique
| otherwise =
t' `setUniqueness` Nonunique
in delve t
-- An alias inhibits uniqueness if it is used in disjoint values.
aliasesMultipleTimes :: PatType -> Names
aliasesMultipleTimes = S.fromList . map fst . filter ((> 1) . snd) . M.toList . delve
where
delve (Scalar (Record fs)) =
foldl' (M.unionWith (+)) mempty $ map delve $ M.elems fs
delve t =
M.fromList $ zip (map aliasVar $ S.toList (aliases t)) $ repeat (1 :: Int)
uniqueParamNames :: [Pat] -> Names
uniqueParamNames =
S.map identName
. S.filter (unique . unInfo . identType)
. foldMap patIdents
boundArrayAliases :: PatType -> S.Set VName
boundArrayAliases (Array als _ _ _) = boundAliases als
boundArrayAliases (Scalar Prim {}) = mempty
boundArrayAliases (Scalar (Record fs)) = foldMap boundArrayAliases fs
boundArrayAliases (Scalar (TypeVar als _ _ _)) = boundAliases als
boundArrayAliases (Scalar Arrow {}) = mempty
boundArrayAliases (Scalar (Sum fs)) =
mconcat $ concatMap (map boundArrayAliases) $ M.elems fs
nothingMustBeUnique :: SrcLoc -> TypeBase () () -> TermTypeM ()
nothingMustBeUnique loc = check
where
check (Array _ Unique _ _) = bad
check (Scalar (TypeVar _ Unique _ _)) = bad
check (Scalar (Record fs)) = mapM_ check fs
check (Scalar (Sum fs)) = mapM_ (mapM_ check) fs
check _ = pure ()
bad = typeError loc mempty "A top-level constant cannot have a unique type."
-- | Verify certain restrictions on function parameters, and bail out
-- on dubious constructions.
--
-- These restrictions apply to all functions (anonymous or otherwise).
-- Top-level functions have further restrictions that are checked
-- during let-generalisation.
verifyFunctionParams :: Maybe Name -> [Pat] -> TermTypeM ()
verifyFunctionParams fname params =
onFailure (CheckingParams fname) $
verifyParams (foldMap patNames params) =<< mapM updateTypes params
where
verifyParams forbidden (p : ps)
| d : _ <- S.toList $ freeInPat p `S.intersection` forbidden =
typeError p mempty . withIndexLink "inaccessible-size" $
"Parameter"
<+> dquotes (pretty p)
</> "refers to size"
<+> dquotes (prettyName d)
<> comma
</> textwrap "which will not be accessible to the caller"
<> comma
</> textwrap "possibly because it is nested in a tuple or record."
</> textwrap "Consider ascribing an explicit type that does not reference "
<> dquotes (prettyName d)
<> "."
| otherwise = verifyParams forbidden' ps
where
forbidden' =
case patternParam p of
(Named v, _) -> forbidden `S.difference` S.singleton v
_ -> forbidden
verifyParams _ [] = pure ()
-- | Move existentials down to the level where they are actually used
-- (i.e. have their "witnesses"). E.g. changes
--
-- @
-- ?[n].bool -> [n]bool
-- @
--
-- to
--
-- @
-- bool -> ?[n].[n]bool
-- @
injectExt :: [VName] -> StructType -> StructRetType
injectExt [] ret = RetType [] ret
injectExt ext ret = RetType ext_here $ deeper ret
where
(immediate, _) = dimUses ret
(ext_here, ext_there) = partition (`S.member` immediate) ext
deeper (Scalar (Prim t)) = Scalar $ Prim t
deeper (Scalar (Record fs)) = Scalar $ Record $ M.map deeper fs
deeper (Scalar (Sum cs)) = Scalar $ Sum $ M.map (map deeper) cs
deeper (Scalar (Arrow als p t1 (RetType t2_ext t2))) =
Scalar $ Arrow als p t1 $ injectExt (ext_there <> t2_ext) t2
deeper (Scalar (TypeVar as u tn targs)) =
Scalar $ TypeVar as u tn $ map deeperArg targs
deeper t@Array {} = t
deeperArg (TypeArgType t loc) = TypeArgType (deeper t) loc
deeperArg (TypeArgDim d loc) = TypeArgDim d loc
-- | Find all type variables in the given type that are covered by the
-- constraints, and produce type parameters that close over them.
--
-- The passed-in list of type parameters is always prepended to the
-- produced list of type parameters.
closeOverTypes ::
Name ->
SrcLoc ->
[TypeParam] ->
[StructType] ->
StructType ->
Constraints ->
TermTypeM ([TypeParam], StructRetType)
closeOverTypes defname defloc tparams paramts ret substs = do
(more_tparams, retext) <-
partitionEithers . catMaybes
<$> mapM closeOver (M.toList $ M.map snd to_close_over)
let mkExt v =
case M.lookup v substs of
Just (_, UnknowableSize {}) -> Just v
_ -> Nothing
pure
( tparams ++ more_tparams,
injectExt (retext ++ mapMaybe mkExt (S.toList $ freeInType ret)) ret
)
where
t = foldFunType paramts $ RetType [] ret
to_close_over = M.filterWithKey (\k _ -> k `S.member` visible) substs
visible = typeVars t <> freeInType t
(produced_sizes, param_sizes) = dimUses t
-- Avoid duplicate type parameters.
closeOver (k, _)
| k `elem` map typeParamName tparams =
pure Nothing
closeOver (k, NoConstraint l usage) =
pure $ Just $ Left $ TypeParamType l k $ srclocOf usage
closeOver (k, ParamType l loc) =
pure $ Just $ Left $ TypeParamType l k loc
closeOver (k, Size Nothing usage) =
pure $ Just $ Left $ TypeParamDim k $ srclocOf usage
closeOver (k, UnknowableSize _ _)
| k `S.member` param_sizes,
k `S.notMember` produced_sizes = do
notes <- dimNotes defloc $ NamedSize $ qualName k
typeError defloc notes . withIndexLink "unknowable-param-def" $
"Unknowable size"
<+> dquotes (prettyName k)
<+> "in parameter of"
<+> dquotes (prettyName defname)
<> ", which is inferred as:"
</> indent 2 (pretty t)
| k `S.member` produced_sizes =
pure $ Just $ Right k
closeOver (_, _) =
pure Nothing
letGeneralise ::
Name ->
SrcLoc ->
[TypeParam] ->
[Pat] ->
StructType ->
TermTypeM ([TypeParam], [Pat], StructRetType)
letGeneralise defname defloc tparams params rettype =
onFailure (CheckingLetGeneralise defname) $ do
now_substs <- getConstraints
-- Candidates for let-generalisation are those type variables that
--
-- (1) were not known before we checked this function, and
--
-- (2) are not used in the (new) definition of any type variables
-- known before we checked this function.
--
-- (3) are not referenced from an overloaded type (for example,
-- are the element types of an incompletely resolved record type).
-- This is a bit more restrictive than I'd like, and SML for
-- example does not have this restriction.
--
-- Criteria (1) and (2) is implemented by looking at the binding
-- level of the type variables.
let keep_type_vars = overloadedTypeVars now_substs
cur_lvl <- curLevel
let candidate k (lvl, _) = (k `S.notMember` keep_type_vars) && lvl >= cur_lvl
new_substs = M.filterWithKey candidate now_substs
(tparams', RetType ret_dims rettype') <-
closeOverTypes
defname
defloc
tparams
(map patternStructType params)
rettype
new_substs
rettype'' <- updateTypes rettype'
let used_sizes =
foldMap freeInType $ rettype'' : map patternStructType params
case filter ((`S.notMember` used_sizes) . typeParamName) $
filter isSizeParam tparams' of
[] -> pure ()
tp : _ -> unusedSize $ SizeBinder (typeParamName tp) (srclocOf tp)
-- We keep those type variables that were not closed over by
-- let-generalisation.
modifyConstraints $ M.filterWithKey $ \k _ -> k `notElem` map typeParamName tparams'
pure (tparams', params, RetType ret_dims rettype'')
checkFunBody ::
[Pat] ->
UncheckedExp ->
Maybe StructType ->
SrcLoc ->
TermTypeM Exp
checkFunBody params body maybe_rettype loc = do
body' <- noSizeEscape $ checkExp body
-- Unify body return type with return annotation, if one exists.
case maybe_rettype of
Just rettype -> do
body_t <- expTypeFully body'
-- We need to turn any sizes provided by "hidden" parameter
-- names into existential sizes instead.
let hidden = hiddenParamNames params
(body_t', _) <-
unscopeType
loc
( M.filterWithKey (const . (`S.member` hidden)) $
foldMap patternMap params
)
body_t
let usage = mkUsage (srclocOf body) "return type annotation"
onFailure (CheckingReturn rettype (toStruct body_t')) $
expect usage rettype $
toStruct body_t'
Nothing -> pure ()
pure body'
arrayOfM ::
(Pretty (Shape dim), Monoid as) =>
SrcLoc ->
TypeBase dim as ->
Shape dim ->
Uniqueness ->
TermTypeM (TypeBase dim as)
arrayOfM loc t shape u = do
arrayElemType (mkUsage loc "use as array element") "type used in array" t
pure $ arrayOf u shape t