futhark-0.28.1: src/Language/Futhark/TypeChecker/Consumption.hs
-- | Check that a value definition does not violate any consumption constraints,
-- via alias analysis.
--
-- This is a very subtle part of the language. The basic idea is "the result of
-- an expression aliases everything that goes into it", but this is in practice
-- too restrictive when we have functions (and polymorphic and higher-order
-- functions!) as well. However, we also do not want to make the user-facing
-- type system too complicated.
--
-- Our solution is to infer more precise function types, that directly talk
-- about alias information, via parametricity. These never escape into the
-- user-facing language.
--
-- Our overall philosophy is that soundness is (of course) non-negotiable, but
-- simplicity is better than flexibility. Futhark is not a language for very
-- fine-grained reasoning about aliasing.
--
-- As an example of the compromise, @x |> copy@ works and produces a fresh
-- result, whilst @id >-> copy@ loses freshness information.
--
-- Further, we only infer freshness for fully saturated higher-order functions,
-- so refactoring to take advantage of partial application may not work.
-- Likewise, we infer only the freshness of the value a function returns, not
-- of what a returned function in turn returns: that must be declared on the
-- returned lambda itself.
module Language.Futhark.TypeChecker.Consumption
( checkValDef,
-- * For testing
Alias (..),
Aliases,
TypeAliases,
inferReturnFreshness,
)
where
import Control.Monad
import Control.Monad.Reader
import Control.Monad.State.Strict
import Data.Bifoldable
import Data.Bifunctor
import Data.DList qualified as DL
import Data.Foldable
import Data.Functor.Const
import Data.Functor.Identity
import Data.List qualified as L
import Data.List.NonEmpty qualified as NE
import Data.Map.Strict qualified as M
import Data.Maybe
import Data.Set qualified as S
import Data.Text qualified as T
import Futhark.Util (nubOrd)
import Futhark.Util.Pretty hiding (space)
import Language.Futhark
import Language.Futhark.Traversals
import Language.Futhark.TypeChecker.Monad (BoundV (..), Notes, TypeError (..), withIndexLink)
import Prelude hiding (mod)
-- | A position within a compound type. A path step is a record field name, or a
-- constructor name followed by the tuple field name of a position in its
-- payload.
type Path = [Name]
-- | A variable together with a path: the component of that variable at that
-- path, as defined by 'traverseLeaves'. See Note [Locations].
type Location = (VName, Path)
-- | Something a value may share memory with. Every constructor but 'AliasSelf'
-- denotes a 'Location'. Its variable may be in scope, or be free: either it has
-- gone out of scope, or it is an internal name standing for an intermediate
-- value. A free alias behaves more like an equivalence class. See
-- uniqueness-error18.fut for an example of why this is necessary.
data Alias
= AliasBound Location
| AliasFree Location
| -- | Used to represent unknowable internal aliasing, which for example may
-- occur for a function that returns a nonfresh abstract type. (That
-- abstract type may internally be a pair of arrays that alias each other.)
AliasSelf
deriving (Eq, Ord, Show)
instance Pretty Alias where
pretty (AliasBound (v, fs)) = prettyAlias v fs
pretty (AliasFree (v, fs)) = "~" <> prettyAlias v fs
pretty AliasSelf = "self"
-- | The location an alias refers to. 'AliasSelf' refers to none.
aliasLoc :: Alias -> Maybe Location
aliasLoc (AliasBound l) = Just l
aliasLoc (AliasFree l) = Just l
aliasLoc AliasSelf = Nothing
-- | The variable an alias refers to. 'AliasSelf' does not refer to any
-- variable, as it denotes aliasing internal to a value.
aliasVar :: Alias -> Maybe VName
aliasVar = fmap fst . aliasLoc
-- | Apply a function to every leaf of a type (every component that is neither a
-- record nor a sum) along with its path.
traverseLeaves ::
(Applicative f) =>
(Path -> TypeBase dim o -> f (TypeBase dim v)) ->
TypeBase dim o ->
f (TypeBase dim v)
traverseLeaves f = go []
where
go p (Scalar (Record ts)) =
Scalar . Record <$> M.traverseWithKey (\k -> go (p ++ [k])) ts
go p (Scalar (Sum cs)) =
Scalar . Sum <$> M.traverseWithKey (\c -> zipWithM (\i -> go (p ++ [c, i])) tupleFieldNames) cs
go p t = f p t
-- | Apply a function to every leaf of a type along with its path.
mapLeaves :: (Path -> TypeBase dim o -> TypeBase dim v) -> TypeBase dim o -> TypeBase dim v
mapLeaves f = runIdentity . traverseLeaves (\p -> Identity . f p)
-- | The leaves of a type along with their paths.
leaves :: TypeBase dim o -> [(Path, TypeBase dim o)]
leaves = getConst . traverseLeaves (\p t -> Const [(p, t)])
-- | The locations these aliases refer to.
aliasLocs :: Aliases -> [Location]
aliasLocs = mapMaybe aliasLoc . S.toList
-- | The variables these aliases refer to. 'AliasSelf' contributes nothing,
-- as it refers to no variable.
aliasVars :: Aliases -> S.Set VName
aliasVars = S.fromList . mapMaybe aliasVar . S.toList
-- | Does this value have internal aliasing, meaning it can neither be consumed
-- nor given a fresh type? See 'AliasSelf'.
selfAliased :: Aliases -> Bool
selfAliased = S.member AliasSelf
-- | Might two values with these aliases share memory? This is not the same
-- question as whether the sets intersect: 'AliasSelf' denotes a property of a
-- single value rather than a shared referent ('aliasVar' is 'Nothing' for it),
-- so two values that both have internal aliasing are not thereby aliases of
-- each other. Avoid comparing alias sets in any other way than through this
-- function.
overlaps :: Aliases -> Aliases -> Bool
overlaps x y = not $ S.disjoint (referents x) (referents y)
where
referents = S.filter (isJust . aliasVar)
prettyAlias :: VName -> [Name] -> Doc ann
prettyAlias v fs = prettyName v <> mconcat (map (("." <>) . prettyName) fs)
instance Pretty (S.Set Alias) where
pretty = braces . commasep . map pretty . S.toList
-- | Does this alias refer to an in-scope variable? 'AliasFree' has left
-- scope and 'AliasSelf' is no variable at all. This is not the way to ask
-- whether two values may share memory; see 'overlaps'.
isBoundAlias :: Alias -> Bool
isBoundAlias AliasBound {} = True
isBoundAlias _ = False
-- | What a value may share memory with.
type Aliases = S.Set Alias
type TypeAliases = TypeBase Size Aliases
-- | @t \`setAliases\` als@ returns @t@, but with @als@ substituted for
-- any already present aliases.
setAliases :: TypeBase dim o1 -> o2 -> TypeBase dim o2
setAliases t = addAliases t . const
-- | @t \`addAliases\` f@ returns @t@, but with any already present
-- aliases replaced by @f@ applied to that aliases.
addAliases :: TypeBase dim o1 -> (o1 -> o2) -> TypeBase dim o2
addAliases = flip second
aliases :: TypeAliases -> Aliases
aliases = bifoldMap (const mempty) id
-- | Add an alias to a leaf of a type. That means we assume the type passed in
-- here is not a compound type.
aliasLeaf :: Alias -> TypeAliases -> TypeAliases
aliasLeaf a (Array als shape et) = Array (S.insert a als) shape et
aliasLeaf a (Scalar (TypeVar als tn args)) = Scalar $ TypeVar (S.insert a als) tn args
aliasLeaf a (Scalar (Arrow als mn d ps rt)) = Scalar $ Arrow (S.insert a als) mn d ps rt
aliasLeaf _ t = t
-- | @insertSelfAliases v t@ adds an alias of @v@ to every component of @t@,
-- noting the path at which the component sits.
insertSelfAliases :: VName -> TypeAliases -> TypeAliases
insertSelfAliases v = mapLeaves $ aliasLeaf . AliasBound . (v,)
-- | Does any component of the value that this type ultimately produces satisfy
-- the predicate? Function types are followed to their (curried) result, as the
-- only way to obtain a value from a function is to apply it.
anyResultComponent :: (ResType -> Bool) -> ResType -> Bool
anyResultComponent p (Scalar (Arrow _ _ _ _ (RetType _ t))) = anyResultComponent p t
anyResultComponent p (Scalar (Record fs)) = any (anyResultComponent p) fs
anyResultComponent p (Scalar (Sum cs)) = any (any (anyResultComponent p)) cs
anyResultComponent p t = p t
-- | The aliases of a use of the global @v@, given its type scheme and the type
-- it is used at. A use of a global name aliases that name, except where
-- parametricity rules it out. In particular, a non-function component whose
-- declared type contains one of the type parameters cannot be (part of) a
-- global, and a function can only yield a value aliasing a global if some
-- nonfresh component of its result is not of that kind. See Note [Parametric
-- results].
globalAliases :: VName -> BoundV -> StructType -> TypeAliases
globalAliases v (BoundV tparams decl) = mapLeaves onLeaf . second (const mempty)
where
tparams' = S.fromList [p | TypeParamType _ p _ <- tparams]
-- A type parameter counts only where it is itself a type, not where it is
-- an argument to an abstract type, which may ignore it.
parametric :: TypeBase Size u -> Bool
parametric (Array _ _ et) = parametric $ Scalar et
parametric (Scalar (TypeVar _ tn _)) = qualLeaf tn `S.member` tparams'
parametric (Scalar (Record fs)) = any parametric fs
parametric (Scalar (Sum cs)) = any (any parametric) cs
parametric _ = False
decl_leaves = leaves decl
onLeaf p t =
case listToMaybe [d | (dp, d) <- decl_leaves, dp `L.isPrefixOf` p] of
Just d@(Scalar Arrow {})
| anyResultComponent maybeGlobal (toRes Nonfresh d) ->
aliasLeaf (AliasBound (v, p)) t
| otherwise -> t
Just d | parametric d -> t
_ -> aliasLeaf (AliasBound (v, p)) t
maybeGlobal t@(Array Nonfresh _ _) = not $ parametric t
maybeGlobal t@(Scalar (TypeVar Nonfresh _ _)) = not $ parametric t
maybeGlobal _ = False
-- | Instantiate the aliases of a local binding at the type of an occurrence,
-- just as the type of a global is instantiated. The binding's type is that of
-- its definition, which for a local function may be polymorphic: where it has a
-- type parameter, every part of what the occurrence instantiates it with gets
-- the aliases, or in a return type the freshness, of that type parameter.
instantiateAliases :: TypeBase Size u -> TypeAliases -> TypeAliases
instantiateAliases
(Scalar (Arrow _ _ _ t_p (RetType _ t_r)))
(Scalar (Arrow als pn d _ (RetType ext r))) =
Scalar $ Arrow als pn d t_p $ RetType ext $ instantiateFreshness t_r r
instantiateAliases (Scalar (Record ts)) (Scalar (Record als)) =
Scalar $ Record $ M.intersectionWith instantiateAliases ts als
instantiateAliases (Scalar (Sum ts)) (Scalar (Sum als)) =
Scalar $ Sum $ M.intersectionWith (zipWith instantiateAliases) ts als
instantiateAliases t als = t `setAliases` aliases als
-- | Like 'instantiateAliases', but for the freshness of a return type.
instantiateFreshness :: TypeBase Size u -> ResType -> ResType
instantiateFreshness
(Scalar (Arrow _ _ _ t_p (RetType _ t_r)))
(Scalar (Arrow u pn d _ (RetType ext r))) =
Scalar $ Arrow u pn d t_p $ RetType ext $ instantiateFreshness t_r r
instantiateFreshness (Scalar (Record ts)) (Scalar (Record rs)) =
Scalar $ Record $ M.intersectionWith instantiateFreshness ts rs
instantiateFreshness (Scalar (Sum ts)) (Scalar (Sum rs)) =
Scalar $ Sum $ M.intersectionWith (zipWith instantiateFreshness) ts rs
instantiateFreshness t r = t `setMode` freshness r
-- | Update the aliases at a given position. It is expected that the second
-- 'TypeAliases' has the same type (modulo alias information) as the field at
-- the given path.
updateAliases :: TypeAliases -> [UpdateStep Info VName] -> TypeAliases -> TypeAliases
updateAliases _ [] ve_als =
ve_als
updateAliases (Scalar (Record fs)) (UpdateStepField f : rest) ve_als
| Just sub <- M.lookup f fs =
Scalar $ Record $ M.insert f (updateAliases sub rest ve_als) fs
updateAliases src_als (UpdateStepSlice _ : _) _ = second (const mempty) src_als
updateAliases src_als _ _ = error $ "updateAliases: no such field in " <> prettyString src_als
data Entry a
= Consumable {entryAliases :: a}
| Nonconsumable {entryAliases :: a}
deriving (Eq, Ord, Show)
instance Functor Entry where
fmap f (Consumable als) = Consumable $ f als
fmap f (Nonconsumable als) = Nonconsumable $ f als
data CheckEnv = CheckEnv
{ envVtable :: M.Map VName (Entry TypeAliases),
-- | Location of the definition we are checking.
envLoc :: Loc,
-- | The declared type of a global, along with the type parameters it is
-- polymorphic in. This is what lets us exploit parametricity; see Note
-- [Parametric results].
envGlobal :: QualName VName -> Maybe BoundV
}
-- | A description of where an artificial compiler-generated
-- intermediate name came from.
data NameReason
= -- | Name is the result of a function application.
NameAppRes (Maybe (QualName VName)) SrcLoc
| -- | Name is a loop result.
NameLoopRes SrcLoc
| -- | Name ties together the components of the result of the given kind
-- of branching expression; see Note [Locations].
NameBranchRes T.Text SrcLoc
nameReason :: SrcLoc -> NameReason -> Doc a
nameReason loc (NameAppRes Nothing apploc) =
"result of application at" <+> pretty (locStrRel loc apploc)
nameReason loc (NameAppRes fname apploc) =
"result of applying"
<+> dquotes (pretty fname)
<+> parens ("at" <+> pretty (locStrRel loc apploc))
nameReason loc (NameLoopRes apploc) =
"result of loop at" <+> pretty (locStrRel loc apploc)
nameReason loc (NameBranchRes what eloc) =
"result of" <+> pretty what <+> "at" <+> pretty (locStrRel loc eloc)
-- | The locations consumed so far, each with where it was consumed.
type Consumed = M.Map Location Loc
data CheckState = CheckState
{ stateConsumed :: Consumed,
stateErrors :: DL.DList TypeError,
stateNames :: M.Map VName NameReason,
stateCounter :: Int
}
newtype CheckM a = CheckM (ReaderT CheckEnv (State CheckState) a)
deriving
( Functor,
Applicative,
Monad,
MonadReader CheckEnv,
MonadState CheckState
)
runCheckM ::
(QualName VName -> Maybe BoundV) ->
Loc ->
CheckM a ->
(a, [TypeError])
runCheckM globals loc (CheckM m) =
let (a, s) = runState (runReaderT m env) initial_state
in (a, DL.toList (stateErrors s))
where
env =
CheckEnv
{ envVtable = mempty,
envLoc = loc,
envGlobal = globals
}
initial_state =
CheckState
{ stateConsumed = mempty,
stateErrors = mempty,
stateNames = mempty,
stateCounter = 0
}
incCounter :: CheckM Int
incCounter =
state $ \s -> (stateCounter s, s {stateCounter = stateCounter s + 1})
-- | The part of a path that steps only into records.
recordPath :: Path -> TypeBase dim o -> Path
recordPath (f : fs) (Scalar (Record ts))
| Just t <- M.lookup f ts = f : recordPath fs t
recordPath _ _ = []
-- | Describe a location for the user. A path into a sum payload is not
-- something the user can write, so the path is cut off at the first sum.
describeLoc :: Location -> CheckM (Doc a)
describeLoc (v, fs) = do
loc <- asks envLoc
fs' <- asks $ maybe fs (recordPath fs . entryAliases) . M.lookup v . envVtable
gets $
maybe ("variable" <+> dquotes (prettyAlias v fs')) (nameReason (srclocOf loc))
. M.lookup v
. stateNames
-- | Describe a variable for the user.
describeVar :: VName -> CheckM (Doc a)
describeVar v = describeLoc (v, [])
-- | Like 'describeVar', but naming a variable written by the programmer without
-- calling it one.
describeName :: VName -> CheckM (Doc a)
describeName v = do
loc <- asks envLoc
gets $
maybe (dquotes (prettyName v)) (nameReason (srclocOf loc))
. M.lookup v
. stateNames
-- | Mark everything as nonconsumable within this action.
noConsumable :: CheckM a -> CheckM a
noConsumable = local $ \env -> env {envVtable = M.map f $ envVtable env}
where
f = Nonconsumable . entryAliases
addError :: (Located loc) => loc -> Notes -> Doc () -> CheckM ()
addError loc notes e = modify $ \s ->
s {stateErrors = DL.snoc (stateErrors s) (TypeError (locOf loc) notes e)}
returnAliased :: Name -> SrcLoc -> CheckM ()
returnAliased name loc =
addError loc mempty . withIndexLink "return-aliased" $
"Fresh-declared return value is aliased to"
<+> dquotes (prettyName name)
<> ", which is not consumable."
-- | Returning a value for a fresh return type is equivalent to consuming it,
-- so a value with internal aliasing cannot be returned that way.
selfAliasedReturn :: (Located loc) => loc -> CheckM ()
selfAliasedReturn loc =
addError loc mempty $
"A fresh-declared component of the return value may have internal aliases,"
</> "and so cannot be declared fresh."
freshReturnAliased :: SrcLoc -> CheckM ()
freshReturnAliased loc =
addError loc mempty . withIndexLink "fresh-return-aliased" $
"A fresh-declared component of the return value is aliased to some other component."
-- | A reason why a component of a function result cannot be fresh.
data Unfresh
= -- | It aliases this variable, which is in scope and not a consumed
-- parameter.
UnfreshAliases VName
| -- | It aliases a location that some other component also aliases.
UnfreshShared
| -- | It may have internal aliasing.
UnfreshSelf
-- | Why a component of the result of a function with these parameters cannot be
-- fresh, given the 'sharedLocations' of the whole result. The component may be
-- fresh exactly when there is no reason. See Note [Locations].
unfreshness :: [Pat ParamType] -> S.Set Location -> TypeAliases -> [Unfresh]
unfreshness params shared t_als =
[UnfreshShared | any (`S.member` shared) (aliasLocs (aliases t_als))]
<> [UnfreshSelf | selfAliased (aliases t_als)]
<> map (UnfreshAliases . fst) (filter (not . consumedParamLoc params) in_scope)
where
-- Mention the parameters before other variables.
in_scope =
L.sortOn ((`notElem` foldMap patNames params) . fst) . nubOrd . aliasLocs $
S.filter isBoundAlias $
aliases t_als
-- | Check that every component of a function result declared fresh may be.
checkReturnAlias :: SrcLoc -> [Pat ParamType] -> ResType -> TypeAliases -> CheckM ()
checkReturnAlias loc params rettp ret_als =
forM_ (returnAliases rettp ret_als) $ \(u, t_als) ->
when (u == Fresh) . mapM_ report $ unfreshness params shared t_als
where
shared = sharedLocations ret_als
report (UnfreshAliases v) = returnAliased (baseName v) loc
report UnfreshShared = freshReturnAliased loc
report UnfreshSelf = selfAliasedReturn loc
returnAliases (Scalar (Record ets1)) (Scalar (Record ets2)) =
concat $ M.elems $ M.intersectionWith returnAliases ets1 ets2
returnAliases expected got =
[(freshness expected, got)]
unscope :: [VName] -> Aliases -> Aliases
unscope bound = S.map f
where
f (AliasBound (v, fs)) =
if v `elem` bound
then AliasFree (v, fs)
else AliasBound (v, fs)
f a = a
-- | Figure out the aliases of each bound name in a pattern.
matchPat :: Pat t -> TypeAliases -> DL.DList (VName, (t, TypeAliases))
matchPat (PatParens p _) t = matchPat p t
matchPat (TuplePat ps _) t
| Just ts <- isTupleRecord t = mconcat $ zipWith matchPat ps ts
matchPat (RecordPat fs1 _) (Scalar (Record fs2)) =
mconcat $
zipWith
matchPat
(map snd (sortFields (M.fromList (map (first unLoc) fs1))))
(map snd (sortFields fs2))
matchPat (Id v (Info t) _) als = DL.singleton (v, (t, als))
matchPat (PatAscription p _ _) t = matchPat p t
matchPat (PatConstr v _ ps _) (Scalar (Sum cs))
| Just ts <- M.lookup v cs = mconcat $ zipWith matchPat ps ts
matchPat Wildcard {} _ = mempty
matchPat PatLit {} _ = mempty
matchPat (PatAttr _ p _) t = matchPat p t
matchPat _ t = error $ "matchPat: pattern does not match " <> prettyString t
bindingPat ::
Pat StructType ->
TypeAliases ->
CheckM (a, TypeAliases) ->
CheckM (a, TypeAliases)
bindingPat p t m = do
void . noConsumable $ traversePat pure (fmap fst . checkExp) p
second (second (unscope (patNames p))) <$> local bind m
where
bind env =
env
{ envVtable =
foldr (uncurry M.insert . f) (envVtable env) (matchPat p t)
}
where
f (v, (_, als)) = (v, Consumable $ insertSelfAliases v als)
bindingParam :: Pat ParamType -> CheckM (a, TypeAliases) -> CheckM (a, TypeAliases)
bindingParam = bindingParamAliasing mempty
-- | Check the size expressions in a type. A size expression may be evaluated
-- before the expression or binding it appears in, so it may consume nothing.
checkSizes :: (Bifoldable t) => t Exp a -> CheckM ()
checkSizes = noConsumable . bitraverse_ checkExp pure
-- | Like 'bindingParam', but every component of the parameter also aliases the
-- given aliases.
bindingParamAliasing :: Aliases -> Pat ParamType -> CheckM (a, TypeAliases) -> CheckM (a, TypeAliases)
bindingParamAliasing als p m = do
mapM_ checkSizes p
second (second (unscope (patNames p))) <$> local bind m
where
bind env =
env
{ envVtable =
foldr (uncurry M.insert . f) (envVtable env) (patternMap p)
}
f (v, t)
| diet t == Consume = (v, Consumable t_als)
| otherwise = (v, Nonconsumable t_als)
where
t_als = second (<> als) $ selfAliasType v t
bindingIdent :: Diet -> Ident StructType -> CheckM (a, TypeAliases) -> CheckM (a, TypeAliases)
bindingIdent d (Ident v (Info t) _) =
fmap (second (second (unscope [v]))) . local bind
where
bind env = env {envVtable = M.insert v t' (envVtable env)}
d' = case d of
Consume -> Consumable
Observe -> Nonconsumable
t' = d' $ selfAliasType v t
bindingParams :: [Pat ParamType] -> CheckM (a, TypeAliases) -> CheckM (a, TypeAliases)
bindingParams params m =
noConsumable $
second (second (unscope (foldMap patNames params)))
<$> foldr bindingParam m params
-- | Bind the names of a loop form, given the aliases of the array a for-in loop
-- iterates over. An element of that array aliases it, as indexing does.
bindingLoopForm :: Aliases -> LoopFormBase Info VName -> CheckM (a, TypeAliases) -> CheckM (a, TypeAliases)
bindingLoopForm _ (For ident _) m = bindingIdent Observe ident m
bindingLoopForm arr_als (ForIn pat _) m = bindingParamAliasing arr_als pat' m
where
pat' = fmap (second (const Observe)) pat
bindingLoopForm _ While {} m = m
bindingFun :: VName -> TypeAliases -> CheckM a -> CheckM a
bindingFun v t = local $ \env ->
env {envVtable = M.insert v (Nonconsumable t) (envVtable env)}
-- | Is this location dead because of something in the consumed set? That is
-- the case if a location on the same variable has been consumed whose path is
-- a prefix of this one, or of which this one is a prefix. The result is where
-- the killing consumption happened.
deadIn :: Consumed -> Location -> Maybe Loc
deadIn cons (v, p) = listToMaybe $ mapMaybe killing $ M.toList on_v
where
on_v = M.takeWhileAntitone ((== v) . fst) $ M.dropWhileAntitone ((< v) . fst) cons
killing ((_, q), loc)
| q `L.isPrefixOf` p || p `L.isPrefixOf` q = Just loc
| otherwise = Nothing
checkIfConsumed :: Loc -> Aliases -> CheckM ()
checkIfConsumed rloc als = do
cons <- gets stateConsumed
names <- gets stateNames
let bad l = (l,) <$> deadIn cons l
-- Mention the variables the programmer wrote before internal names.
internal = (`M.member` names) . fst . fst
forM_ (L.sortOn internal $ mapMaybe bad $ aliasLocs als) $ \(l, wloc) -> do
v' <- describeLoc l
addError rloc mempty . withIndexLink "use-after-consume" $
"Using"
<+> v'
<> ", but this was consumed at"
<+> pretty (locStrRel rloc wloc)
<> ". (Possibly through aliases.)"
consumed :: Consumed -> CheckM ()
consumed vs = modify $ \s -> s {stateConsumed = stateConsumed s <> vs}
consumeAliases :: Loc -> Aliases -> CheckM ()
consumeAliases loc als = do
vtable <- asks envVtable
let isBad v =
case v `M.lookup` vtable of
Just (Nonconsumable {}) -> True
Just _ -> False
Nothing -> True
checkIfConsumable AliasFree {} = pure ()
checkIfConsumable AliasSelf =
addError
loc
mempty
"Consuming a value that may have internal aliases."
checkIfConsumable a
| Just v <- aliasVar a,
isBad v = do
v' <- describeName v
addError loc mempty . withIndexLink "not-consumable" $
"Consuming" <+> v' <> ", which is not consumable."
checkIfConsumable _ = pure ()
-- Mention local variables before globals.
global = maybe False (`M.notMember` vtable) . aliasVar
mapM_ checkIfConsumable $ L.sortOn global $ S.toList als
checkIfConsumed loc als
consumed als'
where
als' = M.fromList $ map (,loc) $ aliasLocs als
-- | Add 'AliasSelf' to every function component of a type, recording that
-- applying it may yield a value with internal aliasing. See Note [Parametric
-- results].
addSelfAliases :: TypeAliases -> TypeAliases
addSelfAliases (Scalar (Arrow als mn d pt rt)) =
Scalar $ Arrow (S.insert AliasSelf als) mn d pt rt
addSelfAliases (Scalar (Record fs)) = Scalar $ Record $ fmap addSelfAliases fs
addSelfAliases (Scalar (Sum cs)) = Scalar $ Sum $ (fmap . fmap) addSelfAliases cs
addSelfAliases t = t
-- | Can a function with this type scheme produce, when its function components
-- are applied, a value whose internal aliasing we cannot see? That is so
-- exactly when some component of what it produces is a nonfresh abstract type
-- that is not one of the type parameters it is polymorphic in: it must then
-- have manufactured that value, rather than been handed it. Intrinsic types
-- (notably accumulators) are exempt, as the compiler does know their
-- representation, and they have no components that could alias each other. See
-- Note [Parametric results].
manufacturesAbstract :: BoundV -> Bool
manufacturesAbstract (BoundV tparams vt) = anyResultComponent manufactured . toRes Nonfresh $ vt
where
tparams' = [v | TypeParamType _ v _ <- tparams]
manufactured (Scalar (TypeVar u t _)) =
u == Nonfresh
&& not (isIntrinsic (qualLeaf t))
&& qualLeaf t `notElem` tparams'
manufactured _ = False
-- | Add 'AliasSelf' to the function components of a value, recording that
-- applying them may produce a value with internal aliasing, when the given
-- declared type says they may. See Note [Parametric results].
maybeAddSelfAliases :: BoundV -> TypeAliases -> TypeAliases
maybeAddSelfAliases tscheme
| manufacturesAbstract tscheme = addSelfAliases
| otherwise = id
-- | Observe the given name here and return its aliases.
observeVar :: Loc -> QualName VName -> StructType -> CheckM TypeAliases
observeVar loc qv t = do
als <-
asks $ \env ->
maybe (isGlobal env) (instantiateAliases t . entryAliases) $
M.lookup v (envVtable env)
checkIfConsumed loc (aliases als)
pure als
where
v = qualLeaf qv
-- The declared type of a global is what makes parametricity visible; if we
-- cannot find it, fall back to the instantiated type, which amounts to
-- assuming no parametricity at all. An intrinsic aliases nothing. See Note
-- [Parametric results].
isGlobal env
| isIntrinsic v = second (const mempty) t
| otherwise =
let tscheme = fromMaybe (BoundV [] t) $ envGlobal env qv
in maybeAddSelfAliases tscheme $ globalAliases v tscheme t
-- Capture any newly consumed locations that occur during the provided action.
contain :: CheckM a -> CheckM (a, Consumed)
contain m = do
prev_cons <- gets stateConsumed
x <- m
new_cons <- gets $ (`M.difference` prev_cons) . stateConsumed
modify $ \s -> s {stateConsumed = prev_cons}
pure (x, new_cons)
-- | The two types are assumed to be approximately structurally equal,
-- but not necessarily regarding sizes. Combines aliases and prefers
-- other information from first argument.
combineAliases :: TypeAliases -> TypeAliases -> TypeAliases
combineAliases (Array als1 et1 shape1) t2 =
Array (als1 <> aliases t2) et1 shape1
combineAliases (Scalar (TypeVar als1 tv1 targs1)) t2 =
Scalar $ TypeVar (als1 <> aliases t2) tv1 targs1
combineAliases (Scalar (Record ts1)) (Scalar (Record ts2)) =
Scalar $ Record $ M.intersectionWith combineAliases ts1 ts2
combineAliases
(Scalar (Arrow als1 mn1 d1 pt1 (RetType dims1 rt1)))
(Scalar (Arrow als2 _ _ _ (RetType _ _))) =
Scalar (Arrow (als1 <> als2) mn1 d1 pt1 (RetType dims1 rt1))
combineAliases (Scalar (Sum cs1)) (Scalar (Sum cs2)) =
Scalar $ Sum $ M.intersectionWith (zipWith combineAliases) cs1 cs2
combineAliases (Scalar (Prim t)) _ = Scalar $ Prim t
combineAliases t1 t2 =
error $ "combineAliases invalid args: " ++ show (t1, t2)
-- | The locations that occur in more than one component of a value. A
-- component aliasing any of them cannot be fresh.
sharedLocations :: TypeAliases -> S.Set Location
sharedLocations =
M.keysSet
. M.filter (> 1)
. M.fromListWith (+)
. concatMap (map (,1 :: Int) . S.toList . S.fromList . aliasLocs)
. aliasParts
-- | Is this location entirely within a part of a parameter that is consumed?
consumedParamLoc :: [Pat ParamType] -> Location -> Bool
consumedParamLoc params (v, fs) =
case maybe [] (filter ((fs `L.isPrefixOf`) . fst) . leaves) $
lookup v (foldMap patternMap params) of
[] -> False
within -> all (consumable . snd) within
where
consumable (Array d _ _) = d == Consume
consumable (Scalar (TypeVar d _ _)) = d == Consume
consumable (Scalar Arrow {}) = False
consumable _ = True
-- | Free variables and their aliases.
boundFreeInExp :: Exp -> CheckM (M.Map VName TypeAliases)
boundFreeInExp e = do
vtable <- asks envVtable
pure $
M.mapMaybe (fmap entryAliases) . M.fromSet (`M.lookup` vtable) $
fvVars (freeInExp e)
-- | The aliases of the free local variables captured by a closure with the given
-- parameters and body, plus any globals that its result aliases, which it may
-- return.
closureAliases :: [Pat ParamType] -> Exp -> TypeAliases -> CheckM Aliases
closureAliases params body body_als = do
vtable <- asks envVtable
free_bound <-
(`M.withoutKeys` S.fromList (foldMap patNames params)) <$> boundFreeInExp body
-- The closure may return aliases to globals, and if the body may have
-- internal aliasing ('AliasSelf'), so may the result of applying the closure.
let isGlobal AliasFree {} = False
isGlobal AliasSelf = True
isGlobal a = maybe False (`M.notMember` vtable) $ aliasVar a
pure $
foldMap aliases (M.elems free_bound)
<> S.filter isGlobal (aliases body_als)
-- | An in-place update through record fields consumes the component at the
-- end of that path, but its result keeps the other components, which must
-- therefore not share memory with it.
checkUpdatePath :: Loc -> [UpdateStep Info VName] -> TypeAliases -> CheckM ()
checkUpdatePath loc steps src_als =
when (foldMap (aliases . snd) inside `overlaps` foldMap (aliases . snd) outside) $
addError loc mempty $
"In-place update of a component that shares memory with"
</> "other components of the same value."
where
(inside, outside) = L.partition ((fieldPath steps `L.isPrefixOf`) . fst) $ leaves src_als
fieldPath (UpdateStepField f : steps') = f : fieldPath steps'
fieldPath _ = []
overlapCheck :: (Pretty src, Pretty ve) => Loc -> (src, TypeAliases) -> (ve, TypeAliases) -> CheckM ()
overlapCheck loc (src, src_als) (ve, ve_als) =
when (aliases src_als `overlaps` aliases ve_als) $
addError loc mempty $
"Source array for in-place update"
</> indent 2 (pretty src)
</> "might alias update value"
</> indent 2 (pretty ve)
</> "Hint: use"
<+> dquotes "copy"
<+> "to remove aliases from the value."
inferReturnFreshness :: [Pat ParamType] -> ResType -> TypeAliases -> ResType
inferReturnFreshness [] ret _ = ret `setMode` Nonfresh
inferReturnFreshness params ret ret_als = delve ret ret_als
where
shared = sharedLocations ret_als
delve (Scalar (Record fs1)) (Scalar (Record fs2)) =
Scalar $ Record $ M.intersectionWith delve fs1 fs2
delve (Scalar (Sum cs1)) (Scalar (Sum cs2)) =
Scalar $ Sum $ M.intersectionWith (zipWith delve) cs1 cs2
delve t t_als =
t `setMode` if null (unfreshness params shared t_als) then Fresh else Nonfresh
checkSubExps :: (ASTMappable e) => e -> CheckM e
checkSubExps = astMap identityMapper {mapOnExp = fmap fst . checkExp}
noAliases :: Exp -> CheckM (Exp, TypeAliases)
noAliases e = do
e' <- checkSubExps e
pure (e', unknownAliases (typeOf e))
-- | The aliases of each leaf of a value.
aliasParts :: TypeAliases -> [Aliases]
aliasParts = map (aliases . snd) . leaves
-- | Are the components of this value pairwise disjoint?
separated :: TypeAliases -> Bool
separated = S.null . sharedLocations
-- | The leaf at the given path, if there is one.
componentAt :: Path -> TypeBase dim o -> Maybe (TypeBase dim o)
componentAt fs = lookup fs . leaves
-- | The locations in the alias set of a location: those of the leaf at that
-- path of the variable's entry in the vtable. Empty for a location that is
-- not a leaf of a variable in scope.
aliasOf :: M.Map VName (Entry TypeAliases) -> Location -> [Location]
aliasOf vtable (v, fs) =
maybe [] (aliasLocs . aliases) $ componentAt fs . entryAliases =<< M.lookup v vtable
-- | The aliases of the components of a value passed for a parameter of this
-- type that the parameter treats with the given diet.
aliasesWithDiet :: Diet -> ParamType -> TypeAliases -> Aliases
aliasesWithDiet d p_t t_als =
foldMap (aliases . snd . snd) . filter ((== d) . diet . snd . fst) $
zip (leaves p_t) (leaves t_als)
-- | Check an expression passed as an argument. This does not pass it; see
-- 'passArgs'.
checkArg :: Exp -> CheckM (Exp, TypeAliases)
checkArg e = do
((e', e_als), e_cons) <- contain $ checkExp e
consumed e_cons
let e_t = typeOf e'
when (e_cons /= mempty && not (orderZero e_t)) $
addError (locOf e) mempty . withIndexLink "consuming-argument" $
"Argument of functional type"
</> indent 2 (pretty e_t)
</> "contains consumption, which is not allowed."
pure (e', e_als)
-- | An alias of a new internal name standing for an intermediate value, with
-- the reason it exists recorded for error messages.
internalAlias :: Name -> NameReason -> CheckM Alias
internalAlias desc reason = do
v <- VName desc <$> incCounter
modify $ \s -> s {stateNames = M.insert v reason $ stateNames s}
pure $ AliasFree (v, [])
-- | Signal an error if a component of an argument that a parameter of this type
-- consumes shares a location with another component of the argument.
noSelfAliases :: Loc -> ParamType -> TypeAliases -> CheckM ()
noSelfAliases loc p_t t =
when (any (`S.member` sharedLocations t) $ aliasLocs $ aliasesWithDiet Consume p_t t) $
addError loc mempty . withIndexLink "self-aliasing-arg" $
"Argument passed for consuming parameter is self-aliased."
-- | Pass checked arguments, each with the type of its parameter, to a function
-- with the given aliases. The call uses the function and every argument, and
-- then consumes what the parameters consume. See Note [Locations].
passArgs :: Loc -> Aliases -> [(ParamType, (Exp, TypeAliases))] -> CheckM ()
passArgs loc f_als args = do
checkIfConsumed loc $ f_als <> foldMap (aliases . snd . snd) args
forM_ (zip [0 :: Int ..] args) $ \(i, (p_t, (e, e_als))) ->
when (diet p_t == Consume) $ do
noSelfAliases (locOf e) p_t e_als
let cons_als = aliasesWithDiet Consume p_t e_als
others = map (snd . snd) . filter ((/= i) . fst) $ zip [0 ..] args
when (cons_als `overlaps` f_als) . addError (locOf e) mempty $
"Argument is consumed, but aliases the function being applied."
case find ((cons_als `overlaps`) . aliases . snd) others of
Nothing -> pure ()
Just (other, other_als) -> do
shared <- describeShared $ aliasLocs $ cons_als `S.intersection` aliases other_als
addError (locOf e) mempty $
"Argument is consumed, but aliases"
</> indent 2 shared
</> "which is also aliased by other argument"
</> indent 2 (pretty other)
</> "at"
<+> pretty (locTextRel (locOf e) (locOf other))
<> "."
-- Passing an argument for a consuming parameter is consumption even
-- when the argument aliases nothing, as what the call returns may hold
-- it (see 'checkBound'). A fresh name records that.
passed <- internalAlias "internal_consumed_arg" $ NameAppRes Nothing $ srclocOf e
consumeAliases (locOf e) $ S.insert passed cons_als
where
-- Name a variable the programmer wrote if there is one.
describeShared locs = do
names <- gets stateNames
case L.partition ((`M.notMember` names) . fst) locs of
((v, fs) : _, _) -> pure $ prettyAlias v fs
([], l : _) -> describeLoc l
([], []) -> pure mempty
selfAliasType :: VName -> TypeBase Size o -> TypeAliases
selfAliasType v = insertSelfAliases v . unknownAliases
-- | The aliases to assume for a value whose provenance we know nothing about:
-- none at all, except what its own type says it may manufacture. This is
-- 'maybeAddSelfAliases' with no type parameters to exploit. See Note
-- [Parametric results].
unknownAliases :: TypeBase Size o -> TypeAliases
unknownAliases t = maybeAddSelfAliases (BoundV [] $ toStruct t) $ second (const mempty) t
-- | @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 :: Aliases -> ResType -> Diet -> TypeAliases -> TypeAliases
returnType _ (Array Fresh et shape) _ _ =
Array mempty et shape
returnType appres (Array Nonfresh et shape) Consume _ =
Array appres et shape
returnType appres (Array Nonfresh et shape) Observe arg =
Array (appres <> aliases arg) et shape
returnType _ (Scalar (TypeVar Fresh t targs)) _ _ =
Scalar $ TypeVar mempty t targs
returnType appres (Scalar (TypeVar Nonfresh t targs)) Consume _ =
Scalar $ TypeVar appres t targs
returnType appres (Scalar (TypeVar Nonfresh t targs)) Observe arg =
Scalar $ TypeVar (appres <> aliases arg) t targs
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 appres (Scalar (Arrow _ v pd t1 (RetType dims t2))) Consume _ =
Scalar $ Arrow appres v pd t1 $ RetType dims t2
returnType appres (Scalar (Arrow _ v pd t1 (RetType dims t2))) Observe arg =
Scalar $ Arrow (appres <> aliases arg) v pd t1 $ RetType dims t2
returnType appres (Scalar (Sum cs)) d arg =
Scalar $ Sum $ (fmap . fmap) (\et -> returnType appres et d arg) cs
-- | Check the argument that an operator section supplies for a parameter of the
-- given type. The section is a function that captures the argument, so, just as
-- a lambda cannot consume what it captures, the parameter cannot be consuming.
checkSectionArg :: TypeAliases -> ParamType -> Exp -> CheckM (Exp, TypeAliases)
checkSectionArg op_als p_t e = do
when (diet p_t == Consume) $
addError (locOf e) mempty $
textwrap "Operator sections may not supply an argument for a consuming parameter."
(e', e_als) <- checkExp e
checkIfConsumed (locOf e) $ aliases op_als
pure (e', e_als)
applyArg :: TypeAliases -> TypeAliases -> TypeAliases
applyArg (Scalar (Arrow closure_als _ d _ (RetType _ rettype))) arg_als =
returnType closure_als rettype d arg_als
applyArg _ arg_als = arg_als
applyLoopArg :: Aliases -> ParamType -> TypeAliases -> ResType -> TypeAliases
applyLoopArg appres (Scalar (Record pfs)) (Scalar (Record afs)) (Scalar (Record rfs)) =
Scalar . Record $
M.mapWithKey
(\k p_t -> applyLoopArg appres p_t (afs M.! k) (rfs M.! k))
pfs
applyLoopArg appres p_t arg_als rettype =
returnType appres rettype (diet p_t) arg_als
-- Loops are tricky because we want to infer the diets of their parameters.
-- This is pretty unusual: we do not do this for ordinary functions.
type Loop = (Pat ParamType, LoopInitBase Info VName, LoopFormBase Info VName, Exp)
-- | Mark bindings of consumed names as Consume, except those under a
-- 'PatAscription', which are left unchanged.
updateParamDiet :: (VName -> Bool) -> Pat ParamType -> Pat ParamType
updateParamDiet cons = recurse
where
recurse (Wildcard (Info t) wloc) =
Wildcard (Info $ t `setMode` Observe) wloc
recurse (PatParens p ploc) =
PatParens (recurse p) ploc
recurse (PatAttr attr p ploc) =
PatAttr attr (recurse p) ploc
recurse (Id name (Info t) iloc) =
Id name (Info $ t `setMode` m) iloc
where
m = if cons name then Consume else Observe
recurse (TuplePat pats ploc) =
TuplePat (map recurse pats) ploc
recurse (RecordPat fs ploc) =
RecordPat (map (fmap recurse) fs) ploc
recurse (PatAscription p t ploc) =
PatAscription p t ploc
recurse p@PatLit {} = p
recurse (PatConstr n t ps ploc) =
PatConstr n t (map recurse ps) ploc
-- | Check the values a loop body returns for its consumed parameters, as the
-- arguments of a call that consumes them: each must be fresh, as the result of
-- a function with the loop parameters as its parameters would have to be.
checkLoopResult :: Loc -> Pat ParamType -> TypeAliases -> CheckM ()
checkLoopResult loop_loc param body_als =
forM_ (matchPat param body_als) $ \(v, (t, als)) ->
when (diet t == Consume) . mapM_ (report v) $ unfreshness [param] shared als
where
shared = sharedLocations body_als
what v = "Return value for consuming loop parameter" <+> dquotes (prettyName v)
report v (UnfreshAliases w) =
addError loop_loc mempty . withIndexLink "consuming-loop-param-aliases" $
what v <+> "aliases" <+> dquotes (prettyName w) <> "."
report v UnfreshShared =
addError loop_loc mempty . withIndexLink "aliases-previously-returned" $
what v <+> "aliases another returned value."
report v UnfreshSelf =
addError loop_loc mempty $
what v <+> "may have internal aliases."
-- | Infer which loop parameters are consumed, and check what the body returns
-- for them. A parameter is consumed if the body consumes it, or if the value
-- returned for a consumed parameter aliases it, as that value is consumed in
-- the next iteration. See Note [Locations].
convergeLoopParam :: Loc -> Pat ParamType -> S.Set VName -> TypeAliases -> CheckM (Pat ParamType)
convergeLoopParam loop_loc param body_cons body_als
| body_cons' /= body_cons = convergeLoopParam loop_loc param body_cons' body_als
| otherwise = do
checkLoopResult loop_loc param' body_als
pure param'
where
param' = updateParamDiet (`S.member` body_cons) param
returned = toList $ matchPat param' body_als
cons_als = foldMap (aliases . snd . snd) $ filter ((== Consume) . diet . fst . snd) returned
body_cons' = body_cons <> S.filter (`elem` patNames param) (aliasVars cons_als)
-- | Check the form of a loop with the given parameter, returning the array a
-- for-in loop iterates over.
checkLoopForm ::
Pat ParamType ->
LoopFormBase Info VName ->
CheckM (LoopFormBase Info VName, Maybe (Exp, TypeAliases))
checkLoopForm _ (ForIn pat e) = do
(e', e_als) <- checkExp e
pure (ForIn pat e', Just (e', e_als))
checkLoopForm param (While cond) = do
-- A condition is evaluated repeatedly and may not consume anything.
((cond', _), _) <-
contain . noConsumable . bindingParam (fmap (second (const Observe)) param) $
checkExp cond
pure (While cond', Nothing)
checkLoopForm _ form = (,Nothing) <$> checkSubExps form
-- | A loop evaluates its initial value and then its form, and then passes the
-- initial value to the first iteration, as if calling a function that also
-- observes the array a for-in loop iterates over. See Note [Locations].
checkLoop :: Loc -> Loop -> CheckM (Loop, TypeAliases)
checkLoop loop_loc (param, arg, form, body) = do
((arg', (arg_e, arg_als)), init_cons) <- contain $ case arg of
LoopInitImplicit (Info e) -> do
(e', e_als) <- checkArg e
pure (LoopInitImplicit (Info e'), (e', e_als))
LoopInitExplicit e -> do
(e', e_als) <- checkArg e
pure (LoopInitExplicit e', (e', e_als))
consumed init_cons
(form', iterated) <- checkLoopForm param form
let arr_als = foldMap (aliases . snd) iterated
-- We pretend that every part of the loop parameter has a consuming diet, as
-- we need to allow consumption in the body, which we then use to infer the
-- proper diet of the parameter.
((body', body_cons), body_als) <-
noConsumable
. bindingParam (updateParamDiet (const True) param)
. bindingLoopForm arr_als form'
$ do
((body', body_als), body_cons) <- contain $ checkExp body
pure ((body', body_cons), body_als)
param' <- convergeLoopParam loop_loc param (S.map fst (M.keysSet body_cons)) body_als
let param_t = patternType param'
iteratedArg (e, e_als) = (toParam Observe (typeOf e), (e, e_als))
(_, entry_cons) <-
contain . passArgs loop_loc mempty $
(param_t, (arg_e, arg_als)) : maybeToList (iteratedArg <$> iterated)
consumed entry_cons
let arg_cons = init_cons <> entry_cons
let checkFree what e = do
free_bound <- boundFreeInExp e
let bad = any (isJust . deadIn arg_cons) . aliasLocs . aliases . snd
forM_ (filter bad $ M.toList free_bound) $ \(v, _) -> do
v' <- describeVar v
addError loop_loc mempty $
what
<+> "uses"
<+> v'
<> " (or an alias),"
</> "but this is consumed by the initial loop argument."
checkFree "Loop body" body
case form of
While cond -> checkFree "Loop condition" cond
_ -> pure ()
loop_al <- internalAlias "internal_loop_result" $ NameLoopRes $ srclocOf loop_loc
-- The value of an observed parameter may come from any observed part of the
-- initial value, or of what the body returns, as the loop may move values
-- between parameters from one iteration to the next.
let loop_als =
applyLoopArg
( S.insert loop_al $
aliasesWithDiet Observe param_t arg_als
<> aliasesWithDiet Observe param_t body_als
)
param_t
arg_als
(paramToRes param_t)
pure
( (param', arg', form', body'),
loop_als `combineAliases` body_als
)
-- | The type parameters at the components of a result, if every component is
-- either primitive or a type parameter.
resultVars :: [VName] -> ResType -> Maybe [VName]
resultVars tps (Scalar (Record fs)) = concat <$> mapM (resultVars tps) (M.elems fs)
resultVars _ (Scalar Prim {}) = Just []
resultVars tps (Scalar (TypeVar _ v []))
| qualLeaf v `elem` tps = Just [qualLeaf v]
resultVars _ _ = Nothing
-- | Does the type parameter occur at no negative position in the type, which
-- is itself at a positive position if the flag is set? An occurrence in the
-- argument of an abstract type counts as negative, as we cannot see where it
-- ends up.
noNegative :: VName -> Bool -> TypeBase dim o -> Bool
noNegative a pos (Array _ _ et) = noNegative a pos (Scalar et)
noNegative _ _ (Scalar Prim {}) = True
noNegative a pos (Scalar (TypeVar _ v targs)) =
(pos || qualLeaf v /= a) && all argOk targs
where
argOk (TypeArgType t) = not $ a `S.member` typeVars t
argOk TypeArgDim {} = True
noNegative a pos (Scalar (Record fs)) = all (noNegative a pos) fs
noNegative a pos (Scalar (Sum cs)) = all (all (noNegative a pos)) cs
noNegative a pos (Scalar (Arrow _ _ _ pt (RetType _ rt))) =
noNegative a (not pos) pt && noNegative a pos rt
-- | The sources of a type parameter among the parameters of a function, as
-- parameter positions and paths through records: the components that are
-- functions which observe their argument and return the type parameter.
-- 'Nothing' if the type parameter occurs at a negative position that is not a
-- source. See Note [Parametric results].
callSources :: VName -> [StructType] -> Maybe [(Int, Path)]
callSources a = fmap concat . zipWithM onParam [0 ..]
where
onParam i = fmap (map (i,)) . onComponent []
onComponent p (Scalar (Record fs)) =
concat <$> mapM (\(k, t) -> onComponent (p ++ [k]) t) (M.toList fs)
onComponent p (Scalar (Arrow _ _ Observe pt (RetType _ (Scalar (TypeVar _ v [])))))
| qualLeaf v == a = [p] <$ guard (noNegative a True pt)
onComponent _ t = [] <$ guard (noNegative a False t)
-- | The sources of the type parameters in the result of a function with this
-- declared type, if parametricity says that the result can only be made of what
-- calls of them return. This is the case when every component of the result is
-- primitive or a type parameter, each type parameter occurs once, and each has
-- a source and no other negative occurrence. See Note [Parametric results].
resultSources :: [TypeParam] -> [StructType] -> ResType -> Maybe [(Int, Path)]
resultSources tparams params res = do
vs <- resultVars [v | TypeParamType _ v _ <- tparams] res
guard $ length (nubOrd vs) == length vs
fmap concat . forM vs $ \v -> do
srcs <- callSources v params
guard $ not $ null srcs
pure srcs
-- | Peel the parameters off a function type, returning their types (in order)
-- and the type of the final result. 'Nothing' for a non-function type. This is
-- 'unfoldFunType' except that it preserves the freshness of the result, which
-- is exactly what we are asking about here.
funParts :: TypeBase Size u -> Maybe ([StructType], ResType)
funParts (Scalar (Arrow _ _ _ pt (RetType _ t))) = Just $ go [pt] t
where
go ps (Scalar (Arrow _ _ _ pt' (RetType _ t'))) = go (pt' : ps) t'
go ps t' = (reverse ps, t')
funParts _ = Nothing
-- | Does applying this function construct its result freshly? That is so when
-- every part of its (curried) result is fresh or primitive. Requiring the
-- result to be order zero keeps us from claiming that a closure over the other
-- arguments aliases nothing.
constructsFresh :: TypeBase Size u -> Bool
constructsFresh t
| Just (_, rt) <- funParts t = orderZero rt && allFresh rt
| otherwise = False
where
allFresh (Scalar (Record fs)) = all allFresh fs
allFresh (Scalar (Sum cs)) = all (all allFresh) cs
allFresh (Scalar Prim {}) = True
allFresh (Scalar (TypeVar u _ _)) = u == Fresh
allFresh (Array u _ _) = u == Fresh
allFresh (Scalar Arrow {}) = False
-- | Mark as fresh the result of a function with this many parameters.
freshenResult :: Int -> TypeBase Size o -> TypeBase Size o
freshenResult n (Scalar (Arrow u pn d pt (RetType ext rt))) =
Scalar . Arrow u pn d pt . RetType ext $
if n == 1 then rt `setMode` Fresh else freshenResult (n - 1) rt
freshenResult _ t = t
-- | The type of a global applied to arguments of the given types, with what
-- parametricity tells us about the freshness of the result recorded in it. Only
-- an application that supplies every parameter of the type is refined. See Note
-- [Parametric results].
parametricFreshness ::
QualName VName ->
StructType ->
[StructType] ->
CheckM StructType
parametricFreshness qn ftype argtypes = do
globals <- asks envGlobal
pure $ fromMaybe ftype $ do
BoundV tparams decl <- globals qn
(param_ts, res) <- funParts decl
guard $ length argtypes == length param_ts
srcs <- resultSources tparams param_ts res
guard $ all (maybe False constructsFresh . argAt) srcs
Just $ freshenResult (length param_ts) ftype
where
argAt (i, p) = componentAt p $ argtypes !! i
-- | Apply a function with the given aliases to checked arguments, returning the
-- aliases of the result.
checkApply :: SrcLoc -> Maybe (QualName VName) -> TypeAliases -> [(Exp, TypeAliases)] -> CheckM TypeAliases
checkApply loc fname f_als args = do
passArgs (locOf loc) (aliases f_als) $ zipWith withParam (diets f_als) args
app_al <- internalAlias "internal_app_result" $ NameAppRes fname loc
pure $ foldl applyArg (second (S.insert app_al) f_als) $ map snd args
where
withParam d (e, e_als) = (toParam d (typeOf e), (e, e_als))
diets :: TypeBase dim o -> [Diet]
diets (Scalar (Arrow _ _ d _ (RetType _ rt))) = d : diets rt
diets _ = repeat Observe
-- | Join the results of the branches of a branching expression (described by
-- the string), given everything consumed by any of them. An alias survives if
-- it and everything it aliases is still alive; the rest are consumed. If the
-- components of some branch's result overlap, the components of the joined
-- result are tied together by a fresh name. See Note [Locations].
joinBranches :: T.Text -> Loc -> Consumed -> NE.NonEmpty TypeAliases -> CheckM TypeAliases
joinBranches what loc all_cons branches = do
vtable <- asks envVtable
let alive = isNothing . deadIn all_cons
keep a = case aliasLoc a of
Nothing -> True
Just l -> alive l && all alive (aliasOf vtable l)
t = foldl1 combineAliases branches
dropped = S.filter (not . keep) $ aliases t
consumed $ all_cons <> M.fromList (map (,loc) (aliasLocs dropped))
tie <-
if all separated branches
then pure id
else S.insert <$> internalAlias "internal_branch_result" (NameBranchRes what (srclocOf loc))
pure $ second (tie . S.filter keep) t
-- | Check an expression whose value is bound to names (described by the
-- string). If that expression is a higher-order type, then it may not have
-- consumed anything. This is because we want to be able to duplicate the
-- computation for defunctionalisation purposes.
checkBound :: Doc () -> Exp -> CheckM (Exp, TypeAliases)
checkBound what e = do
((e', e_als), e_cons) <- contain $ checkExp e
consumed e_cons
let e_t = typeOf e'
when (e_cons /= mempty && not (orderZero e_t)) $
addError (locOf e) mempty . withIndexLink "contains-consumption" $
what
<+> "of higher-order type"
</> indent 2 (pretty e_t)
</> "contains consumption, which is not allowed."
pure (e', e_als)
-- Note that this may modify the type annotations inside the expression, which
-- is why we return a new one.
checkExp :: Exp -> CheckM (Exp, TypeAliases)
-- First we have the complicated cases.
--
checkExp (AppExp (Apply f args loc) appres) = do
-- Futhark evaluates the arguments of an application from right to left, and
-- then the function.
args' <- NE.reverse <$> traverse (traverse checkArg) (NE.reverse args)
f_fresh <- case f of
Var qn (Info t) floc -> do
-- It is important to use the checked arguments here, as their refined
-- types can affect parametricFreshness.
t' <- parametricFreshness qn t $ map (typeOf . fst . snd) $ NE.toList args'
pure $ Var qn (Info t') floc
_ -> pure f
(f', f_als) <- checkExp f_fresh
res_als <- checkApply loc (fname f) f_als $ map snd $ NE.toList args'
pure (AppExp (Apply f' (fmap (second fst) args') loc) appres, res_als)
where
fname (Var v _ _) = Just v
fname (AppExp (Apply e _ _) _) = fname e
fname _ = Nothing
--
checkExp (AppExp (Loop sparams pat loopinit form body loc) appres) = do
((pat', loopinit', form', body'), als) <-
checkLoop (locOf loc) (pat, loopinit, form, body)
pure
( AppExp (Loop sparams pat' loopinit' form' body' loc) appres,
als
)
--
checkExp (AppExp (LetPat sizes p e body loc) appres) = do
(e', e_als) <- checkBound "Let-bound expression" e
bindingPat p e_als $ do
(body', body_als) <- checkExp body
pure
( AppExp (LetPat sizes p e' body' loc) appres,
body_als
)
--
checkExp (AppExp (If cond te fe loc) appres) = do
(cond', _) <- checkExp cond
((te', te_als), te_cons) <- contain $ checkExp te
((fe', fe_als), fe_cons) <- contain $ checkExp fe
comb_als <- joinBranches "if-expression" (locOf loc) (te_cons <> fe_cons) $ te_als NE.:| [fe_als]
pure
( AppExp (If cond' te' fe' loc) appres,
appResType (unInfo appres) `setAliases` mempty `combineAliases` comb_als
)
--
checkExp (AppExp (Match cond cs loc) appres) = do
(cond', cond_als) <- checkBound "Matched expression" cond
((cs', cs_als), cs_cons) <-
first NE.unzip . NE.unzip <$> mapM (checkCase cond_als) cs
comb_als <- joinBranches "match-expression" (locOf loc) (fold cs_cons) cs_als
pure
( AppExp (Match cond' cs' loc) appres,
appResType (unInfo appres) `setAliases` mempty `combineAliases` comb_als
)
where
checkCase cond_als (CasePat p body caseloc) =
contain $ bindingPat p cond_als $ do
(body', body_als) <- checkExp body
pure (CasePat p body' caseloc, body_als)
--
checkExp (AppExp (LetFun fname (typarams, params, retdecl, Info (RetType ext ret), funbody) letbody loc) appres) = do
((ret', funbody'), ftype) <- bindingParams params $ do
mapM_ checkSizes retdecl
-- Throw away the consumption - it can refer only to the parameters anyway.
((funbody', funbody_als), _body_cons) <- contain $ checkExp funbody
checkReturnAlias loc params ret funbody_als
als <- closureAliases params funbody funbody_als
let ret' = maybe (inferReturnFreshness params ret funbody_als) (const ret) retdecl
ftype = funType params (RetType ext ret') `setAliases` als
pure ((ret', funbody'), ftype)
(letbody', letbody_als) <- bindingFun (fst fname) ftype $ checkExp letbody
pure
( AppExp (LetFun fname (typarams, params, retdecl, Info (RetType ext ret'), funbody') letbody' loc) appres,
letbody_als
)
--
checkExp (AppExp (BinOp (op, oploc) (Info op_t) (x, xp) (y, yp) loc) appres) = do
(x', x_als) <- checkArg x
(y', y_als) <- checkArg y
op_t' <- parametricFreshness op op_t [typeOf x', typeOf y']
op_als <- observeVar (locOf oploc) op op_t'
res_als <- checkApply loc (Just op) op_als [(x', x_als), (y', y_als)]
pure
( AppExp (BinOp (op, oploc) (Info op_t') (x', xp) (y', yp) loc) appres,
res_als
)
--
checkExp (Lambda params body te (Info (RetType ext ret)) loc) =
bindingParams params $ do
mapM_ checkSizes te
-- Throw away the consumption - it can refer only to the parameters
-- anyway.
((body', body_als), _body_cons) <- contain $ checkExp body
checkReturnAlias loc params ret body_als
als <- closureAliases params body body_als
let ret' = maybe (inferReturnFreshness params ret body_als) (const ret) te
ftype = funType params (RetType ext ret') `setAliases` als
pure
( Lambda params body' te (Info (RetType ext ret')) loc,
ftype
)
--
checkExp (AppExp (LetWith dst src steps ve body loc) appres) = do
steps' <- mapM checkStep steps
(ve', ve_als) <- checkExp ve
src_als <- observeVar (locOf src) (qualName (identName src)) (unInfo $ identType src)
let hasIndex = any isIndex steps
when hasIndex $ do
overlapCheck (locOf ve) (src, src_als) (ve', ve_als)
checkUpdatePath (locOf loc) steps src_als
consumeAliases (locOf loc) $ aliases src_als
(body', body_als) <- bindingIdent Consume dst $ checkExp body
pure (AppExp (LetWith dst src steps' ve' body' loc) appres, body_als)
where
isIndex UpdateStepSlice {} = True
isIndex _ = False
checkStep (UpdateStepSlice slice) = UpdateStepSlice <$> checkSubExps slice
checkStep (UpdateStepField f) = pure $ UpdateStepField f
--
checkExp (Update src steps ve t loc) = do
steps' <- mapM checkStep steps
(ve', ve_als) <- checkExp ve
(src', src_als) <- checkExp src
checkIfConsumed (locOf loc) $ aliases ve_als
let hasIndex = any isIndex steps
res_als <-
if hasIndex
then do
overlapCheck (locOf ve) (src', src_als) (ve', ve_als)
checkUpdatePath (locOf loc) steps src_als
consumeAliases (locOf loc) $ aliases src_als
pure $ second (const mempty) src_als
else pure $ updateAliases src_als steps ve_als
pure (Update src' steps' ve' t loc, res_als)
where
isIndex UpdateStepSlice {} = True
isIndex _ = False
checkStep (UpdateStepSlice slice) = UpdateStepSlice <$> checkSubExps slice
checkStep (UpdateStepField f) = pure $ UpdateStepField f
-- Cases that simply propagate aliases directly.
checkExp (Var v (Info t) loc) = do
als <- observeVar (locOf loc) v t
checkIfConsumed (locOf loc) (aliases als)
pure (Var v (Info t) loc, als)
checkExp (OpSection v (Info t) loc) = do
als <- observeVar (locOf loc) v t
checkIfConsumed (locOf loc) (aliases als)
pure (OpSection v (Info t) loc, als)
checkExp (OpSectionLeft op ftype arg arginfo retinfo loc) = do
let (Info (_, arg_t, _), Info (pn, pt2)) = arginfo
(Info ret, _) = retinfo
als <- observeVar (locOf loc) op (unInfo ftype)
(arg', arg_als) <- checkSectionArg als arg_t arg
pure
( OpSectionLeft op ftype arg' arginfo retinfo loc,
Scalar $ Arrow (aliases arg_als <> aliases als) pn (diet pt2) (toStruct pt2) ret
)
checkExp (OpSectionRight op ftype arg arginfo retinfo loc) = do
let (Info (pn, pt2), Info (_, arg_t, _)) = arginfo
Info ret = retinfo
als <- observeVar (locOf loc) op (unInfo ftype)
(arg', arg_als) <- checkSectionArg als arg_t arg
pure
( OpSectionRight op ftype arg' arginfo retinfo loc,
Scalar $ Arrow (aliases arg_als <> aliases als) pn (diet pt2) (toStruct pt2) ret
)
checkExp (UpdateSection steps t loc) = do
steps' <- mapM checkStep steps
pure (UpdateSection steps' t loc, unknownAliases (unInfo t))
where
checkStep (UpdateStepField f) = pure $ UpdateStepField f
checkStep (UpdateStepSlice slice) = UpdateStepSlice <$> checkSubExps slice
checkExp (Coerce e te t loc) = do
(e', e_als) <- checkExp e
checkSizes te
pure (Coerce e' te t loc, e_als)
checkExp (Ascript e te loc) = do
(e', e_als) <- checkExp e
checkSizes te
pure (Ascript e' te loc, e_als)
checkExp (AppExp (Index v slice loc) appres) = do
(v', v_als) <- checkExp v
slice' <- checkSubExps slice
checkIfConsumed (locOf loc) $ aliases v_als
pure
( AppExp (Index v' slice' loc) appres,
appResType (unInfo appres) `setAliases` aliases v_als
)
checkExp (Assert e1 e2 t loc) = do
(e1', _) <- checkExp e1
(e2', e2_als) <- checkExp e2
pure (Assert e1' e2' t loc, e2_als)
checkExp (Parens e loc) = do
(e', e_als) <- checkExp e
pure (Parens e' loc, e_als)
checkExp (QualParens v e loc) = do
(e', e_als) <- checkExp e
pure (QualParens v e' loc, e_als)
checkExp (Attr attr e loc) = do
(e', e_als) <- checkExp e
pure (Attr attr e' loc, e_als)
checkExp (Project name e t loc) = do
(e', e_als) <- checkExp e
pure
( Project name e' t loc,
case e_als of
Scalar (Record fs)
| Just name_als <- M.lookup name fs -> name_als
_ -> error $ "checkExp Project: bad type " <> prettyString e_als
)
checkExp (TupLit es loc) = do
(es', es_als) <- mapAndUnzipM checkExp es
checkIfConsumed (locOf loc) $ foldMap aliases es_als
pure (TupLit es' loc, Scalar $ tupleRecord es_als)
checkExp (Constr name es t loc) = do
(es', es_als) <- mapAndUnzipM checkExp es
checkIfConsumed (locOf loc) $ foldMap aliases es_als
pure
( Constr name es' t loc,
case unInfo t of
Scalar (Sum cs) ->
Scalar . Sum . M.insert name es_als $
M.map (map (`setAliases` mempty)) cs
t' -> error $ "checkExp Constr: bad type " <> prettyString t'
)
checkExp (RecordLit fs loc) = do
(fs', fs_als) <- mapAndUnzipM checkField fs
checkIfConsumed (locOf loc) $ foldMap (aliases . snd) fs_als
pure (RecordLit fs' loc, Scalar $ Record $ M.fromList fs_als)
where
checkField (RecordFieldExplicit name e floc) = do
(e', e_als) <- checkExp e
pure (RecordFieldExplicit name e' floc, (unLoc name, e_als))
checkField (RecordFieldImplicit name t floc) = do
name_als <- observeVar (locOf floc) (qualName (unLoc name)) $ unInfo t
pure (RecordFieldImplicit name t floc, (baseName (unLoc name), name_als))
-- Cases that create alias-free values.
checkExp e@(AppExp Range {} _) = noAliases e
checkExp e@IntLit {} = noAliases e
checkExp e@FloatLit {} = noAliases e
checkExp e@Literal {} = noAliases e
checkExp e@StringLit {} = noAliases e
checkExp e@ArrayVal {} = noAliases e
checkExp (ArrayLit es t loc) = do
(es', es_als) <- mapAndUnzipM checkExp es
checkIfConsumed (locOf loc) $ foldMap aliases es_als
pure (ArrayLit es' t loc, unknownAliases (unInfo t))
checkExp e@Negate {} = noAliases e
checkExp e@Not {} = noAliases e
checkExp e@Hole {} = noAliases e
-- | Type-check a value definition. This also infers a new return
-- type that may be fresher than previously.
checkValDef ::
-- | The type scheme of any global, along with the type parameters it is
-- polymorphic in. See Note [Parametric results].
(QualName VName -> Maybe BoundV) ->
(VName, [TypeParam], [Pat ParamType], Exp, ResRetType, Maybe (TypeExp Exp VName), SrcLoc) ->
((Exp, ResRetType), [TypeError])
checkValDef globals (fname, tparams, params, body, RetType ext ret, retdecl, loc) = runCheckM globals' (locOf loc) $ do
fmap fst . bindingParams params $ do
mapM_ checkSizes retdecl
-- A top-level constant is a name like any other.
(body', body_als) <-
if null params then checkBound "Top-level constant" body else checkExp body
checkReturnAlias loc params ret body_als
-- If the user did not provide an annotation (meaning the return type is
-- fully inferred), we infer the freshness. Otherwise, we go with whatever
-- they wanted. This lets the user define nonfresh return types even if the
-- body actually has no aliases.
ret' <- case retdecl of
Just retdecl' -> do
when (null params && fresh ret) $
addError retdecl' mempty "A top-level constant cannot be declared fresh."
pure $ RetType ext ret
Nothing ->
pure $
RetType ext $
inferReturnFreshness params ret body_als
pure
( (body', ret'),
body_als -- Don't matter.
)
where
-- Recursion is monomorphic, so a recursive call is at the type parameters
-- of the definition itself.
globals' qn
| qualLeaf qn == fname = Just $ BoundV tparams $ funType params (RetType ext ret)
| otherwise = globals qn
{-# NOINLINE checkValDef #-}
-- Note [Parametric results]
--
-- Parametricity tells us three things about the result of applying a global
-- function, all read from its *declared* type scheme, which 'envGlobal' looks
-- up: whether the application may have manufactured a value with internal
-- aliasing, whether the result must be fresh because it is the result of an
-- argument that constructs its results freshly, and whether the result may
-- alias a global.
--
-- ## Internal aliasing
--
-- The type system cannot talk about a value that aliases *itself*. For example,
-- a value that is, behind an abstraction boundary, a pair of arrays that are
-- really the same array. Such a value can never be consumed, nor given a fresh
-- type. 'AliasSelf' stands for that possibility. It is not an alias of any
-- variable ('aliasVar' is 'Nothing' for it), so it must never be mistaken for
-- one; ask "might these two values share memory?" through 'overlaps' rather
-- than by comparing alias sets directly. We can think that when 'AliasSelf' is
-- part of an aliasing set then we have "imprecise aliases", and otherwise we
-- have "precise aliases" (but do not take these terms literally; aliasing is
-- almost always an over-approximation).
--
-- Parametricity is what tells us whether such a value can have been
-- manufactured by a given function application.
--
-- The crude answer - a value has internal aliasing whenever it is produced by
-- applying a function whose result type is a nonfresh abstract type - is
-- sound but far too coarse. It refuses
--
-- module pm (M: {type t}) = {
-- def f (x: *M.t) : *M.t = id x
-- }
--
-- because @id@ is instantiated at @M.t -> M.t@. But @id@ manufactures nothing:
-- its declared type @a -> a@ means, by parametricity, that what it returns *is*
-- its argument, whose aliases we know precisely.
--
-- So we perform a more sophisticated reasonong: a function can only manufacture
-- an abstract value if its result mentions an abstract type that is not one of
-- its own type parameters ('manufacturesAbstract'). This is not the same as
-- "the abstract type also occurs in a parameter": a monomorphic @f: M.t -> M.t@
-- inside a module might well be @\_ -> M.mk 5@, so its type tells us nothing
-- (tests/uniqueness/uniqueness-error75.fut). Only genuine polymorphism does.
--
-- Consumption checking sees only instantiated types, so the declared type is
-- looked up when a name is mentioned ('envGlobal', consulted by 'observeVar')
-- and the answer recorded in the type as an 'AliasSelf' on each function
-- component ('addSelfAliases'). From there ordinary alias propagation carries
-- it: through binding, so @let my_mk = M.mk in my_mk n@ still manufactures;
-- through 'returnType', so partial application does not lose it, and neither
-- does passing the function as an argument, so @n |> M.mk@ manufactures even
-- though @|>@ itself does not. No arity bookkeeping is needed, because
-- 'AliasSelf' means the same thing at every arity: on a function, "applying
-- this may yield an internally-aliased value", and on a value, "this may have
-- internal aliasing". 'returnType' moves between the two readings for free as
-- the result stops being an arrow.
--
-- This is a conservative over-approximation we use whenever we have no better
-- information available. Hence 'unknownAliases', used for parameters
-- ('selfAliasType') and for any type we build out of thin air, and hence
-- 'closureAliases' keeping the 'AliasSelf' that a function defined here picked
-- up from its own body. Alias sets are combined by union, and a union of "may"
-- is again a "may"; the join of branches in Note [Locations] drops aliases, but
-- never 'AliasSelf'. In some sense, 'AliasSelf' behaves a bit like the top
-- element of a lattice.
--
-- ## Freshness
--
-- Futhark does not have "freshness polymorphism", but we can infer it in some
-- cases by parametricity. Consider
--
-- def (|>) 'a '^b (x: a) (f: a -> b) : b = f x
--
-- The only way for a function to obtain a value of one of its type parameters
-- is to be handed one. Here @b@ occurs among the parameters only as the result
-- of @f@, so the result of @|>@ is necessarily the result of calling @f@. When
-- @f@ in addition constructs its result freshly - as @copy: t -> *t@ does - so
-- does the application.
--
-- In general, a *source* of a type parameter @b@ is a component of a parameter
-- (reached through records) that is a function @t -> b@ observing its argument
-- ('callSources'). The result of an application is fresh when
-- ('resultSources'):
--
-- - every component of the result is either primitive or a type parameter,
-- and each type parameter occurs in it once;
--
-- - each of these type parameters has a source, and occurs at no negative
-- position among the parameters other than its sources; and
--
-- - the argument given for each source constructs its result freshly.
--
-- A negative occurrence that is not a source, such as a parameter of type @b@
-- or @[]b@, or @b@ in the parameter of a source, is a way for the function to
-- be handed values of @b@ other than by calling a source, and the result may
-- then be one of those. An occurrence in the argument of an abstract type
-- counts, as we cannot see where it ends up. A source must also take a single
-- argument and observe it. We know of no program that goes wrong without this
-- restriction, but the argument above has not been made for curried or
-- consuming functions, so they are not sources. The single occurrence is needed
-- because the function may return the result of one call twice:
--
-- def dup 'a 'b (f: a -> b) (x: a) : (b, b) = let r = f x in (r, r)
--
-- Each component of @dup mk_new x@ is fresh on its own, but they are the same
-- array (tests/uniqueness/uniqueness-error118.fut).
--
-- This is a property of the application, not of @|>@ or of its instantiation:
-- @xs |> copy@ is fresh and @xs |> id@ is not, at the very same instantiation.
-- Recall that the instantiation from Terms.hs does not have freshness
-- propagated, so the result in the type is nonfresh, as specified in the type
-- scheme. However, we here update the _instantiated_ type of @|>@ at the
-- application ('parametricFreshness'), which becomes
--
-- (x: []i32) -> (f: []i32 -> *[]i32) -> *[]i32
--
-- From there the ordinary rule for applying a function with a fresh return
-- type does the rest, and later passes get it for free: the monomorphiser keys
-- instances on the type, so @xs |> copy@ and @xs |> id@ become distinct
-- instances, and 'freshenFromInst' in Futhark.Internalise.Monomorphise carries
-- the freshness into the generated definition. Only the result is marked. The
-- body of that definition is @f x@, with @f@ still declared to return a
-- nonfresh value, but nothing checks the one against the other:
-- defunctionalisation replaces @f@ by the function it is applied to, and the
-- call then has the return type of that function.
--
-- A core restriction is that only an application that supplies every parameter
-- of the function's *type* is refined. A partial application may already have
-- evaluated part of the function's body, and the closure it produces may then
-- hold what that part computed. Consider
--
-- def trap 'a 'b 'c (f: a -> b) (x: a) : c -> b =
-- let r = f x in \(_: c) -> r
--
-- Each call @trap mk_new x u@ computes its own @r@, so its result is fresh. But
-- @k = trap mk_new x@ computes @r@ once, and every call of @k@ returns that
-- same @r@ (tests/higher-order-functions/trap.fut). Read plainly, the result
-- of calling @k@ aliases @k@, which is what makes consuming it safe. The type
-- does not say how much of it a partial application evaluates, so no partial
-- application is refined - an operator section included.
--
-- Which parameter a type variable came from is a fact about the declared type,
-- which the instantiated type does not record, so the applied expression must
-- be a direct mention of a named global. Semantically equal programs are
-- therefore treated differently -
--
-- xs |> copy -- fresh
-- (|>) xs copy -- not fresh
--
-- - and the refinement is lost by anything that obscures the head, including
-- parentheses and @let@. This is never *wrong*, only conservative: a spelling
-- we do not recognise yields the plain reading.
--
-- ## Globals
--
-- A use of a global aliases that global, and globals cannot be consumed. When
-- applying a global function returning a nonfresh result, the result thereby
-- aliases the global, and hence cannot be consumed.
--
-- Parametricity keeps polymorphic functions such as @transpose@ precise
-- ('globalAliases'). An edge case is polymorphic "values", which arise solely
-- (I think) for arrays, as an empty array literal can have any element type. To
-- address this, our semantics for polymorphic values is that they are
-- implicitly functions; re-computed on every access to the global. The
-- monomorphiser ensures that by compiling a polymorphic value as a function of
-- @()@, so that each use computes it anew, just as a size-polymorphic value is
-- a function of its sizes. Hence:
--
-- - A component that is not a function, and whose declared type contains one of
-- the global's type parameters, does not alias the global. So @empty 'a :
-- []a@ aliases nothing, while the first component of @pv 'a : ([]i32, []a)@
-- aliases @pv@. An array such as @[](a, i32)@ also counts: it has elements
-- only if it was handed some, and the only way of pairing them with other
-- data, @zip@, constructs its result freshly.
--
-- - A type parameter that is an argument to an abstract type does not count.
-- The module defining @M.t@ may well have @type t 'a = i32@, and so a value
-- of type @M.t a@ or @[](M.t a)@ may be a global.
--
-- - A function aliases the global exactly when some nonfresh component of its
-- (curried) result is not of that kind. So @transpose@, @reverse@ and @|>@
-- alias nothing, and their results alias only their arguments, while the
-- results of @tail : []i32 -> []i32@ alias @tail@ and cannot be consumed. A
-- function has a single alias set, so in a result such as @([]i32, a)@ the
-- second component is also taken to alias the function.
--
-- Size parameters do not count: as far as types can tell, @zeros [n] : [n]i32@
-- might be (a slice of) a global, so it aliases @zeros@.
--
-- This reasoning needs the type parameters, which monomorphisation removes.
-- Hence, monomorphising a Futhark program results in a program that may no
-- longer be correct as far as (this) alias analysis is concerned.
-- Note [Locations]
--
-- Compound types (records and sums) do not have identity. Instead, we track
-- aliasing and consumption at the level of their components ("leaves"). A
-- "path" is a reference to the component of a compound type.
--
-- A location is a variable together with a path ('Location'); every 'Alias'
-- except 'AliasSelf' denotes one. The consumed set holds locations, and a
-- location is dead if a location on the same variable has been consumed whose
-- path is a prefix of its own, or of which its own is a prefix ('deadIn').
-- Consuming @p.a@ kills @p.a@, everything under it, and @p@ itself; consuming
-- @p@ kills all of @p@.
--
-- The payload of a constructor is treated exactly as a tuple, nested under the
-- constructor name: the payload of @#foo xs ys@ has the paths @[foo, 0]@ and
-- @[foo, 1]@. The components of a sum are therefore separate parts, so
-- @#foo u u@ is self-aliasing just like @(u, u)@, and its payload can be taken
-- apart by pattern matching just like a tuple.
--
-- Using a variable reads all of it: its alias set has a location for each of
-- its leaves, and observing it requires them all to be alive. Projection
-- happens afterwards. So to consume one component of a tuple and keep using
-- another, take the tuple apart first:
--
-- let (a, b) = p in let a[0] = 1 in b -- accepted
-- let a = p.0 in let a[0] = 1 in p.1 -- rejected: p.1 reads p
--
-- Components that may coincide have overlapping alias sets, which is what
-- 'separated' and 'unfreshness' look for. Building a value preserves this, as
-- each component aliases what it was built from, and so does applying a
-- function or running a loop, as every nonfresh component of the result aliases
-- the same internal name. The exceptions are an observed parameter, whose
-- components the caller may have made coincide, and a component with
-- 'AliasSelf'. Neither can be consumed, and the locations of an observed
-- parameter never die.
--
-- The join of the branches of an @if@ or @match@ ('joinBranches') keeps an alias of the combined branch
-- results if it is 'AliasSelf', or if its location and every location in its
-- alias set ('aliasOf') are alive after the branches; the other aliases are
-- consumed. Filtering by liveness in this way, rather than subtracting the
-- consumed set, is closed under aliasing: if an alias survives, so does
-- everything it aliases. This is the only place where aliases are dropped, and
-- it may drop the evidence that two components coincide. Consider
--
-- let (r0, r1) = if c then (u, u) else (let z = u with [0] = 5 in (a, b))
--
-- The else branch consumes @u@, so the filter alone would leave the aliases
-- @({a}, {b})@, claiming that the components of the result are separate, which
-- is false when @c@ holds. So when the components of some branch's result
-- overlap, the join adds an alias of a fresh name to every component of the
-- combined result. Being fresh, it is alive after the branches, and as it is
-- consumed along with any component, consuming @r0@ kills @r1@.
--
-- Futhark is not in A-normal form, but an expression that builds a value from
-- operands behaves as if it were: it evaluates all of its operands, and then
-- uses their values. This covers tuples, records, constructors and arrays,
-- indexing, operator sections, and function application (which evaluates its
-- arguments from right to left, and then the function). So the value of an
-- operand must not alias anything that a later operand consumes. A function
-- application then consumes what its parameters consume. A consumed component
-- of an argument must not share a location with any other component of that
-- argument ('noSelfAliases'), and must not overlap the function being applied
-- or any other argument ('passArgs'). The diet of a function parameter is the
-- same for all of its components, but that of a loop parameter is not.
--
-- A loop is checked as a recursive call whose arguments are what its body
-- returns ('checkLoopResult'). The value returned for a consumed loop
-- parameter is consumed in the next iteration, so it must be fresh in exactly
-- the sense below, with the loop parameters as the parameters. The diets of
-- the loop parameters are inferred first: a parameter is consumed if the body
-- consumes it or the value returned for a consumed parameter aliases it
-- ('convergeLoopParam').
--
-- A component of a function's result may be fresh exactly when every in-scope
-- location it aliases lies within a consumed part of a parameter, none of its
-- locations occurs in another component, and it is not 'selfAliased'. The one
-- predicate ('unfreshness') both infers fresh return types and checks declared
-- ones, so declared freshness never exceeds what would be inferred.