-- | 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 :: Constraints -> Set VName
overloadedTypeVars = forall a. Monoid a => [a] -> a
mconcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall {a}. (a, Constraint) -> Set VName
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [a]
M.elems
  where
    f :: (a, Constraint) -> Set VName
f (a
_, HasFields Map Name (TypeBase Size ())
fs Usage
_) = forall a. Monoid a => [a] -> a
mconcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall as dim. Monoid as => TypeBase dim as -> Set VName
typeVars forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [a]
M.elems Map Name (TypeBase Size ())
fs
    f (a, Constraint)
_ = forall a. Monoid a => a
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 :: SrcLoc -> PatType -> PatType -> TermTypeM (PatType, [VName])
unifyBranchTypes SrcLoc
loc PatType
t1 PatType
t2 =
  forall a. Checking -> TermTypeM a -> TermTypeM a
onFailure (TypeBase Size () -> TypeBase Size () -> Checking
CheckingBranches (forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct PatType
t1) (forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct PatType
t2)) forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *).
MonadUnify m =>
Usage -> PatType -> PatType -> m (PatType, [VName])
unifyMostCommon (SrcLoc -> Text -> Usage
mkUsage SrcLoc
loc Text
"unification of branch results") PatType
t1 PatType
t2

unifyBranches :: SrcLoc -> Exp -> Exp -> TermTypeM (PatType, [VName])
unifyBranches :: SrcLoc -> Exp -> Exp -> TermTypeM (PatType, [VName])
unifyBranches SrcLoc
loc Exp
e1 Exp
e2 = do
  PatType
e1_t <- Exp -> TermTypeM PatType
expTypeFully Exp
e1
  PatType
e2_t <- Exp -> TermTypeM PatType
expTypeFully Exp
e2
  SrcLoc -> PatType -> PatType -> TermTypeM (PatType, [VName])
unifyBranchTypes SrcLoc
loc PatType
e1_t PatType
e2_t

sliceShape ::
  Maybe (SrcLoc, Rigidity) ->
  Slice ->
  TypeBase Size as ->
  TermTypeM (TypeBase Size as, [VName])
sliceShape :: forall as.
Maybe (SrcLoc, Rigidity)
-> Slice
-> TypeBase Size as
-> TermTypeM (TypeBase Size as, [VName])
sliceShape Maybe (SrcLoc, Rigidity)
r Slice
slice t :: TypeBase Size as
t@(Array as
als Uniqueness
u (Shape [Size]
orig_dims) ScalarTypeBase Size ()
et) =
  forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT ([Size] -> TypeBase Size as
setDims forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {t :: (* -> *) -> * -> *}.
(MonadTrans t, MonadState [VName] (t TermTypeM)) =>
Slice -> [Size] -> t TermTypeM [Size]
adjustDims Slice
slice [Size]
orig_dims) []
  where
    setDims :: [Size] -> TypeBase Size as
setDims [] = forall dim as. Int -> TypeBase dim as -> TypeBase dim as
stripArray (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Size]
orig_dims) TypeBase Size as
t
    setDims [Size]
dims' = forall dim as.
as
-> Uniqueness
-> Shape dim
-> ScalarTypeBase dim ()
-> TypeBase dim as
Array as
als Uniqueness
u (forall dim. [dim] -> Shape dim
Shape [Size]
dims') ScalarTypeBase Size ()
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 :: Rigidity -> Bool
isRigid Rigid {} = Bool
True
    isRigid Rigidity
_ = Bool
False
    refine_sizes :: Bool
refine_sizes = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Rigidity -> Bool
isRigid forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) Maybe (SrcLoc, Rigidity)
r

    sliceSize :: Size -> Maybe Exp -> Maybe Exp -> Maybe Exp -> t TermTypeM Size
sliceSize Size
orig_d Maybe Exp
i Maybe Exp
j Maybe Exp
stride =
      case Maybe (SrcLoc, Rigidity)
r of
        Just (SrcLoc
loc, Rigid RigidSource
_) -> do
          (Size
d, Maybe VName
ext) <-
            forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. SrcLoc -> SizeSource -> TermTypeM (Size, Maybe VName)
extSize SrcLoc
loc forall a b. (a -> b) -> a -> b
$
              Maybe Size
-> Maybe (ExpBase NoInfo VName)
-> Maybe (ExpBase NoInfo VName)
-> Maybe (ExpBase NoInfo VName)
-> SizeSource
SourceSlice Maybe Size
orig_d' (Exp -> ExpBase NoInfo VName
bareExp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Exp
i) (Exp -> ExpBase NoInfo VName
bareExp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Exp
j) (Exp -> ExpBase NoInfo VName
bareExp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Exp
stride)
          forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (forall a. Maybe a -> [a]
maybeToList Maybe VName
ext ++)
          forall (f :: * -> *) a. Applicative f => a -> f a
pure Size
d
        Just (SrcLoc
loc, Rigidity
Nonrigid) ->
          forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ QualName VName -> Size
NamedSize forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall v. v -> QualName v
qualName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadUnify m =>
SrcLoc -> Rigidity -> Name -> m VName
newDimVar SrcLoc
loc Rigidity
Nonrigid Name
"slice_dim"
        Maybe (SrcLoc, Rigidity)
Nothing -> do
          VName
v <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadTypeChecker m => Name -> m VName
newID Name
"slice_anydim"
          forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (VName
v :)
          forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ QualName VName -> Size
NamedSize forall a b. (a -> b) -> a -> b
$ forall v. v -> QualName v
qualName VName
v
      where
        -- The original size does not matter if the slice is fully specified.
        orig_d' :: Maybe Size
orig_d'
          | forall a. Maybe a -> Bool
isJust Maybe Exp
i, forall a. Maybe a -> Bool
isJust Maybe Exp
j = forall a. Maybe a
Nothing
          | Bool
otherwise = forall a. a -> Maybe a
Just Size
orig_d

    adjustDims :: Slice -> [Size] -> t TermTypeM [Size]
adjustDims (DimFix {} : Slice
idxes') (Size
_ : [Size]
dims) =
      Slice -> [Size] -> t TermTypeM [Size]
adjustDims Slice
idxes' [Size]
dims
    -- Pat match some known slices to be non-existential.
    adjustDims (DimSlice Maybe Exp
i Maybe Exp
j Maybe Exp
stride : Slice
idxes') (Size
_ : [Size]
dims)
      | Bool
refine_sizes,
        forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True ((forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just Int64
0) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Exp -> Maybe Int64
isInt64) Maybe Exp
i,
        Just Size
j' <- Exp -> Maybe Size
maybeDimFromExp forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Maybe Exp
j,
        forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True ((forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just Int64
1) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Exp -> Maybe Int64
isInt64) Maybe Exp
stride =
          (Size
j' :) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Slice -> [Size] -> t TermTypeM [Size]
adjustDims Slice
idxes' [Size]
dims
    adjustDims (DimSlice Maybe Exp
Nothing Maybe Exp
Nothing Maybe Exp
stride : Slice
idxes') (Size
d : [Size]
dims)
      | Bool
refine_sizes,
        forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False ((forall a. Eq a => a -> a -> Bool
== Int64
1) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Num a => a -> a
abs) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Exp -> Maybe Int64
isInt64) Maybe Exp
stride =
          (Size
d :) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Slice -> [Size] -> t TermTypeM [Size]
adjustDims Slice
idxes' [Size]
dims
    adjustDims (DimSlice Maybe Exp
i Maybe Exp
j Maybe Exp
stride : Slice
idxes') (Size
d : [Size]
dims) =
      (:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {t :: (* -> *) -> * -> *}.
(MonadTrans t, MonadState [VName] (t TermTypeM)) =>
Size -> Maybe Exp -> Maybe Exp -> Maybe Exp -> t TermTypeM Size
sliceSize Size
d Maybe Exp
i Maybe Exp
j Maybe Exp
stride forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Slice -> [Size] -> t TermTypeM [Size]
adjustDims Slice
idxes' [Size]
dims
    adjustDims Slice
_ [Size]
dims =
      forall (f :: * -> *) a. Applicative f => a -> f a
pure [Size]
dims
sliceShape Maybe (SrcLoc, Rigidity)
_ Slice
_ TypeBase Size as
t = forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeBase Size as
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 :: [PatBase Info VName] -> Occurrences -> TermTypeM Aliasing
lexicalClosure [PatBase Info VName]
params Occurrences
closure = do
  Map VName ValBinding
vtable <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks forall a b. (a -> b) -> a -> b
$ TermScope -> Map VName ValBinding
scopeVtable forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermEnv -> TermScope
termScope
  let isGlobal :: VName -> Bool
isGlobal VName
v = case VName
v forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` Map VName ValBinding
vtable of
        Just (BoundV Locality
Global [TypeParamBase VName]
_ PatType
_) -> Bool
True
        Just EqualityF {} -> Bool
True
        Just OverloadedF {} -> Bool
True
        Just (BoundV Locality
Local [TypeParamBase VName]
_ PatType
_) -> Bool
False
        Just (BoundV Locality
Nonlocal [TypeParamBase VName]
_ PatType
_) -> Bool
False
        Just WasConsumed {} -> Bool
False
        Maybe ValBinding
Nothing -> Bool
False
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map VName -> Alias
AliasBound forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> Set a -> Set a
S.filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. VName -> Bool
isGlobal) forall a b. (a -> b) -> a -> b
$
    Occurrences -> Set VName
allOccurring Occurrences
closure forall a. Ord a => Set a -> Set a -> Set a
S.\\ forall a. Monoid a => [a] -> a
mconcat (forall a b. (a -> b) -> [a] -> [b]
map forall (f :: * -> *) vn.
(Functor f, Ord vn) =>
PatBase f vn -> Set vn
patNames [PatBase Info VName]
params)

noAliasesIfOverloaded :: PatType -> TermTypeM PatType
noAliasesIfOverloaded :: PatType -> TermTypeM PatType
noAliasesIfOverloaded t :: PatType
t@(Scalar (TypeVar Aliasing
_ Uniqueness
u QualName VName
tn [])) = do
  Maybe Constraint
subst <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (forall vn. QualName vn -> vn
qualLeaf QualName VName
tn) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
  case Maybe Constraint
subst of
    Just Overloaded {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as.
as
-> Uniqueness
-> QualName VName
-> [TypeArg dim]
-> ScalarTypeBase dim as
TypeVar forall a. Monoid a => a
mempty Uniqueness
u QualName VName
tn []
    Maybe Constraint
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure PatType
t
noAliasesIfOverloaded PatType
t =
  forall (f :: * -> *) a. Applicative f => a -> f a
pure PatType
t

checkAscript ::
  SrcLoc ->
  UncheckedTypeExp ->
  UncheckedExp ->
  TermTypeM (TypeExp VName, Exp)
checkAscript :: SrcLoc
-> UncheckedTypeExp
-> ExpBase NoInfo Name
-> TermTypeM (TypeExp VName, Exp)
checkAscript SrcLoc
loc UncheckedTypeExp
te ExpBase NoInfo Name
e = do
  (TypeExp VName
te', TypeBase Size ()
decl_t, [VName]
_) <- UncheckedTypeExp
-> TermTypeM (TypeExp VName, TypeBase Size (), [VName])
checkTypeExpNonrigid UncheckedTypeExp
te
  Exp
e' <- ExpBase NoInfo Name -> TermTypeM Exp
checkExp ExpBase NoInfo Name
e
  TypeBase Size ()
e_t <- forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp -> TermTypeM PatType
expTypeFully Exp
e'

  forall a. Checking -> TermTypeM a -> TermTypeM a
onFailure (TypeBase Size () -> TypeBase Size () -> Checking
CheckingAscription TypeBase Size ()
decl_t TypeBase Size ()
e_t) forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *).
MonadUnify m =>
Usage -> TypeBase Size () -> TypeBase Size () -> m ()
unify (SrcLoc -> Text -> Usage
mkUsage SrcLoc
loc Text
"type ascription") TypeBase Size ()
decl_t TypeBase Size ()
e_t

  forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeExp VName
te', Exp
e')

checkCoerce ::
  SrcLoc ->
  UncheckedTypeExp ->
  UncheckedExp ->
  TermTypeM (TypeExp VName, StructType, Exp, [VName])
checkCoerce :: SrcLoc
-> UncheckedTypeExp
-> ExpBase NoInfo Name
-> TermTypeM (TypeExp VName, TypeBase Size (), Exp, [VName])
checkCoerce SrcLoc
loc UncheckedTypeExp
te ExpBase NoInfo Name
e = do
  (TypeExp VName
te', TypeBase Size ()
te_t, [VName]
ext) <- UncheckedTypeExp
-> RigidSource
-> TermTypeM (TypeExp VName, TypeBase Size (), [VName])
checkTypeExpRigid UncheckedTypeExp
te RigidSource
RigidCoerce
  Exp
e' <- ExpBase NoInfo Name -> TermTypeM Exp
checkExp ExpBase NoInfo Name
e
  TypeBase Size ()
e_t <- forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp -> TermTypeM PatType
expTypeFully Exp
e'

  (TypeBase Size ()
e_t_nonrigid, Map VName Size
_) <-
    forall als.
SrcLoc
-> Rigidity
-> Name
-> TypeBase Size als
-> TermTypeM (TypeBase Size als, Map VName Size)
allDimsFreshInType SrcLoc
loc Rigidity
Nonrigid Name
"coerce_d" TypeBase Size ()
e_t

  forall a. Checking -> TermTypeM a -> TermTypeM a
onFailure (TypeBase Size () -> TypeBase Size () -> Checking
CheckingAscription TypeBase Size ()
te_t TypeBase Size ()
e_t) forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *).
MonadUnify m =>
Usage -> TypeBase Size () -> TypeBase Size () -> m ()
unify (SrcLoc -> Text -> Usage
mkUsage SrcLoc
loc Text
"type ascription") TypeBase Size ()
te_t TypeBase Size ()
e_t_nonrigid

  TypeBase Size ()
te_t' <- forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully TypeBase Size ()
te_t

  forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeExp VName
te', TypeBase Size ()
te_t', Exp
e', [VName]
ext)

unscopeType ::
  SrcLoc ->
  M.Map VName Ident ->
  PatType ->
  TermTypeM (PatType, [VName])
unscopeType :: SrcLoc
-> Map VName (IdentBase Info VName)
-> PatType
-> TermTypeM (PatType, [VName])
unscopeType SrcLoc
tloc Map VName (IdentBase Info VName)
unscoped PatType
t = do
  (PatType
t', Map VName VName
m) <- forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (forall (f :: * -> *) fdim tdim als.
Applicative f =>
(Set VName -> DimPos -> fdim -> f tdim)
-> TypeBase fdim als -> f (TypeBase tdim als)
traverseDims forall {t :: (* -> *) -> * -> *} {m :: * -> *} {p}.
(MonadState (Map VName VName) (t m), MonadTrans t, MonadUnify m) =>
Set VName -> p -> Size -> t m Size
onDim PatType
t) forall a. Monoid a => a
mempty
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (PatType
t' forall dim asf ast.
TypeBase dim asf -> (asf -> ast) -> TypeBase dim ast
`addAliases` forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map Alias -> Alias
unAlias, forall k a. Map k a -> [a]
M.elems Map VName VName
m)
  where
    onDim :: Set VName -> p -> Size -> t m Size
onDim Set VName
bound p
_ (NamedSize QualName VName
d)
      | Just SrcLoc
loc <- forall a. Located a => a -> SrcLoc
srclocOf forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (forall vn. QualName vn -> vn
qualLeaf QualName VName
d) Map VName (IdentBase Info VName)
unscoped,
        Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall vn. QualName vn -> vn
qualLeaf QualName VName
d forall a. Ord a => a -> Set a -> Bool
`S.member` Set VName
bound =
          forall {t :: (* -> *) -> * -> *} {m :: * -> *}.
(MonadState (Map VName VName) (t m), MonadTrans t, MonadUnify m) =>
SrcLoc -> VName -> t m Size
inst SrcLoc
loc forall a b. (a -> b) -> a -> b
$ forall vn. QualName vn -> vn
qualLeaf QualName VName
d
    onDim Set VName
_ p
_ Size
d = forall (f :: * -> *) a. Applicative f => a -> f a
pure Size
d

    inst :: SrcLoc -> VName -> t m Size
inst SrcLoc
loc VName
d = do
      Maybe VName
prev <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
d
      case Maybe VName
prev of
        Just VName
d' -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ QualName VName -> Size
NamedSize forall a b. (a -> b) -> a -> b
$ forall v. v -> QualName v
qualName VName
d'
        Maybe VName
Nothing -> do
          VName
d' <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadUnify m =>
SrcLoc -> Rigidity -> Name -> m VName
newDimVar SrcLoc
tloc (RigidSource -> Rigidity
Rigid forall a b. (a -> b) -> a -> b
$ SrcLoc -> VName -> RigidSource
RigidOutOfScope SrcLoc
loc VName
d) Name
"d"
          forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
d VName
d'
          forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ QualName VName -> Size
NamedSize forall a b. (a -> b) -> a -> b
$ forall v. v -> QualName v
qualName VName
d'

    unAlias :: Alias -> Alias
unAlias (AliasBound VName
v) | VName
v forall k a. Ord k => k -> Map k a -> Bool
`M.member` Map VName (IdentBase Info VName)
unscoped = VName -> Alias
AliasFree VName
v
    unAlias Alias
a = Alias
a

-- 'checkApplyExp' is like 'checkExp', but tries to find the "root
-- function", for better error messages.
checkApplyExp :: UncheckedExp -> TermTypeM (Exp, ApplyOp)
checkApplyExp :: ExpBase NoInfo Name -> TermTypeM (Exp, ApplyOp)
checkApplyExp (AppExp (Apply ExpBase NoInfo Name
e1 ExpBase NoInfo Name
e2 NoInfo (Diet, Maybe VName)
_ SrcLoc
loc) NoInfo AppRes
_) = do
  Arg
arg <- ExpBase NoInfo Name -> TermTypeM Arg
checkArg ExpBase NoInfo Name
e2
  (Exp
e1', (Maybe (QualName VName)
fname, Int
i)) <- ExpBase NoInfo Name -> TermTypeM (Exp, ApplyOp)
checkApplyExp ExpBase NoInfo Name
e1
  PatType
t <- Exp -> TermTypeM PatType
expType Exp
e1'
  (TypeBase Size ()
t1, PatType
rt, Maybe VName
argext, [VName]
exts) <- SrcLoc
-> ApplyOp
-> PatType
-> Arg
-> TermTypeM (TypeBase Size (), PatType, Maybe VName, [VName])
checkApply SrcLoc
loc (Maybe (QualName VName)
fname, Int
i) PatType
t Arg
arg
  forall (f :: * -> *) a. Applicative f => a -> f a
pure
    ( forall (f :: * -> *) vn.
AppExpBase f vn -> f AppRes -> ExpBase f vn
AppExp
        (forall (f :: * -> *) vn.
ExpBase f vn
-> ExpBase f vn
-> f (Diet, Maybe VName)
-> SrcLoc
-> AppExpBase f vn
Apply Exp
e1' (Arg -> Exp
argExp Arg
arg) (forall a. a -> Info a
Info (forall shape as. TypeBase shape as -> Diet
diet TypeBase Size ()
t1, Maybe VName
argext)) SrcLoc
loc)
        (forall a. a -> Info a
Info forall a b. (a -> b) -> a -> b
$ PatType -> [VName] -> AppRes
AppRes PatType
rt [VName]
exts),
      (Maybe (QualName VName)
fname, Int
i forall a. Num a => a -> a -> a
+ Int
1)
    )
checkApplyExp ExpBase NoInfo Name
e = do
  Exp
e' <- ExpBase NoInfo Name -> TermTypeM Exp
checkExp ExpBase NoInfo Name
e
  forall (f :: * -> *) a. Applicative f => a -> f a
pure
    ( Exp
e',
      ( case Exp
e' of
          Var QualName VName
qn Info PatType
_ SrcLoc
_ -> forall a. a -> Maybe a
Just QualName VName
qn
          Exp
_ -> forall a. Maybe a
Nothing,
        Int
0
      )
    )

checkExp :: UncheckedExp -> TermTypeM Exp
checkExp :: ExpBase NoInfo Name -> TermTypeM Exp
checkExp (Literal PrimValue
val SrcLoc
loc) =
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn. PrimValue -> SrcLoc -> ExpBase f vn
Literal PrimValue
val SrcLoc
loc
checkExp (Hole NoInfo PatType
_ SrcLoc
loc) = do
  PatType
t <- forall (m :: * -> *) als dim.
(MonadUnify m, Monoid als) =>
SrcLoc -> Name -> m (TypeBase dim als)
newTypeVar SrcLoc
loc Name
"t"
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn. f PatType -> SrcLoc -> ExpBase f vn
Hole (forall a. a -> Info a
Info forall a b. (a -> b) -> a -> b
$ PatType
t forall dim as. TypeBase dim as -> Uniqueness -> TypeBase dim as
`setUniqueness` Uniqueness
Unique) SrcLoc
loc
checkExp (StringLit [Word8]
vs SrcLoc
loc) =
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn. [Word8] -> SrcLoc -> ExpBase f vn
StringLit [Word8]
vs SrcLoc
loc
checkExp (IntLit Integer
val NoInfo PatType
NoInfo SrcLoc
loc) = do
  TypeBase Size ()
t <- forall (m :: * -> *) als dim.
(MonadUnify m, Monoid als) =>
SrcLoc -> Name -> m (TypeBase dim als)
newTypeVar SrcLoc
loc Name
"t"
  forall (m :: * -> *).
MonadUnify m =>
[PrimType] -> Usage -> TypeBase Size () -> m ()
mustBeOneOf [PrimType]
anyNumberType (SrcLoc -> Text -> Usage
mkUsage SrcLoc
loc Text
"integer literal") TypeBase Size ()
t
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
Integer -> f PatType -> SrcLoc -> ExpBase f vn
IntLit Integer
val (forall a. a -> Info a
Info forall a b. (a -> b) -> a -> b
$ forall dim as. TypeBase dim as -> TypeBase dim Aliasing
fromStruct TypeBase Size ()
t) SrcLoc
loc
checkExp (FloatLit Double
val NoInfo PatType
NoInfo SrcLoc
loc) = do
  TypeBase Size ()
t <- forall (m :: * -> *) als dim.
(MonadUnify m, Monoid als) =>
SrcLoc -> Name -> m (TypeBase dim als)
newTypeVar SrcLoc
loc Name
"t"
  forall (m :: * -> *).
MonadUnify m =>
[PrimType] -> Usage -> TypeBase Size () -> m ()
mustBeOneOf [PrimType]
anyFloatType (SrcLoc -> Text -> Usage
mkUsage SrcLoc
loc Text
"float literal") TypeBase Size ()
t
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
Double -> f PatType -> SrcLoc -> ExpBase f vn
FloatLit Double
val (forall a. a -> Info a
Info forall a b. (a -> b) -> a -> b
$ forall dim as. TypeBase dim as -> TypeBase dim Aliasing
fromStruct TypeBase Size ()
t) SrcLoc
loc
checkExp (TupLit [ExpBase NoInfo Name]
es SrcLoc
loc) =
  forall (f :: * -> *) vn. [ExpBase f vn] -> SrcLoc -> ExpBase f vn
TupLit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ExpBase NoInfo Name -> TermTypeM Exp
checkExp [ExpBase NoInfo Name]
es forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure SrcLoc
loc
checkExp (RecordLit [FieldBase NoInfo Name]
fs SrcLoc
loc) = do
  [FieldBase Info VName]
fs' <- forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall {t :: (* -> *) -> * -> *}.
(MonadState (Map Name SrcLoc) (t TermTypeM), MonadTrans t) =>
FieldBase NoInfo Name -> t TermTypeM (FieldBase Info VName)
checkField [FieldBase NoInfo Name]
fs) forall a. Monoid a => a
mempty

  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn. [FieldBase f vn] -> SrcLoc -> ExpBase f vn
RecordLit [FieldBase Info VName]
fs' SrcLoc
loc
  where
    checkField :: FieldBase NoInfo Name -> t TermTypeM (FieldBase Info VName)
checkField (RecordFieldExplicit Name
f ExpBase NoInfo Name
e SrcLoc
rloc) = do
      forall {a} {b} {t :: (* -> *) -> * -> *} {m :: * -> *} {a}.
(MonadState (Map a b) (t m), Ord a, MonadTrans t,
 MonadTypeChecker m, Pretty a, Located a, Located b) =>
a -> a -> t m ()
errIfAlreadySet Name
f SrcLoc
rloc
      forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Name
f SrcLoc
rloc
      forall (f :: * -> *) vn.
Name -> ExpBase f vn -> SrcLoc -> FieldBase f vn
RecordFieldExplicit Name
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ExpBase NoInfo Name -> TermTypeM Exp
checkExp ExpBase NoInfo Name
e) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure SrcLoc
rloc
    checkField (RecordFieldImplicit Name
name NoInfo PatType
NoInfo SrcLoc
rloc) = do
      forall {a} {b} {t :: (* -> *) -> * -> *} {m :: * -> *} {a}.
(MonadState (Map a b) (t m), Ord a, MonadTrans t,
 MonadTypeChecker m, Pretty a, Located a, Located b) =>
a -> a -> t m ()
errIfAlreadySet Name
name SrcLoc
rloc
      (QualName [VName]
_ VName
name', PatType
t) <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadTypeChecker m =>
SrcLoc -> QualName Name -> m (QualName VName, PatType)
lookupVar SrcLoc
rloc forall a b. (a -> b) -> a -> b
$ forall v. v -> QualName v
qualName Name
name
      forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Name
name SrcLoc
rloc
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
vn -> f PatType -> SrcLoc -> FieldBase f vn
RecordFieldImplicit VName
name' (forall a. a -> Info a
Info PatType
t) SrcLoc
rloc

    errIfAlreadySet :: a -> a -> t m ()
errIfAlreadySet a
f a
rloc = do
      Maybe b
maybe_sloc <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup a
f
      case Maybe b
maybe_sloc of
        Just b
sloc ->
          forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError a
rloc forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
            Doc ()
"Field"
              forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty a
f)
              forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"previously defined at"
              forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall a b. (Located a, Located b) => a -> b -> String
locStrRel a
rloc b
sloc) forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
        Maybe b
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkExp (ArrayLit [ExpBase NoInfo Name]
all_es NoInfo PatType
_ SrcLoc
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 [ExpBase NoInfo Name]
all_es of
    [] -> do
      PatType
et <- forall (m :: * -> *) als dim.
(MonadUnify m, Monoid als) =>
SrcLoc -> Name -> m (TypeBase dim als)
newTypeVar SrcLoc
loc Name
"t"
      PatType
t <- forall dim as.
(Pretty (Shape dim), Monoid as) =>
SrcLoc
-> TypeBase dim as
-> Shape dim
-> Uniqueness
-> TermTypeM (TypeBase dim as)
arrayOfM SrcLoc
loc PatType
et (forall dim. [dim] -> Shape dim
Shape [Int -> Size
ConstSize Int
0]) Uniqueness
Unique
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
[ExpBase f vn] -> f PatType -> SrcLoc -> ExpBase f vn
ArrayLit [] (forall a. a -> Info a
Info PatType
t) SrcLoc
loc
    ExpBase NoInfo Name
e : [ExpBase NoInfo Name]
es -> do
      Exp
e' <- ExpBase NoInfo Name -> TermTypeM Exp
checkExp ExpBase NoInfo Name
e
      PatType
et <- Exp -> TermTypeM PatType
expType Exp
e'
      [Exp]
es' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Text -> TypeBase Size () -> Exp -> TermTypeM Exp
unifies Text
"type of first array element" (forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct PatType
et) forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< ExpBase NoInfo Name -> TermTypeM Exp
checkExp) [ExpBase NoInfo Name]
es
      PatType
et' <- forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully PatType
et
      PatType
t <- forall dim as.
(Pretty (Shape dim), Monoid as) =>
SrcLoc
-> TypeBase dim as
-> Shape dim
-> Uniqueness
-> TermTypeM (TypeBase dim as)
arrayOfM SrcLoc
loc PatType
et' (forall dim. [dim] -> Shape dim
Shape [Int -> Size
ConstSize forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Int
length [ExpBase NoInfo Name]
all_es]) Uniqueness
Unique
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
[ExpBase f vn] -> f PatType -> SrcLoc -> ExpBase f vn
ArrayLit (Exp
e' forall a. a -> [a] -> [a]
: [Exp]
es') (forall a. a -> Info a
Info PatType
t) SrcLoc
loc
checkExp (AppExp (Range ExpBase NoInfo Name
start Maybe (ExpBase NoInfo Name)
maybe_step Inclusiveness (ExpBase NoInfo Name)
end SrcLoc
loc) NoInfo AppRes
_) = do
  Exp
start' <- Text -> [PrimType] -> Exp -> TermTypeM Exp
require Text
"use in range expression" [PrimType]
anySignedType forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExpBase NoInfo Name -> TermTypeM Exp
checkExp ExpBase NoInfo Name
start
  TypeBase Size ()
start_t <- forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp -> TermTypeM PatType
expTypeFully Exp
start'
  Maybe Exp
maybe_step' <- case Maybe (ExpBase NoInfo Name)
maybe_step of
    Maybe (ExpBase NoInfo Name)
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
    Just ExpBase NoInfo Name
step -> do
      let warning :: TermTypeM ()
warning = forall (m :: * -> *) loc.
(MonadTypeChecker m, Located loc) =>
loc -> Doc () -> m ()
warn SrcLoc
loc Doc ()
"First and second element of range are identical, this will produce an empty array."
      case (ExpBase NoInfo Name
start, ExpBase NoInfo Name
step) of
        (Literal PrimValue
x SrcLoc
_, Literal PrimValue
y SrcLoc
_) -> forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (PrimValue
x forall a. Eq a => a -> a -> Bool
== PrimValue
y) TermTypeM ()
warning
        (Var QualName Name
x_name NoInfo PatType
_ SrcLoc
_, Var QualName Name
y_name NoInfo PatType
_ SrcLoc
_) -> forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (QualName Name
x_name forall a. Eq a => a -> a -> Bool
== QualName Name
y_name) TermTypeM ()
warning
        (ExpBase NoInfo Name, ExpBase NoInfo Name)
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Text -> TypeBase Size () -> Exp -> TermTypeM Exp
unifies Text
"use in range expression" TypeBase Size ()
start_t forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExpBase NoInfo Name -> TermTypeM Exp
checkExp ExpBase NoInfo Name
step)

  let unifyRange :: ExpBase NoInfo Name -> TermTypeM Exp
unifyRange ExpBase NoInfo Name
e = Text -> TypeBase Size () -> Exp -> TermTypeM Exp
unifies Text
"use in range expression" TypeBase Size ()
start_t forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExpBase NoInfo Name -> TermTypeM Exp
checkExp ExpBase NoInfo Name
e
  Inclusiveness Exp
end' <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ExpBase NoInfo Name -> TermTypeM Exp
unifyRange Inclusiveness (ExpBase NoInfo Name)
end

  PatType
end_t <- case Inclusiveness Exp
end' of
    DownToExclusive Exp
e -> Exp -> TermTypeM PatType
expType Exp
e
    ToInclusive Exp
e -> Exp -> TermTypeM PatType
expType Exp
e
    UpToExclusive Exp
e -> Exp -> TermTypeM PatType
expType Exp
e

  -- Special case some ranges to give them a known size.
  let dimFromBound :: Exp -> TermTypeM (Size, Maybe VName)
dimFromBound = (Exp -> SizeSource) -> Exp -> TermTypeM (Size, Maybe VName)
dimFromExp (ExpBase NoInfo VName -> SizeSource
SourceBound forall b c a. (b -> c) -> (a -> b) -> a -> c
. Exp -> ExpBase NoInfo VName
bareExp)
  (Size
dim, Maybe VName
retext) <-
    case (Exp -> Maybe Int64
isInt64 Exp
start', Exp -> Maybe Int64
isInt64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Exp
maybe_step', Inclusiveness Exp
end') of
      (Just Int64
0, Just (Just Int64
1), UpToExclusive Exp
end'')
        | Scalar (Prim (Signed IntType
Int64)) <- PatType
end_t ->
            Exp -> TermTypeM (Size, Maybe VName)
dimFromBound Exp
end''
      (Just Int64
0, Maybe (Maybe Int64)
Nothing, UpToExclusive Exp
end'')
        | Scalar (Prim (Signed IntType
Int64)) <- PatType
end_t ->
            Exp -> TermTypeM (Size, Maybe VName)
dimFromBound Exp
end''
      (Just Int64
1, Just (Just Int64
2), ToInclusive Exp
end'')
        | Scalar (Prim (Signed IntType
Int64)) <- PatType
end_t ->
            Exp -> TermTypeM (Size, Maybe VName)
dimFromBound Exp
end''
      (Maybe Int64, Maybe (Maybe Int64), Inclusiveness Exp)
_ -> do
        VName
d <- forall (m :: * -> *).
MonadUnify m =>
SrcLoc -> Rigidity -> Name -> m VName
newDimVar SrcLoc
loc (RigidSource -> Rigidity
Rigid RigidSource
RigidRange) Name
"range_dim"
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (QualName VName -> Size
NamedSize forall a b. (a -> b) -> a -> b
$ forall v. v -> QualName v
qualName VName
d, forall a. a -> Maybe a
Just VName
d)

  TypeBase Size ()
t <- forall dim as.
(Pretty (Shape dim), Monoid as) =>
SrcLoc
-> TypeBase dim as
-> Shape dim
-> Uniqueness
-> TermTypeM (TypeBase dim as)
arrayOfM SrcLoc
loc TypeBase Size ()
start_t (forall dim. [dim] -> Shape dim
Shape [Size
dim]) Uniqueness
Unique
  let res :: AppRes
res = PatType -> [VName] -> AppRes
AppRes (TypeBase Size ()
t forall dim asf ast. TypeBase dim asf -> ast -> TypeBase dim ast
`setAliases` forall a. Monoid a => a
mempty) (forall a. Maybe a -> [a]
maybeToList Maybe VName
retext)

  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
AppExpBase f vn -> f AppRes -> ExpBase f vn
AppExp (forall (f :: * -> *) vn.
ExpBase f vn
-> Maybe (ExpBase f vn)
-> Inclusiveness (ExpBase f vn)
-> SrcLoc
-> AppExpBase f vn
Range Exp
start' Maybe Exp
maybe_step' Inclusiveness Exp
end' SrcLoc
loc) (forall a. a -> Info a
Info AppRes
res)
checkExp (Ascript ExpBase NoInfo Name
e UncheckedTypeExp
te SrcLoc
loc) = do
  (TypeExp VName
te', Exp
e') <- SrcLoc
-> UncheckedTypeExp
-> ExpBase NoInfo Name
-> TermTypeM (TypeExp VName, Exp)
checkAscript SrcLoc
loc UncheckedTypeExp
te ExpBase NoInfo Name
e
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
ExpBase f vn -> TypeExp vn -> SrcLoc -> ExpBase f vn
Ascript Exp
e' TypeExp VName
te' SrcLoc
loc
checkExp (AppExp (Coerce ExpBase NoInfo Name
e UncheckedTypeExp
te SrcLoc
loc) NoInfo AppRes
_) = do
  (TypeExp VName
te', TypeBase Size ()
te_t, Exp
e', [VName]
ext) <- SrcLoc
-> UncheckedTypeExp
-> ExpBase NoInfo Name
-> TermTypeM (TypeExp VName, TypeBase Size (), Exp, [VName])
checkCoerce SrcLoc
loc UncheckedTypeExp
te ExpBase NoInfo Name
e
  PatType
t <- Exp -> TermTypeM PatType
expTypeFully Exp
e'
  PatType
t' <- forall as (m :: * -> *) d1 d2.
(Monoid as, Monad m) =>
([VName] -> d1 -> d2 -> m d1)
-> TypeBase d1 as -> TypeBase d2 as -> m (TypeBase d1 as)
matchDims (forall a b. a -> b -> a
const forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> b -> a
const forall (f :: * -> *) a. Applicative f => a -> f a
pure) PatType
t forall a b. (a -> b) -> a -> b
$ forall dim as. TypeBase dim as -> TypeBase dim Aliasing
fromStruct TypeBase Size ()
te_t
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
AppExpBase f vn -> f AppRes -> ExpBase f vn
AppExp (forall (f :: * -> *) vn.
ExpBase f vn -> TypeExp vn -> SrcLoc -> AppExpBase f vn
Coerce Exp
e' TypeExp VName
te' SrcLoc
loc) (forall a. a -> Info a
Info forall a b. (a -> b) -> a -> b
$ PatType -> [VName] -> AppRes
AppRes PatType
t' [VName]
ext)
checkExp (AppExp (BinOp (QualName Name
op, SrcLoc
oploc) NoInfo PatType
NoInfo (ExpBase NoInfo Name
e1, NoInfo (TypeBase Size (), Maybe VName)
_) (ExpBase NoInfo Name
e2, NoInfo (TypeBase Size (), Maybe VName)
_) SrcLoc
loc) NoInfo AppRes
NoInfo) = do
  (QualName VName
op', PatType
ftype) <- forall (m :: * -> *).
MonadTypeChecker m =>
SrcLoc -> QualName Name -> m (QualName VName, PatType)
lookupVar SrcLoc
oploc QualName Name
op
  Arg
e1_arg <- ExpBase NoInfo Name -> TermTypeM Arg
checkArg ExpBase NoInfo Name
e1
  Arg
e2_arg <- ExpBase NoInfo Name -> TermTypeM Arg
checkArg ExpBase NoInfo Name
e2

  -- Note that the application to the first operand cannot fix any
  -- existential sizes, because it must by necessity be a function.
  (TypeBase Size ()
p1_t, PatType
rt, Maybe VName
p1_ext, [VName]
_) <- SrcLoc
-> ApplyOp
-> PatType
-> Arg
-> TermTypeM (TypeBase Size (), PatType, Maybe VName, [VName])
checkApply SrcLoc
loc (forall a. a -> Maybe a
Just QualName VName
op', Int
0) PatType
ftype Arg
e1_arg
  (TypeBase Size ()
p2_t, PatType
rt', Maybe VName
p2_ext, [VName]
retext) <- SrcLoc
-> ApplyOp
-> PatType
-> Arg
-> TermTypeM (TypeBase Size (), PatType, Maybe VName, [VName])
checkApply SrcLoc
loc (forall a. a -> Maybe a
Just QualName VName
op', Int
1) PatType
rt Arg
e2_arg

  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
    forall (f :: * -> *) vn.
AppExpBase f vn -> f AppRes -> ExpBase f vn
AppExp
      ( forall (f :: * -> *) vn.
(QualName vn, SrcLoc)
-> f PatType
-> (ExpBase f vn, f (TypeBase Size (), Maybe VName))
-> (ExpBase f vn, f (TypeBase Size (), Maybe VName))
-> SrcLoc
-> AppExpBase f vn
BinOp
          (QualName VName
op', SrcLoc
oploc)
          (forall a. a -> Info a
Info PatType
ftype)
          (Arg -> Exp
argExp Arg
e1_arg, forall a. a -> Info a
Info (forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct TypeBase Size ()
p1_t, Maybe VName
p1_ext))
          (Arg -> Exp
argExp Arg
e2_arg, forall a. a -> Info a
Info (forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct TypeBase Size ()
p2_t, Maybe VName
p2_ext))
          SrcLoc
loc
      )
      (forall a. a -> Info a
Info (PatType -> [VName] -> AppRes
AppRes PatType
rt' [VName]
retext))
checkExp (Project Name
k ExpBase NoInfo Name
e NoInfo PatType
NoInfo SrcLoc
loc) = do
  Exp
e' <- ExpBase NoInfo Name -> TermTypeM Exp
checkExp ExpBase NoInfo Name
e
  PatType
t <- Exp -> TermTypeM PatType
expType Exp
e'
  PatType
kt <- forall (m :: * -> *).
MonadUnify m =>
Usage -> Name -> PatType -> m PatType
mustHaveField (SrcLoc -> Text -> Usage
mkUsage SrcLoc
loc forall a b. (a -> b) -> a -> b
$ forall a. Doc a -> Text
docText forall a b. (a -> b) -> a -> b
$ Doc Any
"projection of field " forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty Name
k)) Name
k PatType
t
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
Name -> ExpBase f vn -> f PatType -> SrcLoc -> ExpBase f vn
Project Name
k Exp
e' (forall a. a -> Info a
Info PatType
kt) SrcLoc
loc
checkExp (AppExp (If ExpBase NoInfo Name
e1 ExpBase NoInfo Name
e2 ExpBase NoInfo Name
e3 SrcLoc
loc) NoInfo AppRes
_) =
  forall a b.
TermTypeM a -> (a -> Occurrences -> TermTypeM b) -> TermTypeM b
sequentially TermTypeM Exp
checkCond forall a b. (a -> b) -> a -> b
$ \Exp
e1' Occurrences
_ -> do
    ((Exp
e2', Exp
e3'), Occurrences
dflow) <- forall a. TermTypeM a -> TermTypeM (a, Occurrences)
tapOccurrences forall a b. (a -> b) -> a -> b
$ ExpBase NoInfo Name -> TermTypeM Exp
checkExp ExpBase NoInfo Name
e2 forall a b. TermTypeM a -> TermTypeM b -> TermTypeM (a, b)
`alternative` ExpBase NoInfo Name -> TermTypeM Exp
checkExp ExpBase NoInfo Name
e3

    (PatType
brancht, [VName]
retext) <- SrcLoc -> Exp -> Exp -> TermTypeM (PatType, [VName])
unifyBranches SrcLoc
loc Exp
e2' Exp
e3'
    let t' :: PatType
t' = forall dim asf ast.
TypeBase dim asf -> (asf -> ast) -> TypeBase dim ast
addAliases PatType
brancht forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> Set a -> Set a
S.filter forall a b. (a -> b) -> a -> b
$ (forall a. Ord a => a -> Set a -> Bool
`S.notMember` Occurrences -> Set VName
allConsumed Occurrences
dflow) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Alias -> VName
aliasVar

    forall (m :: * -> *) dim as.
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage -> Text -> TypeBase dim as -> m ()
zeroOrderType
      (SrcLoc -> Text -> Usage
mkUsage SrcLoc
loc Text
"returning value of this type from 'if' expression")
      Text
"type returned from branch"
      PatType
t'

    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
AppExpBase f vn -> f AppRes -> ExpBase f vn
AppExp (forall (f :: * -> *) vn.
ExpBase f vn
-> ExpBase f vn -> ExpBase f vn -> SrcLoc -> AppExpBase f vn
If Exp
e1' Exp
e2' Exp
e3' SrcLoc
loc) (forall a. a -> Info a
Info forall a b. (a -> b) -> a -> b
$ PatType -> [VName] -> AppRes
AppRes PatType
t' [VName]
retext)
  where
    checkCond :: TermTypeM Exp
checkCond = do
      Exp
e1' <- ExpBase NoInfo Name -> TermTypeM Exp
checkExp ExpBase NoInfo Name
e1
      let bool :: TypeBase dim as
bool = forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as. PrimType -> ScalarTypeBase dim as
Prim PrimType
Bool
      TypeBase Size ()
e1_t <- forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp -> TermTypeM PatType
expType Exp
e1'
      forall a. Checking -> TermTypeM a -> TermTypeM a
onFailure ([TypeBase Size ()] -> TypeBase Size () -> Checking
CheckingRequired [forall {dim} {as}. TypeBase dim as
bool] TypeBase Size ()
e1_t) forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *).
MonadUnify m =>
Usage -> TypeBase Size () -> TypeBase Size () -> m ()
unify (SrcLoc -> Text -> Usage
mkUsage (forall a. Located a => a -> SrcLoc
srclocOf Exp
e1') Text
"use as 'if' condition") forall {dim} {as}. TypeBase dim as
bool TypeBase Size ()
e1_t
      forall (f :: * -> *) a. Applicative f => a -> f a
pure Exp
e1'
checkExp (Parens ExpBase NoInfo Name
e SrcLoc
loc) =
  forall (f :: * -> *) vn. ExpBase f vn -> SrcLoc -> ExpBase f vn
Parens forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExpBase NoInfo Name -> TermTypeM Exp
checkExp ExpBase NoInfo Name
e forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure SrcLoc
loc
checkExp (QualParens (QualName Name
modname, SrcLoc
modnameloc) ExpBase NoInfo Name
e SrcLoc
loc) = do
  (QualName VName
modname', Mod
mod) <- forall (m :: * -> *).
MonadTypeChecker m =>
SrcLoc -> QualName Name -> m (QualName VName, Mod)
lookupMod SrcLoc
loc QualName Name
modname
  case Mod
mod of
    ModEnv Env
env -> forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (TermEnv -> Env -> TermEnv
`withEnv` QualName VName -> Env -> Env
qualifyEnv QualName VName
modname' Env
env) forall a b. (a -> b) -> a -> b
$ do
      Exp
e' <- ExpBase NoInfo Name -> TermTypeM Exp
checkExp ExpBase NoInfo Name
e
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
(QualName vn, SrcLoc) -> ExpBase f vn -> SrcLoc -> ExpBase f vn
QualParens (QualName VName
modname', SrcLoc
modnameloc) Exp
e' SrcLoc
loc
    ModFun {} ->
      forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc forall a. Monoid a => a
mempty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ann. Doc ann -> Doc ann -> Doc ann
withIndexLink Doc ()
"module-is-parametric" forall a b. (a -> b) -> a -> b
$
        Doc ()
"Module" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty QualName Name
modname forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
" is a parametric module."
  where
    qualifyEnv :: QualName VName -> Env -> Env
qualifyEnv QualName VName
modname' Env
env =
      Env
env {envNameMap :: NameMap
envNameMap = forall a b k. (a -> b) -> Map k a -> Map k b
M.map (forall {vn}. QualName vn -> QualName vn -> QualName vn
qualify' QualName VName
modname') forall a b. (a -> b) -> a -> b
$ Env -> NameMap
envNameMap Env
env}
    qualify' :: QualName vn -> QualName vn -> QualName vn
qualify' QualName vn
modname' (QualName [vn]
qs vn
name) =
      forall vn. [vn] -> vn -> QualName vn
QualName (forall vn. QualName vn -> [vn]
qualQuals QualName vn
modname' forall a. [a] -> [a] -> [a]
++ [forall vn. QualName vn -> vn
qualLeaf QualName vn
modname'] forall a. [a] -> [a] -> [a]
++ [vn]
qs) vn
name
checkExp (Var QualName Name
qn NoInfo PatType
NoInfo SrcLoc
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.

  (QualName VName
qn', PatType
t, [Name]
fields) <- forall {e} {m :: * -> *}.
(MonadError e m, MonadTypeChecker m) =>
[Name] -> Name -> m (QualName VName, PatType, [Name])
findRootVar (forall vn. QualName vn -> [vn]
qualQuals QualName Name
qn) (forall vn. QualName vn -> vn
qualLeaf QualName Name
qn)

  forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Exp -> Name -> TermTypeM Exp
checkField (forall (f :: * -> *) vn.
QualName vn -> f PatType -> SrcLoc -> ExpBase f vn
Var QualName VName
qn' (forall a. a -> Info a
Info PatType
t) SrcLoc
loc) [Name]
fields
  where
    findRootVar :: [Name] -> Name -> m (QualName VName, PatType, [Name])
findRootVar [Name]
qs Name
name =
      (forall {a} {b} {a}. (a, b) -> (a, b, [a])
whenFound forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadTypeChecker m =>
SrcLoc -> QualName Name -> m (QualName VName, PatType)
lookupVar SrcLoc
loc (forall vn. [vn] -> vn -> QualName vn
QualName [Name]
qs Name
name)) forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` [Name] -> Name -> e -> m (QualName VName, PatType, [Name])
notFound [Name]
qs Name
name

    whenFound :: (a, b) -> (a, b, [a])
whenFound (a
qn', b
t) = (a
qn', b
t, [])

    notFound :: [Name] -> Name -> e -> m (QualName VName, PatType, [Name])
notFound [Name]
qs Name
name e
err
      | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Name]
qs = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError e
err
      | Bool
otherwise = do
          (QualName VName
qn', PatType
t, [Name]
fields) <-
            [Name] -> Name -> m (QualName VName, PatType, [Name])
findRootVar (forall a. [a] -> [a]
init [Name]
qs) (forall a. [a] -> a
last [Name]
qs)
              forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` forall a b. a -> b -> a
const (forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError e
err)
          forall (f :: * -> *) a. Applicative f => a -> f a
pure (QualName VName
qn', PatType
t, [Name]
fields forall a. [a] -> [a] -> [a]
++ [Name
name])

    checkField :: Exp -> Name -> TermTypeM Exp
checkField Exp
e Name
k = do
      PatType
t <- Exp -> TermTypeM PatType
expType Exp
e
      let usage :: Usage
usage = SrcLoc -> Text -> Usage
mkUsage SrcLoc
loc forall a b. (a -> b) -> a -> b
$ forall a. Doc a -> Text
docText forall a b. (a -> b) -> a -> b
$ Doc Any
"projection of field " forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty Name
k)
      PatType
kt <- forall (m :: * -> *).
MonadUnify m =>
Usage -> Name -> PatType -> m PatType
mustHaveField Usage
usage Name
k PatType
t
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
Name -> ExpBase f vn -> f PatType -> SrcLoc -> ExpBase f vn
Project Name
k Exp
e (forall a. a -> Info a
Info PatType
kt) SrcLoc
loc
checkExp (Negate ExpBase NoInfo Name
arg SrcLoc
loc) = do
  Exp
arg' <- Text -> [PrimType] -> Exp -> TermTypeM Exp
require Text
"numeric negation" [PrimType]
anyNumberType forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExpBase NoInfo Name -> TermTypeM Exp
checkExp ExpBase NoInfo Name
arg
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn. ExpBase f vn -> SrcLoc -> ExpBase f vn
Negate Exp
arg' SrcLoc
loc
checkExp (Not ExpBase NoInfo Name
arg SrcLoc
loc) = do
  Exp
arg' <- Text -> [PrimType] -> Exp -> TermTypeM Exp
require Text
"logical negation" (PrimType
Bool forall a. a -> [a] -> [a]
: [PrimType]
anyIntType) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExpBase NoInfo Name -> TermTypeM Exp
checkExp ExpBase NoInfo Name
arg
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn. ExpBase f vn -> SrcLoc -> ExpBase f vn
Not Exp
arg' SrcLoc
loc
checkExp e :: ExpBase NoInfo Name
e@(AppExp Apply {} NoInfo AppRes
_) = forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExpBase NoInfo Name -> TermTypeM (Exp, ApplyOp)
checkApplyExp ExpBase NoInfo Name
e
checkExp (AppExp (LetPat [SizeBinder Name]
sizes PatBase NoInfo Name
pat ExpBase NoInfo Name
e ExpBase NoInfo Name
body SrcLoc
loc) NoInfo AppRes
_) =
  forall a b.
TermTypeM a -> (a -> Occurrences -> TermTypeM b) -> TermTypeM b
sequentially (ExpBase NoInfo Name -> TermTypeM Exp
checkExp ExpBase NoInfo Name
e) forall a b. (a -> b) -> a -> b
$ \Exp
e' Occurrences
e_occs -> do
    -- Not technically an ascription, but we want the pattern to have
    -- exactly the type of 'e'.
    PatType
t <- Exp -> TermTypeM PatType
expType Exp
e'
    case Occurrences -> Maybe Occurrence
anyConsumption Occurrences
e_occs of
      Just Occurrence
c ->
        let msg :: Text
msg = Text
"type computed with consumption at " forall a. Semigroup a => a -> a -> a
<> forall a. Located a => a -> Text
locText (Occurrence -> SrcLoc
location Occurrence
c)
         in forall (m :: * -> *) dim as.
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage -> Text -> TypeBase dim as -> m ()
zeroOrderType (SrcLoc -> Text -> Usage
mkUsage SrcLoc
loc Text
"consumption in right-hand side of 'let'-binding") Text
msg PatType
t
      Maybe Occurrence
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

    forall a. TermTypeM a -> TermTypeM a
incLevel forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
[SizeBinder Name]
-> ([SizeBinder VName] -> TermTypeM a) -> TermTypeM a
bindingSizes [SizeBinder Name]
sizes forall a b. (a -> b) -> a -> b
$ \[SizeBinder VName]
sizes' ->
      forall a.
[SizeBinder VName]
-> PatBase NoInfo Name
-> InferredType
-> (PatBase Info VName -> TermTypeM a)
-> TermTypeM a
bindingPat [SizeBinder VName]
sizes' PatBase NoInfo Name
pat (PatType -> InferredType
Ascribed PatType
t) forall a b. (a -> b) -> a -> b
$ \PatBase Info VName
pat' -> do
        Exp
body' <- ExpBase NoInfo Name -> TermTypeM Exp
checkExp ExpBase NoInfo Name
body
        (PatType
body_t, [VName]
retext) <-
          SrcLoc
-> Map VName (IdentBase Info VName)
-> PatType
-> TermTypeM (PatType, [VName])
unscopeType SrcLoc
loc ([SizeBinder VName] -> Map VName (IdentBase Info VName)
sizesMap [SizeBinder VName]
sizes' forall a. Semigroup a => a -> a -> a
<> forall (f :: * -> *).
Functor f =>
PatBase f VName -> Map VName (IdentBase f VName)
patternMap PatBase Info VName
pat') forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Exp -> TermTypeM PatType
expTypeFully Exp
body'

        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
AppExpBase f vn -> f AppRes -> ExpBase f vn
AppExp (forall (f :: * -> *) vn.
[SizeBinder vn]
-> PatBase f vn
-> ExpBase f vn
-> ExpBase f vn
-> SrcLoc
-> AppExpBase f vn
LetPat [SizeBinder VName]
sizes' PatBase Info VName
pat' Exp
e' Exp
body' SrcLoc
loc) (forall a. a -> Info a
Info forall a b. (a -> b) -> a -> b
$ PatType -> [VName] -> AppRes
AppRes PatType
body_t [VName]
retext)
  where
    sizesMap :: [SizeBinder VName] -> Map VName (IdentBase Info VName)
sizesMap = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall {vn}. SizeBinder vn -> Map vn (IdentBase Info vn)
onSize
    onSize :: SizeBinder vn -> Map vn (IdentBase Info vn)
onSize SizeBinder vn
size =
      forall k a. k -> a -> Map k a
M.singleton (forall vn. SizeBinder vn -> vn
sizeName SizeBinder vn
size) forall a b. (a -> b) -> a -> b
$
        forall (f :: * -> *) vn.
vn -> f PatType -> SrcLoc -> IdentBase f vn
Ident (forall vn. SizeBinder vn -> vn
sizeName SizeBinder vn
size) (forall a. a -> Info a
Info (forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as. PrimType -> ScalarTypeBase dim as
Prim forall a b. (a -> b) -> a -> b
$ IntType -> PrimType
Signed IntType
Int64)) (forall a. Located a => a -> SrcLoc
srclocOf SizeBinder vn
size)
checkExp (AppExp (LetFun Name
name ([TypeParamBase Name]
tparams, [PatBase NoInfo Name]
params, Maybe UncheckedTypeExp
maybe_retdecl, NoInfo StructRetType
NoInfo, ExpBase NoInfo Name
e) ExpBase NoInfo Name
body SrcLoc
loc) NoInfo AppRes
_) =
  forall a b.
TermTypeM a -> (a -> Occurrences -> TermTypeM b) -> TermTypeM b
sequentially ((Name, Maybe UncheckedTypeExp, [TypeParamBase Name],
 [PatBase NoInfo Name], ExpBase NoInfo Name, SrcLoc)
-> TermTypeM
     ([TypeParamBase VName], [PatBase Info VName],
      Maybe (TypeExp VName), StructRetType, Exp)
checkBinding (Name
name, Maybe UncheckedTypeExp
maybe_retdecl, [TypeParamBase Name]
tparams, [PatBase NoInfo Name]
params, ExpBase NoInfo Name
e, SrcLoc
loc)) forall a b. (a -> b) -> a -> b
$
    \([TypeParamBase VName]
tparams', [PatBase Info VName]
params', Maybe (TypeExp VName)
maybe_retdecl', StructRetType
rettype, Exp
e') Occurrences
closure -> do
      Aliasing
closure' <- [PatBase Info VName] -> Occurrences -> TermTypeM Aliasing
lexicalClosure [PatBase Info VName]
params' Occurrences
closure

      forall (m :: * -> *) a.
MonadTypeChecker m =>
[(Namespace, Name)] -> m a -> m a
bindSpaced [(Namespace
Term, Name
name)] forall a b. (a -> b) -> a -> b
$ do
        VName
name' <- forall (m :: * -> *).
MonadTypeChecker m =>
Namespace -> Name -> SrcLoc -> m VName
checkName Namespace
Term Name
name SrcLoc
loc

        let arrow :: (PName, TypeBase dim ())
-> RetTypeBase dim () -> RetTypeBase dim ()
arrow (PName
xp, TypeBase dim ()
xt) RetTypeBase dim ()
yt = forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [] forall a b. (a -> b) -> a -> b
$ forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as.
as
-> PName
-> TypeBase dim ()
-> RetTypeBase dim as
-> ScalarTypeBase dim as
Arrow () PName
xp TypeBase dim ()
xt RetTypeBase dim ()
yt
            RetType [VName]
_ TypeBase Size ()
ftype = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (forall {dim}.
(PName, TypeBase dim ())
-> RetTypeBase dim () -> RetTypeBase dim ()
arrow forall b c a. (b -> c) -> (a -> b) -> a -> c
. PatBase Info VName -> (PName, TypeBase Size ())
patternParam) StructRetType
rettype [PatBase Info VName]
params'
            entry :: ValBinding
entry = Locality -> [TypeParamBase VName] -> PatType -> ValBinding
BoundV Locality
Local [TypeParamBase VName]
tparams' forall a b. (a -> b) -> a -> b
$ TypeBase Size ()
ftype forall dim asf ast. TypeBase dim asf -> ast -> TypeBase dim ast
`setAliases` Aliasing
closure'
            bindF :: TermScope -> TermScope
bindF TermScope
scope =
              TermScope
scope
                { scopeVtable :: Map VName ValBinding
scopeVtable =
                    forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
name' ValBinding
entry forall a b. (a -> b) -> a -> b
$ TermScope -> Map VName ValBinding
scopeVtable TermScope
scope,
                  scopeNameMap :: NameMap
scopeNameMap =
                    forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (Namespace
Term, Name
name) (forall v. v -> QualName v
qualName VName
name') forall a b. (a -> b) -> a -> b
$
                      TermScope -> NameMap
scopeNameMap TermScope
scope
                }
        Exp
body' <- forall a. (TermScope -> TermScope) -> TermTypeM a -> TermTypeM a
localScope TermScope -> TermScope
bindF forall a b. (a -> b) -> a -> b
$ ExpBase NoInfo Name -> TermTypeM Exp
checkExp ExpBase NoInfo Name
body

        -- We fake an ident here, but it's OK as it can't be a size
        -- anyway.
        let fake_ident :: IdentBase Info VName
fake_ident = forall (f :: * -> *) vn.
vn -> f PatType -> SrcLoc -> IdentBase f vn
Ident VName
name' (forall a. a -> Info a
Info forall a b. (a -> b) -> a -> b
$ forall dim as. TypeBase dim as -> TypeBase dim Aliasing
fromStruct TypeBase Size ()
ftype) forall a. Monoid a => a
mempty
        (PatType
body_t, [VName]
ext) <-
          SrcLoc
-> Map VName (IdentBase Info VName)
-> PatType
-> TermTypeM (PatType, [VName])
unscopeType SrcLoc
loc (forall k a. k -> a -> Map k a
M.singleton VName
name' IdentBase Info VName
fake_ident)
            forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Exp -> TermTypeM PatType
expTypeFully Exp
body'

        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
          forall (f :: * -> *) vn.
AppExpBase f vn -> f AppRes -> ExpBase f vn
AppExp
            ( forall (f :: * -> *) vn.
vn
-> ([TypeParamBase vn], [PatBase f vn], Maybe (TypeExp vn),
    f StructRetType, ExpBase f vn)
-> ExpBase f vn
-> SrcLoc
-> AppExpBase f vn
LetFun
                VName
name'
                ([TypeParamBase VName]
tparams', [PatBase Info VName]
params', Maybe (TypeExp VName)
maybe_retdecl', forall a. a -> Info a
Info StructRetType
rettype, Exp
e')
                Exp
body'
                SrcLoc
loc
            )
            (forall a. a -> Info a
Info forall a b. (a -> b) -> a -> b
$ PatType -> [VName] -> AppRes
AppRes PatType
body_t [VName]
ext)
checkExp (AppExp (LetWith IdentBase NoInfo Name
dest IdentBase NoInfo Name
src SliceBase NoInfo Name
slice ExpBase NoInfo Name
ve ExpBase NoInfo Name
body SrcLoc
loc) NoInfo AppRes
_) =
  forall a b.
TermTypeM a -> (a -> Occurrences -> TermTypeM b) -> TermTypeM b
sequentially (IdentBase NoInfo Name -> TermTypeM (IdentBase Info VName)
checkIdent IdentBase NoInfo Name
src) forall a b. (a -> b) -> a -> b
$ \IdentBase Info VName
src' Occurrences
_ -> do
    Slice
slice' <- SliceBase NoInfo Name -> TermTypeM Slice
checkSlice SliceBase NoInfo Name
slice
    (TypeBase Size ()
t, TypeBase Size ()
_) <- SrcLoc
-> Name -> Int -> TermTypeM (TypeBase Size (), TypeBase Size ())
newArrayType (forall a. Located a => a -> SrcLoc
srclocOf IdentBase NoInfo Name
src) Name
"src" forall a b. (a -> b) -> a -> b
$ Slice -> Int
sliceDims Slice
slice'
    forall (m :: * -> *).
MonadUnify m =>
Usage -> TypeBase Size () -> TypeBase Size () -> m ()
unify (SrcLoc -> Text -> Usage
mkUsage SrcLoc
loc Text
"type of target array") TypeBase Size ()
t forall a b. (a -> b) -> a -> b
$ forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct forall a b. (a -> b) -> a -> b
$ forall a. Info a -> a
unInfo forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn. IdentBase f vn -> f PatType
identType IdentBase Info VName
src'

    -- Need the fully normalised type here to get the proper aliasing information.
    PatType
src_t <- forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully forall a b. (a -> b) -> a -> b
$ forall a. Info a -> a
unInfo forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn. IdentBase f vn -> f PatType
identType IdentBase Info VName
src'

    (TypeBase Size ()
elemt, [VName]
_) <- forall as.
Maybe (SrcLoc, Rigidity)
-> Slice
-> TypeBase Size as
-> TermTypeM (TypeBase Size as, [VName])
sliceShape (forall a. a -> Maybe a
Just (SrcLoc
loc, Rigidity
Nonrigid)) Slice
slice' forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully TypeBase Size ()
t

    forall a b.
TermTypeM a -> (a -> Occurrences -> TermTypeM b) -> TermTypeM b
sequentially (Text -> TypeBase Size () -> Exp -> TermTypeM Exp
unifies Text
"type of target array" (forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct TypeBase Size ()
elemt) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExpBase NoInfo Name -> TermTypeM Exp
checkExp ExpBase NoInfo Name
ve) forall a b. (a -> b) -> a -> b
$ \Exp
ve' Occurrences
_ -> do
      PatType
ve_t <- Exp -> TermTypeM PatType
expTypeFully Exp
ve'
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (VName -> Alias
AliasBound (forall (f :: * -> *) vn. IdentBase f vn -> vn
identName IdentBase Info VName
src') forall a. Ord a => a -> Set a -> Bool
`S.member` forall as shape. Monoid as => TypeBase shape as -> as
aliases PatType
ve_t) forall a b. (a -> b) -> a -> b
$
        forall arr src a.
(Pretty arr, Pretty src) =>
arr -> src -> SrcLoc -> TermTypeM a
badLetWithValue IdentBase NoInfo Name
src ExpBase NoInfo Name
ve SrcLoc
loc

      forall a.
IdentBase NoInfo Name
-> PatType -> (IdentBase Info VName -> TermTypeM a) -> TermTypeM a
bindingIdent IdentBase NoInfo Name
dest (PatType
src_t forall dim asf ast. TypeBase dim asf -> ast -> TypeBase dim ast
`setAliases` forall a. Set a
S.empty) forall a b. (a -> b) -> a -> b
$ \IdentBase Info VName
dest' -> do
        Exp
body' <- forall a. IdentBase Info VName -> TermTypeM a -> TermTypeM a
consuming IdentBase Info VName
src' forall a b. (a -> b) -> a -> b
$ ExpBase NoInfo Name -> TermTypeM Exp
checkExp ExpBase NoInfo Name
body
        (PatType
body_t, [VName]
ext) <-
          SrcLoc
-> Map VName (IdentBase Info VName)
-> PatType
-> TermTypeM (PatType, [VName])
unscopeType SrcLoc
loc (forall k a. k -> a -> Map k a
M.singleton (forall (f :: * -> *) vn. IdentBase f vn -> vn
identName IdentBase Info VName
dest') IdentBase Info VName
dest')
            forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Exp -> TermTypeM PatType
expTypeFully Exp
body'
        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
AppExpBase f vn -> f AppRes -> ExpBase f vn
AppExp (forall (f :: * -> *) vn.
IdentBase f vn
-> IdentBase f vn
-> SliceBase f vn
-> ExpBase f vn
-> ExpBase f vn
-> SrcLoc
-> AppExpBase f vn
LetWith IdentBase Info VName
dest' IdentBase Info VName
src' Slice
slice' Exp
ve' Exp
body' SrcLoc
loc) (forall a. a -> Info a
Info forall a b. (a -> b) -> a -> b
$ PatType -> [VName] -> AppRes
AppRes PatType
body_t [VName]
ext)
checkExp (Update ExpBase NoInfo Name
src SliceBase NoInfo Name
slice ExpBase NoInfo Name
ve SrcLoc
loc) = do
  Slice
slice' <- SliceBase NoInfo Name -> TermTypeM Slice
checkSlice SliceBase NoInfo Name
slice
  (TypeBase Size ()
t, TypeBase Size ()
_) <- SrcLoc
-> Name -> Int -> TermTypeM (TypeBase Size (), TypeBase Size ())
newArrayType (forall a. Located a => a -> SrcLoc
srclocOf ExpBase NoInfo Name
src) Name
"src" forall a b. (a -> b) -> a -> b
$ Slice -> Int
sliceDims Slice
slice'
  (TypeBase Size ()
elemt, [VName]
_) <- forall as.
Maybe (SrcLoc, Rigidity)
-> Slice
-> TypeBase Size as
-> TermTypeM (TypeBase Size as, [VName])
sliceShape (forall a. a -> Maybe a
Just (SrcLoc
loc, Rigidity
Nonrigid)) Slice
slice' forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully TypeBase Size ()
t

  forall a b.
TermTypeM a -> (a -> Occurrences -> TermTypeM b) -> TermTypeM b
sequentially (ExpBase NoInfo Name -> TermTypeM Exp
checkExp ExpBase NoInfo Name
ve forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Text -> TypeBase Size () -> Exp -> TermTypeM Exp
unifies Text
"type of target array" TypeBase Size ()
elemt) forall a b. (a -> b) -> a -> b
$ \Exp
ve' Occurrences
_ ->
    forall a b.
TermTypeM a -> (a -> Occurrences -> TermTypeM b) -> TermTypeM b
sequentially (ExpBase NoInfo Name -> TermTypeM Exp
checkExp ExpBase NoInfo Name
src forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Text -> TypeBase Size () -> Exp -> TermTypeM Exp
unifies Text
"type of target array" TypeBase Size ()
t) forall a b. (a -> b) -> a -> b
$ \Exp
src' Occurrences
_ -> do
      PatType
src_t <- Exp -> TermTypeM PatType
expTypeFully Exp
src'

      let src_als :: Aliasing
src_als = forall as shape. Monoid as => TypeBase shape as -> as
aliases PatType
src_t
      PatType
ve_t <- Exp -> TermTypeM PatType
expTypeFully Exp
ve'
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Set a -> Bool
S.null forall a b. (a -> b) -> a -> b
$ Aliasing
src_als forall a. Ord a => Set a -> Set a -> Set a
`S.intersection` forall as shape. Monoid as => TypeBase shape as -> as
aliases PatType
ve_t) forall a b. (a -> b) -> a -> b
$ forall arr src a.
(Pretty arr, Pretty src) =>
arr -> src -> SrcLoc -> TermTypeM a
badLetWithValue ExpBase NoInfo Name
src ExpBase NoInfo Name
ve SrcLoc
loc

      SrcLoc -> Aliasing -> TermTypeM ()
consume SrcLoc
loc Aliasing
src_als
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
ExpBase f vn
-> SliceBase f vn -> ExpBase f vn -> SrcLoc -> ExpBase f vn
Update Exp
src' Slice
slice' Exp
ve' SrcLoc
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 ExpBase NoInfo Name
src [Name]
fields ExpBase NoInfo Name
ve NoInfo PatType
NoInfo SrcLoc
loc) = do
  Exp
src' <- ExpBase NoInfo Name -> TermTypeM Exp
checkExp ExpBase NoInfo Name
src
  Exp
ve' <- ExpBase NoInfo Name -> TermTypeM Exp
checkExp ExpBase NoInfo Name
ve
  PatType
a <- Exp -> TermTypeM PatType
expTypeFully Exp
src'
  forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m ()
foldM_ (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadUnify m =>
Usage -> Name -> PatType -> m PatType
mustHaveField Usage
usage) PatType
a [Name]
fields
  PatType
ve_t <- Exp -> TermTypeM PatType
expType Exp
ve'
  PatType
updated_t <- forall {as}.
[Name]
-> TypeBase Size as
-> TypeBase Size as
-> TermTypeM (TypeBase Size as)
updateField [Name]
fields PatType
ve_t forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Exp -> TermTypeM PatType
expTypeFully Exp
src'
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
ExpBase f vn
-> [Name] -> ExpBase f vn -> f PatType -> SrcLoc -> ExpBase f vn
RecordUpdate Exp
src' [Name]
fields Exp
ve' (forall a. a -> Info a
Info PatType
updated_t) SrcLoc
loc
  where
    usage :: Usage
usage = SrcLoc -> Text -> Usage
mkUsage SrcLoc
loc Text
"record update"
    updateField :: [Name]
-> TypeBase Size as
-> TypeBase Size as
-> TermTypeM (TypeBase Size as)
updateField [] TypeBase Size as
ve_t TypeBase Size as
src_t = do
      (TypeBase Size as
src_t', Map VName Size
_) <- forall als.
SrcLoc
-> Rigidity
-> Name
-> TypeBase Size als
-> TermTypeM (TypeBase Size als, Map VName Size)
allDimsFreshInType SrcLoc
loc Rigidity
Nonrigid Name
"any" TypeBase Size as
src_t
      forall a. Checking -> TermTypeM a -> TermTypeM a
onFailure ([Name] -> TypeBase Size () -> TypeBase Size () -> Checking
CheckingRecordUpdate [Name]
fields (forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct TypeBase Size as
src_t') (forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct TypeBase Size as
ve_t)) forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *).
MonadUnify m =>
Usage -> TypeBase Size () -> TypeBase Size () -> m ()
unify Usage
usage (forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct TypeBase Size as
src_t') (forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct TypeBase Size as
ve_t)
      -- Important that we return ve_t so that we get the right aliases.
      forall (f :: * -> *) a. Applicative f => a -> f a
pure TypeBase Size as
ve_t
    updateField (Name
f : [Name]
fs) TypeBase Size as
ve_t (Scalar (Record Map Name (TypeBase Size as)
m))
      | Just TypeBase Size as
f_t <- forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
f Map Name (TypeBase Size as)
m = do
          TypeBase Size as
f_t' <- [Name]
-> TypeBase Size as
-> TypeBase Size as
-> TermTypeM (TypeBase Size as)
updateField [Name]
fs TypeBase Size as
ve_t TypeBase Size as
f_t
          forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as. Map Name (TypeBase dim as) -> ScalarTypeBase dim as
Record forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Name
f TypeBase Size as
f_t' Map Name (TypeBase Size as)
m
    updateField [Name]
_ TypeBase Size as
_ TypeBase Size as
_ =
      forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc forall a. Monoid a => a
mempty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ann. Doc ann -> Doc ann -> Doc ann
withIndexLink Doc ()
"record-type-not-known" forall a b. (a -> b) -> a -> b
$
        Doc ()
"Full type of"
          forall ann. Doc ann -> Doc ann -> Doc ann
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a ann. Pretty a => a -> Doc ann
pretty ExpBase NoInfo Name
src)
          forall ann. Doc ann -> Doc ann -> Doc ann
</> forall a. Text -> Doc a
textwrap Text
" is not known at this point.  Add a type annotation to the original record to disambiguate."

--
checkExp (AppExp (Index ExpBase NoInfo Name
e SliceBase NoInfo Name
slice SrcLoc
loc) NoInfo AppRes
_) = do
  Slice
slice' <- SliceBase NoInfo Name -> TermTypeM Slice
checkSlice SliceBase NoInfo Name
slice
  (TypeBase Size ()
t, TypeBase Size ()
_) <- SrcLoc
-> Name -> Int -> TermTypeM (TypeBase Size (), TypeBase Size ())
newArrayType SrcLoc
loc Name
"e" forall a b. (a -> b) -> a -> b
$ Slice -> Int
sliceDims Slice
slice'
  Exp
e' <- Text -> TypeBase Size () -> Exp -> TermTypeM Exp
unifies Text
"being indexed at" TypeBase Size ()
t forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExpBase NoInfo Name -> TermTypeM Exp
checkExp ExpBase NoInfo Name
e
  -- XXX, the RigidSlice here will be overridden in sliceShape with a proper value.
  (PatType
t', [VName]
retext) <-
    forall as.
Maybe (SrcLoc, Rigidity)
-> Slice
-> TypeBase Size as
-> TermTypeM (TypeBase Size as, [VName])
sliceShape (forall a. a -> Maybe a
Just (SrcLoc
loc, RigidSource -> Rigidity
Rigid (Maybe Size -> Text -> RigidSource
RigidSlice forall a. Maybe a
Nothing Text
""))) Slice
slice'
      forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Exp -> TermTypeM PatType
expTypeFully Exp
e'

  -- Remove aliases if the result is an overloaded type, because that
  -- will certainly not be aliased.
  PatType
t'' <- PatType -> TermTypeM PatType
noAliasesIfOverloaded PatType
t'

  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
AppExpBase f vn -> f AppRes -> ExpBase f vn
AppExp (forall (f :: * -> *) vn.
ExpBase f vn -> SliceBase f vn -> SrcLoc -> AppExpBase f vn
Index Exp
e' Slice
slice' SrcLoc
loc) (forall a. a -> Info a
Info forall a b. (a -> b) -> a -> b
$ PatType -> [VName] -> AppRes
AppRes PatType
t'' [VName]
retext)
checkExp (Assert ExpBase NoInfo Name
e1 ExpBase NoInfo Name
e2 NoInfo Text
NoInfo SrcLoc
loc) = do
  Exp
e1' <- Text -> [PrimType] -> Exp -> TermTypeM Exp
require Text
"being asserted" [PrimType
Bool] forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExpBase NoInfo Name -> TermTypeM Exp
checkExp ExpBase NoInfo Name
e1
  Exp
e2' <- ExpBase NoInfo Name -> TermTypeM Exp
checkExp ExpBase NoInfo Name
e2
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
ExpBase f vn -> ExpBase f vn -> f Text -> SrcLoc -> ExpBase f vn
Assert Exp
e1' Exp
e2' (forall a. a -> Info a
Info (forall a. Pretty a => a -> Text
prettyText ExpBase NoInfo Name
e1)) SrcLoc
loc
checkExp (Lambda [PatBase NoInfo Name]
params ExpBase NoInfo Name
body Maybe UncheckedTypeExp
rettype_te NoInfo (Aliasing, StructRetType)
NoInfo SrcLoc
loc) = do
  ([PatBase Info VName]
params', Exp
body', PatType
body_t, Maybe (TypeExp VName)
rettype', Info (Aliasing, StructRetType)
info) <-
    forall a. TermTypeM a -> TermTypeM a
removeSeminullOccurrences forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. TermTypeM a -> TermTypeM a
noUnique forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. TermTypeM a -> TermTypeM a
incLevel forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
[TypeParamBase Name]
-> [PatBase NoInfo Name]
-> ([TypeParamBase VName] -> [PatBase Info VName] -> TermTypeM a)
-> TermTypeM a
bindingParams [] [PatBase NoInfo Name]
params forall a b. (a -> b) -> a -> b
$ \[TypeParamBase VName]
_ [PatBase Info VName]
params' -> do
      Maybe (TypeExp VName, TypeBase Size (), [VName])
rettype_checked <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse UncheckedTypeExp
-> TermTypeM (TypeExp VName, TypeBase Size (), [VName])
checkTypeExpNonrigid Maybe UncheckedTypeExp
rettype_te
      let declared_rettype :: Maybe (TypeBase Size ())
declared_rettype =
            case Maybe (TypeExp VName, TypeBase Size (), [VName])
rettype_checked of
              Just (TypeExp VName
_, TypeBase Size ()
st, [VName]
_) -> forall a. a -> Maybe a
Just TypeBase Size ()
st
              Maybe (TypeExp VName, TypeBase Size (), [VName])
Nothing -> forall a. Maybe a
Nothing
      (Exp
body', Occurrences
closure) <-
        forall a. TermTypeM a -> TermTypeM (a, Occurrences)
tapOccurrences forall a b. (a -> b) -> a -> b
$ [PatBase Info VName]
-> ExpBase NoInfo Name
-> Maybe (TypeBase Size ())
-> SrcLoc
-> TermTypeM Exp
checkFunBody [PatBase Info VName]
params' ExpBase NoInfo Name
body Maybe (TypeBase Size ())
declared_rettype SrcLoc
loc
      PatType
body_t <- Exp -> TermTypeM PatType
expTypeFully Exp
body'

      [PatBase Info VName]
params'' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall e. ASTMappable e => e -> TermTypeM e
updateTypes [PatBase Info VName]
params'

      (Maybe (TypeExp VName)
rettype', StructRetType
rettype_st) <-
        case Maybe (TypeExp VName, TypeBase Size (), [VName])
rettype_checked of
          Just (TypeExp VName
te, TypeBase Size ()
st, [VName]
ext) -> do
            let st_structural :: TypeBase () ()
st_structural = forall dim as. TypeBase dim as -> TypeBase () ()
toStructural TypeBase Size ()
st
            SrcLoc
-> TypeBase () ()
-> [PatBase Info VName]
-> PatType
-> TermTypeM ()
checkReturnAlias SrcLoc
loc TypeBase () ()
st_structural [PatBase Info VName]
params'' PatType
body_t
            forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. a -> Maybe a
Just TypeExp VName
te, forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
ext TypeBase Size ()
st)
          Maybe (TypeExp VName, TypeBase Size (), [VName])
Nothing -> do
            StructRetType
ret <-
              forall {m :: * -> *} {as}.
(MonadUnify m, Monoid as) =>
[PatBase Info VName] -> TypeBase Size as -> m (RetTypeBase Size as)
inferReturnSizes [PatBase Info VName]
params'' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct forall a b. (a -> b) -> a -> b
$
                [PatBase Info VName] -> PatType -> PatType
inferReturnUniqueness [PatBase Info VName]
params'' PatType
body_t
            forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Maybe a
Nothing, StructRetType
ret)

      Aliasing
closure' <- [PatBase Info VName] -> Occurrences -> TermTypeM Aliasing
lexicalClosure [PatBase Info VName]
params'' Occurrences
closure

      forall (f :: * -> *) a. Applicative f => a -> f a
pure ([PatBase Info VName]
params'', Exp
body', PatType
body_t, Maybe (TypeExp VName)
rettype', forall a. a -> Info a
Info (Aliasing
closure', StructRetType
rettype_st))

  [PatBase Info VName] -> PatType -> SrcLoc -> TermTypeM ()
checkGlobalAliases [PatBase Info VName]
params' PatType
body_t SrcLoc
loc
  Maybe Name -> [PatBase Info VName] -> TermTypeM ()
verifyFunctionParams forall a. Maybe a
Nothing [PatBase Info VName]
params'

  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
[PatBase f vn]
-> ExpBase f vn
-> Maybe (TypeExp vn)
-> f (Aliasing, StructRetType)
-> SrcLoc
-> ExpBase f vn
Lambda [PatBase Info VName]
params' Exp
body' Maybe (TypeExp VName)
rettype' Info (Aliasing, StructRetType)
info SrcLoc
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 :: [PatBase Info VName] -> TypeBase Size as -> m (RetTypeBase Size as)
inferReturnSizes [PatBase Info VName]
params' TypeBase Size as
ret = do
      Int
cur_lvl <- forall (m :: * -> *). MonadUnify m => m Int
curLevel
      let named :: (PName, b) -> Maybe VName
named (Named VName
x, b
_) = forall a. a -> Maybe a
Just VName
x
          named (PName
Unnamed, b
_) = forall a. Maybe a
Nothing
          param_names :: [VName]
param_names = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (forall {b}. (PName, b) -> Maybe VName
named forall b c a. (b -> c) -> (a -> b) -> a -> c
. PatBase Info VName -> (PName, TypeBase Size ())
patternParam) [PatBase Info VName]
params'
          pos_sizes :: Set VName
pos_sizes =
            forall als. TypeBase Size als -> Set VName
sizeNamesPos forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall as dim pas.
Monoid as =>
[TypeBase dim pas] -> RetTypeBase dim as -> TypeBase dim as
foldFunType (forall a b. (a -> b) -> [a] -> [b]
map PatBase Info VName -> TypeBase Size ()
patternStructType [PatBase Info VName]
params') forall a b. (a -> b) -> a -> b
$
              forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [] TypeBase Size as
ret
          hide :: VName -> (Int, b) -> Bool
hide VName
k (Int
lvl, b
_) =
            Int
lvl forall a. Ord a => a -> a -> Bool
>= Int
cur_lvl Bool -> Bool -> Bool
&& VName
k forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [VName]
param_names Bool -> Bool -> Bool
&& VName
k forall a. Ord a => a -> Set a -> Bool
`S.notMember` Set VName
pos_sizes

      Set VName
hidden_sizes <-
        forall a. Ord a => [a] -> Set a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [k]
M.keys forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. (k -> a -> Bool) -> Map k a -> Map k a
M.filterWithKey forall {b}. VName -> (Int, b) -> Bool
hide forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints

      let onDim :: VName -> Set VName
onDim VName
name
            | VName
name forall a. Ord a => a -> Set a -> Bool
`S.member` Set VName
hidden_sizes = forall a. a -> Set a
S.singleton VName
name
          onDim VName
_ = forall a. Monoid a => a
mempty

      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType (forall a. Set a -> [a]
S.toList forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap VName -> Set VName
onDim forall a b. (a -> b) -> a -> b
$ forall als. TypeBase Size als -> Set VName
freeInType TypeBase Size as
ret) TypeBase Size as
ret
checkExp (OpSection QualName Name
op NoInfo PatType
_ SrcLoc
loc) = do
  (QualName VName
op', PatType
ftype) <- forall (m :: * -> *).
MonadTypeChecker m =>
SrcLoc -> QualName Name -> m (QualName VName, PatType)
lookupVar SrcLoc
loc QualName Name
op
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
QualName vn -> f PatType -> SrcLoc -> ExpBase f vn
OpSection QualName VName
op' (forall a. a -> Info a
Info PatType
ftype) SrcLoc
loc
checkExp (OpSectionLeft QualName Name
op NoInfo PatType
_ ExpBase NoInfo Name
e (NoInfo (PName, TypeBase Size (), Maybe VName),
 NoInfo (PName, TypeBase Size ()))
_ (NoInfo (RetTypeBase Size Aliasing), NoInfo [VName])
_ SrcLoc
loc) = do
  (QualName VName
op', PatType
ftype) <- forall (m :: * -> *).
MonadTypeChecker m =>
SrcLoc -> QualName Name -> m (QualName VName, PatType)
lookupVar SrcLoc
loc QualName Name
op
  Arg
e_arg <- ExpBase NoInfo Name -> TermTypeM Arg
checkArg ExpBase NoInfo Name
e
  (TypeBase Size ()
t1, PatType
rt, Maybe VName
argext, [VName]
retext) <- SrcLoc
-> ApplyOp
-> PatType
-> Arg
-> TermTypeM (TypeBase Size (), PatType, Maybe VName, [VName])
checkApply SrcLoc
loc (forall a. a -> Maybe a
Just QualName VName
op', Int
0) PatType
ftype Arg
e_arg
  case (PatType
ftype, PatType
rt) of
    (Scalar (Arrow Aliasing
_ PName
m1 TypeBase Size ()
_ RetTypeBase Size Aliasing
_), Scalar (Arrow Aliasing
_ PName
m2 TypeBase Size ()
t2 RetTypeBase Size Aliasing
rettype)) ->
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
        forall (f :: * -> *) vn.
QualName vn
-> f PatType
-> ExpBase f vn
-> (f (PName, TypeBase Size (), Maybe VName),
    f (PName, TypeBase Size ()))
-> (f (RetTypeBase Size Aliasing), f [VName])
-> SrcLoc
-> ExpBase f vn
OpSectionLeft
          QualName VName
op'
          (forall a. a -> Info a
Info PatType
ftype)
          (Arg -> Exp
argExp Arg
e_arg)
          (forall a. a -> Info a
Info (PName
m1, forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct TypeBase Size ()
t1, Maybe VName
argext), forall a. a -> Info a
Info (PName
m2, forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct TypeBase Size ()
t2))
          (forall a. a -> Info a
Info RetTypeBase Size Aliasing
rettype, forall a. a -> Info a
Info [VName]
retext)
          SrcLoc
loc
    (PatType, PatType)
_ ->
      forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
        Doc ()
"Operator section with invalid operator of type" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty PatType
ftype
checkExp (OpSectionRight QualName Name
op NoInfo PatType
_ ExpBase NoInfo Name
e (NoInfo (PName, TypeBase Size ()),
 NoInfo (PName, TypeBase Size (), Maybe VName))
_ NoInfo (RetTypeBase Size Aliasing)
NoInfo SrcLoc
loc) = do
  (QualName VName
op', PatType
ftype) <- forall (m :: * -> *).
MonadTypeChecker m =>
SrcLoc -> QualName Name -> m (QualName VName, PatType)
lookupVar SrcLoc
loc QualName Name
op
  Arg
e_arg <- ExpBase NoInfo Name -> TermTypeM Arg
checkArg ExpBase NoInfo Name
e
  case PatType
ftype of
    Scalar (Arrow Aliasing
as1 PName
m1 TypeBase Size ()
t1 (RetType [] (Scalar (Arrow Aliasing
as2 PName
m2 TypeBase Size ()
t2 (RetType [VName]
dims2 PatType
ret))))) -> do
      (TypeBase Size ()
t2', PatType
ret', Maybe VName
argext, [VName]
_) <-
        SrcLoc
-> ApplyOp
-> PatType
-> Arg
-> TermTypeM (TypeBase Size (), PatType, Maybe VName, [VName])
checkApply
          SrcLoc
loc
          (forall a. a -> Maybe a
Just QualName VName
op', Int
1)
          (forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as.
as
-> PName
-> TypeBase dim ()
-> RetTypeBase dim as
-> ScalarTypeBase dim as
Arrow Aliasing
as2 PName
m2 TypeBase Size ()
t2 forall a b. (a -> b) -> a -> b
$ forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [] forall a b. (a -> b) -> a -> b
$ forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as.
as
-> PName
-> TypeBase dim ()
-> RetTypeBase dim as
-> ScalarTypeBase dim as
Arrow Aliasing
as1 PName
m1 TypeBase Size ()
t1 forall a b. (a -> b) -> a -> b
$ forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [] PatType
ret)
          Arg
e_arg
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
        forall (f :: * -> *) vn.
QualName vn
-> f PatType
-> ExpBase f vn
-> (f (PName, TypeBase Size ()),
    f (PName, TypeBase Size (), Maybe VName))
-> f (RetTypeBase Size Aliasing)
-> SrcLoc
-> ExpBase f vn
OpSectionRight
          QualName VName
op'
          (forall a. a -> Info a
Info PatType
ftype)
          (Arg -> Exp
argExp Arg
e_arg)
          (forall a. a -> Info a
Info (PName
m1, forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct TypeBase Size ()
t1), forall a. a -> Info a
Info (PName
m2, forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct TypeBase Size ()
t2', Maybe VName
argext))
          (forall a. a -> Info a
Info forall a b. (a -> b) -> a -> b
$ forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
dims2 forall a b. (a -> b) -> a -> b
$ forall dim asf ast.
TypeBase dim asf -> (asf -> ast) -> TypeBase dim ast
addAliases PatType
ret (forall a. Semigroup a => a -> a -> a
<> forall as shape. Monoid as => TypeBase shape as -> as
aliases PatType
ret'))
          SrcLoc
loc
    PatType
_ ->
      forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
        Doc ()
"Operator section with invalid operator of type" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty PatType
ftype
checkExp (ProjectSection [Name]
fields NoInfo PatType
NoInfo SrcLoc
loc) = do
  PatType
a <- forall (m :: * -> *) als dim.
(MonadUnify m, Monoid als) =>
SrcLoc -> Name -> m (TypeBase dim als)
newTypeVar SrcLoc
loc Name
"a"
  let usage :: Usage
usage = SrcLoc -> Text -> Usage
mkUsage SrcLoc
loc Text
"projection at"
  PatType
b <- forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadUnify m =>
Usage -> Name -> PatType -> m PatType
mustHaveField Usage
usage) PatType
a [Name]
fields
  let ft :: PatType
ft = forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as.
as
-> PName
-> TypeBase dim ()
-> RetTypeBase dim as
-> ScalarTypeBase dim as
Arrow forall a. Monoid a => a
mempty PName
Unnamed (forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct PatType
a) forall a b. (a -> b) -> a -> b
$ forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [] PatType
b
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
[Name] -> f PatType -> SrcLoc -> ExpBase f vn
ProjectSection [Name]
fields (forall a. a -> Info a
Info PatType
ft) SrcLoc
loc
checkExp (IndexSection SliceBase NoInfo Name
slice NoInfo PatType
NoInfo SrcLoc
loc) = do
  Slice
slice' <- SliceBase NoInfo Name -> TermTypeM Slice
checkSlice SliceBase NoInfo Name
slice
  (TypeBase Size ()
t, TypeBase Size ()
_) <- SrcLoc
-> Name -> Int -> TermTypeM (TypeBase Size (), TypeBase Size ())
newArrayType SrcLoc
loc Name
"e" forall a b. (a -> b) -> a -> b
$ Slice -> Int
sliceDims Slice
slice'
  (TypeBase Size ()
t', [VName]
retext) <- forall as.
Maybe (SrcLoc, Rigidity)
-> Slice
-> TypeBase Size as
-> TermTypeM (TypeBase Size as, [VName])
sliceShape forall a. Maybe a
Nothing Slice
slice' TypeBase Size ()
t
  let ft :: PatType
ft = forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as.
as
-> PName
-> TypeBase dim ()
-> RetTypeBase dim as
-> ScalarTypeBase dim as
Arrow forall a. Monoid a => a
mempty PName
Unnamed TypeBase Size ()
t forall a b. (a -> b) -> a -> b
$ forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
retext forall a b. (a -> b) -> a -> b
$ forall dim as. TypeBase dim as -> TypeBase dim Aliasing
fromStruct TypeBase Size ()
t'
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
SliceBase f vn -> f PatType -> SrcLoc -> ExpBase f vn
IndexSection Slice
slice' (forall a. a -> Info a
Info PatType
ft) SrcLoc
loc
checkExp (AppExp (DoLoop [VName]
_ PatBase NoInfo Name
mergepat ExpBase NoInfo Name
mergeexp LoopFormBase NoInfo Name
form ExpBase NoInfo Name
loopbody SrcLoc
loc) NoInfo AppRes
_) = do
  (([VName]
sparams, PatBase Info VName
mergepat', Exp
mergeexp', LoopFormBase Info VName
form', Exp
loopbody'), AppRes
appres) <-
    (ExpBase NoInfo Name -> TermTypeM Exp)
-> UncheckedLoop -> SrcLoc -> TermTypeM (CheckedLoop, AppRes)
checkDoLoop ExpBase NoInfo Name -> TermTypeM Exp
checkExp (PatBase NoInfo Name
mergepat, ExpBase NoInfo Name
mergeexp, LoopFormBase NoInfo Name
form, ExpBase NoInfo Name
loopbody) SrcLoc
loc
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
    forall (f :: * -> *) vn.
AppExpBase f vn -> f AppRes -> ExpBase f vn
AppExp
      (forall (f :: * -> *) vn.
[VName]
-> PatBase f vn
-> ExpBase f vn
-> LoopFormBase f vn
-> ExpBase f vn
-> SrcLoc
-> AppExpBase f vn
DoLoop [VName]
sparams PatBase Info VName
mergepat' Exp
mergeexp' LoopFormBase Info VName
form' Exp
loopbody' SrcLoc
loc)
      (forall a. a -> Info a
Info AppRes
appres)
checkExp (Constr Name
name [ExpBase NoInfo Name]
es NoInfo PatType
NoInfo SrcLoc
loc) = do
  TypeBase Size ()
t <- forall (m :: * -> *) als dim.
(MonadUnify m, Monoid als) =>
SrcLoc -> Name -> m (TypeBase dim als)
newTypeVar SrcLoc
loc Name
"t"
  [Exp]
es' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ExpBase NoInfo Name -> TermTypeM Exp
checkExp [ExpBase NoInfo Name]
es
  [PatType]
ets <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Exp -> TermTypeM PatType
expTypeFully [Exp]
es'
  forall (m :: * -> *).
MonadUnify m =>
Usage -> Name -> TypeBase Size () -> [TypeBase Size ()] -> m ()
mustHaveConstr (SrcLoc -> Text -> Usage
mkUsage SrcLoc
loc Text
"use of constructor") Name
name TypeBase Size ()
t (forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PatType]
ets)
  -- A sum value aliases *anything* that went into its construction.
  let als :: Aliasing
als = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall as shape. Monoid as => TypeBase shape as -> as
aliases [PatType]
ets
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
Name -> [ExpBase f vn] -> f PatType -> SrcLoc -> ExpBase f vn
Constr Name
name [Exp]
es' (forall a. a -> Info a
Info forall a b. (a -> b) -> a -> b
$ forall dim as. TypeBase dim as -> TypeBase dim Aliasing
fromStruct TypeBase Size ()
t forall dim asf ast.
TypeBase dim asf -> (asf -> ast) -> TypeBase dim ast
`addAliases` (forall a. Semigroup a => a -> a -> a
<> Aliasing
als)) SrcLoc
loc
checkExp (AppExp (Match ExpBase NoInfo Name
e NonEmpty (CaseBase NoInfo Name)
cs SrcLoc
loc) NoInfo AppRes
_) =
  forall a b.
TermTypeM a -> (a -> Occurrences -> TermTypeM b) -> TermTypeM b
sequentially (ExpBase NoInfo Name -> TermTypeM Exp
checkExp ExpBase NoInfo Name
e) forall a b. (a -> b) -> a -> b
$ \Exp
e' Occurrences
_ -> do
    PatType
mt <- Exp -> TermTypeM PatType
expTypeFully Exp
e'
    (NonEmpty (CaseBase Info VName)
cs', PatType
t, [VName]
retext) <- PatType
-> NonEmpty (CaseBase NoInfo Name)
-> TermTypeM (NonEmpty (CaseBase Info VName), PatType, [VName])
checkCases PatType
mt NonEmpty (CaseBase NoInfo Name)
cs
    forall (m :: * -> *) dim as.
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage -> Text -> TypeBase dim as -> m ()
zeroOrderType
      (SrcLoc -> Text -> Usage
mkUsage SrcLoc
loc Text
"being returned 'match'")
      Text
"type returned from pattern match"
      PatType
t
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
AppExpBase f vn -> f AppRes -> ExpBase f vn
AppExp (forall (f :: * -> *) vn.
ExpBase f vn
-> NonEmpty (CaseBase f vn) -> SrcLoc -> AppExpBase f vn
Match Exp
e' NonEmpty (CaseBase Info VName)
cs' SrcLoc
loc) (forall a. a -> Info a
Info forall a b. (a -> b) -> a -> b
$ PatType -> [VName] -> AppRes
AppRes PatType
t [VName]
retext)
checkExp (Attr AttrInfo Name
info ExpBase NoInfo Name
e SrcLoc
loc) =
  forall (f :: * -> *) vn.
AttrInfo vn -> ExpBase f vn -> SrcLoc -> ExpBase f vn
Attr forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadTypeChecker m =>
AttrInfo Name -> m (AttrInfo VName)
checkAttr AttrInfo Name
info forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ExpBase NoInfo Name -> TermTypeM Exp
checkExp ExpBase NoInfo Name
e forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure SrcLoc
loc

checkCases ::
  PatType ->
  NE.NonEmpty (CaseBase NoInfo Name) ->
  TermTypeM (NE.NonEmpty (CaseBase Info VName), PatType, [VName])
checkCases :: PatType
-> NonEmpty (CaseBase NoInfo Name)
-> TermTypeM (NonEmpty (CaseBase Info VName), PatType, [VName])
checkCases PatType
mt NonEmpty (CaseBase NoInfo Name)
rest_cs =
  case forall a. NonEmpty a -> (a, Maybe (NonEmpty a))
NE.uncons NonEmpty (CaseBase NoInfo Name)
rest_cs of
    (CaseBase NoInfo Name
c, Maybe (NonEmpty (CaseBase NoInfo Name))
Nothing) -> do
      (CaseBase Info VName
c', PatType
t, [VName]
retext) <- PatType
-> CaseBase NoInfo Name
-> TermTypeM (CaseBase Info VName, PatType, [VName])
checkCase PatType
mt CaseBase NoInfo Name
c
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. a -> NonEmpty a
NE.singleton CaseBase Info VName
c', PatType
t, [VName]
retext)
    (CaseBase NoInfo Name
c, Just NonEmpty (CaseBase NoInfo Name)
cs) -> do
      (((CaseBase Info VName
c', PatType
c_t, [VName]
_), (NonEmpty (CaseBase Info VName)
cs', PatType
cs_t, [VName]
_)), Occurrences
dflow) <-
        forall a. TermTypeM a -> TermTypeM (a, Occurrences)
tapOccurrences forall a b. (a -> b) -> a -> b
$ PatType
-> CaseBase NoInfo Name
-> TermTypeM (CaseBase Info VName, PatType, [VName])
checkCase PatType
mt CaseBase NoInfo Name
c forall a b. TermTypeM a -> TermTypeM b -> TermTypeM (a, b)
`alternative` PatType
-> NonEmpty (CaseBase NoInfo Name)
-> TermTypeM (NonEmpty (CaseBase Info VName), PatType, [VName])
checkCases PatType
mt NonEmpty (CaseBase NoInfo Name)
cs
      (PatType
brancht, [VName]
retext) <- SrcLoc -> PatType -> PatType -> TermTypeM (PatType, [VName])
unifyBranchTypes (forall a. Located a => a -> SrcLoc
srclocOf CaseBase NoInfo Name
c) PatType
c_t PatType
cs_t
      let t :: PatType
t =
            forall dim asf ast.
TypeBase dim asf -> (asf -> ast) -> TypeBase dim ast
addAliases
              PatType
brancht
              (forall a. Ord a => Set a -> Set a -> Set a
`S.difference` forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map VName -> Alias
AliasBound (Occurrences -> Set VName
allConsumed Occurrences
dflow))
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. a -> NonEmpty a -> NonEmpty a
NE.cons CaseBase Info VName
c' NonEmpty (CaseBase Info VName)
cs', PatType
t, [VName]
retext)

checkCase ::
  PatType ->
  CaseBase NoInfo Name ->
  TermTypeM (CaseBase Info VName, PatType, [VName])
checkCase :: PatType
-> CaseBase NoInfo Name
-> TermTypeM (CaseBase Info VName, PatType, [VName])
checkCase PatType
mt (CasePat PatBase NoInfo Name
p ExpBase NoInfo Name
e SrcLoc
loc) =
  forall a.
[SizeBinder VName]
-> PatBase NoInfo Name
-> InferredType
-> (PatBase Info VName -> TermTypeM a)
-> TermTypeM a
bindingPat [] PatBase NoInfo Name
p (PatType -> InferredType
Ascribed PatType
mt) forall a b. (a -> b) -> a -> b
$ \PatBase Info VName
p' -> do
    Exp
e' <- ExpBase NoInfo Name -> TermTypeM Exp
checkExp ExpBase NoInfo Name
e
    (PatType
t, [VName]
retext) <- SrcLoc
-> Map VName (IdentBase Info VName)
-> PatType
-> TermTypeM (PatType, [VName])
unscopeType SrcLoc
loc (forall (f :: * -> *).
Functor f =>
PatBase f VName -> Map VName (IdentBase f VName)
patternMap PatBase Info VName
p') forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Exp -> TermTypeM PatType
expTypeFully Exp
e'
    forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (f :: * -> *) vn.
PatBase f vn -> ExpBase f vn -> SrcLoc -> CaseBase f vn
CasePat PatBase Info VName
p' Exp
e' SrcLoc
loc, PatType
t, [VName]
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 (forall a b. a -> Unmatched b -> Unmatched a
forall a b. (a -> b) -> Unmatched a -> Unmatched b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Unmatched b -> Unmatched a
$c<$ :: forall a b. a -> Unmatched b -> Unmatched a
fmap :: forall a b. (a -> b) -> Unmatched a -> Unmatched b
$cfmap :: forall a b. (a -> b) -> Unmatched a -> Unmatched b
Functor, Int -> Unmatched p -> ShowS
forall p. Show p => Int -> Unmatched p -> ShowS
forall p. Show p => [Unmatched p] -> ShowS
forall p. Show p => Unmatched p -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Unmatched p] -> ShowS
$cshowList :: forall p. Show p => [Unmatched p] -> ShowS
show :: Unmatched p -> String
$cshow :: forall p. Show p => Unmatched p -> String
showsPrec :: Int -> Unmatched p -> ShowS
$cshowsPrec :: forall p. Show p => Int -> Unmatched p -> ShowS
Show)

instance Pretty (Unmatched (PatBase Info VName)) where
  pretty :: forall ann. Unmatched (PatBase Info VName) -> Doc ann
pretty Unmatched (PatBase Info VName)
um = case Unmatched (PatBase Info VName)
um of
    (UnmatchedNum PatBase Info VName
p [PatLit]
nums) -> forall {v} {f :: * -> *} {ann}.
(Eq v, IsName v, Annot f) =>
PatBase f v -> Doc ann
pretty' PatBase Info VName
p forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"where p is not one of" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty [PatLit]
nums
    (UnmatchedBool PatBase Info VName
p) -> forall {v} {f :: * -> *} {ann}.
(Eq v, IsName v, Annot f) =>
PatBase f v -> Doc ann
pretty' PatBase Info VName
p
    (UnmatchedConstr PatBase Info VName
p) -> forall {v} {f :: * -> *} {ann}.
(Eq v, IsName v, Annot f) =>
PatBase f v -> Doc ann
pretty' PatBase Info VName
p
    (Unmatched PatBase Info VName
p) -> forall {v} {f :: * -> *} {ann}.
(Eq v, IsName v, Annot f) =>
PatBase f v -> Doc ann
pretty' PatBase Info VName
p
    where
      pretty' :: PatBase f v -> Doc ann
pretty' (PatAscription PatBase f v
p TypeExp v
t SrcLoc
_) = forall a ann. Pretty a => a -> Doc ann
pretty PatBase f v
p forall a. Semigroup a => a -> a -> a
<> Doc ann
":" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty TypeExp v
t
      pretty' (PatParens PatBase f v
p SrcLoc
_) = forall ann. Doc ann -> Doc ann
parens forall a b. (a -> b) -> a -> b
$ PatBase f v -> Doc ann
pretty' PatBase f v
p
      pretty' (PatAttr AttrInfo v
_ PatBase f v
p SrcLoc
_) = forall ann. Doc ann -> Doc ann
parens forall a b. (a -> b) -> a -> b
$ PatBase f v -> Doc ann
pretty' PatBase f v
p
      pretty' (Id v
v f PatType
_ SrcLoc
_) = forall v a. IsName v => v -> Doc a
prettyName v
v
      pretty' (TuplePat [PatBase f v]
pats SrcLoc
_) = forall ann. Doc ann -> Doc ann
parens forall a b. (a -> b) -> a -> b
$ forall a. [Doc a] -> Doc a
commasep forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map PatBase f v -> Doc ann
pretty' [PatBase f v]
pats
      pretty' (RecordPat [(Name, PatBase f v)]
fs SrcLoc
_) = forall ann. Doc ann -> Doc ann
braces forall a b. (a -> b) -> a -> b
$ forall a. [Doc a] -> Doc a
commasep forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (Name, PatBase f v) -> Doc ann
ppField [(Name, PatBase f v)]
fs
        where
          ppField :: (Name, PatBase f v) -> Doc ann
ppField (Name
name, PatBase f v
t) = forall a ann. Pretty a => a -> Doc ann
pretty (Name -> String
nameToString Name
name) forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann
equals forall a. Semigroup a => a -> a -> a
<> PatBase f v -> Doc ann
pretty' PatBase f v
t
      pretty' Wildcard {} = Doc ann
"_"
      pretty' (PatLit PatLit
e f PatType
_ SrcLoc
_) = forall a ann. Pretty a => a -> Doc ann
pretty PatLit
e
      pretty' (PatConstr Name
n f PatType
_ [PatBase f v]
ps SrcLoc
_) = Doc ann
"#" forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty Name
n forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a. [Doc a] -> Doc a
sep (forall a b. (a -> b) -> [a] -> [b]
map PatBase f v -> Doc ann
pretty' [PatBase f v]
ps)

checkIdent :: IdentBase NoInfo Name -> TermTypeM Ident
checkIdent :: IdentBase NoInfo Name -> TermTypeM (IdentBase Info VName)
checkIdent (Ident Name
name NoInfo PatType
_ SrcLoc
loc) = do
  (QualName [VName]
_ VName
name', PatType
vt) <- forall (m :: * -> *).
MonadTypeChecker m =>
SrcLoc -> QualName Name -> m (QualName VName, PatType)
lookupVar SrcLoc
loc (forall v. v -> QualName v
qualName Name
name)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
vn -> f PatType -> SrcLoc -> IdentBase f vn
Ident VName
name' (forall a. a -> Info a
Info PatType
vt) SrcLoc
loc

checkSlice :: UncheckedSlice -> TermTypeM Slice
checkSlice :: SliceBase NoInfo Name -> TermTypeM Slice
checkSlice = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM DimIndexBase NoInfo Name -> TermTypeM (DimIndexBase Info VName)
checkDimIndex
  where
    checkDimIndex :: DimIndexBase NoInfo Name -> TermTypeM (DimIndexBase Info VName)
checkDimIndex (DimFix ExpBase NoInfo Name
i) =
      forall (f :: * -> *) vn. ExpBase f vn -> DimIndexBase f vn
DimFix forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Text -> [PrimType] -> Exp -> TermTypeM Exp
require Text
"use as index" [PrimType]
anySignedType forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExpBase NoInfo Name -> TermTypeM Exp
checkExp ExpBase NoInfo Name
i)
    checkDimIndex (DimSlice Maybe (ExpBase NoInfo Name)
i Maybe (ExpBase NoInfo Name)
j Maybe (ExpBase NoInfo Name)
s) =
      forall (f :: * -> *) vn.
Maybe (ExpBase f vn)
-> Maybe (ExpBase f vn)
-> Maybe (ExpBase f vn)
-> DimIndexBase f vn
DimSlice forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (ExpBase NoInfo Name) -> TermTypeM (Maybe Exp)
check Maybe (ExpBase NoInfo Name)
i forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe (ExpBase NoInfo Name) -> TermTypeM (Maybe Exp)
check Maybe (ExpBase NoInfo Name)
j forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe (ExpBase NoInfo Name) -> TermTypeM (Maybe Exp)
check Maybe (ExpBase NoInfo Name)
s

    check :: Maybe (ExpBase NoInfo Name) -> TermTypeM (Maybe Exp)
check =
      forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing) forall a b. (a -> b) -> a -> b
$
        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> TypeBase Size () -> Exp -> TermTypeM Exp
unifies Text
"use as index" (forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as. PrimType -> ScalarTypeBase dim as
Prim forall a b. (a -> b) -> a -> b
$ IntType -> PrimType
Signed IntType
Int64) forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< ExpBase NoInfo Name -> TermTypeM Exp
checkExp

-- The number of dimensions affected by this slice (so the minimum
-- rank of the array we are slicing).
sliceDims :: Slice -> Int
sliceDims :: Slice -> Int
sliceDims = forall (t :: * -> *) a. Foldable t => t a -> Int
length

type Arg = (Exp, PatType, Occurrences, SrcLoc)

argExp :: Arg -> Exp
argExp :: Arg -> Exp
argExp (Exp
e, PatType
_, Occurrences
_, SrcLoc
_) = Exp
e

argType :: Arg -> PatType
argType :: Arg -> PatType
argType (Exp
_, PatType
t, Occurrences
_, SrcLoc
_) = PatType
t

checkArg :: UncheckedExp -> TermTypeM Arg
checkArg :: ExpBase NoInfo Name -> TermTypeM Arg
checkArg ExpBase NoInfo Name
arg = do
  (Exp
arg', Occurrences
dflow) <- forall a. TermTypeM a -> TermTypeM (a, Occurrences)
collectOccurrences forall a b. (a -> b) -> a -> b
$ ExpBase NoInfo Name -> TermTypeM Exp
checkExp ExpBase NoInfo Name
arg
  PatType
arg_t <- Exp -> TermTypeM PatType
expType Exp
arg'
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp
arg', PatType
arg_t, Occurrences
dflow, forall a. Located a => a -> SrcLoc
srclocOf Exp
arg')

instantiateDimsInReturnType ::
  SrcLoc ->
  Maybe (QualName VName) ->
  RetTypeBase Size als ->
  TermTypeM (TypeBase Size als, [VName])
instantiateDimsInReturnType :: forall als.
SrcLoc
-> Maybe (QualName VName)
-> RetTypeBase Size als
-> TermTypeM (TypeBase Size als, [VName])
instantiateDimsInReturnType SrcLoc
tloc Maybe (QualName VName)
fname =
  forall (m :: * -> *) als.
MonadUnify m =>
SrcLoc
-> Rigidity
-> RetTypeBase Size als
-> m (TypeBase Size als, [VName])
instantiateEmptyArrayDims SrcLoc
tloc forall a b. (a -> b) -> a -> b
$ RigidSource -> Rigidity
Rigid forall a b. (a -> b) -> a -> b
$ Maybe (QualName VName) -> RigidSource
RigidRet Maybe (QualName VName)
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 :: forall als. TypeBase Size als -> Set VName
boundInsideType (Array as
_ Uniqueness
_ Shape Size
_ ScalarTypeBase Size ()
t) = forall als. TypeBase Size als -> Set VName
boundInsideType (forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar ScalarTypeBase Size ()
t)
boundInsideType (Scalar Prim {}) = forall a. Monoid a => a
mempty
boundInsideType (Scalar (TypeVar as
_ Uniqueness
_ QualName VName
_ [TypeArg Size]
targs)) = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap TypeArg Size -> Set VName
f [TypeArg Size]
targs
  where
    f :: TypeArg Size -> Set VName
f (TypeArgType TypeBase Size ()
t SrcLoc
_) = forall als. TypeBase Size als -> Set VName
boundInsideType TypeBase Size ()
t
    f TypeArgDim {} = forall a. Monoid a => a
mempty
boundInsideType (Scalar (Record Map Name (TypeBase Size as)
fs)) = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall als. TypeBase Size als -> Set VName
boundInsideType Map Name (TypeBase Size as)
fs
boundInsideType (Scalar (Sum Map Name [TypeBase Size as]
cs)) = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall als. TypeBase Size als -> Set VName
boundInsideType) Map Name [TypeBase Size as]
cs
boundInsideType (Scalar (Arrow as
_ PName
pn TypeBase Size ()
t1 (RetType [VName]
dims TypeBase Size as
t2))) =
  Set VName
pn' forall a. Semigroup a => a -> a -> a
<> forall als. TypeBase Size als -> Set VName
boundInsideType TypeBase Size ()
t1 forall a. Semigroup a => a -> a -> a
<> forall a. Ord a => [a] -> Set a
S.fromList [VName]
dims forall a. Semigroup a => a -> a -> a
<> forall als. TypeBase Size als -> Set VName
boundInsideType TypeBase Size as
t2
  where
    pn' :: Set VName
pn' = case PName
pn of
      PName
Unnamed -> forall a. Monoid a => a
mempty
      Named VName
v -> forall a. a -> Set a
S.singleton VName
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 :: TypeBase Size () -> (Set VName, Set VName)
dimUses = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall s a. State s a -> s -> s
execState forall a. Monoid a => a
mempty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) fdim tdim als.
Applicative f =>
(Set VName -> DimPos -> fdim -> f tdim)
-> TypeBase fdim als -> f (TypeBase tdim als)
traverseDims forall {f :: * -> *}.
MonadState (Set VName, Set VName) f =>
Set VName -> DimPos -> Size -> f ()
f
  where
    f :: Set VName -> DimPos -> Size -> f ()
f Set VName
bound DimPos
_ (NamedSize QualName VName
v) | forall vn. QualName vn -> vn
qualLeaf QualName VName
v forall a. Ord a => a -> Set a -> Bool
`S.member` Set VName
bound = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    f Set VName
_ DimPos
PosImmediate (NamedSize QualName VName
v) = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((forall a. a -> Set a
S.singleton (forall vn. QualName vn -> vn
qualLeaf QualName VName
v), forall a. Monoid a => a
mempty) <>)
    f Set VName
_ DimPos
PosParam (NamedSize QualName VName
v) = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((forall a. Monoid a => a
mempty, forall a. a -> Set a
S.singleton (forall vn. QualName vn -> vn
qualLeaf QualName VName
v)) <>)
    f Set VName
_ DimPos
_ Size
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

checkApply ::
  SrcLoc ->
  ApplyOp ->
  PatType ->
  Arg ->
  TermTypeM (StructType, PatType, Maybe VName, [VName])
checkApply :: SrcLoc
-> ApplyOp
-> PatType
-> Arg
-> TermTypeM (TypeBase Size (), PatType, Maybe VName, [VName])
checkApply
  SrcLoc
loc
  (Maybe (QualName VName)
fname, Int
_)
  (Scalar (Arrow Aliasing
as PName
pname TypeBase Size ()
tp1 RetTypeBase Size Aliasing
tp2))
  (Exp
argexp, PatType
argtype, Occurrences
dflow, SrcLoc
argloc) =
    forall a. Checking -> TermTypeM a -> TermTypeM a
onFailure (Maybe (QualName VName)
-> Exp -> TypeBase Size () -> TypeBase Size () -> Checking
CheckingApply Maybe (QualName VName)
fname Exp
argexp TypeBase Size ()
tp1 (forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct PatType
argtype)) forall a b. (a -> b) -> a -> b
$ do
      forall (m :: * -> *).
MonadUnify m =>
Usage -> TypeBase Size () -> TypeBase Size () -> m ()
expect (SrcLoc -> Text -> Usage
mkUsage SrcLoc
argloc Text
"use as function argument") (forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct TypeBase Size ()
tp1) (forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct PatType
argtype)

      -- Perform substitutions of instantiated variables in the types.
      TypeBase Size ()
tp1' <- forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully TypeBase Size ()
tp1
      (PatType
tp2', [VName]
ext) <- forall als.
SrcLoc
-> Maybe (QualName VName)
-> RetTypeBase Size als
-> TermTypeM (TypeBase Size als, [VName])
instantiateDimsInReturnType SrcLoc
loc Maybe (QualName VName)
fname forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully RetTypeBase Size Aliasing
tp2
      PatType
argtype' <- forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully PatType
argtype

      -- Check whether this would produce an impossible return type.
      let (Set VName
tp2_produced_dims, Set VName
tp2_paramdims) = TypeBase Size () -> (Set VName, Set VName)
dimUses forall a b. (a -> b) -> a -> b
$ forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct PatType
tp2'
          problematic :: Set VName
problematic = forall a. Ord a => [a] -> Set a
S.fromList [VName]
ext forall a. Semigroup a => a -> a -> a
<> forall als. TypeBase Size als -> Set VName
boundInsideType PatType
argtype'
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a. Ord a => a -> Set a -> Bool
`S.member` Set VName
problematic) (Set VName
tp2_paramdims forall a. Ord a => Set a -> Set a -> Set a
`S.difference` Set VName
tp2_produced_dims)) forall a b. (a -> b) -> a -> b
$ do
        forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc forall a. Monoid a => a
mempty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ann. Doc ann -> Doc ann -> Doc ann
withIndexLink Doc ()
"existential-param-ret" forall a b. (a -> b) -> a -> b
$
          Doc ()
"Existential size would appear in function parameter of return type:"
            forall ann. Doc ann -> Doc ann -> Doc ann
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a ann. Pretty a => a -> Doc ann
pretty (forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
ext PatType
tp2'))
            forall ann. Doc ann -> Doc ann -> Doc ann
</> forall a. Text -> Doc a
textwrap Text
"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."

      Occurrences -> TermTypeM ()
occur [Aliasing -> SrcLoc -> Occurrence
observation Aliasing
as SrcLoc
loc]

      Occurrences -> TermTypeM ()
checkOccurrences Occurrences
dflow

      case Occurrences -> Maybe Occurrence
anyConsumption Occurrences
dflow of
        Just Occurrence
c ->
          let msg :: Text
msg = Text
"type of expression with consumption at " forall a. Semigroup a => a -> a -> a
<> forall a. Located a => a -> Text
locText (Occurrence -> SrcLoc
location Occurrence
c)
           in forall (m :: * -> *) dim as.
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage -> Text -> TypeBase dim as -> m ()
zeroOrderType (SrcLoc -> Text -> Usage
mkUsage SrcLoc
argloc Text
"potential consumption in expression") Text
msg TypeBase Size ()
tp1
        Maybe Occurrence
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

      Occurrences
occurs <- (Occurrences
dflow `seqOccurrences`) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SrcLoc -> PatType -> Diet -> TermTypeM Occurrences
consumeArg SrcLoc
argloc PatType
argtype' (forall shape as. TypeBase shape as -> Diet
diet TypeBase Size ()
tp1')

      SrcLoc -> Aliasing -> TermTypeM ()
checkIfConsumable SrcLoc
loc forall a b. (a -> b) -> a -> b
$ forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map VName -> Alias
AliasBound forall a b. (a -> b) -> a -> b
$ Occurrences -> Set VName
allConsumed Occurrences
occurs
      Occurrences -> TermTypeM ()
occur Occurrences
occurs

      -- Unification ignores uniqueness in higher-order arguments, so
      -- we check for that here.
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall dim as. TypeBase dim as -> TypeBase () ()
toStructural PatType
argtype' TypeBase () () -> TypeBase () () -> Bool
`subtypeOf` forall dim as. TypeBase dim as -> Uniqueness -> TypeBase dim as
setUniqueness (forall dim as. TypeBase dim as -> TypeBase () ()
toStructural TypeBase Size ()
tp1') Uniqueness
Nonunique) forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc forall a. Monoid a => a
mempty Doc ()
"Consumption/aliasing does not match."

      (Maybe VName
argext, VName -> Maybe (Subst StructRetType)
parsubst) <-
        case PName
pname of
          Named VName
pname'
            | (Scalar (Prim (Signed IntType
Int64))) <- TypeBase Size ()
tp1' -> do
                (Size
d, Maybe VName
argext) <- Maybe (QualName VName) -> Exp -> TermTypeM (Size, Maybe VName)
sizeFromArg Maybe (QualName VName)
fname Exp
argexp
                forall (f :: * -> *) a. Applicative f => a -> f a
pure
                  ( Maybe VName
argext,
                    (forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` forall k a. k -> a -> Map k a
M.singleton VName
pname' (forall t. Size -> Subst t
SizeSubst Size
d))
                  )
          PName
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Maybe a
Nothing, forall a b. a -> b -> a
const forall a. Maybe a
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).
      VName
v <- forall (m :: * -> *). MonadTypeChecker m => Name -> m VName
newID Name
"internal_app_result"
      forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \TermTypeState
s -> TermTypeState
s {stateNames :: Map VName NameReason
stateNames = forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
v (Maybe (QualName VName) -> SrcLoc -> NameReason
NameAppRes Maybe (QualName VName)
fname SrcLoc
loc) forall a b. (a -> b) -> a -> b
$ TermTypeState -> Map VName NameReason
stateNames TermTypeState
s}
      let appres :: Aliasing
appres = forall a. a -> Set a
S.singleton forall a b. (a -> b) -> a -> b
$ VName -> Alias
AliasFree VName
v
      let tp2'' :: PatType
tp2'' = forall a.
Substitutable a =>
(VName -> Maybe (Subst StructRetType)) -> a -> a
applySubst VName -> Maybe (Subst StructRetType)
parsubst forall a b. (a -> b) -> a -> b
$ Aliasing -> PatType -> Diet -> PatType -> PatType
returnType Aliasing
appres PatType
tp2' (forall shape as. TypeBase shape as -> Diet
diet TypeBase Size ()
tp1') PatType
argtype'

      forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeBase Size ()
tp1', PatType
tp2'', Maybe VName
argext, [VName]
ext)
checkApply SrcLoc
loc ApplyOp
fname tfun :: PatType
tfun@(Scalar TypeVar {}) Arg
arg = do
  TypeBase Size ()
tv <- forall (m :: * -> *) als dim.
(MonadUnify m, Monoid als) =>
SrcLoc -> Name -> m (TypeBase dim als)
newTypeVar SrcLoc
loc Name
"b"
  -- Change the uniqueness of the argument type because we never want
  -- to infer that a function is consuming.
  let argt_nonunique :: TypeBase Size ()
argt_nonunique = forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct (Arg -> PatType
argType Arg
arg) forall dim as. TypeBase dim as -> Uniqueness -> TypeBase dim as
`setUniqueness` Uniqueness
Nonunique
  forall (m :: * -> *).
MonadUnify m =>
Usage -> TypeBase Size () -> TypeBase Size () -> m ()
unify (SrcLoc -> Text -> Usage
mkUsage SrcLoc
loc Text
"use as function") (forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct PatType
tfun) forall a b. (a -> b) -> a -> b
$
    forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$
      forall dim as.
as
-> PName
-> TypeBase dim ()
-> RetTypeBase dim as
-> ScalarTypeBase dim as
Arrow forall a. Monoid a => a
mempty PName
Unnamed TypeBase Size ()
argt_nonunique forall a b. (a -> b) -> a -> b
$
        forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [] TypeBase Size ()
tv
  PatType
tfun' <- forall (m :: * -> *). MonadUnify m => PatType -> m PatType
normPatType PatType
tfun
  SrcLoc
-> ApplyOp
-> PatType
-> Arg
-> TermTypeM (TypeBase Size (), PatType, Maybe VName, [VName])
checkApply SrcLoc
loc ApplyOp
fname PatType
tfun' Arg
arg
checkApply SrcLoc
loc (Maybe (QualName VName)
fname, Int
prev_applied) PatType
ftype (Exp
argexp, PatType
_, Occurrences
_, SrcLoc
_) = do
  let fname' :: Doc ann
fname' = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc ann
"expression" (forall ann. Doc ann -> Doc ann
dquotes forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a ann. Pretty a => a -> Doc ann
pretty) Maybe (QualName VName)
fname

  forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
    if Int
prev_applied forall a. Eq a => a -> a -> Bool
== Int
0
      then
        Doc ()
"Cannot apply"
          forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann
fname'
          forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"as function, as it has type:"
          forall ann. Doc ann -> Doc ann -> Doc ann
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a ann. Pretty a => a -> Doc ann
pretty PatType
ftype)
      else
        Doc ()
"Cannot apply"
          forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann
fname'
          forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"to argument #" forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty (Int
prev_applied forall a. Num a => a -> a -> a
+ Int
1)
          forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a b. Doc a -> Doc b
shorten forall a b. (a -> b) -> a -> b
$ forall ann. Doc ann -> Doc ann
group forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty a => a -> Doc ann
pretty Exp
argexp) forall a. Semigroup a => a -> a -> a
<> Doc ()
","
          forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"as"
          forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann
fname'
          forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"only takes"
          forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty Int
prev_applied
          forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
arguments forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
  where
    arguments :: Doc ()
arguments
      | Int
prev_applied forall a. Eq a => a -> a -> Bool
== Int
1 = Doc ()
"argument"
      | Bool
otherwise = Doc ()
"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 :: Aliasing -> PatType -> Diet -> PatType -> PatType
returnType Aliasing
_ (Array Aliasing
_ Uniqueness
Unique Shape Size
et ScalarTypeBase Size ()
shape) Diet
_ PatType
_ =
  forall dim as.
as
-> Uniqueness
-> Shape dim
-> ScalarTypeBase dim ()
-> TypeBase dim as
Array forall a. Monoid a => a
mempty Uniqueness
Nonunique Shape Size
et ScalarTypeBase Size ()
shape -- Intentional!
returnType Aliasing
appres (Array Aliasing
als Uniqueness
Nonunique Shape Size
et ScalarTypeBase Size ()
shape) Diet
d PatType
arg =
  forall dim as.
as
-> Uniqueness
-> Shape dim
-> ScalarTypeBase dim ()
-> TypeBase dim as
Array (Aliasing
appres forall a. Semigroup a => a -> a -> a
<> Aliasing
als forall a. Semigroup a => a -> a -> a
<> Aliasing
arg_als) Uniqueness
Nonunique Shape Size
et ScalarTypeBase Size ()
shape
  where
    arg_als :: Aliasing
arg_als = forall as shape. Monoid as => TypeBase shape as -> as
aliases forall a b. (a -> b) -> a -> b
$ forall as shape.
Monoid as =>
TypeBase shape as -> Diet -> TypeBase shape as
maskAliases PatType
arg Diet
d
returnType Aliasing
appres (Scalar (Record Map Name PatType
fs)) Diet
d PatType
arg =
  forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as. Map Name (TypeBase dim as) -> ScalarTypeBase dim as
Record forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\PatType
et -> Aliasing -> PatType -> Diet -> PatType -> PatType
returnType Aliasing
appres PatType
et Diet
d PatType
arg) Map Name PatType
fs
returnType Aliasing
_ (Scalar (Prim PrimType
t)) Diet
_ PatType
_ =
  forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as. PrimType -> ScalarTypeBase dim as
Prim PrimType
t
returnType Aliasing
_ (Scalar (TypeVar Aliasing
_ Uniqueness
Unique QualName VName
t [TypeArg Size]
targs)) Diet
_ PatType
_ =
  forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as.
as
-> Uniqueness
-> QualName VName
-> [TypeArg dim]
-> ScalarTypeBase dim as
TypeVar forall a. Monoid a => a
mempty Uniqueness
Nonunique QualName VName
t [TypeArg Size]
targs -- Intentional!
returnType Aliasing
appres (Scalar (TypeVar Aliasing
als Uniqueness
Nonunique QualName VName
t [TypeArg Size]
targs)) Diet
d PatType
arg =
  forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as.
as
-> Uniqueness
-> QualName VName
-> [TypeArg dim]
-> ScalarTypeBase dim as
TypeVar (Aliasing
appres forall a. Semigroup a => a -> a -> a
<> Aliasing
als forall a. Semigroup a => a -> a -> a
<> Aliasing
arg_als) Uniqueness
Unique QualName VName
t [TypeArg Size]
targs
  where
    arg_als :: Aliasing
arg_als = forall as shape. Monoid as => TypeBase shape as -> as
aliases forall a b. (a -> b) -> a -> b
$ forall as shape.
Monoid as =>
TypeBase shape as -> Diet -> TypeBase shape as
maskAliases PatType
arg Diet
d
returnType Aliasing
_ (Scalar (Arrow Aliasing
old_als PName
v TypeBase Size ()
t1 (RetType [VName]
dims PatType
t2))) Diet
d PatType
arg =
  forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as.
as
-> PName
-> TypeBase dim ()
-> RetTypeBase dim as
-> ScalarTypeBase dim as
Arrow Aliasing
als PName
v (TypeBase Size ()
t1 forall dim asf ast. TypeBase dim asf -> ast -> TypeBase dim ast
`setAliases` forall a. Monoid a => a
mempty) forall a b. (a -> b) -> a -> b
$ forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
dims forall a b. (a -> b) -> a -> b
$ PatType
t2 forall dim asf ast. TypeBase dim asf -> ast -> TypeBase dim ast
`setAliases` Aliasing
als
  where
    -- Make sure to propagate the aliases of an existing closure.
    als :: Aliasing
als = Aliasing
old_als forall a. Semigroup a => a -> a -> a
<> forall as shape. Monoid as => TypeBase shape as -> as
aliases (forall as shape.
Monoid as =>
TypeBase shape as -> Diet -> TypeBase shape as
maskAliases PatType
arg Diet
d)
returnType Aliasing
appres (Scalar (Sum Map Name [PatType]
cs)) Diet
d PatType
arg =
  forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as. Map Name [TypeBase dim as] -> ScalarTypeBase dim as
Sum forall a b. (a -> b) -> a -> b
$ (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) (\PatType
et -> Aliasing -> PatType -> Diet -> PatType -> PatType
returnType Aliasing
appres PatType
et Diet
d PatType
arg) Map Name [PatType]
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 :: forall as shape.
Monoid as =>
TypeBase shape as -> Diet -> TypeBase shape as
maskAliases TypeBase shape as
t Diet
Consume = TypeBase shape as
t forall dim asf ast. TypeBase dim asf -> ast -> TypeBase dim ast
`setAliases` forall a. Monoid a => a
mempty
maskAliases TypeBase shape as
t Diet
Observe = TypeBase shape as
t
maskAliases (Scalar (Record Map Name (TypeBase shape as)
ets)) (RecordDiet Map Name Diet
ds) =
  forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as. Map Name (TypeBase dim as) -> ScalarTypeBase dim as
Record forall a b. (a -> b) -> a -> b
$ forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith forall as shape.
Monoid as =>
TypeBase shape as -> Diet -> TypeBase shape as
maskAliases Map Name (TypeBase shape as)
ets Map Name Diet
ds
maskAliases (Scalar (Sum Map Name [TypeBase shape as]
ets)) (SumDiet Map Name [Diet]
ds) =
  forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as. Map Name [TypeBase dim as] -> ScalarTypeBase dim as
Sum forall a b. (a -> b) -> a -> b
$ forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall as shape.
Monoid as =>
TypeBase shape as -> Diet -> TypeBase shape as
maskAliases) Map Name [TypeBase shape as]
ets Map Name [Diet]
ds
maskAliases TypeBase shape as
t FuncDiet {} = TypeBase shape as
t
maskAliases TypeBase shape as
_ Diet
_ = forall a. HasCallStack => String -> a
error String
"Invalid arguments passed to maskAliases."

consumeArg :: SrcLoc -> PatType -> Diet -> TermTypeM [Occurrence]
consumeArg :: SrcLoc -> PatType -> Diet -> TermTypeM Occurrences
consumeArg SrcLoc
loc (Scalar (Record Map Name PatType
ets)) (RecordDiet Map Name Diet
ds) =
  forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [a]
M.elems forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a b. (a -> b) -> a -> b
$ SrcLoc -> PatType -> Diet -> TermTypeM Occurrences
consumeArg SrcLoc
loc) (forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith (,) Map Name PatType
ets Map Name Diet
ds)
consumeArg SrcLoc
loc (Scalar (Sum Map Name [PatType]
ets)) (SumDiet Map Name [Diet]
ds) =
  forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a b. (a -> b) -> a -> b
$ SrcLoc -> PatType -> Diet -> TermTypeM Occurrences
consumeArg SrcLoc
loc) (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [a]
M.elems forall a b. (a -> b) -> a -> b
$ forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith forall a b. [a] -> [b] -> [(a, b)]
zip Map Name [PatType]
ets Map Name [Diet]
ds)
consumeArg SrcLoc
loc (Scalar (Arrow Aliasing
_ PName
_ TypeBase Size ()
t1 RetTypeBase Size Aliasing
_)) (FuncDiet Diet
d Diet
_)
  | Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall {dim}. TypeBase dim () -> Diet -> Bool
contravariantArg TypeBase Size ()
t1 Diet
d =
      forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc forall a. Monoid a => a
mempty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ann. Doc ann -> Doc ann -> Doc ann
withIndexLink Doc ()
"consuming-argument" forall a b. (a -> b) -> a -> b
$
        Doc ()
"Non-consuming higher-order parameter passed consuming argument."
  where
    contravariantArg :: TypeBase dim () -> Diet -> Bool
contravariantArg (Array ()
_ Uniqueness
Unique Shape dim
_ ScalarTypeBase dim ()
_) Diet
Observe =
      Bool
False
    contravariantArg (Scalar (TypeVar ()
_ Uniqueness
Unique QualName VName
_ [TypeArg dim]
_)) Diet
Observe =
      Bool
False
    contravariantArg (Scalar (Record Map Name (TypeBase dim ())
ets)) (RecordDiet Map Name Diet
ds) =
      forall (t :: * -> *). Foldable t => t Bool -> Bool
and (forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith TypeBase dim () -> Diet -> Bool
contravariantArg Map Name (TypeBase dim ())
ets Map Name Diet
ds)
    contravariantArg (Scalar (Arrow ()
_ PName
_ TypeBase dim ()
tp (RetType [VName]
_ TypeBase dim ()
tr))) (FuncDiet Diet
dp Diet
dr) =
      TypeBase dim () -> Diet -> Bool
contravariantArg TypeBase dim ()
tp Diet
dp Bool -> Bool -> Bool
&& TypeBase dim () -> Diet -> Bool
contravariantArg TypeBase dim ()
tr Diet
dr
    contravariantArg TypeBase dim ()
_ Diet
_ =
      Bool
True
consumeArg SrcLoc
loc PatType
at Diet
Consume = forall (f :: * -> *) a. Applicative f => a -> f a
pure [Aliasing -> SrcLoc -> Occurrence
consumption (forall as shape. Monoid as => TypeBase shape as -> as
aliases PatType
at) SrcLoc
loc]
consumeArg SrcLoc
loc PatType
at Diet
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure [Aliasing -> SrcLoc -> Occurrence
observation (forall as shape. Monoid as => TypeBase shape as -> as
aliases PatType
at) SrcLoc
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 :: ExpBase NoInfo Name -> TypeM ([TypeParamBase VName], Exp)
checkOneExp ExpBase NoInfo Name
e = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. TermTypeM a -> TypeM (a, Occurrences)
runTermTypeM forall a b. (a -> b) -> a -> b
$ do
  Exp
e' <- ExpBase NoInfo Name -> TermTypeM Exp
checkExp ExpBase NoInfo Name
e
  let t :: TypeBase Size ()
t = forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct forall a b. (a -> b) -> a -> b
$ Exp -> PatType
typeOf Exp
e'
  ([TypeParamBase VName]
tparams, [PatBase Info VName]
_, StructRetType
_) <-
    Name
-> SrcLoc
-> [TypeParamBase VName]
-> [PatBase Info VName]
-> TypeBase Size ()
-> TermTypeM
     ([TypeParamBase VName], [PatBase Info VName], StructRetType)
letGeneralise (String -> Name
nameFromString String
"<exp>") (forall a. Located a => a -> SrcLoc
srclocOf ExpBase NoInfo Name
e) [] [] TypeBase Size ()
t
  Set VName -> TermTypeM ()
fixOverloadedTypes forall a b. (a -> b) -> a -> b
$ forall as dim. Monoid as => TypeBase dim as -> Set VName
typeVars TypeBase Size ()
t
  Exp
e'' <- forall e. ASTMappable e => e -> TermTypeM e
updateTypes Exp
e'
  Exp -> TermTypeM ()
localChecks Exp
e''
  Exp -> TermTypeM ()
causalityCheck Exp
e''
  forall (f :: * -> *) a. Applicative f => a -> f a
pure ([TypeParamBase VName]
tparams, Exp
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 :: Exp -> TermTypeM ()
causalityCheck Exp
binding_body = do
  Constraints
constraints <- forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints

  let checkCausality :: Doc ()
-> Set VName
-> TypeBase Size as
-> a
-> Maybe (t (Either TypeError) a)
checkCausality Doc ()
what Set VName
known TypeBase Size as
t a
loc
        | (VName
d, SrcLoc
dloc) : [(VName, SrcLoc)]
_ <-
            forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (forall {a} {a}.
Ord a =>
Map a (a, Constraint) -> Set a -> a -> Maybe (a, SrcLoc)
unknown Constraints
constraints Set VName
known) forall a b. (a -> b) -> a -> b
$
              forall a. Set a -> [a]
S.toList forall a b. (a -> b) -> a -> b
$
                forall als. TypeBase Size als -> Set VName
freeInType forall a b. (a -> b) -> a -> b
$
                  forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct TypeBase Size as
t =
            forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall {v} {a} {b} {b}.
(IsName v, Pretty a, Located b) =>
Doc () -> Loc -> v -> b -> a -> Either TypeError b
causality Doc ()
what (forall a. Located a => a -> Loc
locOf a
loc) VName
d SrcLoc
dloc TypeBase Size as
t
        | Bool
otherwise = forall a. Maybe a
Nothing

      checkParamCausality :: Set VName -> PatBase Info VName -> Maybe (t (Either TypeError) a)
checkParamCausality Set VName
known PatBase Info VName
p =
        forall {t :: (* -> *) -> * -> *} {a} {as} {a}.
(MonadTrans t, Located a) =>
Doc ()
-> Set VName
-> TypeBase Size as
-> a
-> Maybe (t (Either TypeError) a)
checkCausality (forall a ann. Pretty a => a -> Doc ann
pretty PatBase Info VName
p) Set VName
known (PatBase Info VName -> PatType
patternType PatBase Info VName
p) (forall a. Located a => a -> Loc
locOf PatBase Info VName
p)

      onExp ::
        S.Set VName ->
        Exp ->
        StateT (S.Set VName) (Either TypeError) Exp

      onExp :: Set VName -> Exp -> StateT (Set VName) (Either TypeError) Exp
onExp Set VName
known (Var QualName VName
v (Info PatType
t) SrcLoc
loc)
        | Just StateT (Set VName) (Either TypeError) Exp
bad <- forall {t :: (* -> *) -> * -> *} {a} {as} {a}.
(MonadTrans t, Located a) =>
Doc ()
-> Set VName
-> TypeBase Size as
-> a
-> Maybe (t (Either TypeError) a)
checkCausality (forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty QualName VName
v)) Set VName
known PatType
t SrcLoc
loc =
            StateT (Set VName) (Either TypeError) Exp
bad
      onExp Set VName
known (ProjectSection [Name]
_ (Info PatType
t) SrcLoc
loc)
        | Just StateT (Set VName) (Either TypeError) Exp
bad <- forall {t :: (* -> *) -> * -> *} {a} {as} {a}.
(MonadTrans t, Located a) =>
Doc ()
-> Set VName
-> TypeBase Size as
-> a
-> Maybe (t (Either TypeError) a)
checkCausality Doc ()
"projection section" Set VName
known PatType
t SrcLoc
loc =
            StateT (Set VName) (Either TypeError) Exp
bad
      onExp Set VName
known (IndexSection Slice
_ (Info PatType
t) SrcLoc
loc)
        | Just StateT (Set VName) (Either TypeError) Exp
bad <- forall {t :: (* -> *) -> * -> *} {a} {as} {a}.
(MonadTrans t, Located a) =>
Doc ()
-> Set VName
-> TypeBase Size as
-> a
-> Maybe (t (Either TypeError) a)
checkCausality Doc ()
"projection section" Set VName
known PatType
t SrcLoc
loc =
            StateT (Set VName) (Either TypeError) Exp
bad
      onExp Set VName
known (OpSectionRight QualName VName
_ (Info PatType
t) Exp
_ (Info (PName, TypeBase Size ()),
 Info (PName, TypeBase Size (), Maybe VName))
_ Info (RetTypeBase Size Aliasing)
_ SrcLoc
loc)
        | Just StateT (Set VName) (Either TypeError) Exp
bad <- forall {t :: (* -> *) -> * -> *} {a} {as} {a}.
(MonadTrans t, Located a) =>
Doc ()
-> Set VName
-> TypeBase Size as
-> a
-> Maybe (t (Either TypeError) a)
checkCausality Doc ()
"operator section" Set VName
known PatType
t SrcLoc
loc =
            StateT (Set VName) (Either TypeError) Exp
bad
      onExp Set VName
known (OpSectionLeft QualName VName
_ (Info PatType
t) Exp
_ (Info (PName, TypeBase Size (), Maybe VName),
 Info (PName, TypeBase Size ()))
_ (Info (RetTypeBase Size Aliasing), Info [VName])
_ SrcLoc
loc)
        | Just StateT (Set VName) (Either TypeError) Exp
bad <- forall {t :: (* -> *) -> * -> *} {a} {as} {a}.
(MonadTrans t, Located a) =>
Doc ()
-> Set VName
-> TypeBase Size as
-> a
-> Maybe (t (Either TypeError) a)
checkCausality Doc ()
"operator section" Set VName
known PatType
t SrcLoc
loc =
            StateT (Set VName) (Either TypeError) Exp
bad
      onExp Set VName
known (ArrayLit [] (Info PatType
t) SrcLoc
loc)
        | Just StateT (Set VName) (Either TypeError) Exp
bad <- forall {t :: (* -> *) -> * -> *} {a} {as} {a}.
(MonadTrans t, Located a) =>
Doc ()
-> Set VName
-> TypeBase Size as
-> a
-> Maybe (t (Either TypeError) a)
checkCausality Doc ()
"empty array" Set VName
known PatType
t SrcLoc
loc =
            StateT (Set VName) (Either TypeError) Exp
bad
      onExp Set VName
known (Hole (Info PatType
t) SrcLoc
loc)
        | Just StateT (Set VName) (Either TypeError) Exp
bad <- forall {t :: (* -> *) -> * -> *} {a} {as} {a}.
(MonadTrans t, Located a) =>
Doc ()
-> Set VName
-> TypeBase Size as
-> a
-> Maybe (t (Either TypeError) a)
checkCausality Doc ()
"hole" Set VName
known PatType
t SrcLoc
loc =
            StateT (Set VName) (Either TypeError) Exp
bad
      onExp Set VName
known (Lambda [PatBase Info VName]
params Exp
_ Maybe (TypeExp VName)
_ Info (Aliasing, StructRetType)
_ SrcLoc
_)
        | StateT (Set VName) (Either TypeError) Exp
bad : [StateT (Set VName) (Either TypeError) Exp]
_ <- forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (forall {t :: (* -> *) -> * -> *} {a}.
MonadTrans t =>
Set VName -> PatBase Info VName -> Maybe (t (Either TypeError) a)
checkParamCausality Set VName
known) [PatBase Info VName]
params =
            StateT (Set VName) (Either TypeError) Exp
bad
      onExp Set VName
known e :: Exp
e@(AppExp (LetPat [SizeBinder VName]
_ PatBase Info VName
_ Exp
bindee_e Exp
body_e SrcLoc
_) (Info AppRes
res)) = do
        Set VName
-> Exp
-> Exp
-> [VName]
-> StateT (Set VName) (Either TypeError) ()
sequencePoint Set VName
known Exp
bindee_e Exp
body_e forall a b. (a -> b) -> a -> b
$ AppRes -> [VName]
appResExt AppRes
res
        forall (f :: * -> *) a. Applicative f => a -> f a
pure Exp
e
      onExp Set VName
known e :: Exp
e@(AppExp (Apply Exp
f Exp
arg (Info (Diet
_, Maybe VName
p)) SrcLoc
_) (Info AppRes
res)) = do
        Set VName
-> Exp
-> Exp
-> [VName]
-> StateT (Set VName) (Either TypeError) ()
sequencePoint Set VName
known Exp
arg Exp
f forall a b. (a -> b) -> a -> b
$ forall a. Maybe a -> [a]
maybeToList Maybe VName
p forall a. [a] -> [a] -> [a]
++ AppRes -> [VName]
appResExt AppRes
res
        forall (f :: * -> *) a. Applicative f => a -> f a
pure Exp
e
      onExp
        Set VName
known
        e :: Exp
e@(AppExp (BinOp (QualName VName
f, SrcLoc
floc) Info PatType
ft (Exp
x, Info (TypeBase Size ()
_, Maybe VName
xp)) (Exp
y, Info (TypeBase Size ()
_, Maybe VName
yp)) SrcLoc
_) (Info AppRes
res)) = do
          Set VName
args_known <-
            forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$
              forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT (Set VName
-> Exp
-> Exp
-> [VName]
-> StateT (Set VName) (Either TypeError) ()
sequencePoint Set VName
known Exp
x Exp
y forall a b. (a -> b) -> a -> b
$ forall a. [Maybe a] -> [a]
catMaybes [Maybe VName
xp, Maybe VName
yp]) forall a. Monoid a => a
mempty
          forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ Set VName -> Exp -> StateT (Set VName) (Either TypeError) Exp
onExp (Set VName
args_known forall a. Semigroup a => a -> a -> a
<> Set VName
known) (forall (f :: * -> *) vn.
QualName vn -> f PatType -> SrcLoc -> ExpBase f vn
Var QualName VName
f Info PatType
ft SrcLoc
floc)
          forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Set VName
args_known forall a. Semigroup a => a -> a -> a
<> forall a. Ord a => [a] -> Set a
S.fromList (AppRes -> [VName]
appResExt AppRes
res)) <>)
          forall (f :: * -> *) a. Applicative f => a -> f a
pure Exp
e
      onExp Set VName
known e :: Exp
e@(AppExp AppExpBase Info VName
e' (Info AppRes
res)) = do
        forall {a}.
ASTMappable a =>
Set VName -> a -> StateT (Set VName) (Either TypeError) ()
recurse Set VName
known AppExpBase Info VName
e'
        forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (forall a. Semigroup a => a -> a -> a
<> forall a. Ord a => [a] -> Set a
S.fromList (AppRes -> [VName]
appResExt AppRes
res))
        forall (f :: * -> *) a. Applicative f => a -> f a
pure Exp
e
      onExp Set VName
known Exp
e = do
        forall {a}.
ASTMappable a =>
Set VName -> a -> StateT (Set VName) (Either TypeError) ()
recurse Set VName
known Exp
e
        forall (f :: * -> *) a. Applicative f => a -> f a
pure Exp
e

      recurse :: Set VName -> a -> StateT (Set VName) (Either TypeError) ()
recurse Set VName
known = forall (f :: * -> *) a. Functor f => f a -> f ()
void forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall x (m :: * -> *).
(ASTMappable x, Monad m) =>
ASTMapper m -> x -> m x
astMap ASTMapper (StateT (Set VName) (Either TypeError))
mapper
        where
          mapper :: ASTMapper (StateT (Set VName) (Either TypeError))
mapper = forall (m :: * -> *). Monad m => ASTMapper m
identityMapper {mapOnExp :: Exp -> StateT (Set VName) (Either TypeError) Exp
mapOnExp = Set VName -> Exp -> StateT (Set VName) (Either TypeError) Exp
onExp Set VName
known}

      sequencePoint :: Set VName
-> Exp
-> Exp
-> [VName]
-> StateT (Set VName) (Either TypeError) ()
sequencePoint Set VName
known Exp
x Exp
y [VName]
ext = do
        Set VName
new_known <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT (Set VName -> Exp -> StateT (Set VName) (Either TypeError) Exp
onExp Set VName
known Exp
x) forall a. Monoid a => a
mempty
        forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ Set VName -> Exp -> StateT (Set VName) (Either TypeError) Exp
onExp (Set VName
new_known forall a. Semigroup a => a -> a -> a
<> Set VName
known) Exp
y
        forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Set VName
new_known forall a. Semigroup a => a -> a -> a
<> forall a. Ord a => [a] -> Set a
S.fromList [VName]
ext) <>)

  forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (Set VName -> Exp -> StateT (Set VName) (Either TypeError) Exp
onExp forall a. Monoid a => a
mempty Exp
binding_body) forall a. Monoid a => a
mempty
  where
    unknown :: Map a (a, Constraint) -> Set a -> a -> Maybe (a, SrcLoc)
unknown Map a (a, Constraint)
constraints Set a
known a
v = do
      forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ a
v forall a. Ord a => a -> Set a -> Bool
`S.notMember` Set a
known
      SrcLoc
loc <- forall {k} {a}. Ord k => Map k (a, Constraint) -> k -> Maybe SrcLoc
unknowable Map a (a, Constraint)
constraints a
v
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
v, SrcLoc
loc)

    unknowable :: Map k (a, Constraint) -> k -> Maybe SrcLoc
unknowable Map k (a, Constraint)
constraints k
v =
      case forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup k
v Map k (a, Constraint)
constraints of
        Just (UnknowableSize SrcLoc
loc RigidSource
_) -> forall a. a -> Maybe a
Just SrcLoc
loc
        Maybe Constraint
_ -> forall a. Maybe a
Nothing

    causality :: Doc () -> Loc -> v -> b -> a -> Either TypeError b
causality Doc ()
what Loc
loc v
d b
dloc a
t =
      forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. Loc -> Notes -> Doc () -> TypeError
TypeError Loc
loc forall a. Monoid a => a
mempty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ann. Doc ann -> Doc ann -> Doc ann
withIndexLink Doc ()
"causality-check" forall a b. (a -> b) -> a -> b
$
        Doc ()
"Causality check: size"
          forall ann. Doc ann -> Doc ann -> Doc ann
</> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName v
d)
          forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"needed for type of"
          forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
what forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann
colon
          forall ann. Doc ann -> Doc ann -> Doc ann
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a ann. Pretty a => a -> Doc ann
pretty a
t)
          forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"But"
          forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName v
d)
          forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"is computed at"
          forall ann. Doc ann -> Doc ann -> Doc ann
</> forall a ann. Pretty a => a -> Doc ann
pretty (forall a b. (Located a, Located b) => a -> b -> String
locStrRel Loc
loc b
dloc) forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
          forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
""
          forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"Hint:"
          forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
align
            ( forall a. Text -> Doc a
textwrap Text
"Bind the expression producing"
                forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName v
d)
                forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"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 :: Exp -> TermTypeM ()
localChecks = forall (f :: * -> *) a. Functor f => f a -> f ()
void forall b c a. (b -> c) -> (a -> b) -> a -> c
. Exp -> TermTypeM Exp
check
  where
    check :: Exp -> TermTypeM Exp
check e :: Exp
e@(AppExp (Match Exp
_ NonEmpty (CaseBase Info VName)
cs SrcLoc
loc) Info AppRes
_) = do
      let ps :: NonEmpty (PatBase Info VName)
ps = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(CasePat PatBase Info VName
p Exp
_ SrcLoc
_) -> PatBase Info VName
p) NonEmpty (CaseBase Info VName)
cs
      case [PatBase Info VName] -> [Match]
unmatched forall a b. (a -> b) -> a -> b
$ forall a. NonEmpty a -> [a]
NE.toList NonEmpty (PatBase Info VName)
ps of
        [] -> Exp -> TermTypeM Exp
recurse Exp
e
        [Match]
ps' ->
          forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc forall a. Monoid a => a
mempty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ann. Doc ann -> Doc ann -> Doc ann
withIndexLink Doc ()
"unmatched-cases" forall a b. (a -> b) -> a -> b
$
            Doc ()
"Unmatched cases in match expression:"
              forall ann. Doc ann -> Doc ann -> Doc ann
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a. [Doc a] -> Doc a
stack (forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [Match]
ps'))
    check e :: Exp
e@(IntLit Integer
x Info PatType
ty SrcLoc
loc) =
      Exp
e forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ case Info PatType
ty of
        Info (Scalar (Prim PrimType
t)) -> forall {f :: * -> *} {loc} {a} {a}.
(MonadTypeChecker f, Located loc, Pretty a, Pretty a) =>
Bool -> a -> a -> loc -> f ()
errorBounds (forall {a}. Integral a => a -> PrimType -> Bool
inBoundsI Integer
x PrimType
t) Integer
x PrimType
t SrcLoc
loc
        Info PatType
_ -> forall a. HasCallStack => String -> a
error String
"Inferred type of int literal is not a number"
    check e :: Exp
e@(FloatLit Double
x Info PatType
ty SrcLoc
loc) =
      Exp
e forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ case Info PatType
ty of
        Info (Scalar (Prim (FloatType FloatType
t))) -> forall {f :: * -> *} {loc} {a} {a}.
(MonadTypeChecker f, Located loc, Pretty a, Pretty a) =>
Bool -> a -> a -> loc -> f ()
errorBounds (forall {a}. RealFloat a => a -> FloatType -> Bool
inBoundsF Double
x FloatType
t) Double
x FloatType
t SrcLoc
loc
        Info PatType
_ -> forall a. HasCallStack => String -> a
error String
"Inferred type of float literal is not a float"
    check e :: Exp
e@(Negate (IntLit Integer
x Info PatType
ty SrcLoc
loc1) SrcLoc
loc2) =
      Exp
e forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ case Info PatType
ty of
        Info (Scalar (Prim PrimType
t)) -> forall {f :: * -> *} {loc} {a} {a}.
(MonadTypeChecker f, Located loc, Pretty a, Pretty a) =>
Bool -> a -> a -> loc -> f ()
errorBounds (forall {a}. Integral a => a -> PrimType -> Bool
inBoundsI (-Integer
x) PrimType
t) (-Integer
x) PrimType
t (SrcLoc
loc1 forall a. Semigroup a => a -> a -> a
<> SrcLoc
loc2)
        Info PatType
_ -> forall a. HasCallStack => String -> a
error String
"Inferred type of int literal is not a number"
    check e :: Exp
e@(AppExp (BinOp (QualName [] VName
v, SrcLoc
_) Info PatType
_ (Exp
_, Info (Array {}, Maybe VName
_)) (Exp, Info (TypeBase Size (), Maybe VName))
_ SrcLoc
loc) Info AppRes
_)
      | VName -> Name
baseName VName
v forall a. Eq a => a -> a -> Bool
== Name
"==",
        VName -> Int
baseTag VName
v forall a. Ord a => a -> a -> Bool
<= Int
maxIntrinsicTag = do
          forall (m :: * -> *) loc.
(MonadTypeChecker m, Located loc) =>
loc -> Doc () -> m ()
warn SrcLoc
loc forall a b. (a -> b) -> a -> b
$
            forall a. Text -> Doc a
textwrap
              Text
"Comparing arrays with \"==\" is deprecated and will stop working in a future revision of the language."
          Exp -> TermTypeM Exp
recurse Exp
e
    check Exp
e = Exp -> TermTypeM Exp
recurse Exp
e
    recurse :: Exp -> TermTypeM Exp
recurse = forall x (m :: * -> *).
(ASTMappable x, Monad m) =>
ASTMapper m -> x -> m x
astMap forall (m :: * -> *). Monad m => ASTMapper m
identityMapper {mapOnExp :: Exp -> TermTypeM Exp
mapOnExp = Exp -> TermTypeM Exp
check}

    bitWidth :: IntType -> Int
bitWidth IntType
ty = Int
8 forall a. Num a => a -> a -> a
* forall a. Num a => IntType -> a
intByteSize IntType
ty :: Int

    inBoundsI :: a -> PrimType -> Bool
inBoundsI a
x (Signed IntType
t) = a
x forall a. Ord a => a -> a -> Bool
>= -a
2 forall a b. (Num a, Integral b) => a -> b -> a
^ (IntType -> Int
bitWidth IntType
t forall a. Num a => a -> a -> a
- Int
1) Bool -> Bool -> Bool
&& a
x forall a. Ord a => a -> a -> Bool
< a
2 forall a b. (Num a, Integral b) => a -> b -> a
^ (IntType -> Int
bitWidth IntType
t forall a. Num a => a -> a -> a
- Int
1)
    inBoundsI a
x (Unsigned IntType
t) = a
x forall a. Ord a => a -> a -> Bool
>= a
0 Bool -> Bool -> Bool
&& a
x forall a. Ord a => a -> a -> Bool
< a
2 forall a b. (Num a, Integral b) => a -> b -> a
^ IntType -> Int
bitWidth IntType
t
    inBoundsI a
x (FloatType FloatType
Float16) = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. RealFloat a => a -> Bool
isInfinite (forall a b. (Integral a, Num b) => a -> b
fromIntegral a
x :: Half)
    inBoundsI a
x (FloatType FloatType
Float32) = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. RealFloat a => a -> Bool
isInfinite (forall a b. (Integral a, Num b) => a -> b
fromIntegral a
x :: Float)
    inBoundsI a
x (FloatType FloatType
Float64) = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. RealFloat a => a -> Bool
isInfinite (forall a b. (Integral a, Num b) => a -> b
fromIntegral a
x :: Double)
    inBoundsI a
_ PrimType
Bool = forall a. HasCallStack => String -> a
error String
"Inferred type of int literal is not a number"
    inBoundsF :: a -> FloatType -> Bool
inBoundsF a
x FloatType
Float16 = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. RealFloat a => a -> Bool
isInfinite (forall a b. (Real a, Fractional b) => a -> b
realToFrac a
x :: Float)
    inBoundsF a
x FloatType
Float32 = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. RealFloat a => a -> Bool
isInfinite (forall a b. (Real a, Fractional b) => a -> b
realToFrac a
x :: Float)
    inBoundsF a
x FloatType
Float64 = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. RealFloat a => a -> Bool
isInfinite a
x

    errorBounds :: Bool -> a -> a -> loc -> f ()
errorBounds Bool
inBounds a
x a
ty loc
loc =
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
inBounds forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError loc
loc forall a. Monoid a => a
mempty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ann. Doc ann -> Doc ann -> Doc ann
withIndexLink Doc ()
"literal-out-of-bounds" forall a b. (a -> b) -> a -> b
$
          Doc ()
"Literal "
            forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty a
x
            forall a. Semigroup a => a -> a -> a
<> Doc ()
" out of bounds for inferred type "
            forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty a
ty
            forall a. Semigroup a => a -> a -> a
<> Doc ()
"."

-- | 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 :: (Name, Maybe UncheckedTypeExp, [TypeParamBase Name],
 [PatBase NoInfo Name], ExpBase NoInfo Name, SrcLoc)
-> TypeM
     (VName, [TypeParamBase VName], [PatBase Info VName],
      Maybe (TypeExp VName), StructRetType, Exp)
checkFunDef (Name
fname, Maybe UncheckedTypeExp
maybe_retdecl, [TypeParamBase Name]
tparams, [PatBase NoInfo Name]
params, ExpBase NoInfo Name
body, SrcLoc
loc) =
  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. TermTypeM a -> TypeM (a, Occurrences)
runTermTypeM forall a b. (a -> b) -> a -> b
$ do
    ([TypeParamBase VName]
tparams', [PatBase Info VName]
params', Maybe (TypeExp VName)
maybe_retdecl', RetType [VName]
dims TypeBase Size ()
rettype', Exp
body') <-
      (Name, Maybe UncheckedTypeExp, [TypeParamBase Name],
 [PatBase NoInfo Name], ExpBase NoInfo Name, SrcLoc)
-> TermTypeM
     ([TypeParamBase VName], [PatBase Info VName],
      Maybe (TypeExp VName), StructRetType, Exp)
checkBinding (Name
fname, Maybe UncheckedTypeExp
maybe_retdecl, [TypeParamBase Name]
tparams, [PatBase NoInfo Name]
params, ExpBase NoInfo Name
body, SrcLoc
loc)

    -- Since this is a top-level function, we also resolve overloaded
    -- types, using either defaults or complaining about ambiguities.
    Set VName -> TermTypeM ()
fixOverloadedTypes forall a b. (a -> b) -> a -> b
$
      forall as dim. Monoid as => TypeBase dim as -> Set VName
typeVars TypeBase Size ()
rettype' forall a. Semigroup a => a -> a -> a
<> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (forall as dim. Monoid as => TypeBase dim as -> Set VName
typeVars forall b c a. (b -> c) -> (a -> b) -> a -> c
. PatBase Info VName -> PatType
patternType) [PatBase Info VName]
params'

    -- Then replace all inferred types in the body and parameters.
    Exp
body'' <- forall e. ASTMappable e => e -> TermTypeM e
updateTypes Exp
body'
    [PatBase Info VName]
params'' <- forall e. ASTMappable e => e -> TermTypeM e
updateTypes [PatBase Info VName]
params'
    Maybe (TypeExp VName)
maybe_retdecl'' <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall e. ASTMappable e => e -> TermTypeM e
updateTypes Maybe (TypeExp VName)
maybe_retdecl'
    TypeBase Size ()
rettype'' <- forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully TypeBase Size ()
rettype'

    -- Check if the function body can actually be evaluated.
    Exp -> TermTypeM ()
causalityCheck Exp
body''

    -- Check for various problems.
    Exp -> TermTypeM ()
localChecks Exp
body''

    forall (m :: * -> *) a.
MonadTypeChecker m =>
[(Namespace, Name)] -> m a -> m a
bindSpaced [(Namespace
Term, Name
fname)] forall a b. (a -> b) -> a -> b
$ do
      VName
fname' <- forall (m :: * -> *).
MonadTypeChecker m =>
Namespace -> Name -> SrcLoc -> m VName
checkName Namespace
Term Name
fname SrcLoc
loc
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Name -> String
nameToString Name
fname forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
doNotShadow) forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc forall a. Monoid a => a
mempty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ann. Doc ann -> Doc ann -> Doc ann
withIndexLink Doc ()
"may-not-be-redefined" forall a b. (a -> b) -> a -> b
$
          Doc ()
"The" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall v a. IsName v => v -> Doc a
prettyName Name
fname forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"operator may not be redefined."

      forall (f :: * -> *) a. Applicative f => a -> f a
pure (VName
fname', [TypeParamBase VName]
tparams', [PatBase Info VName]
params'', Maybe (TypeExp VName)
maybe_retdecl'', forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
dims TypeBase Size ()
rettype'', Exp
body'')

-- | This is "fixing" as in "setting them", not "correcting them".  We
-- only make very conservative fixing.
fixOverloadedTypes :: Names -> TermTypeM ()
fixOverloadedTypes :: Set VName -> TermTypeM ()
fixOverloadedTypes Set VName
tyvars_at_toplevel =
  forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall {m :: * -> *}.
(MonadUnify m, MonadTypeChecker m) =>
(VName, Constraint) -> m ()
fixOverloaded forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [(k, a)]
M.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b k. (a -> b) -> Map k a -> Map k b
M.map forall a b. (a, b) -> b
snd
  where
    fixOverloaded :: (VName, Constraint) -> m ()
fixOverloaded (VName
v, Overloaded [PrimType]
ots Usage
usage)
      | IntType -> PrimType
Signed IntType
Int32 forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [PrimType]
ots = do
          forall (m :: * -> *).
MonadUnify m =>
Usage -> TypeBase Size () -> TypeBase Size () -> m ()
unify Usage
usage (forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar (forall dim as.
as
-> Uniqueness
-> QualName VName
-> [TypeArg dim]
-> ScalarTypeBase dim as
TypeVar () Uniqueness
Nonunique (forall v. v -> QualName v
qualName VName
v) [])) forall a b. (a -> b) -> a -> b
$
            forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$
              forall dim as. PrimType -> ScalarTypeBase dim as
Prim forall a b. (a -> b) -> a -> b
$
                IntType -> PrimType
Signed IntType
Int32
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (VName
v forall a. Ord a => a -> Set a -> Bool
`S.member` Set VName
tyvars_at_toplevel) forall a b. (a -> b) -> a -> b
$
            forall (m :: * -> *) loc.
(MonadTypeChecker m, Located loc) =>
loc -> Doc () -> m ()
warn Usage
usage Doc ()
"Defaulting ambiguous type to i32."
      | FloatType -> PrimType
FloatType FloatType
Float64 forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [PrimType]
ots = do
          forall (m :: * -> *).
MonadUnify m =>
Usage -> TypeBase Size () -> TypeBase Size () -> m ()
unify Usage
usage (forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar (forall dim as.
as
-> Uniqueness
-> QualName VName
-> [TypeArg dim]
-> ScalarTypeBase dim as
TypeVar () Uniqueness
Nonunique (forall v. v -> QualName v
qualName VName
v) [])) forall a b. (a -> b) -> a -> b
$
            forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$
              forall dim as. PrimType -> ScalarTypeBase dim as
Prim forall a b. (a -> b) -> a -> b
$
                FloatType -> PrimType
FloatType FloatType
Float64
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (VName
v forall a. Ord a => a -> Set a -> Bool
`S.member` Set VName
tyvars_at_toplevel) forall a b. (a -> b) -> a -> b
$
            forall (m :: * -> *) loc.
(MonadTypeChecker m, Located loc) =>
loc -> Doc () -> m ()
warn Usage
usage Doc ()
"Defaulting ambiguous type to f64."
      | Bool
otherwise =
          forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError Usage
usage forall a. Monoid a => a
mempty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ann. Doc ann -> Doc ann -> Doc ann
withIndexLink Doc ()
"ambiguous-type" forall a b. (a -> b) -> a -> b
$
            Doc ()
"Type is ambiguous (could be one of"
              forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a. [Doc a] -> Doc a
commasep (forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [PrimType]
ots) forall a. Semigroup a => a -> a -> a
<> Doc ()
")."
              forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"Add a type annotation to disambiguate the type."
    fixOverloaded (VName
v, NoConstraint Liftedness
_ Usage
usage) = do
      -- See #1552.
      forall (m :: * -> *).
MonadUnify m =>
Usage -> TypeBase Size () -> TypeBase Size () -> m ()
unify Usage
usage (forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar (forall dim as.
as
-> Uniqueness
-> QualName VName
-> [TypeArg dim]
-> ScalarTypeBase dim as
TypeVar () Uniqueness
Nonunique (forall v. v -> QualName v
qualName VName
v) [])) forall a b. (a -> b) -> a -> b
$
        forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$
          forall dim as. [TypeBase dim as] -> ScalarTypeBase dim as
tupleRecord []
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (VName
v forall a. Ord a => a -> Set a -> Bool
`S.member` Set VName
tyvars_at_toplevel) forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *) loc.
(MonadTypeChecker m, Located loc) =>
loc -> Doc () -> m ()
warn Usage
usage Doc ()
"Defaulting ambiguous type to ()."
    fixOverloaded (VName
_, Equality Usage
usage) =
      forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError Usage
usage forall a. Monoid a => a
mempty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ann. Doc ann -> Doc ann -> Doc ann
withIndexLink Doc ()
"ambiguous-type" forall a b. (a -> b) -> a -> b
$
        Doc ()
"Type is ambiguous (must be equality type)."
          forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"Add a type annotation to disambiguate the type."
    fixOverloaded (VName
_, HasFields Map Name (TypeBase Size ())
fs Usage
usage) =
      forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError Usage
usage forall a. Monoid a => a
mempty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ann. Doc ann -> Doc ann -> Doc ann
withIndexLink Doc ()
"ambiguous-type" forall a b. (a -> b) -> a -> b
$
        Doc ()
"Type is ambiguous.  Must be record with fields:"
          forall ann. Doc ann -> Doc ann -> Doc ann
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a. [Doc a] -> Doc a
stack forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall {a} {a} {ann}. (Pretty a, Pretty a) => (a, a) -> Doc ann
field forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
M.toList Map Name (TypeBase Size ())
fs)
          forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"Add a type annotation to disambiguate the type."
      where
        field :: (a, a) -> Doc ann
field (a
l, a
t) = forall a ann. Pretty a => a -> Doc ann
pretty a
l forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann
colon forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
align (forall a ann. Pretty a => a -> Doc ann
pretty a
t)
    fixOverloaded (VName
_, HasConstrs Map Name [TypeBase Size ()]
cs Usage
usage) =
      forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError Usage
usage forall a. Monoid a => a
mempty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ann. Doc ann -> Doc ann -> Doc ann
withIndexLink Doc ()
"ambiguous-type" forall a b. (a -> b) -> a -> b
$
        Doc ()
"Type is ambiguous (must be a sum type with constructors:"
          forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall dim as. Map Name [TypeBase dim as] -> ScalarTypeBase dim as
Sum Map Name [TypeBase Size ()]
cs) forall a. Semigroup a => a -> a -> a
<> Doc ()
")."
          forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"Add a type annotation to disambiguate the type."
    fixOverloaded (VName
v, Size Maybe Size
Nothing (Usage Maybe Text
Nothing SrcLoc
loc)) =
      forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc forall a. Monoid a => a
mempty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ann. Doc ann -> Doc ann -> Doc ann
withIndexLink Doc ()
"ambiguous-size" forall a b. (a -> b) -> a -> b
$
        Doc ()
"Ambiguous size" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName VName
v) forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
    fixOverloaded (VName
v, Size Maybe Size
Nothing (Usage (Just Text
u) SrcLoc
loc)) =
      forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc forall a. Monoid a => a
mempty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ann. Doc ann -> Doc ann -> Doc ann
withIndexLink Doc ()
"ambiguous-size" forall a b. (a -> b) -> a -> b
$
        Doc ()
"Ambiguous size" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName VName
v) forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"arising from" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty Text
u forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
    fixOverloaded (VName, Constraint)
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

hiddenParamNames :: [Pat] -> Names
hiddenParamNames :: [PatBase Info VName] -> Set VName
hiddenParamNames [PatBase Info VName]
params = Set VName
hidden
  where
    param_all_names :: Set VName
param_all_names = forall a. Monoid a => [a] -> a
mconcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall (f :: * -> *) vn.
(Functor f, Ord vn) =>
PatBase f vn -> Set vn
patNames [PatBase Info VName]
params
    named :: (PName, b) -> Maybe VName
named (Named VName
x, b
_) = forall a. a -> Maybe a
Just VName
x
    named (PName
Unnamed, b
_) = forall a. Maybe a
Nothing
    param_names :: Set VName
param_names =
      forall a. Ord a => [a] -> Set a
S.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (forall {b}. (PName, b) -> Maybe VName
named forall b c a. (b -> c) -> (a -> b) -> a -> c
. PatBase Info VName -> (PName, TypeBase Size ())
patternParam) [PatBase Info VName]
params
    hidden :: Set VName
hidden = Set VName
param_all_names forall a. Ord a => Set a -> Set a -> Set a
`S.difference` Set VName
param_names

inferredReturnType :: SrcLoc -> [Pat] -> PatType -> TermTypeM StructType
inferredReturnType :: SrcLoc
-> [PatBase Info VName] -> PatType -> TermTypeM (TypeBase Size ())
inferredReturnType SrcLoc
loc [PatBase Info VName]
params PatType
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.
  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) forall a b. (a -> b) -> a -> b
$
    SrcLoc
-> Map VName (IdentBase Info VName)
-> PatType
-> TermTypeM (PatType, [VName])
unscopeType SrcLoc
loc Map VName (IdentBase Info VName)
hidden_params forall a b. (a -> b) -> a -> b
$
      [PatBase Info VName] -> PatType -> PatType
inferReturnUniqueness [PatBase Info VName]
params PatType
t
  where
    hidden_params :: Map VName (IdentBase Info VName)
hidden_params = forall k a. (k -> a -> Bool) -> Map k a -> Map k a
M.filterWithKey (forall a b. a -> b -> a
const forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. Ord a => a -> Set a -> Bool
`S.member` Set VName
hidden)) forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall (f :: * -> *).
Functor f =>
PatBase f VName -> Map VName (IdentBase f VName)
patternMap [PatBase Info VName]
params
    hidden :: Set VName
hidden = [PatBase Info VName] -> Set VName
hiddenParamNames [PatBase Info VName]
params

checkReturnAlias :: SrcLoc -> TypeBase () () -> [Pat] -> PatType -> TermTypeM ()
checkReturnAlias :: SrcLoc
-> TypeBase () ()
-> [PatBase Info VName]
-> PatType
-> TermTypeM ()
checkReturnAlias SrcLoc
loc TypeBase () ()
rettp [PatBase Info VName]
params =
  forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m ()
foldM_ (forall {t :: * -> *}.
Foldable t =>
t (PatBase Info VName)
-> Set (Uniqueness, VName)
-> (Uniqueness, Set VName)
-> TermTypeM (Set (Uniqueness, VName))
checkReturnAlias' [PatBase Info VName]
params) forall a. Set a
S.empty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {shape} {as} {shape}.
TypeBase shape as
-> TypeBase shape Aliasing -> [(Uniqueness, Set VName)]
returnAliasing TypeBase () ()
rettp
  where
    checkReturnAlias' :: t (PatBase Info VName)
-> Set (Uniqueness, VName)
-> (Uniqueness, Set VName)
-> TermTypeM (Set (Uniqueness, VName))
checkReturnAlias' t (PatBase Info VName)
params' Set (Uniqueness, VName)
seen (Uniqueness
Unique, Set VName
names)
      | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a. Ord a => a -> Set a -> Bool
`S.member` forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map forall a b. (a, b) -> b
snd Set (Uniqueness, VName)
seen) forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
S.toList Set VName
names =
          forall a. SrcLoc -> TermTypeM a
uniqueReturnAliased SrcLoc
loc
      | Bool
otherwise = do
          forall {t :: * -> *}.
Foldable t =>
t (PatBase Info VName) -> Set VName -> TermTypeM ()
notAliasingParam t (PatBase Info VName)
params' Set VName
names
          forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Set (Uniqueness, VName)
seen forall a. Ord a => Set a -> Set a -> Set a
`S.union` forall {t} {a}. (Ord t, Ord a) => t -> Set a -> Set (t, a)
tag Uniqueness
Unique Set VName
names
    checkReturnAlias' t (PatBase Info VName)
_ Set (Uniqueness, VName)
seen (Uniqueness
Nonunique, Set VName
names)
      | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a. Ord a => a -> Set a -> Bool
`S.member` Set (Uniqueness, VName)
seen) forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
S.toList forall a b. (a -> b) -> a -> b
$ forall {t} {a}. (Ord t, Ord a) => t -> Set a -> Set (t, a)
tag Uniqueness
Unique Set VName
names =
          forall a. SrcLoc -> TermTypeM a
uniqueReturnAliased SrcLoc
loc
      | Bool
otherwise = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Set (Uniqueness, VName)
seen forall a. Ord a => Set a -> Set a -> Set a
`S.union` forall {t} {a}. (Ord t, Ord a) => t -> Set a -> Set (t, a)
tag Uniqueness
Nonunique Set VName
names

    notAliasingParam :: t (PatBase Info VName) -> Set VName -> TermTypeM ()
notAliasingParam t (PatBase Info VName)
params' Set VName
names =
      forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ t (PatBase Info VName)
params' forall a b. (a -> b) -> a -> b
$ \PatBase Info VName
p ->
        let consumedNonunique :: IdentBase Info VName -> Bool
consumedNonunique IdentBase Info VName
p' =
              Bool -> Bool
not (forall shape as. TypeBase shape as -> Bool
unique forall a b. (a -> b) -> a -> b
$ forall a. Info a -> a
unInfo forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn. IdentBase f vn -> f PatType
identType IdentBase Info VName
p') Bool -> Bool -> Bool
&& (forall (f :: * -> *) vn. IdentBase f vn -> vn
identName IdentBase Info VName
p' forall a. Ord a => a -> Set a -> Bool
`S.member` Set VName
names)
         in case forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find IdentBase Info VName -> Bool
consumedNonunique forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
S.toList forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
(Functor f, Ord vn) =>
PatBase f vn -> Set (IdentBase f vn)
patIdents PatBase Info VName
p of
              Just IdentBase Info VName
p' ->
                Name -> SrcLoc -> TermTypeM ()
returnAliased (VName -> Name
baseName forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn. IdentBase f vn -> vn
identName IdentBase Info VName
p') SrcLoc
loc
              Maybe (IdentBase Info VName)
Nothing ->
                forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

    tag :: t -> Set a -> Set (t, a)
tag t
u = forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (t
u,)

    returnAliasing :: TypeBase shape as
-> TypeBase shape Aliasing -> [(Uniqueness, Set VName)]
returnAliasing (Scalar (Record Map Name (TypeBase shape as)
ets1)) (Scalar (Record Map Name (TypeBase shape Aliasing)
ets2)) =
      forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [a]
M.elems forall a b. (a -> b) -> a -> b
$ forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith TypeBase shape as
-> TypeBase shape Aliasing -> [(Uniqueness, Set VName)]
returnAliasing Map Name (TypeBase shape as)
ets1 Map Name (TypeBase shape Aliasing)
ets2
    returnAliasing TypeBase shape as
expected TypeBase shape Aliasing
got =
      [(forall shape as. TypeBase shape as -> Uniqueness
uniqueness TypeBase shape as
expected, forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map Alias -> VName
aliasVar forall a b. (a -> b) -> a -> b
$ forall as shape. Monoid as => TypeBase shape as -> as
aliases TypeBase shape Aliasing
got)]

checkBinding ::
  ( Name,
    Maybe UncheckedTypeExp,
    [UncheckedTypeParam],
    [UncheckedPat],
    UncheckedExp,
    SrcLoc
  ) ->
  TermTypeM
    ( [TypeParam],
      [Pat],
      Maybe (TypeExp VName),
      StructRetType,
      Exp
    )
checkBinding :: (Name, Maybe UncheckedTypeExp, [TypeParamBase Name],
 [PatBase NoInfo Name], ExpBase NoInfo Name, SrcLoc)
-> TermTypeM
     ([TypeParamBase VName], [PatBase Info VName],
      Maybe (TypeExp VName), StructRetType, Exp)
checkBinding (Name
fname, Maybe UncheckedTypeExp
maybe_retdecl, [TypeParamBase Name]
tparams, [PatBase NoInfo Name]
params, ExpBase NoInfo Name
body, SrcLoc
loc) =
  forall a. TermTypeM a -> TermTypeM a
noUnique forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. TermTypeM a -> TermTypeM a
incLevel forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
[TypeParamBase Name]
-> [PatBase NoInfo Name]
-> ([TypeParamBase VName] -> [PatBase Info VName] -> TermTypeM a)
-> TermTypeM a
bindingParams [TypeParamBase Name]
tparams [PatBase NoInfo Name]
params forall a b. (a -> b) -> a -> b
$ \[TypeParamBase VName]
tparams' [PatBase Info VName]
params' -> do
    Maybe (TypeExp VName, TypeBase Size (), [VName])
maybe_retdecl' <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse UncheckedTypeExp
-> TermTypeM (TypeExp VName, TypeBase Size (), [VName])
checkTypeExpNonrigid Maybe UncheckedTypeExp
maybe_retdecl

    Exp
body' <-
      [PatBase Info VName]
-> ExpBase NoInfo Name
-> Maybe (TypeBase Size ())
-> SrcLoc
-> TermTypeM Exp
checkFunBody
        [PatBase Info VName]
params'
        ExpBase NoInfo Name
body
        ((\(TypeExp VName
_, TypeBase Size ()
x, [VName]
_) -> TypeBase Size ()
x) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (TypeExp VName, TypeBase Size (), [VName])
maybe_retdecl')
        (forall b a. b -> (a -> b) -> Maybe a -> b
maybe SrcLoc
loc forall a. Located a => a -> SrcLoc
srclocOf Maybe UncheckedTypeExp
maybe_retdecl)

    [PatBase Info VName]
params'' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall e. ASTMappable e => e -> TermTypeM e
updateTypes [PatBase Info VName]
params'
    PatType
body_t <- Exp -> TermTypeM PatType
expTypeFully Exp
body'

    (Maybe (TypeExp VName)
maybe_retdecl'', TypeBase Size ()
rettype) <- case Maybe (TypeExp VName, TypeBase Size (), [VName])
maybe_retdecl' of
      Just (TypeExp VName
retdecl', TypeBase Size ()
ret, [VName]
_) -> do
        let rettype_structural :: TypeBase () ()
rettype_structural = forall dim as. TypeBase dim as -> TypeBase () ()
toStructural TypeBase Size ()
ret
        SrcLoc
-> TypeBase () ()
-> [PatBase Info VName]
-> PatType
-> TermTypeM ()
checkReturnAlias SrcLoc
loc TypeBase () ()
rettype_structural [PatBase Info VName]
params'' PatType
body_t

        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PatBase NoInfo Name]
params) forall a b. (a -> b) -> a -> b
$ SrcLoc -> TypeBase () () -> TermTypeM ()
nothingMustBeUnique SrcLoc
loc TypeBase () ()
rettype_structural

        TypeBase Size ()
ret' <- forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully TypeBase Size ()
ret

        forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. a -> Maybe a
Just TypeExp VName
retdecl', TypeBase Size ()
ret')
      Maybe (TypeExp VName, TypeBase Size (), [VName])
Nothing
        | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PatBase NoInfo Name]
params ->
            forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Maybe a
Nothing, forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct forall a b. (a -> b) -> a -> b
$ PatType
body_t forall dim as. TypeBase dim as -> Uniqueness -> TypeBase dim as
`setUniqueness` Uniqueness
Nonunique)
        | Bool
otherwise -> do
            TypeBase Size ()
body_t' <- SrcLoc
-> [PatBase Info VName] -> PatType -> TermTypeM (TypeBase Size ())
inferredReturnType SrcLoc
loc [PatBase Info VName]
params'' PatType
body_t
            forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Maybe a
Nothing, TypeBase Size ()
body_t')

    Maybe Name -> [PatBase Info VName] -> TermTypeM ()
verifyFunctionParams (forall a. a -> Maybe a
Just Name
fname) [PatBase Info VName]
params''

    ([TypeParamBase VName]
tparams'', [PatBase Info VName]
params''', StructRetType
rettype') <-
      Name
-> SrcLoc
-> [TypeParamBase VName]
-> [PatBase Info VName]
-> TypeBase Size ()
-> TermTypeM
     ([TypeParamBase VName], [PatBase Info VName], StructRetType)
letGeneralise Name
fname SrcLoc
loc [TypeParamBase VName]
tparams' [PatBase Info VName]
params'' TypeBase Size ()
rettype

    [PatBase Info VName] -> PatType -> SrcLoc -> TermTypeM ()
checkGlobalAliases [PatBase Info VName]
params'' PatType
body_t SrcLoc
loc

    forall (f :: * -> *) a. Applicative f => a -> f a
pure ([TypeParamBase VName]
tparams'', [PatBase Info VName]
params''', Maybe (TypeExp VName)
maybe_retdecl'', StructRetType
rettype', Exp
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 :: forall als. TypeBase Size als -> Set VName
sizeNamesPos (Scalar (Arrow als
_ PName
_ TypeBase Size ()
t1 (RetType [VName]
_ TypeBase Size als
t2))) = forall als. TypeBase Size als -> Set VName
onParam TypeBase Size ()
t1 forall a. Semigroup a => a -> a -> a
<> forall als. TypeBase Size als -> Set VName
sizeNamesPos TypeBase Size als
t2
  where
    onParam :: TypeBase Size als -> S.Set VName
    onParam :: forall als. TypeBase Size als -> Set VName
onParam (Scalar Arrow {}) = forall a. Monoid a => a
mempty
    onParam (Scalar (Record Map Name (TypeBase Size als)
fs)) = forall a. Monoid a => [a] -> a
mconcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall als. TypeBase Size als -> Set VName
onParam forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [a]
M.elems Map Name (TypeBase Size als)
fs
    onParam (Scalar (TypeVar als
_ Uniqueness
_ QualName VName
_ [TypeArg Size]
targs)) = forall a. Monoid a => [a] -> a
mconcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map TypeArg Size -> Set VName
onTypeArg [TypeArg Size]
targs
    onParam TypeBase Size als
t = forall als. TypeBase Size als -> Set VName
freeInType TypeBase Size als
t
    onTypeArg :: TypeArg Size -> Set VName
onTypeArg (TypeArgDim (NamedSize QualName VName
d) SrcLoc
_) = forall a. a -> Set a
S.singleton forall a b. (a -> b) -> a -> b
$ forall vn. QualName vn -> vn
qualLeaf QualName VName
d
    onTypeArg (TypeArgDim Size
_ SrcLoc
_) = forall a. Monoid a => a
mempty
    onTypeArg (TypeArgType TypeBase Size ()
t SrcLoc
_) = forall als. TypeBase Size als -> Set VName
onParam TypeBase Size ()
t
sizeNamesPos TypeBase Size als
_ = forall a. Monoid a => a
mempty

checkGlobalAliases :: [Pat] -> PatType -> SrcLoc -> TermTypeM ()
checkGlobalAliases :: [PatBase Info VName] -> PatType -> SrcLoc -> TermTypeM ()
checkGlobalAliases [PatBase Info VName]
params PatType
body_t SrcLoc
loc = do
  Map VName ValBinding
vtable <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks forall a b. (a -> b) -> a -> b
$ TermScope -> Map VName ValBinding
scopeVtable forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermEnv -> TermScope
termScope
  let isGlobal :: VName -> Bool
isGlobal VName
v = case VName
v forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` Map VName ValBinding
vtable of
        Just (BoundV Locality
Global [TypeParamBase VName]
_ PatType
_) -> Bool
True
        Maybe ValBinding
_ -> Bool
False
  let als :: [VName]
als =
        forall a. (a -> Bool) -> [a] -> [a]
filter VName -> Bool
isGlobal forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
S.toList forall a b. (a -> b) -> a -> b
$
          PatType -> Set VName
boundArrayAliases PatType
body_t forall a. Ord a => Set a -> Set a -> Set a
`S.difference` forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall (f :: * -> *) vn.
(Functor f, Ord vn) =>
PatBase f vn -> Set vn
patNames [PatBase Info VName]
params
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PatBase Info VName]
params) forall a b. (a -> b) -> a -> b
$ case [VName]
als of
    VName
v : [VName]
_ ->
      forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc forall a. Monoid a => a
mempty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ann. Doc ann -> Doc ann -> Doc ann
withIndexLink Doc ()
"alias-free-variable" forall a b. (a -> b) -> a -> b
$
        Doc ()
"Function result aliases the free variable "
          forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName VName
v)
          forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
          forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"Use"
          forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes Doc ()
"copy"
          forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"to break the aliasing."
    [VName]
_ ->
      forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

inferReturnUniqueness :: [Pat] -> PatType -> PatType
inferReturnUniqueness :: [PatBase Info VName] -> PatType -> PatType
inferReturnUniqueness [PatBase Info VName]
params PatType
t =
  let forbidden :: Set VName
forbidden = PatType -> Set VName
aliasesMultipleTimes PatType
t
      uniques :: Set VName
uniques = [PatBase Info VName] -> Set VName
uniqueParamNames [PatBase Info VName]
params
      delve :: PatType -> PatType
delve (Scalar (Record Map Name PatType
fs)) =
        forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as. Map Name (TypeBase dim as) -> ScalarTypeBase dim as
Record forall a b. (a -> b) -> a -> b
$ forall a b k. (a -> b) -> Map k a -> Map k b
M.map PatType -> PatType
delve Map Name PatType
fs
      delve PatType
t'
        | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a. Ord a => a -> Set a -> Bool
`S.member` Set VName
uniques) (PatType -> Set VName
boundArrayAliases PatType
t'),
          Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((forall a. Ord a => a -> Set a -> Bool
`S.member` Set VName
forbidden) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Alias -> VName
aliasVar) (forall as shape. Monoid as => TypeBase shape as -> as
aliases PatType
t') =
            PatType
t' forall dim as. TypeBase dim as -> Uniqueness -> TypeBase dim as
`setUniqueness` Uniqueness
Unique
        | Bool
otherwise =
            PatType
t' forall dim as. TypeBase dim as -> Uniqueness -> TypeBase dim as
`setUniqueness` Uniqueness
Nonunique
   in PatType -> PatType
delve PatType
t

-- An alias inhibits uniqueness if it is used in disjoint values.
aliasesMultipleTimes :: PatType -> Names
aliasesMultipleTimes :: PatType -> Set VName
aliasesMultipleTimes = forall a. Ord a => [a] -> Set a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter ((forall a. Ord a => a -> a -> Bool
> Int
1) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [(k, a)]
M.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {shape}. TypeBase shape Aliasing -> Map VName Int
delve
  where
    delve :: TypeBase shape Aliasing -> Map VName Int
delve (Scalar (Record Map Name (TypeBase shape Aliasing)
fs)) =
      forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith forall a. Num a => a -> a -> a
(+)) forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map TypeBase shape Aliasing -> Map VName Int
delve forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [a]
M.elems Map Name (TypeBase shape Aliasing)
fs
    delve TypeBase shape Aliasing
t =
      forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip (forall a b. (a -> b) -> [a] -> [b]
map Alias -> VName
aliasVar forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
S.toList (forall as shape. Monoid as => TypeBase shape as -> as
aliases TypeBase shape Aliasing
t)) forall a b. (a -> b) -> a -> b
$ forall a. a -> [a]
repeat (Int
1 :: Int)

uniqueParamNames :: [Pat] -> Names
uniqueParamNames :: [PatBase Info VName] -> Set VName
uniqueParamNames =
  forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map forall (f :: * -> *) vn. IdentBase f vn -> vn
identName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> Set a -> Set a
S.filter (forall shape as. TypeBase shape as -> Bool
unique forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Info a -> a
unInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) vn. IdentBase f vn -> f PatType
identType)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall (f :: * -> *) vn.
(Functor f, Ord vn) =>
PatBase f vn -> Set (IdentBase f vn)
patIdents

boundArrayAliases :: PatType -> S.Set VName
boundArrayAliases :: PatType -> Set VName
boundArrayAliases (Array Aliasing
als Uniqueness
_ Shape Size
_ ScalarTypeBase Size ()
_) = Aliasing -> Set VName
boundAliases Aliasing
als
boundArrayAliases (Scalar Prim {}) = forall a. Monoid a => a
mempty
boundArrayAliases (Scalar (Record Map Name PatType
fs)) = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap PatType -> Set VName
boundArrayAliases Map Name PatType
fs
boundArrayAliases (Scalar (TypeVar Aliasing
als Uniqueness
_ QualName VName
_ [TypeArg Size]
_)) = Aliasing -> Set VName
boundAliases Aliasing
als
boundArrayAliases (Scalar Arrow {}) = forall a. Monoid a => a
mempty
boundArrayAliases (Scalar (Sum Map Name [PatType]
fs)) =
  forall a. Monoid a => [a] -> a
mconcat forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall a b. (a -> b) -> [a] -> [b]
map PatType -> Set VName
boundArrayAliases) forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [a]
M.elems Map Name [PatType]
fs

nothingMustBeUnique :: SrcLoc -> TypeBase () () -> TermTypeM ()
nothingMustBeUnique :: SrcLoc -> TypeBase () () -> TermTypeM ()
nothingMustBeUnique SrcLoc
loc = forall {dim} {as}. TypeBase dim as -> TermTypeM ()
check
  where
    check :: TypeBase dim as -> TermTypeM ()
check (Array as
_ Uniqueness
Unique Shape dim
_ ScalarTypeBase dim ()
_) = forall {a}. TermTypeM a
bad
    check (Scalar (TypeVar as
_ Uniqueness
Unique QualName VName
_ [TypeArg dim]
_)) = forall {a}. TermTypeM a
bad
    check (Scalar (Record Map Name (TypeBase dim as)
fs)) = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ TypeBase dim as -> TermTypeM ()
check Map Name (TypeBase dim as)
fs
    check (Scalar (Sum Map Name [TypeBase dim as]
fs)) = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ TypeBase dim as -> TermTypeM ()
check) Map Name [TypeBase dim as]
fs
    check TypeBase dim as
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    bad :: TermTypeM a
bad = forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc forall a. Monoid a => a
mempty Doc ()
"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 :: Maybe Name -> [PatBase Info VName] -> TermTypeM ()
verifyFunctionParams Maybe Name
fname [PatBase Info VName]
params =
  forall a. Checking -> TermTypeM a -> TermTypeM a
onFailure (Maybe Name -> Checking
CheckingParams Maybe Name
fname) forall a b. (a -> b) -> a -> b
$
    forall {m :: * -> *}.
MonadTypeChecker m =>
Set VName -> [PatBase Info VName] -> m ()
verifyParams (forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall (f :: * -> *) vn.
(Functor f, Ord vn) =>
PatBase f vn -> Set vn
patNames [PatBase Info VName]
params) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall e. ASTMappable e => e -> TermTypeM e
updateTypes [PatBase Info VName]
params
  where
    verifyParams :: Set VName -> [PatBase Info VName] -> m ()
verifyParams Set VName
forbidden (PatBase Info VName
p : [PatBase Info VName]
ps)
      | VName
d : [VName]
_ <- forall a. Set a -> [a]
S.toList forall a b. (a -> b) -> a -> b
$ PatBase Info VName -> Set VName
freeInPat PatBase Info VName
p forall a. Ord a => Set a -> Set a -> Set a
`S.intersection` Set VName
forbidden =
          forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError PatBase Info VName
p forall a. Monoid a => a
mempty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ann. Doc ann -> Doc ann -> Doc ann
withIndexLink Doc ()
"inaccessible-size" forall a b. (a -> b) -> a -> b
$
            Doc ()
"Parameter"
              forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty PatBase Info VName
p)
              forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"refers to size"
              forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName VName
d)
                forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann
comma
              forall ann. Doc ann -> Doc ann -> Doc ann
</> forall a. Text -> Doc a
textwrap Text
"which will not be accessible to the caller"
                forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann
comma
              forall ann. Doc ann -> Doc ann -> Doc ann
</> forall a. Text -> Doc a
textwrap Text
"possibly because it is nested in a tuple or record."
              forall ann. Doc ann -> Doc ann -> Doc ann
</> forall a. Text -> Doc a
textwrap Text
"Consider ascribing an explicit type that does not reference "
                forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName VName
d)
                forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
      | Bool
otherwise = Set VName -> [PatBase Info VName] -> m ()
verifyParams Set VName
forbidden' [PatBase Info VName]
ps
      where
        forbidden' :: Set VName
forbidden' =
          case PatBase Info VName -> (PName, TypeBase Size ())
patternParam PatBase Info VName
p of
            (Named VName
v, TypeBase Size ()
_) -> Set VName
forbidden forall a. Ord a => Set a -> Set a -> Set a
`S.difference` forall a. a -> Set a
S.singleton VName
v
            (PName, TypeBase Size ())
_ -> Set VName
forbidden
    verifyParams Set VName
_ [] = forall (f :: * -> *) a. Applicative f => a -> f a
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 :: [VName] -> TypeBase Size () -> StructRetType
injectExt [] TypeBase Size ()
ret = forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [] TypeBase Size ()
ret
injectExt [VName]
ext TypeBase Size ()
ret = forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
ext_here forall a b. (a -> b) -> a -> b
$ TypeBase Size () -> TypeBase Size ()
deeper TypeBase Size ()
ret
  where
    (Set VName
immediate, Set VName
_) = TypeBase Size () -> (Set VName, Set VName)
dimUses TypeBase Size ()
ret
    ([VName]
ext_here, [VName]
ext_there) = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (forall a. Ord a => a -> Set a -> Bool
`S.member` Set VName
immediate) [VName]
ext
    deeper :: TypeBase Size () -> TypeBase Size ()
deeper (Scalar (Prim PrimType
t)) = forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as. PrimType -> ScalarTypeBase dim as
Prim PrimType
t
    deeper (Scalar (Record Map Name (TypeBase Size ())
fs)) = forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as. Map Name (TypeBase dim as) -> ScalarTypeBase dim as
Record forall a b. (a -> b) -> a -> b
$ forall a b k. (a -> b) -> Map k a -> Map k b
M.map TypeBase Size () -> TypeBase Size ()
deeper Map Name (TypeBase Size ())
fs
    deeper (Scalar (Sum Map Name [TypeBase Size ()]
cs)) = forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as. Map Name [TypeBase dim as] -> ScalarTypeBase dim as
Sum forall a b. (a -> b) -> a -> b
$ forall a b k. (a -> b) -> Map k a -> Map k b
M.map (forall a b. (a -> b) -> [a] -> [b]
map TypeBase Size () -> TypeBase Size ()
deeper) Map Name [TypeBase Size ()]
cs
    deeper (Scalar (Arrow ()
als PName
p TypeBase Size ()
t1 (RetType [VName]
t2_ext TypeBase Size ()
t2))) =
      forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as.
as
-> PName
-> TypeBase dim ()
-> RetTypeBase dim as
-> ScalarTypeBase dim as
Arrow ()
als PName
p TypeBase Size ()
t1 forall a b. (a -> b) -> a -> b
$ [VName] -> TypeBase Size () -> StructRetType
injectExt ([VName]
ext_there forall a. Semigroup a => a -> a -> a
<> [VName]
t2_ext) TypeBase Size ()
t2
    deeper (Scalar (TypeVar ()
as Uniqueness
u QualName VName
tn [TypeArg Size]
targs)) =
      forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as.
as
-> Uniqueness
-> QualName VName
-> [TypeArg dim]
-> ScalarTypeBase dim as
TypeVar ()
as Uniqueness
u QualName VName
tn forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map TypeArg Size -> TypeArg Size
deeperArg [TypeArg Size]
targs
    deeper t :: TypeBase Size ()
t@Array {} = TypeBase Size ()
t

    deeperArg :: TypeArg Size -> TypeArg Size
deeperArg (TypeArgType TypeBase Size ()
t SrcLoc
loc) = forall dim. TypeBase dim () -> SrcLoc -> TypeArg dim
TypeArgType (TypeBase Size () -> TypeBase Size ()
deeper TypeBase Size ()
t) SrcLoc
loc
    deeperArg (TypeArgDim Size
d SrcLoc
loc) = forall dim. dim -> SrcLoc -> TypeArg dim
TypeArgDim Size
d SrcLoc
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 :: Name
-> SrcLoc
-> [TypeParamBase VName]
-> [TypeBase Size ()]
-> TypeBase Size ()
-> Constraints
-> TermTypeM ([TypeParamBase VName], StructRetType)
closeOverTypes Name
defname SrcLoc
defloc [TypeParamBase VName]
tparams [TypeBase Size ()]
paramts TypeBase Size ()
ret Constraints
substs = do
  ([TypeParamBase VName]
more_tparams, [VName]
retext) <-
    forall a b. [Either a b] -> ([a], [b])
partitionEithers forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [Maybe a] -> [a]
catMaybes
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall {f :: * -> *}.
(MonadUnify f, MonadTypeChecker f) =>
(VName, Constraint)
-> f (Maybe (Either (TypeParamBase VName) VName))
closeOver (forall k a. Map k a -> [(k, a)]
M.toList forall a b. (a -> b) -> a -> b
$ forall a b k. (a -> b) -> Map k a -> Map k b
M.map forall a b. (a, b) -> b
snd Constraints
to_close_over)
  let mkExt :: VName -> Maybe VName
mkExt VName
v =
        case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
v Constraints
substs of
          Just (Int
_, UnknowableSize {}) -> forall a. a -> Maybe a
Just VName
v
          Maybe (Int, Constraint)
_ -> forall a. Maybe a
Nothing
  forall (f :: * -> *) a. Applicative f => a -> f a
pure
    ( [TypeParamBase VName]
tparams forall a. [a] -> [a] -> [a]
++ [TypeParamBase VName]
more_tparams,
      [VName] -> TypeBase Size () -> StructRetType
injectExt ([VName]
retext forall a. [a] -> [a] -> [a]
++ forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe VName -> Maybe VName
mkExt (forall a. Set a -> [a]
S.toList forall a b. (a -> b) -> a -> b
$ forall als. TypeBase Size als -> Set VName
freeInType TypeBase Size ()
ret)) TypeBase Size ()
ret
    )
  where
    t :: TypeBase Size ()
t = forall as dim pas.
Monoid as =>
[TypeBase dim pas] -> RetTypeBase dim as -> TypeBase dim as
foldFunType [TypeBase Size ()]
paramts forall a b. (a -> b) -> a -> b
$ forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [] TypeBase Size ()
ret
    to_close_over :: Constraints
to_close_over = forall k a. (k -> a -> Bool) -> Map k a -> Map k a
M.filterWithKey (\VName
k (Int, Constraint)
_ -> VName
k forall a. Ord a => a -> Set a -> Bool
`S.member` Set VName
visible) Constraints
substs
    visible :: Set VName
visible = forall as dim. Monoid as => TypeBase dim as -> Set VName
typeVars TypeBase Size ()
t forall a. Semigroup a => a -> a -> a
<> forall als. TypeBase Size als -> Set VName
freeInType TypeBase Size ()
t

    (Set VName
produced_sizes, Set VName
param_sizes) = TypeBase Size () -> (Set VName, Set VName)
dimUses TypeBase Size ()
t

    -- Avoid duplicate type parameters.
    closeOver :: (VName, Constraint)
-> f (Maybe (Either (TypeParamBase VName) VName))
closeOver (VName
k, Constraint
_)
      | VName
k forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` forall a b. (a -> b) -> [a] -> [b]
map forall vn. TypeParamBase vn -> vn
typeParamName [TypeParamBase VName]
tparams =
          forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
    closeOver (VName
k, NoConstraint Liftedness
l Usage
usage) =
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall vn. Liftedness -> vn -> SrcLoc -> TypeParamBase vn
TypeParamType Liftedness
l VName
k forall a b. (a -> b) -> a -> b
$ forall a. Located a => a -> SrcLoc
srclocOf Usage
usage
    closeOver (VName
k, ParamType Liftedness
l SrcLoc
loc) =
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall vn. Liftedness -> vn -> SrcLoc -> TypeParamBase vn
TypeParamType Liftedness
l VName
k SrcLoc
loc
    closeOver (VName
k, Size Maybe Size
Nothing Usage
usage) =
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall vn. vn -> SrcLoc -> TypeParamBase vn
TypeParamDim VName
k forall a b. (a -> b) -> a -> b
$ forall a. Located a => a -> SrcLoc
srclocOf Usage
usage
    closeOver (VName
k, UnknowableSize SrcLoc
_ RigidSource
_)
      | VName
k forall a. Ord a => a -> Set a -> Bool
`S.member` Set VName
param_sizes,
        VName
k forall a. Ord a => a -> Set a -> Bool
`S.notMember` Set VName
produced_sizes = do
          Notes
notes <- forall a (m :: * -> *).
(Located a, MonadUnify m) =>
a -> Size -> m Notes
dimNotes SrcLoc
defloc forall a b. (a -> b) -> a -> b
$ QualName VName -> Size
NamedSize forall a b. (a -> b) -> a -> b
$ forall v. v -> QualName v
qualName VName
k
          forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
defloc Notes
notes forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ann. Doc ann -> Doc ann -> Doc ann
withIndexLink Doc ()
"unknowable-param-def" forall a b. (a -> b) -> a -> b
$
            Doc ()
"Unknowable size"
              forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName VName
k)
              forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"in parameter of"
              forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName Name
defname)
                forall a. Semigroup a => a -> a -> a
<> Doc ()
", which is inferred as:"
              forall ann. Doc ann -> Doc ann -> Doc ann
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a ann. Pretty a => a -> Doc ann
pretty TypeBase Size ()
t)
      | VName
k forall a. Ord a => a -> Set a -> Bool
`S.member` Set VName
produced_sizes =
          forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right VName
k
    closeOver (VName
_, Constraint
_) =
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing

letGeneralise ::
  Name ->
  SrcLoc ->
  [TypeParam] ->
  [Pat] ->
  StructType ->
  TermTypeM ([TypeParam], [Pat], StructRetType)
letGeneralise :: Name
-> SrcLoc
-> [TypeParamBase VName]
-> [PatBase Info VName]
-> TypeBase Size ()
-> TermTypeM
     ([TypeParamBase VName], [PatBase Info VName], StructRetType)
letGeneralise Name
defname SrcLoc
defloc [TypeParamBase VName]
tparams [PatBase Info VName]
params TypeBase Size ()
rettype =
  forall a. Checking -> TermTypeM a -> TermTypeM a
onFailure (Name -> Checking
CheckingLetGeneralise Name
defname) forall a b. (a -> b) -> a -> b
$ do
    Constraints
now_substs <- forall (m :: * -> *). MonadUnify m => m Constraints
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 :: Set VName
keep_type_vars = Constraints -> Set VName
overloadedTypeVars Constraints
now_substs

    Int
cur_lvl <- forall (m :: * -> *). MonadUnify m => m Int
curLevel
    let candidate :: VName -> (Int, b) -> Bool
candidate VName
k (Int
lvl, b
_) = (VName
k forall a. Ord a => a -> Set a -> Bool
`S.notMember` Set VName
keep_type_vars) Bool -> Bool -> Bool
&& Int
lvl forall a. Ord a => a -> a -> Bool
>= Int
cur_lvl
        new_substs :: Constraints
new_substs = forall k a. (k -> a -> Bool) -> Map k a -> Map k a
M.filterWithKey forall {b}. VName -> (Int, b) -> Bool
candidate Constraints
now_substs

    ([TypeParamBase VName]
tparams', RetType [VName]
ret_dims TypeBase Size ()
rettype') <-
      Name
-> SrcLoc
-> [TypeParamBase VName]
-> [TypeBase Size ()]
-> TypeBase Size ()
-> Constraints
-> TermTypeM ([TypeParamBase VName], StructRetType)
closeOverTypes
        Name
defname
        SrcLoc
defloc
        [TypeParamBase VName]
tparams
        (forall a b. (a -> b) -> [a] -> [b]
map PatBase Info VName -> TypeBase Size ()
patternStructType [PatBase Info VName]
params)
        TypeBase Size ()
rettype
        Constraints
new_substs

    TypeBase Size ()
rettype'' <- forall e. ASTMappable e => e -> TermTypeM e
updateTypes TypeBase Size ()
rettype'

    let used_sizes :: Set VName
used_sizes =
          forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall als. TypeBase Size als -> Set VName
freeInType forall a b. (a -> b) -> a -> b
$ TypeBase Size ()
rettype'' forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map PatBase Info VName -> TypeBase Size ()
patternStructType [PatBase Info VName]
params
    case forall a. (a -> Bool) -> [a] -> [a]
filter ((forall a. Ord a => a -> Set a -> Bool
`S.notMember` Set VName
used_sizes) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall vn. TypeParamBase vn -> vn
typeParamName) forall a b. (a -> b) -> a -> b
$
      forall a. (a -> Bool) -> [a] -> [a]
filter forall vn. TypeParamBase vn -> Bool
isSizeParam [TypeParamBase VName]
tparams' of
      [] -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      TypeParamBase VName
tp : [TypeParamBase VName]
_ -> forall (m :: * -> *) a.
MonadTypeChecker m =>
SizeBinder VName -> m a
unusedSize forall a b. (a -> b) -> a -> b
$ forall vn. vn -> SrcLoc -> SizeBinder vn
SizeBinder (forall vn. TypeParamBase vn -> vn
typeParamName TypeParamBase VName
tp) (forall a. Located a => a -> SrcLoc
srclocOf TypeParamBase VName
tp)

    -- We keep those type variables that were not closed over by
    -- let-generalisation.
    forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints forall a b. (a -> b) -> a -> b
$ forall k a. (k -> a -> Bool) -> Map k a -> Map k a
M.filterWithKey forall a b. (a -> b) -> a -> b
$ \VName
k (Int, Constraint)
_ -> VName
k forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` forall a b. (a -> b) -> [a] -> [b]
map forall vn. TypeParamBase vn -> vn
typeParamName [TypeParamBase VName]
tparams'

    forall (f :: * -> *) a. Applicative f => a -> f a
pure ([TypeParamBase VName]
tparams', [PatBase Info VName]
params, forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
ret_dims TypeBase Size ()
rettype'')

checkFunBody ::
  [Pat] ->
  UncheckedExp ->
  Maybe StructType ->
  SrcLoc ->
  TermTypeM Exp
checkFunBody :: [PatBase Info VName]
-> ExpBase NoInfo Name
-> Maybe (TypeBase Size ())
-> SrcLoc
-> TermTypeM Exp
checkFunBody [PatBase Info VName]
params ExpBase NoInfo Name
body Maybe (TypeBase Size ())
maybe_rettype SrcLoc
loc = do
  Exp
body' <- forall a. TermTypeM a -> TermTypeM a
noSizeEscape forall a b. (a -> b) -> a -> b
$ ExpBase NoInfo Name -> TermTypeM Exp
checkExp ExpBase NoInfo Name
body

  -- Unify body return type with return annotation, if one exists.
  case Maybe (TypeBase Size ())
maybe_rettype of
    Just TypeBase Size ()
rettype -> do
      PatType
body_t <- Exp -> TermTypeM PatType
expTypeFully Exp
body'
      -- We need to turn any sizes provided by "hidden" parameter
      -- names into existential sizes instead.
      let hidden :: Set VName
hidden = [PatBase Info VName] -> Set VName
hiddenParamNames [PatBase Info VName]
params
      (PatType
body_t', [VName]
_) <-
        SrcLoc
-> Map VName (IdentBase Info VName)
-> PatType
-> TermTypeM (PatType, [VName])
unscopeType
          SrcLoc
loc
          ( forall k a. (k -> a -> Bool) -> Map k a -> Map k a
M.filterWithKey (forall a b. a -> b -> a
const forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. Ord a => a -> Set a -> Bool
`S.member` Set VName
hidden)) forall a b. (a -> b) -> a -> b
$
              forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall (f :: * -> *).
Functor f =>
PatBase f VName -> Map VName (IdentBase f VName)
patternMap [PatBase Info VName]
params
          )
          PatType
body_t

      let usage :: Usage
usage = SrcLoc -> Text -> Usage
mkUsage (forall a. Located a => a -> SrcLoc
srclocOf ExpBase NoInfo Name
body) Text
"return type annotation"
      forall a. Checking -> TermTypeM a -> TermTypeM a
onFailure (TypeBase Size () -> TypeBase Size () -> Checking
CheckingReturn TypeBase Size ()
rettype (forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct PatType
body_t')) forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *).
MonadUnify m =>
Usage -> TypeBase Size () -> TypeBase Size () -> m ()
expect Usage
usage TypeBase Size ()
rettype forall a b. (a -> b) -> a -> b
$
          forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct PatType
body_t'
    Maybe (TypeBase Size ())
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

  forall (f :: * -> *) a. Applicative f => a -> f a
pure Exp
body'

arrayOfM ::
  (Pretty (Shape dim), Monoid as) =>
  SrcLoc ->
  TypeBase dim as ->
  Shape dim ->
  Uniqueness ->
  TermTypeM (TypeBase dim as)
arrayOfM :: forall dim as.
(Pretty (Shape dim), Monoid as) =>
SrcLoc
-> TypeBase dim as
-> Shape dim
-> Uniqueness
-> TermTypeM (TypeBase dim as)
arrayOfM SrcLoc
loc TypeBase dim as
t Shape dim
shape Uniqueness
u = do
  forall (m :: * -> *) dim as.
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage -> Text -> TypeBase dim as -> m ()
arrayElemType (SrcLoc -> Text -> Usage
mkUsage SrcLoc
loc Text
"use as array element") Text
"type used in array" TypeBase dim as
t
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall as dim.
Monoid as =>
Uniqueness -> Shape dim -> TypeBase dim as -> TypeBase dim as
arrayOf Uniqueness
u Shape dim
shape TypeBase dim as
t