-- | Facilities for type-checking terms.  Factored out of
-- "Language.Futhark.TypeChecker.Terms" to prevent the module from
-- being gigantic.
--
-- Incidentally also a nice place to put Haddock comments to make the
-- internal API of the type checker easier to browse.
module Language.Futhark.TypeChecker.Terms.Monad
  ( TermTypeM,
    runTermTypeM,
    liftTypeM,
    ValBinding (..),
    Locality (..),
    SizeSource (SourceBound, SourceSlice),
    NameReason (..),
    InferredType (..),
    Checking (..),
    withEnv,
    localScope,
    TermEnv (..),
    TermScope (..),
    TermTypeState (..),
    onFailure,
    extSize,
    expType,
    expTypeFully,
    constrain,
    newArrayType,
    allDimsFreshInType,
    updateTypes,

    -- * Primitive checking
    unifies,
    require,
    checkTypeExpNonrigid,
    checkTypeExpRigid,

    -- * Sizes
    isInt64,
    maybeDimFromExp,
    dimFromExp,
    sizeFromArg,
    noSizeEscape,

    -- * Control flow
    collectOccurrences,
    tapOccurrences,
    alternative,
    sequentially,
    incLevel,

    -- * Consumption and uniqueness
    Names,
    Occurrence (..),
    Occurrences,
    noUnique,
    removeSeminullOccurrences,
    occur,
    observe,
    consume,
    consuming,
    observation,
    consumption,
    checkIfConsumable,
    seqOccurrences,
    checkOccurrences,
    allConsumed,

    -- * Errors
    unusedSize,
    uniqueReturnAliased,
    returnAliased,
    badLetWithValue,
    anyConsumption,
    allOccurring,
  )
where

import Control.Monad
import Control.Monad.Except
import Control.Monad.Reader
import Control.Monad.State
import Data.Bifunctor
import Data.Bitraversable
import Data.Char (isAscii)
import Data.List (find, isPrefixOf, sort)
import Data.Map.Strict qualified as M
import Data.Maybe
import Data.Set qualified as S
import Data.Text qualified as T
import Futhark.Util.Pretty hiding (space)
import Language.Futhark
import Language.Futhark.Semantic (includeToFilePath)
import Language.Futhark.Traversals
import Language.Futhark.TypeChecker.Monad hiding (BoundV)
import Language.Futhark.TypeChecker.Monad qualified as TypeM
import Language.Futhark.TypeChecker.Types
import Language.Futhark.TypeChecker.Unify hiding (Usage)
import Prelude hiding (mod)

--- Uniqueness

data Usage
  = Consumed SrcLoc
  | Observed SrcLoc
  deriving (Usage -> Usage -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Usage -> Usage -> Bool
$c/= :: Usage -> Usage -> Bool
== :: Usage -> Usage -> Bool
$c== :: Usage -> Usage -> Bool
Eq, Eq Usage
Usage -> Usage -> Bool
Usage -> Usage -> Ordering
Usage -> Usage -> Usage
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Usage -> Usage -> Usage
$cmin :: Usage -> Usage -> Usage
max :: Usage -> Usage -> Usage
$cmax :: Usage -> Usage -> Usage
>= :: Usage -> Usage -> Bool
$c>= :: Usage -> Usage -> Bool
> :: Usage -> Usage -> Bool
$c> :: Usage -> Usage -> Bool
<= :: Usage -> Usage -> Bool
$c<= :: Usage -> Usage -> Bool
< :: Usage -> Usage -> Bool
$c< :: Usage -> Usage -> Bool
compare :: Usage -> Usage -> Ordering
$ccompare :: Usage -> Usage -> Ordering
Ord, Int -> Usage -> ShowS
[Usage] -> ShowS
Usage -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Usage] -> ShowS
$cshowList :: [Usage] -> ShowS
show :: Usage -> String
$cshow :: Usage -> String
showsPrec :: Int -> Usage -> ShowS
$cshowsPrec :: Int -> Usage -> ShowS
Show)

type Names = S.Set VName

-- | The consumption set is a Maybe so we can distinguish whether a
-- consumption took place, but the variable went out of scope since,
-- or no consumption at all took place.
data Occurrence = Occurrence
  { Occurrence -> Set VName
observed :: Names,
    Occurrence -> Maybe (Set VName)
consumed :: Maybe Names,
    Occurrence -> SrcLoc
location :: SrcLoc
  }
  deriving (Occurrence -> Occurrence -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Occurrence -> Occurrence -> Bool
$c/= :: Occurrence -> Occurrence -> Bool
== :: Occurrence -> Occurrence -> Bool
$c== :: Occurrence -> Occurrence -> Bool
Eq, Int -> Occurrence -> ShowS
Occurrences -> ShowS
Occurrence -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: Occurrences -> ShowS
$cshowList :: Occurrences -> ShowS
show :: Occurrence -> String
$cshow :: Occurrence -> String
showsPrec :: Int -> Occurrence -> ShowS
$cshowsPrec :: Int -> Occurrence -> ShowS
Show)

instance Located Occurrence where
  locOf :: Occurrence -> Loc
locOf = forall a. Located a => a -> Loc
locOf forall b c a. (b -> c) -> (a -> b) -> a -> c
. Occurrence -> SrcLoc
location

observation :: Aliasing -> SrcLoc -> Occurrence
observation :: Aliasing -> SrcLoc -> Occurrence
observation = forall a b c. (a -> b -> c) -> b -> a -> c
flip Set VName -> Maybe (Set VName) -> SrcLoc -> Occurrence
Occurrence forall a. Maybe a
Nothing forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map Alias -> VName
aliasVar

consumption :: Aliasing -> SrcLoc -> Occurrence
consumption :: Aliasing -> SrcLoc -> Occurrence
consumption = Set VName -> Maybe (Set VName) -> SrcLoc -> Occurrence
Occurrence forall a. Set a
S.empty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map Alias -> VName
aliasVar

-- | A null occurence is one that we can remove without affecting
-- anything.
nullOccurrence :: Occurrence -> Bool
nullOccurrence :: Occurrence -> Bool
nullOccurrence Occurrence
occ = forall a. Set a -> Bool
S.null (Occurrence -> Set VName
observed Occurrence
occ) Bool -> Bool -> Bool
&& forall a. Maybe a -> Bool
isNothing (Occurrence -> Maybe (Set VName)
consumed Occurrence
occ)

-- | A seminull occurence is one that does not contain references to
-- any variables in scope.  The big difference is that a seminull
-- occurence may denote a consumption, as long as the array that was
-- consumed is now out of scope.
seminullOccurrence :: Occurrence -> Bool
seminullOccurrence :: Occurrence -> Bool
seminullOccurrence Occurrence
occ = forall a. Set a -> Bool
S.null (Occurrence -> Set VName
observed Occurrence
occ) Bool -> Bool -> Bool
&& forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True forall a. Set a -> Bool
S.null (Occurrence -> Maybe (Set VName)
consumed Occurrence
occ)

type Occurrences = [Occurrence]

type UsageMap = M.Map VName [Usage]

usageMap :: Occurrences -> UsageMap
usageMap :: Occurrences -> UsageMap
usageMap = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl UsageMap -> Occurrence -> UsageMap
comb forall k a. Map k a
M.empty
  where
    comb :: UsageMap -> Occurrence -> UsageMap
comb UsageMap
m (Occurrence Set VName
obs Maybe (Set VName)
cons SrcLoc
loc) =
      let m' :: UsageMap
m' = forall a b. (a -> b -> a) -> a -> Set b -> a
S.foldl' (forall {k} {a}. Ord k => a -> Map k [a] -> k -> Map k [a]
ins forall a b. (a -> b) -> a -> b
$ SrcLoc -> Usage
Observed SrcLoc
loc) UsageMap
m Set VName
obs
       in forall a b. (a -> b -> a) -> a -> Set b -> a
S.foldl' (forall {k} {a}. Ord k => a -> Map k [a] -> k -> Map k [a]
ins forall a b. (a -> b) -> a -> b
$ SrcLoc -> Usage
Consumed SrcLoc
loc) UsageMap
m' forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe forall a. Monoid a => a
mempty Maybe (Set VName)
cons
    ins :: a -> Map k [a] -> k -> Map k [a]
ins a
v Map k [a]
m k
k = forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
M.insertWith forall a. [a] -> [a] -> [a]
(++) k
k [a
v] Map k [a]
m

combineOccurrences :: VName -> Usage -> Usage -> TermTypeM Usage
combineOccurrences :: VName -> Usage -> Usage -> TermTypeM Usage
combineOccurrences VName
_ (Observed SrcLoc
loc) (Observed SrcLoc
_) = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ SrcLoc -> Usage
Observed SrcLoc
loc
combineOccurrences VName
name (Consumed SrcLoc
wloc) (Observed SrcLoc
rloc) =
  forall a. VName -> SrcLoc -> SrcLoc -> TermTypeM a
useAfterConsume VName
name SrcLoc
rloc SrcLoc
wloc
combineOccurrences VName
name (Observed SrcLoc
rloc) (Consumed SrcLoc
wloc) =
  forall a. VName -> SrcLoc -> SrcLoc -> TermTypeM a
useAfterConsume VName
name SrcLoc
rloc SrcLoc
wloc
combineOccurrences VName
name (Consumed SrcLoc
loc1) (Consumed SrcLoc
loc2) =
  forall a. VName -> SrcLoc -> SrcLoc -> TermTypeM a
useAfterConsume VName
name (forall a. Ord a => a -> a -> a
max SrcLoc
loc1 SrcLoc
loc2) (forall a. Ord a => a -> a -> a
min SrcLoc
loc1 SrcLoc
loc2)

checkOccurrences :: Occurrences -> TermTypeM ()
checkOccurrences :: Occurrences -> TermTypeM ()
checkOccurrences = forall (f :: * -> *) a. Functor f => f a -> f ()
void forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) k a b.
Applicative t =>
(k -> a -> t b) -> Map k a -> t (Map k b)
M.traverseWithKey VName -> [Usage] -> TermTypeM ()
comb forall b c a. (b -> c) -> (a -> b) -> a -> c
. Occurrences -> UsageMap
usageMap
  where
    comb :: VName -> [Usage] -> TermTypeM ()
comb VName
_ [] = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    comb VName
name (Usage
u : [Usage]
us) = forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m ()
foldM_ (VName -> Usage -> Usage -> TermTypeM Usage
combineOccurrences VName
name) Usage
u [Usage]
us

allObserved :: Occurrences -> Names
allObserved :: Occurrences -> Set VName
allObserved = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map Occurrence -> Set VName
observed

allConsumed :: Occurrences -> Names
allConsumed :: Occurrences -> Set VName
allConsumed = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall a. a -> Maybe a -> a
fromMaybe forall a. Monoid a => a
mempty forall b c a. (b -> c) -> (a -> b) -> a -> c
. Occurrence -> Maybe (Set VName)
consumed)

allOccurring :: Occurrences -> Names
allOccurring :: Occurrences -> Set VName
allOccurring Occurrences
occs = Occurrences -> Set VName
allConsumed Occurrences
occs forall a. Semigroup a => a -> a -> a
<> Occurrences -> Set VName
allObserved Occurrences
occs

-- | Find any consumption that references a variable in scope.
anyConsumption :: Occurrences -> Maybe Occurrence
anyConsumption :: Occurrences -> Maybe Occurrence
anyConsumption = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> Bool
null) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Occurrence -> Maybe (Set VName)
consumed)

seqOccurrences :: Occurrences -> Occurrences -> Occurrences
seqOccurrences :: Occurrences -> Occurrences -> Occurrences
seqOccurrences Occurrences
occurs1 Occurrences
occurs2 =
  forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Occurrence -> Bool
nullOccurrence) forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Occurrence -> Occurrence
filt Occurrences
occurs1 forall a. [a] -> [a] -> [a]
++ Occurrences
occurs2
  where
    filt :: Occurrence -> Occurrence
filt Occurrence
occ =
      Occurrence
occ {observed :: Set VName
observed = Occurrence -> Set VName
observed Occurrence
occ forall a. Ord a => Set a -> Set a -> Set a
`S.difference` Set VName
postcons}
    postcons :: Set VName
postcons = Occurrences -> Set VName
allConsumed Occurrences
occurs2

altOccurrences :: Occurrences -> Occurrences -> Occurrences
altOccurrences :: Occurrences -> Occurrences -> Occurrences
altOccurrences Occurrences
occurs1 Occurrences
occurs2 =
  forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Occurrence -> Bool
nullOccurrence) forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Occurrence -> Occurrence
filt1 Occurrences
occurs1 forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map Occurrence -> Occurrence
filt2 Occurrences
occurs2
  where
    filt1 :: Occurrence -> Occurrence
filt1 Occurrence
occ =
      Occurrence
occ
        { consumed :: Maybe (Set VName)
consumed = forall a. Ord a => Set a -> Set a -> Set a
S.difference forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Occurrence -> Maybe (Set VName)
consumed Occurrence
occ forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Set VName
cons2,
          observed :: Set VName
observed = Occurrence -> Set VName
observed Occurrence
occ forall a. Ord a => Set a -> Set a -> Set a
`S.difference` Set VName
cons2
        }
    filt2 :: Occurrence -> Occurrence
filt2 Occurrence
occ =
      Occurrence
occ
        { consumed :: Maybe (Set VName)
consumed = Occurrence -> Maybe (Set VName)
consumed Occurrence
occ,
          observed :: Set VName
observed = Occurrence -> Set VName
observed Occurrence
occ forall a. Ord a => Set a -> Set a -> Set a
`S.difference` Set VName
cons1
        }
    cons1 :: Set VName
cons1 = Occurrences -> Set VName
allConsumed Occurrences
occurs1
    cons2 :: Set VName
cons2 = Occurrences -> Set VName
allConsumed Occurrences
occurs2

-- | How something was bound.
data Locality
  = -- | In the current function
    Local
  | -- | In an enclosing function, but not the current one.
    Nonlocal
  | -- | At global scope.
    Global
  deriving (Int -> Locality -> ShowS
[Locality] -> ShowS
Locality -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Locality] -> ShowS
$cshowList :: [Locality] -> ShowS
show :: Locality -> String
$cshow :: Locality -> String
showsPrec :: Int -> Locality -> ShowS
$cshowsPrec :: Int -> Locality -> ShowS
Show, Locality -> Locality -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Locality -> Locality -> Bool
$c/= :: Locality -> Locality -> Bool
== :: Locality -> Locality -> Bool
$c== :: Locality -> Locality -> Bool
Eq, Eq Locality
Locality -> Locality -> Bool
Locality -> Locality -> Ordering
Locality -> Locality -> Locality
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Locality -> Locality -> Locality
$cmin :: Locality -> Locality -> Locality
max :: Locality -> Locality -> Locality
$cmax :: Locality -> Locality -> Locality
>= :: Locality -> Locality -> Bool
$c>= :: Locality -> Locality -> Bool
> :: Locality -> Locality -> Bool
$c> :: Locality -> Locality -> Bool
<= :: Locality -> Locality -> Bool
$c<= :: Locality -> Locality -> Bool
< :: Locality -> Locality -> Bool
$c< :: Locality -> Locality -> Bool
compare :: Locality -> Locality -> Ordering
$ccompare :: Locality -> Locality -> Ordering
Ord)

data ValBinding
  = -- | Aliases in parameters indicate the lexical
    -- closure.
    BoundV Locality [TypeParam] PatType
  | OverloadedF [PrimType] [Maybe PrimType] (Maybe PrimType)
  | EqualityF
  | WasConsumed SrcLoc
  deriving (Int -> ValBinding -> ShowS
[ValBinding] -> ShowS
ValBinding -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ValBinding] -> ShowS
$cshowList :: [ValBinding] -> ShowS
show :: ValBinding -> String
$cshow :: ValBinding -> String
showsPrec :: Int -> ValBinding -> ShowS
$cshowsPrec :: Int -> ValBinding -> ShowS
Show)

--- Errors

describeVar :: SrcLoc -> VName -> TermTypeM (Doc a)
describeVar :: forall a. SrcLoc -> VName -> TermTypeM (Doc a)
describeVar SrcLoc
loc VName
v =
  forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets forall a b. (a -> b) -> a -> b
$
    forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Doc a
"variable" 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. SrcLoc -> NameReason -> Doc a
nameReason SrcLoc
loc)
      forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
v
      forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermTypeState -> Map VName NameReason
stateNames

useAfterConsume :: VName -> SrcLoc -> SrcLoc -> TermTypeM a
useAfterConsume :: forall a. VName -> SrcLoc -> SrcLoc -> TermTypeM a
useAfterConsume VName
name SrcLoc
rloc SrcLoc
wloc = do
  Doc ()
name' <- forall a. SrcLoc -> VName -> TermTypeM (Doc a)
describeVar SrcLoc
rloc VName
name
  forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
rloc 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 ()
"use-after-consume" forall a b. (a -> b) -> a -> b
$
    Doc ()
"Using"
      forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
name' forall a. Semigroup a => a -> a -> a
<> Doc ()
", but this was consumed 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 SrcLoc
rloc SrcLoc
wloc) forall a. Semigroup a => a -> a -> a
<> Doc ()
".  (Possibly through aliasing.)"

badLetWithValue :: (Pretty arr, Pretty src) => arr -> src -> SrcLoc -> TermTypeM a
badLetWithValue :: forall arr src a.
(Pretty arr, Pretty src) =>
arr -> src -> SrcLoc -> TermTypeM a
badLetWithValue arr
arre src
vale 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 a b. (a -> b) -> a -> b
$
    Doc ()
"Source array for in-place update"
      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 arr
arre)
      forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"might alias update value"
      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 src
vale)
      forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"Hint: 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 remove aliases from the value."

returnAliased :: Name -> SrcLoc -> TermTypeM ()
returnAliased :: Name -> SrcLoc -> TermTypeM ()
returnAliased Name
name 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 ()
"return-aliased" forall a b. (a -> b) -> a -> b
$
    Doc ()
"Unique-typed return value is aliased to"
      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
name) forall a. Semigroup a => a -> a -> a
<> Doc ()
", which is not consumable."

uniqueReturnAliased :: SrcLoc -> TermTypeM a
uniqueReturnAliased :: forall a. SrcLoc -> TermTypeM a
uniqueReturnAliased 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 ()
"unique-return-aliased" forall a b. (a -> b) -> a -> b
$
    Doc ()
"A unique-typed component of the return value is aliased to some other component."

notConsumable :: MonadTypeChecker m => SrcLoc -> Doc () -> m b
notConsumable :: forall (m :: * -> *) b.
MonadTypeChecker m =>
SrcLoc -> Doc () -> m b
notConsumable SrcLoc
loc Doc ()
v =
  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 ()
"not-consumable" forall a b. (a -> b) -> a -> b
$
    Doc ()
"Would consume" forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
v forall a. Semigroup a => a -> a -> a
<> Doc ()
", which is not consumable."

unusedSize :: (MonadTypeChecker m) => SizeBinder VName -> m a
unusedSize :: forall (m :: * -> *) a.
MonadTypeChecker m =>
SizeBinder VName -> m a
unusedSize SizeBinder VName
p =
  forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SizeBinder 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 ()
"unused-size" forall a b. (a -> b) -> a -> b
$
    Doc ()
"Size" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty SizeBinder VName
p forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"unused in pattern."

--- Scope management

data InferredType
  = NoneInferred
  | Ascribed PatType

data Checking
  = CheckingApply (Maybe (QualName VName)) Exp StructType StructType
  | CheckingReturn StructType StructType
  | CheckingAscription StructType StructType
  | CheckingLetGeneralise Name
  | CheckingParams (Maybe Name)
  | CheckingPat UncheckedPat InferredType
  | CheckingLoopBody StructType StructType
  | CheckingLoopInitial StructType StructType
  | CheckingRecordUpdate [Name] StructType StructType
  | CheckingRequired [StructType] StructType
  | CheckingBranches StructType StructType

instance Pretty Checking where
  pretty :: forall ann. Checking -> Doc ann
pretty (CheckingApply Maybe (QualName VName)
f Exp
e StructType
expected StructType
actual) =
    forall {ann}. Doc ann
header
      forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ann
"Expected:"
      forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
align (forall a ann. Pretty a => a -> Doc ann
pretty StructType
expected)
      forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ann
"Actual:  "
      forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
align (forall a ann. Pretty a => a -> Doc ann
pretty StructType
actual)
    where
      header :: Doc ann
header =
        case Maybe (QualName VName)
f of
          Maybe (QualName VName)
Nothing ->
            Doc ann
"Cannot apply function to"
              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
e) forall a. Semigroup a => a -> a -> a
<> Doc ann
" (invalid type)."
          Just QualName VName
fname ->
            Doc ann
"Cannot apply"
              forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty QualName VName
fname)
              forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"to"
              forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes (forall ann. Doc ann -> Doc ann
align forall a b. (a -> b) -> a -> b
$ 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
e) forall a. Semigroup a => a -> a -> a
<> Doc ann
" (invalid type)."
  pretty (CheckingReturn StructType
expected StructType
actual) =
    Doc ann
"Function body does not have expected type."
      forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ann
"Expected:"
      forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
align (forall a ann. Pretty a => a -> Doc ann
pretty StructType
expected)
      forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ann
"Actual:  "
      forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
align (forall a ann. Pretty a => a -> Doc ann
pretty StructType
actual)
  pretty (CheckingAscription StructType
expected StructType
actual) =
    Doc ann
"Expression does not have expected type from explicit ascription."
      forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ann
"Expected:"
      forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
align (forall a ann. Pretty a => a -> Doc ann
pretty StructType
expected)
      forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ann
"Actual:  "
      forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
align (forall a ann. Pretty a => a -> Doc ann
pretty StructType
actual)
  pretty (CheckingLetGeneralise Name
fname) =
    Doc ann
"Cannot generalise type of" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty Name
fname) forall a. Semigroup a => a -> a -> a
<> Doc ann
"."
  pretty (CheckingParams Maybe Name
fname) =
    Doc ann
"Invalid use of parameters in" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes forall {ann}. Doc ann
fname' forall a. Semigroup a => a -> a -> a
<> Doc ann
"."
    where
      fname' :: Doc ann
fname' = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc ann
"anonymous function" forall a ann. Pretty a => a -> Doc ann
pretty Maybe Name
fname
  pretty (CheckingPat UncheckedPat
pat InferredType
NoneInferred) =
    Doc ann
"Invalid pattern" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty UncheckedPat
pat) forall a. Semigroup a => a -> a -> a
<> Doc ann
"."
  pretty (CheckingPat UncheckedPat
pat (Ascribed PatType
t)) =
    Doc ann
"Pat"
      forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty UncheckedPat
pat)
      forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"cannot match value of 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
t)
  pretty (CheckingLoopBody StructType
expected StructType
actual) =
    Doc ann
"Loop body does not have expected type."
      forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ann
"Expected:"
      forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
align (forall a ann. Pretty a => a -> Doc ann
pretty StructType
expected)
      forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ann
"Actual:  "
      forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
align (forall a ann. Pretty a => a -> Doc ann
pretty StructType
actual)
  pretty (CheckingLoopInitial StructType
expected StructType
actual) =
    Doc ann
"Initial loop values do not have expected type."
      forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ann
"Expected:"
      forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
align (forall a ann. Pretty a => a -> Doc ann
pretty StructType
expected)
      forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ann
"Actual:  "
      forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
align (forall a ann. Pretty a => a -> Doc ann
pretty StructType
actual)
  pretty (CheckingRecordUpdate [Name]
fs StructType
expected StructType
actual) =
    Doc ann
"Type mismatch when updating record field"
      forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes forall {ann}. Doc ann
fs' forall a. Semigroup a => a -> a -> a
<> Doc ann
"."
      forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ann
"Existing:"
      forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
align (forall a ann. Pretty a => a -> Doc ann
pretty StructType
expected)
      forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ann
"New:     "
      forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
align (forall a ann. Pretty a => a -> Doc ann
pretty StructType
actual)
    where
      fs' :: Doc ann
fs' = forall a. Monoid a => [a] -> a
mconcat forall a b. (a -> b) -> a -> b
$ forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate Doc ann
"." forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [Name]
fs
  pretty (CheckingRequired [StructType
expected] StructType
actual) =
    Doc ann
"Expression must must have type"
      forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty StructType
expected forall a. Semigroup a => a -> a -> a
<> Doc ann
"."
      forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ann
"Actual type:"
      forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
align (forall a ann. Pretty a => a -> Doc ann
pretty StructType
actual)
  pretty (CheckingRequired [StructType]
expected StructType
actual) =
    Doc ann
"Type of expression must must be one of "
      forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall {ann}. Doc ann
expected' forall a. Semigroup a => a -> a -> a
<> Doc ann
"."
      forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ann
"Actual type:"
      forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
align (forall a ann. Pretty a => a -> Doc ann
pretty StructType
actual)
    where
      expected' :: Doc a
expected' = forall a. [Doc a] -> Doc a
commasep (forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [StructType]
expected)
  pretty (CheckingBranches StructType
t1 StructType
t2) =
    Doc ann
"Branches differ in type."
      forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ann
"Former:"
      forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty StructType
t1
      forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ann
"Latter:"
      forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty StructType
t2

-- | Type checking happens with access to this environment.  The
-- 'TermScope' will be extended during type-checking as bindings come into
-- scope.
data TermEnv = TermEnv
  { TermEnv -> TermScope
termScope :: TermScope,
    TermEnv -> Maybe Checking
termChecking :: Maybe Checking,
    TermEnv -> Int
termLevel :: Level
  }

data TermScope = TermScope
  { TermScope -> Map VName ValBinding
scopeVtable :: M.Map VName ValBinding,
    TermScope -> Map VName TypeBinding
scopeTypeTable :: M.Map VName TypeBinding,
    TermScope -> Map VName Mod
scopeModTable :: M.Map VName Mod,
    TermScope -> NameMap
scopeNameMap :: NameMap
  }
  deriving (Int -> TermScope -> ShowS
[TermScope] -> ShowS
TermScope -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TermScope] -> ShowS
$cshowList :: [TermScope] -> ShowS
show :: TermScope -> String
$cshow :: TermScope -> String
showsPrec :: Int -> TermScope -> ShowS
$cshowsPrec :: Int -> TermScope -> ShowS
Show)

instance Semigroup TermScope where
  TermScope Map VName ValBinding
vt1 Map VName TypeBinding
tt1 Map VName Mod
mt1 NameMap
nt1 <> :: TermScope -> TermScope -> TermScope
<> TermScope Map VName ValBinding
vt2 Map VName TypeBinding
tt2 Map VName Mod
mt2 NameMap
nt2 =
    Map VName ValBinding
-> Map VName TypeBinding -> Map VName Mod -> NameMap -> TermScope
TermScope (Map VName ValBinding
vt2 forall k a. Ord k => Map k a -> Map k a -> Map k a
`M.union` Map VName ValBinding
vt1) (Map VName TypeBinding
tt2 forall k a. Ord k => Map k a -> Map k a -> Map k a
`M.union` Map VName TypeBinding
tt1) (Map VName Mod
mt1 forall k a. Ord k => Map k a -> Map k a -> Map k a
`M.union` Map VName Mod
mt2) (NameMap
nt2 forall k a. Ord k => Map k a -> Map k a -> Map k a
`M.union` NameMap
nt1)

envToTermScope :: Env -> TermScope
envToTermScope :: Env -> TermScope
envToTermScope Env
env =
  TermScope
    { scopeVtable :: Map VName ValBinding
scopeVtable = Map VName ValBinding
vtable,
      scopeTypeTable :: Map VName TypeBinding
scopeTypeTable = Env -> Map VName TypeBinding
envTypeTable Env
env,
      scopeNameMap :: NameMap
scopeNameMap = Env -> NameMap
envNameMap Env
env,
      scopeModTable :: Map VName Mod
scopeModTable = Env -> Map VName Mod
envModTable Env
env
    }
  where
    vtable :: Map VName ValBinding
vtable = forall k a b. (k -> a -> b) -> Map k a -> Map k b
M.mapWithKey VName -> BoundV -> ValBinding
valBinding forall a b. (a -> b) -> a -> b
$ Env -> Map VName BoundV
envVtable Env
env
    valBinding :: VName -> BoundV -> ValBinding
valBinding VName
k (TypeM.BoundV [TypeParam]
tps StructType
v) =
      Locality -> [TypeParam] -> PatType -> ValBinding
BoundV Locality
Global [TypeParam]
tps forall a b. (a -> b) -> a -> b
$ forall {as} {dim} {as}.
Monoid as =>
as -> TypeBase dim as -> TypeBase dim as
selfAliasing (forall a. a -> Set a
S.singleton (VName -> Alias
AliasBound VName
k)) StructType
v
    -- FIXME: hack, #1675
    selfAliasing :: as -> TypeBase dim as -> TypeBase dim as
selfAliasing as
als (Scalar (Record Map Name (TypeBase dim as)
ts)) =
      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 (as -> TypeBase dim as -> TypeBase dim as
selfAliasing as
als) Map Name (TypeBase dim as)
ts
    selfAliasing as
als TypeBase dim as
t =
      TypeBase dim as
t forall dim asf ast. TypeBase dim asf -> ast -> TypeBase dim ast
`setAliases` (if forall dim as. TypeBase dim as -> Int
arrayRank TypeBase dim as
t forall a. Ord a => a -> a -> Bool
> Int
0 then as
als else forall a. Monoid a => a
mempty)

withEnv :: TermEnv -> Env -> TermEnv
withEnv :: TermEnv -> Env -> TermEnv
withEnv TermEnv
tenv Env
env = TermEnv
tenv {termScope :: TermScope
termScope = TermEnv -> TermScope
termScope TermEnv
tenv forall a. Semigroup a => a -> a -> a
<> Env -> TermScope
envToTermScope Env
env}

-- | Wrap a function name to give it a vacuous Eq instance for SizeSource.
newtype FName = FName (Maybe (QualName VName))
  deriving (Int -> FName -> ShowS
[FName] -> ShowS
FName -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FName] -> ShowS
$cshowList :: [FName] -> ShowS
show :: FName -> String
$cshow :: FName -> String
showsPrec :: Int -> FName -> ShowS
$cshowsPrec :: Int -> FName -> ShowS
Show)

instance Eq FName where
  FName
_ == :: FName -> FName -> Bool
== FName
_ = Bool
True

instance Ord FName where
  compare :: FName -> FName -> Ordering
compare FName
_ FName
_ = Ordering
EQ

-- | What was the source of some existential size?  This is used for
-- using the same existential variable if the same source is
-- encountered in multiple locations.
data SizeSource
  = SourceArg FName (ExpBase NoInfo VName)
  | SourceBound (ExpBase NoInfo VName)
  | SourceSlice
      (Maybe Size)
      (Maybe (ExpBase NoInfo VName))
      (Maybe (ExpBase NoInfo VName))
      (Maybe (ExpBase NoInfo VName))
  deriving (SizeSource -> SizeSource -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SizeSource -> SizeSource -> Bool
$c/= :: SizeSource -> SizeSource -> Bool
== :: SizeSource -> SizeSource -> Bool
$c== :: SizeSource -> SizeSource -> Bool
Eq, Eq SizeSource
SizeSource -> SizeSource -> Bool
SizeSource -> SizeSource -> Ordering
SizeSource -> SizeSource -> SizeSource
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: SizeSource -> SizeSource -> SizeSource
$cmin :: SizeSource -> SizeSource -> SizeSource
max :: SizeSource -> SizeSource -> SizeSource
$cmax :: SizeSource -> SizeSource -> SizeSource
>= :: SizeSource -> SizeSource -> Bool
$c>= :: SizeSource -> SizeSource -> Bool
> :: SizeSource -> SizeSource -> Bool
$c> :: SizeSource -> SizeSource -> Bool
<= :: SizeSource -> SizeSource -> Bool
$c<= :: SizeSource -> SizeSource -> Bool
< :: SizeSource -> SizeSource -> Bool
$c< :: SizeSource -> SizeSource -> Bool
compare :: SizeSource -> SizeSource -> Ordering
$ccompare :: SizeSource -> SizeSource -> Ordering
Ord, Int -> SizeSource -> ShowS
[SizeSource] -> ShowS
SizeSource -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SizeSource] -> ShowS
$cshowList :: [SizeSource] -> ShowS
show :: SizeSource -> String
$cshow :: SizeSource -> String
showsPrec :: Int -> SizeSource -> ShowS
$cshowsPrec :: Int -> SizeSource -> ShowS
Show)

-- | A description of where an artificial compiler-generated
-- intermediate name came from.
data NameReason
  = -- | Name is the result of a function application.
    NameAppRes (Maybe (QualName VName)) SrcLoc

nameReason :: SrcLoc -> NameReason -> Doc a
nameReason :: forall a. SrcLoc -> NameReason -> Doc a
nameReason SrcLoc
loc (NameAppRes Maybe (QualName VName)
Nothing SrcLoc
apploc) =
  Doc a
"result of application 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 SrcLoc
loc SrcLoc
apploc)
nameReason SrcLoc
loc (NameAppRes Maybe (QualName VName)
fname SrcLoc
apploc) =
  Doc a
"result of applying"
    forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty Maybe (QualName VName)
fname)
    forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
parens (Doc a
"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 SrcLoc
loc SrcLoc
apploc))

-- | The state is a set of constraints and a counter for generating
-- type names.  This is distinct from the usual counter we use for
-- generating unique names, as these will be user-visible.
data TermTypeState = TermTypeState
  { TermTypeState -> Constraints
stateConstraints :: Constraints,
    TermTypeState -> Int
stateCounter :: !Int,
    -- | Mapping function arguments encountered to
    -- the sizes they ended up generating (when
    -- they could not be substituted directly).
    -- This happens for function arguments that are
    -- not constants or names.
    TermTypeState -> Map SizeSource VName
stateDimTable :: M.Map SizeSource VName,
    TermTypeState -> Map VName NameReason
stateNames :: M.Map VName NameReason,
    TermTypeState -> Occurrences
stateOccs :: Occurrences
  }

newtype TermTypeM a
  = TermTypeM (ReaderT TermEnv (StateT TermTypeState TypeM) a)
  deriving
    ( Applicative TermTypeM
forall a. a -> TermTypeM a
forall a b. TermTypeM a -> TermTypeM b -> TermTypeM b
forall a b. TermTypeM a -> (a -> TermTypeM b) -> TermTypeM b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: forall a. a -> TermTypeM a
$creturn :: forall a. a -> TermTypeM a
>> :: forall a b. TermTypeM a -> TermTypeM b -> TermTypeM b
$c>> :: forall a b. TermTypeM a -> TermTypeM b -> TermTypeM b
>>= :: forall a b. TermTypeM a -> (a -> TermTypeM b) -> TermTypeM b
$c>>= :: forall a b. TermTypeM a -> (a -> TermTypeM b) -> TermTypeM b
Monad,
      forall a b. a -> TermTypeM b -> TermTypeM a
forall a b. (a -> b) -> TermTypeM a -> TermTypeM 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 -> TermTypeM b -> TermTypeM a
$c<$ :: forall a b. a -> TermTypeM b -> TermTypeM a
fmap :: forall a b. (a -> b) -> TermTypeM a -> TermTypeM b
$cfmap :: forall a b. (a -> b) -> TermTypeM a -> TermTypeM b
Functor,
      Functor TermTypeM
forall a. a -> TermTypeM a
forall a b. TermTypeM a -> TermTypeM b -> TermTypeM a
forall a b. TermTypeM a -> TermTypeM b -> TermTypeM b
forall a b. TermTypeM (a -> b) -> TermTypeM a -> TermTypeM b
forall a b c.
(a -> b -> c) -> TermTypeM a -> TermTypeM b -> TermTypeM c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: forall a b. TermTypeM a -> TermTypeM b -> TermTypeM a
$c<* :: forall a b. TermTypeM a -> TermTypeM b -> TermTypeM a
*> :: forall a b. TermTypeM a -> TermTypeM b -> TermTypeM b
$c*> :: forall a b. TermTypeM a -> TermTypeM b -> TermTypeM b
liftA2 :: forall a b c.
(a -> b -> c) -> TermTypeM a -> TermTypeM b -> TermTypeM c
$cliftA2 :: forall a b c.
(a -> b -> c) -> TermTypeM a -> TermTypeM b -> TermTypeM c
<*> :: forall a b. TermTypeM (a -> b) -> TermTypeM a -> TermTypeM b
$c<*> :: forall a b. TermTypeM (a -> b) -> TermTypeM a -> TermTypeM b
pure :: forall a. a -> TermTypeM a
$cpure :: forall a. a -> TermTypeM a
Applicative,
      MonadReader TermEnv,
      MonadState TermTypeState,
      MonadError TypeError
    )

liftTypeM :: TypeM a -> TermTypeM a
liftTypeM :: forall a. TypeM a -> TermTypeM a
liftTypeM = forall a.
ReaderT TermEnv (StateT TermTypeState TypeM) a -> TermTypeM a
TermTypeM forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift

incCounter :: TermTypeM Int
incCounter :: TermTypeM Int
incCounter = do
  TermTypeState
s <- forall s (m :: * -> *). MonadState s m => m s
get
  forall s (m :: * -> *). MonadState s m => s -> m ()
put TermTypeState
s {stateCounter :: Int
stateCounter = TermTypeState -> Int
stateCounter TermTypeState
s forall a. Num a => a -> a -> a
+ Int
1}
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ TermTypeState -> Int
stateCounter TermTypeState
s

constrain :: VName -> Constraint -> TermTypeM ()
constrain :: VName -> Constraint -> TermTypeM ()
constrain VName
v Constraint
c = do
  Int
lvl <- forall (m :: * -> *). MonadUnify m => m Int
curLevel
  forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
v (Int
lvl, Constraint
c)

instance MonadUnify TermTypeM where
  getConstraints :: TermTypeM Constraints
getConstraints = forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TermTypeState -> Constraints
stateConstraints
  putConstraints :: Constraints -> TermTypeM ()
putConstraints Constraints
x = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \TermTypeState
s -> TermTypeState
s {stateConstraints :: Constraints
stateConstraints = Constraints
x}

  newTypeVar :: forall als dim.
Monoid als =>
SrcLoc -> Name -> TermTypeM (TypeBase dim als)
newTypeVar SrcLoc
loc Name
desc = do
    Int
i <- TermTypeM Int
incCounter
    VName
v <- forall (m :: * -> *). MonadTypeChecker m => Name -> m VName
newID forall a b. (a -> b) -> a -> b
$ Name -> Int -> Name
mkTypeVarName Name
desc Int
i
    VName -> Constraint -> TermTypeM ()
constrain VName
v forall a b. (a -> b) -> a -> b
$ Liftedness -> Usage -> Constraint
NoConstraint Liftedness
Lifted forall a b. (a -> b) -> a -> b
$ SrcLoc -> Usage
mkUsage' SrcLoc
loc
    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
Nonunique (forall v. v -> QualName v
qualName VName
v) []

  curLevel :: TermTypeM Int
curLevel = forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks TermEnv -> Int
termLevel

  newDimVar :: SrcLoc -> Rigidity -> Name -> TermTypeM VName
newDimVar SrcLoc
loc Rigidity
rigidity Name
name = do
    VName
dim <- forall (m :: * -> *). MonadTypeChecker m => Name -> m VName
newTypeName Name
name
    case Rigidity
rigidity of
      Rigid RigidSource
rsrc -> VName -> Constraint -> TermTypeM ()
constrain VName
dim forall a b. (a -> b) -> a -> b
$ SrcLoc -> RigidSource -> Constraint
UnknowableSize SrcLoc
loc RigidSource
rsrc
      Rigidity
Nonrigid -> VName -> Constraint -> TermTypeM ()
constrain VName
dim forall a b. (a -> b) -> a -> b
$ Maybe Size -> Usage -> Constraint
Size forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ SrcLoc -> Usage
mkUsage' SrcLoc
loc
    forall (f :: * -> *) a. Applicative f => a -> f a
pure VName
dim

  unifyError :: forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> Doc () -> TermTypeM a
unifyError loc
loc Notes
notes BreadCrumbs
bcs Doc ()
doc = do
    Maybe Checking
checking <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks TermEnv -> Maybe Checking
termChecking
    case Maybe Checking
checking of
      Just Checking
checking' ->
        forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$
          Loc -> Notes -> Doc () -> TypeError
TypeError (forall a. Located a => a -> Loc
locOf loc
loc) Notes
notes forall a b. (a -> b) -> a -> b
$
            forall a ann. Pretty a => a -> Doc ann
pretty Checking
checking' forall a. Semigroup a => a -> a -> a
<> forall {ann}. Doc ann
line forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
doc forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty BreadCrumbs
bcs
      Maybe Checking
Nothing ->
        forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ Loc -> Notes -> Doc () -> TypeError
TypeError (forall a. Located a => a -> Loc
locOf loc
loc) Notes
notes forall a b. (a -> b) -> a -> b
$ Doc ()
doc forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty BreadCrumbs
bcs

  matchError :: forall loc a.
Located loc =>
loc
-> Notes -> BreadCrumbs -> StructType -> StructType -> TermTypeM a
matchError loc
loc Notes
notes BreadCrumbs
bcs StructType
t1 StructType
t2 = do
    Maybe Checking
checking <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks TermEnv -> Maybe Checking
termChecking
    case Maybe Checking
checking of
      Just Checking
checking'
        | BreadCrumbs -> Bool
hasNoBreadCrumbs BreadCrumbs
bcs ->
            forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$
              Loc -> Notes -> Doc () -> TypeError
TypeError (forall a. Located a => a -> Loc
locOf loc
loc) Notes
notes forall a b. (a -> b) -> a -> b
$
                forall a ann. Pretty a => a -> Doc ann
pretty Checking
checking'
        | Bool
otherwise ->
            forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$
              Loc -> Notes -> Doc () -> TypeError
TypeError (forall a. Located a => a -> Loc
locOf loc
loc) Notes
notes forall a b. (a -> b) -> a -> b
$
                forall a ann. Pretty a => a -> Doc ann
pretty Checking
checking' forall a. Semigroup a => a -> a -> a
<> forall {ann}. Doc ann
line forall ann. Doc ann -> Doc ann -> Doc ann
</> forall {ann}. Doc ann
doc forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty BreadCrumbs
bcs
      Maybe Checking
Nothing ->
        forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ Loc -> Notes -> Doc () -> TypeError
TypeError (forall a. Located a => a -> Loc
locOf loc
loc) Notes
notes forall a b. (a -> b) -> a -> b
$ forall {ann}. Doc ann
doc forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty BreadCrumbs
bcs
    where
      doc :: Doc a
doc =
        Doc a
"Types"
          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 StructType
t1)
          forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc a
"and"
          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 StructType
t2)
          forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc a
"do not match."

-- | Instantiate a type scheme with fresh type variables for its type
-- parameters. Returns the names of the fresh type variables, the
-- instance list, and the instantiated type.
instantiateTypeScheme ::
  QualName VName ->
  SrcLoc ->
  [TypeParam] ->
  PatType ->
  TermTypeM ([VName], PatType)
instantiateTypeScheme :: QualName VName
-> SrcLoc -> [TypeParam] -> PatType -> TermTypeM ([VName], PatType)
instantiateTypeScheme QualName VName
qn SrcLoc
loc [TypeParam]
tparams PatType
t = do
  let tnames :: [VName]
tnames = forall a b. (a -> b) -> [a] -> [b]
map forall vn. TypeParamBase vn -> vn
typeParamName [TypeParam]
tparams
  ([VName]
tparam_names, [Subst (RetTypeBase Size ())]
tparam_substs) <- forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM (forall as dim.
Monoid as =>
QualName VName
-> SrcLoc
-> TypeParam
-> TermTypeM (VName, Subst (RetTypeBase dim as))
instantiateTypeParam QualName VName
qn SrcLoc
loc) [TypeParam]
tparams
  let substs :: Map VName (Subst (RetTypeBase Size ()))
substs = 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 [VName]
tnames [Subst (RetTypeBase Size ())]
tparam_substs
      t' :: PatType
t' = forall a. Substitutable a => TypeSubs -> a -> a
applySubst (forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` Map VName (Subst (RetTypeBase Size ()))
substs) PatType
t
  forall (f :: * -> *) a. Applicative f => a -> f a
pure ([VName]
tparam_names, PatType
t')

-- | Create a new type name and insert it (unconstrained) in the
-- substitution map.
instantiateTypeParam ::
  Monoid as =>
  QualName VName ->
  SrcLoc ->
  TypeParam ->
  TermTypeM (VName, Subst (RetTypeBase dim as))
instantiateTypeParam :: forall as dim.
Monoid as =>
QualName VName
-> SrcLoc
-> TypeParam
-> TermTypeM (VName, Subst (RetTypeBase dim as))
instantiateTypeParam QualName VName
qn SrcLoc
loc TypeParam
tparam = do
  Int
i <- TermTypeM Int
incCounter
  let name :: Name
name = String -> Name
nameFromString (forall a. (a -> Bool) -> [a] -> [a]
takeWhile Char -> Bool
isAscii (VName -> String
baseString (forall vn. TypeParamBase vn -> vn
typeParamName TypeParam
tparam)))
  VName
v <- forall (m :: * -> *). MonadTypeChecker m => Name -> m VName
newID forall a b. (a -> b) -> a -> b
$ Name -> Int -> Name
mkTypeVarName Name
name Int
i
  case TypeParam
tparam of
    TypeParamType Liftedness
x VName
_ SrcLoc
_ -> do
      VName -> Constraint -> TermTypeM ()
constrain VName
v forall b c a. (b -> c) -> (a -> b) -> a -> c
. Liftedness -> Usage -> Constraint
NoConstraint Liftedness
x forall b c a. (b -> c) -> (a -> b) -> a -> c
. SrcLoc -> Text -> Usage
mkUsage SrcLoc
loc forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Doc a -> Text
docText forall a b. (a -> b) -> a -> b
$
        Doc Any
"instantiated type parameter of " forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty QualName VName
qn)
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (VName
v, forall t. [TypeParam] -> t -> Subst t
Subst [] 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
-> Uniqueness
-> QualName VName
-> [TypeArg dim]
-> ScalarTypeBase dim as
TypeVar forall a. Monoid a => a
mempty Uniqueness
Nonunique (forall v. v -> QualName v
qualName VName
v) [])
    TypeParamDim {} -> do
      VName -> Constraint -> TermTypeM ()
constrain VName
v forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Size -> Usage -> Constraint
Size forall a. Maybe a
Nothing forall b c a. (b -> c) -> (a -> b) -> a -> c
. SrcLoc -> Text -> Usage
mkUsage SrcLoc
loc forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Doc a -> Text
docText forall a b. (a -> b) -> a -> b
$
        Doc Any
"instantiated size parameter of " forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty QualName VName
qn)
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (VName
v, forall t. Size -> Subst t
SizeSubst 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)

checkQualNameWithEnv :: Namespace -> QualName Name -> SrcLoc -> TermTypeM (TermScope, QualName VName)
checkQualNameWithEnv :: Namespace
-> QualName Name -> SrcLoc -> TermTypeM (TermScope, QualName VName)
checkQualNameWithEnv Namespace
space qn :: QualName Name
qn@(QualName [Name]
quals Name
name) SrcLoc
loc = do
  TermScope
scope <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks TermEnv -> TermScope
termScope
  TermScope -> [Name] -> TermTypeM (TermScope, QualName VName)
descend TermScope
scope [Name]
quals
  where
    descend :: TermScope -> [Name] -> TermTypeM (TermScope, QualName VName)
descend TermScope
scope []
      | Just QualName VName
name' <- forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Namespace
space, Name
name) forall a b. (a -> b) -> a -> b
$ TermScope -> NameMap
scopeNameMap TermScope
scope =
          forall (f :: * -> *) a. Applicative f => a -> f a
pure (TermScope
scope, QualName VName
name')
      | Bool
otherwise =
          forall (m :: * -> *) a.
MonadTypeChecker m =>
Namespace -> QualName Name -> SrcLoc -> m a
unknownVariable Namespace
space QualName Name
qn SrcLoc
loc
    descend TermScope
scope (Name
q : [Name]
qs)
      | Just (QualName [VName]
_ VName
q') <- forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Namespace
Term, Name
q) forall a b. (a -> b) -> a -> b
$ TermScope -> NameMap
scopeNameMap TermScope
scope,
        Just Mod
res <- forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
q' forall a b. (a -> b) -> a -> b
$ TermScope -> Map VName Mod
scopeModTable TermScope
scope =
          case Mod
res of
            -- Check if we are referring to the magical intrinsics
            -- module.
            Mod
_
              | VName -> Int
baseTag VName
q' forall a. Ord a => a -> a -> Bool
<= Int
maxIntrinsicTag ->
                  Namespace
-> QualName Name -> SrcLoc -> TermTypeM (TermScope, QualName VName)
checkIntrinsic Namespace
space QualName Name
qn SrcLoc
loc
            ModEnv Env
q_scope -> do
              (TermScope
scope', QualName [VName]
qs' VName
name') <- TermScope -> [Name] -> TermTypeM (TermScope, QualName VName)
descend (Env -> TermScope
envToTermScope Env
q_scope) [Name]
qs
              forall (f :: * -> *) a. Applicative f => a -> f a
pure (TermScope
scope', forall vn. [vn] -> vn -> QualName vn
QualName (VName
q' forall a. a -> [a] -> [a]
: [VName]
qs') VName
name')
            ModFun {} -> forall (m :: * -> *) a. MonadTypeChecker m => SrcLoc -> m a
unappliedFunctor SrcLoc
loc
      | Bool
otherwise =
          forall (m :: * -> *) a.
MonadTypeChecker m =>
Namespace -> QualName Name -> SrcLoc -> m a
unknownVariable Namespace
space QualName Name
qn SrcLoc
loc

checkIntrinsic :: Namespace -> QualName Name -> SrcLoc -> TermTypeM (TermScope, QualName VName)
checkIntrinsic :: Namespace
-> QualName Name -> SrcLoc -> TermTypeM (TermScope, QualName VName)
checkIntrinsic Namespace
space qn :: QualName Name
qn@(QualName [Name]
_ Name
name) SrcLoc
loc
  | Just QualName VName
v <- forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Namespace
space, Name
name) NameMap
intrinsicsNameMap = do
      ImportName
me <- forall a. TypeM a -> TermTypeM a
liftTypeM TypeM ImportName
askImportName
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (String -> Bool
isBuiltin (ImportName -> String
includeToFilePath ImportName
me)) forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *) loc.
(MonadTypeChecker m, Located loc) =>
loc -> Doc () -> m ()
warn SrcLoc
loc Doc ()
"Using intrinsic functions directly can easily crash the compiler or result in wrong code generation."
      TermScope
scope <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks TermEnv -> TermScope
termScope
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (TermScope
scope, QualName VName
v)
  | Bool
otherwise =
      forall (m :: * -> *) a.
MonadTypeChecker m =>
Namespace -> QualName Name -> SrcLoc -> m a
unknownVariable Namespace
space QualName Name
qn SrcLoc
loc

localScope :: (TermScope -> TermScope) -> TermTypeM a -> TermTypeM a
localScope :: forall a. (TermScope -> TermScope) -> TermTypeM a -> TermTypeM a
localScope TermScope -> TermScope
f = forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local forall a b. (a -> b) -> a -> b
$ \TermEnv
tenv -> TermEnv
tenv {termScope :: TermScope
termScope = TermScope -> TermScope
f forall a b. (a -> b) -> a -> b
$ TermEnv -> TermScope
termScope TermEnv
tenv}

instance MonadTypeChecker TermTypeM where
  warn :: forall loc. Located loc => loc -> Doc () -> TermTypeM ()
warn loc
loc Doc ()
problem = forall a. TypeM a -> TermTypeM a
liftTypeM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) loc.
(MonadTypeChecker m, Located loc) =>
loc -> Doc () -> m ()
warn loc
loc Doc ()
problem
  newName :: VName -> TermTypeM VName
newName = forall a. TypeM a -> TermTypeM a
liftTypeM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadTypeChecker m => VName -> m VName
newName
  newID :: Name -> TermTypeM VName
newID = forall a. TypeM a -> TermTypeM a
liftTypeM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadTypeChecker m => Name -> m VName
newID

  newTypeName :: Name -> TermTypeM VName
newTypeName Name
name = do
    Int
i <- TermTypeM Int
incCounter
    forall (m :: * -> *). MonadTypeChecker m => Name -> m VName
newID forall a b. (a -> b) -> a -> b
$ Name -> Int -> Name
mkTypeVarName Name
name Int
i

  checkQualName :: Namespace -> QualName Name -> SrcLoc -> TermTypeM (QualName VName)
checkQualName Namespace
space QualName Name
name SrcLoc
loc = forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Namespace
-> QualName Name -> SrcLoc -> TermTypeM (TermScope, QualName VName)
checkQualNameWithEnv Namespace
space QualName Name
name SrcLoc
loc

  bindNameMap :: forall a. NameMap -> TermTypeM a -> TermTypeM a
bindNameMap NameMap
m = forall a. (TermScope -> TermScope) -> TermTypeM a -> TermTypeM a
localScope forall a b. (a -> b) -> a -> b
$ \TermScope
scope ->
    TermScope
scope {scopeNameMap :: NameMap
scopeNameMap = NameMap
m forall a. Semigroup a => a -> a -> a
<> TermScope -> NameMap
scopeNameMap TermScope
scope}

  bindVal :: forall a. VName -> BoundV -> TermTypeM a -> TermTypeM a
bindVal VName
v (TypeM.BoundV [TypeParam]
tps StructType
t) = forall a. (TermScope -> TermScope) -> TermTypeM a -> TermTypeM a
localScope forall a b. (a -> b) -> a -> b
$ \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
v ValBinding
vb forall a b. (a -> b) -> a -> b
$ TermScope -> Map VName ValBinding
scopeVtable TermScope
scope}
    where
      vb :: ValBinding
vb = Locality -> [TypeParam] -> PatType -> ValBinding
BoundV Locality
Local [TypeParam]
tps forall a b. (a -> b) -> a -> b
$ forall dim as. TypeBase dim as -> TypeBase dim Aliasing
fromStruct StructType
t

  lookupType :: SrcLoc
-> QualName Name
-> TermTypeM
     (QualName VName, [TypeParam], RetTypeBase Size (), Liftedness)
lookupType SrcLoc
loc QualName Name
qn = do
    Env
outer_env <- forall a. TypeM a -> TermTypeM a
liftTypeM TypeM Env
askEnv
    (TermScope
scope, qn' :: QualName VName
qn'@(QualName [VName]
qs VName
name)) <- Namespace
-> QualName Name -> SrcLoc -> TermTypeM (TermScope, QualName VName)
checkQualNameWithEnv Namespace
Type QualName Name
qn SrcLoc
loc
    case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
name forall a b. (a -> b) -> a -> b
$ TermScope -> Map VName TypeBinding
scopeTypeTable TermScope
scope of
      Maybe TypeBinding
Nothing -> forall (m :: * -> *) a.
MonadTypeChecker m =>
SrcLoc -> QualName Name -> m a
unknownType SrcLoc
loc QualName Name
qn
      Just (TypeAbbr Liftedness
l [TypeParam]
ps (RetType [VName]
dims StructType
def)) ->
        forall (f :: * -> *) a. Applicative f => a -> f a
pure
          ( QualName VName
qn',
            [TypeParam]
ps,
            forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
dims forall a b. (a -> b) -> a -> b
$ forall as.
Env -> [VName] -> [VName] -> TypeBase Size as -> TypeBase Size as
qualifyTypeVars Env
outer_env (forall a b. (a -> b) -> [a] -> [b]
map forall vn. TypeParamBase vn -> vn
typeParamName [TypeParam]
ps) [VName]
qs StructType
def,
            Liftedness
l
          )

  lookupMod :: SrcLoc -> QualName Name -> TermTypeM (QualName VName, Mod)
lookupMod SrcLoc
loc QualName Name
qn = do
    (TermScope
scope, qn' :: QualName VName
qn'@(QualName [VName]
_ VName
name)) <- Namespace
-> QualName Name -> SrcLoc -> TermTypeM (TermScope, QualName VName)
checkQualNameWithEnv Namespace
Term QualName Name
qn SrcLoc
loc
    case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
name forall a b. (a -> b) -> a -> b
$ TermScope -> Map VName Mod
scopeModTable TermScope
scope of
      Maybe Mod
Nothing -> forall (m :: * -> *) a.
MonadTypeChecker m =>
Namespace -> QualName Name -> SrcLoc -> m a
unknownVariable Namespace
Term QualName Name
qn SrcLoc
loc
      Just Mod
m -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (QualName VName
qn', Mod
m)

  lookupVar :: SrcLoc -> QualName Name -> TermTypeM (QualName VName, PatType)
lookupVar SrcLoc
loc QualName Name
qn = do
    Env
outer_env <- forall a. TypeM a -> TermTypeM a
liftTypeM TypeM Env
askEnv
    (TermScope
scope, qn' :: QualName VName
qn'@(QualName [VName]
qs VName
name)) <- Namespace
-> QualName Name -> SrcLoc -> TermTypeM (TermScope, QualName VName)
checkQualNameWithEnv Namespace
Term QualName Name
qn SrcLoc
loc
    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
"use of " forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty QualName Name
qn)

    PatType
t <- case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
name forall a b. (a -> b) -> a -> b
$ TermScope -> Map VName ValBinding
scopeVtable TermScope
scope of
      Maybe ValBinding
Nothing ->
        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 ()
"Unknown variable" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty QualName Name
qn) forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
      Just (WasConsumed SrcLoc
wloc) -> forall a. VName -> SrcLoc -> SrcLoc -> TermTypeM a
useAfterConsume VName
name SrcLoc
loc SrcLoc
wloc
      Just (BoundV Locality
_ [TypeParam]
tparams PatType
t)
        | String
"_" forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` VName -> String
baseString VName
name -> forall (m :: * -> *) a.
MonadTypeChecker m =>
SrcLoc -> QualName Name -> m a
underscoreUse SrcLoc
loc QualName Name
qn
        | Bool
otherwise -> do
            ([VName]
tnames, PatType
t') <- QualName VName
-> SrcLoc -> [TypeParam] -> PatType -> TermTypeM ([VName], PatType)
instantiateTypeScheme QualName VName
qn' SrcLoc
loc [TypeParam]
tparams PatType
t
            forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall as.
Env -> [VName] -> [VName] -> TypeBase Size as -> TypeBase Size as
qualifyTypeVars Env
outer_env [VName]
tnames [VName]
qs PatType
t'
      Just ValBinding
EqualityF -> do
        StructType
argtype <- forall (m :: * -> *) als dim.
(MonadUnify m, Monoid als) =>
SrcLoc -> Name -> m (TypeBase dim als)
newTypeVar SrcLoc
loc Name
"t"
        forall (m :: * -> *) dim as.
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage -> TypeBase dim as -> m ()
equalityType Usage
usage StructType
argtype
        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 b c a. (b -> c) -> (a -> b) -> a -> c
. forall dim as.
as
-> PName
-> Diet
-> TypeBase dim ()
-> RetTypeBase dim as
-> ScalarTypeBase dim as
Arrow forall a. Monoid a => a
mempty PName
Unnamed Diet
Observe StructType
argtype forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
-> Diet
-> TypeBase dim ()
-> RetTypeBase dim as
-> ScalarTypeBase dim as
Arrow forall a. Monoid a => a
mempty PName
Unnamed Diet
Observe StructType
argtype 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. PrimType -> ScalarTypeBase dim as
Prim PrimType
Bool
      Just (OverloadedF [PrimType]
ts [Maybe PrimType]
pts Maybe PrimType
rt) -> do
        StructType
argtype <- 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 -> StructType -> m ()
mustBeOneOf [PrimType]
ts Usage
usage StructType
argtype
        let ([StructType]
pts', StructType
rt') = forall {dim} {as}.
TypeBase dim as
-> [Maybe PrimType]
-> Maybe PrimType
-> ([TypeBase dim ()], TypeBase dim ())
instOverloaded StructType
argtype [Maybe PrimType]
pts Maybe PrimType
rt
            arrow :: TypeBase dim () -> TypeBase dim as -> TypeBase dim as
arrow TypeBase dim ()
xt TypeBase dim as
yt = forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as.
as
-> PName
-> Diet
-> TypeBase dim ()
-> RetTypeBase dim as
-> ScalarTypeBase dim as
Arrow forall a. Monoid a => a
mempty PName
Unnamed Diet
Observe TypeBase dim ()
xt forall a b. (a -> b) -> a -> b
$ forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [] TypeBase dim as
yt
        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall dim as. TypeBase dim as -> TypeBase dim Aliasing
fromStruct forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall {as} {dim}.
Monoid as =>
TypeBase dim () -> TypeBase dim as -> TypeBase dim as
arrow StructType
rt' [StructType]
pts'

    Ident -> TermTypeM ()
observe 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
t) SrcLoc
loc
    forall (f :: * -> *) a. Applicative f => a -> f a
pure (QualName VName
qn', PatType
t)
    where
      instOverloaded :: TypeBase dim as
-> [Maybe PrimType]
-> Maybe PrimType
-> ([TypeBase dim ()], TypeBase dim ())
instOverloaded TypeBase dim as
argtype [Maybe PrimType]
pts Maybe PrimType
rt =
        ( forall a b. (a -> b) -> [a] -> [b]
map (forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct TypeBase dim as
argtype) (forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall dim as. PrimType -> ScalarTypeBase dim as
Prim)) [Maybe PrimType]
pts,
          forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct TypeBase dim as
argtype) (forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall dim as. PrimType -> ScalarTypeBase dim as
Prim) Maybe PrimType
rt
        )

  checkNamedSize :: SrcLoc -> QualName Name -> TermTypeM (QualName VName)
checkNamedSize SrcLoc
loc QualName Name
v = do
    (QualName VName
v', PatType
t) <- forall (m :: * -> *).
MonadTypeChecker m =>
SrcLoc -> QualName Name -> m (QualName VName, PatType)
lookupVar SrcLoc
loc QualName Name
v
    forall a. Checking -> TermTypeM a -> TermTypeM a
onFailure ([StructType] -> StructType -> Checking
CheckingRequired [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 dim as. TypeBase dim as -> TypeBase dim ()
toStruct PatType
t)) forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify (SrcLoc -> Text -> Usage
mkUsage SrcLoc
loc Text
"use as array size") (forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct PatType
t) 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
Int64
    forall (f :: * -> *) a. Applicative f => a -> f a
pure QualName VName
v'

  typeError :: forall loc a. Located loc => loc -> Notes -> Doc () -> TermTypeM a
typeError loc
loc Notes
notes Doc ()
s = do
    Maybe Checking
checking <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks TermEnv -> Maybe Checking
termChecking
    case Maybe Checking
checking of
      Just Checking
checking' ->
        forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ Loc -> Notes -> Doc () -> TypeError
TypeError (forall a. Located a => a -> Loc
locOf loc
loc) Notes
notes (forall a ann. Pretty a => a -> Doc ann
pretty Checking
checking' forall a. Semigroup a => a -> a -> a
<> forall {ann}. Doc ann
line forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
s)
      Maybe Checking
Nothing ->
        forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ Loc -> Notes -> Doc () -> TypeError
TypeError (forall a. Located a => a -> Loc
locOf loc
loc) Notes
notes Doc ()
s

onFailure :: Checking -> TermTypeM a -> TermTypeM a
onFailure :: forall a. Checking -> TermTypeM a -> TermTypeM a
onFailure Checking
c = forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local forall a b. (a -> b) -> a -> b
$ \TermEnv
env -> TermEnv
env {termChecking :: Maybe Checking
termChecking = forall a. a -> Maybe a
Just Checking
c}

extSize :: SrcLoc -> SizeSource -> TermTypeM (Size, Maybe VName)
extSize :: SrcLoc -> SizeSource -> TermTypeM (Size, Maybe VName)
extSize SrcLoc
loc SizeSource
e = 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 SizeSource
e forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermTypeState -> Map SizeSource VName
stateDimTable
  case Maybe VName
prev of
    Maybe VName
Nothing -> do
      let rsrc :: RigidSource
rsrc = case SizeSource
e of
            SourceArg (FName Maybe (QualName VName)
fname) ExpBase NoInfo VName
e' ->
              Maybe (QualName VName) -> Text -> RigidSource
RigidArg Maybe (QualName VName)
fname forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Text
prettyTextOneLine ExpBase NoInfo VName
e'
            SourceBound ExpBase NoInfo VName
e' ->
              Text -> RigidSource
RigidBound forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Text
prettyTextOneLine ExpBase NoInfo VName
e'
            SourceSlice Maybe Size
d Maybe (ExpBase NoInfo VName)
i Maybe (ExpBase NoInfo VName)
j Maybe (ExpBase NoInfo VName)
s ->
              Maybe Size -> Text -> RigidSource
RigidSlice Maybe Size
d forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Text
prettyTextOneLine forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
Maybe (ExpBase f vn)
-> Maybe (ExpBase f vn)
-> Maybe (ExpBase f vn)
-> DimIndexBase f vn
DimSlice Maybe (ExpBase NoInfo VName)
i Maybe (ExpBase NoInfo VName)
j Maybe (ExpBase NoInfo VName)
s
      VName
d <- forall (m :: * -> *).
MonadUnify m =>
SrcLoc -> Rigidity -> Name -> m VName
newDimVar SrcLoc
loc (RigidSource -> Rigidity
Rigid RigidSource
rsrc) Name
"n"
      forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \TermTypeState
s -> TermTypeState
s {stateDimTable :: Map SizeSource VName
stateDimTable = forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert SizeSource
e VName
d forall a b. (a -> b) -> a -> b
$ TermTypeState -> Map SizeSource VName
stateDimTable TermTypeState
s}
      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
        )
    Just VName
d ->
      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
        )

incLevel :: TermTypeM a -> TermTypeM a
incLevel :: forall a. TermTypeM a -> TermTypeM a
incLevel = forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local forall a b. (a -> b) -> a -> b
$ \TermEnv
env -> TermEnv
env {termLevel :: Int
termLevel = TermEnv -> Int
termLevel TermEnv
env forall a. Num a => a -> a -> a
+ Int
1}

-- | Get the type of an expression, with top level type variables
-- substituted.  Never call 'typeOf' directly (except in a few
-- carefully inspected locations)!
expType :: Exp -> TermTypeM PatType
expType :: Exp -> TermTypeM PatType
expType = forall (m :: * -> *). MonadUnify m => PatType -> m PatType
normPatType forall b c a. (b -> c) -> (a -> b) -> a -> c
. Exp -> PatType
typeOf

-- | Get the type of an expression, with all type variables
-- substituted.  Slower than 'expType', but sometimes necessary.
-- Never call 'typeOf' directly (except in a few carefully inspected
-- locations)!
expTypeFully :: Exp -> TermTypeM PatType
expTypeFully :: Exp -> TermTypeM PatType
expTypeFully = forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully forall b c a. (b -> c) -> (a -> b) -> a -> c
. Exp -> PatType
typeOf

newArrayType :: SrcLoc -> Name -> Int -> TermTypeM (StructType, StructType)
newArrayType :: SrcLoc -> Name -> Int -> TermTypeM (StructType, StructType)
newArrayType SrcLoc
loc Name
desc Int
r = do
  VName
v <- forall (m :: * -> *). MonadTypeChecker m => Name -> m VName
newTypeName Name
desc
  VName -> Constraint -> TermTypeM ()
constrain VName
v forall a b. (a -> b) -> a -> b
$ Liftedness -> Usage -> Constraint
NoConstraint Liftedness
Unlifted forall a b. (a -> b) -> a -> b
$ SrcLoc -> Usage
mkUsage' SrcLoc
loc
  [VName]
dims <- forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
r forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadUnify m =>
SrcLoc -> Rigidity -> Name -> m VName
newDimVar SrcLoc
loc Rigidity
Nonrigid Name
"dim"
  let rowt :: ScalarTypeBase dim ()
rowt = forall dim as.
as
-> Uniqueness
-> QualName VName
-> [TypeArg dim]
-> ScalarTypeBase dim as
TypeVar () Uniqueness
Nonunique (forall v. v -> QualName v
qualName VName
v) []
  forall (f :: * -> *) a. Applicative f => a -> f a
pure
    ( forall dim as.
as
-> Uniqueness
-> Shape dim
-> ScalarTypeBase dim ()
-> TypeBase dim as
Array () Uniqueness
Nonunique (forall dim. [dim] -> Shape dim
Shape forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (QualName VName -> Size
NamedSize forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall v. v -> QualName v
qualName) [VName]
dims) forall {dim}. ScalarTypeBase dim ()
rowt,
      forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall {dim}. ScalarTypeBase dim ()
rowt
    )

-- | Replace *all* dimensions with distinct fresh size variables.
allDimsFreshInType ::
  SrcLoc ->
  Rigidity ->
  Name ->
  TypeBase Size als ->
  TermTypeM (TypeBase Size als, M.Map VName Size)
allDimsFreshInType :: forall als.
SrcLoc
-> Rigidity
-> Name
-> TypeBase Size als
-> TermTypeM (TypeBase Size als, Map VName Size)
allDimsFreshInType SrcLoc
loc Rigidity
r Name
desc TypeBase Size als
t =
  forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bitraverse forall {t :: (* -> *) -> * -> *} {m :: * -> *} {a}.
(MonadTrans t, MonadUnify m, MonadState (Map VName a) (t m)) =>
a -> t m Size
onDim forall (f :: * -> *) a. Applicative f => a -> f a
pure TypeBase Size als
t) forall a. Monoid a => a
mempty
  where
    onDim :: a -> t m Size
onDim a
d = 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 :: * -> *).
MonadUnify m =>
SrcLoc -> Rigidity -> Name -> m VName
newDimVar SrcLoc
loc Rigidity
r Name
desc
      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
v a
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
v

-- | Replace all type variables with their concrete types.
updateTypes :: ASTMappable e => e -> TermTypeM e
updateTypes :: forall e. ASTMappable e => e -> TermTypeM e
updateTypes = forall x (m :: * -> *).
(ASTMappable x, Monad m) =>
ASTMapper m -> x -> m x
astMap ASTMapper TermTypeM
tv
  where
    tv :: ASTMapper TermTypeM
tv =
      ASTMapper
        { mapOnExp :: Exp -> TermTypeM Exp
mapOnExp = forall x (m :: * -> *).
(ASTMappable x, Monad m) =>
ASTMapper m -> x -> m x
astMap ASTMapper TermTypeM
tv,
          mapOnName :: VName -> TermTypeM VName
mapOnName = forall (f :: * -> *) a. Applicative f => a -> f a
pure,
          mapOnStructType :: StructType -> TermTypeM StructType
mapOnStructType = forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully,
          mapOnPatType :: PatType -> TermTypeM PatType
mapOnPatType = forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully,
          mapOnStructRetType :: RetTypeBase Size () -> TermTypeM (RetTypeBase Size ())
mapOnStructRetType = forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully,
          mapOnPatRetType :: RetTypeBase Size Aliasing -> TermTypeM (RetTypeBase Size Aliasing)
mapOnPatRetType = forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully
        }

--- Basic checking

unifies :: T.Text -> StructType -> Exp -> TermTypeM Exp
unifies :: Text -> StructType -> Exp -> TermTypeM Exp
unifies Text
why StructType
t Exp
e = do
  forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify (SrcLoc -> Text -> Usage
mkUsage (forall a. Located a => a -> SrcLoc
srclocOf Exp
e) Text
why) StructType
t forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Exp -> TermTypeM PatType
expType Exp
e
  forall (f :: * -> *) a. Applicative f => a -> f a
pure Exp
e

-- | @require ts e@ causes a 'TypeError' if @expType e@ is not one of
-- the types in @ts@.  Otherwise, simply returns @e@.
require :: T.Text -> [PrimType] -> Exp -> TermTypeM Exp
require :: Text -> [PrimType] -> Exp -> TermTypeM Exp
require Text
why [PrimType]
ts Exp
e = do
  forall (m :: * -> *).
MonadUnify m =>
[PrimType] -> Usage -> StructType -> m ()
mustBeOneOf [PrimType]
ts (SrcLoc -> Text -> Usage
mkUsage (forall a. Located a => a -> SrcLoc
srclocOf Exp
e) Text
why) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Exp -> TermTypeM PatType
expType Exp
e
  forall (f :: * -> *) a. Applicative f => a -> f a
pure Exp
e

termCheckTypeExp ::
  TypeExp NoInfo Name ->
  TermTypeM (TypeExp Info VName, [VName], StructRetType)
termCheckTypeExp :: TypeExp NoInfo Name
-> TermTypeM (TypeExp Info VName, [VName], RetTypeBase Size ())
termCheckTypeExp TypeExp NoInfo Name
te = do
  (TypeExp Info VName
te', [VName]
svars, RetTypeBase Size ()
rettype, Liftedness
_l) <- forall (m :: * -> *).
MonadTypeChecker m =>
TypeExp NoInfo Name
-> m (TypeExp Info VName, [VName], RetTypeBase Size (), Liftedness)
checkTypeExp TypeExp NoInfo Name
te

  -- No guarantee that the locally bound sizes in rettype are globally
  -- unique, but we want to turn them into size variables, so let's
  -- give them some unique names.  Maybe this should be done below,
  -- where we actually turn these into size variables?
  RetType [VName]
dims StructType
st <- forall (m :: * -> *).
MonadTypeChecker m =>
RetTypeBase Size () -> m (RetTypeBase Size ())
renameRetType RetTypeBase Size ()
rettype

  -- Observe the sizes so we do not get any warnings about them not
  -- being used.
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ VName -> TermTypeM ()
observeDim forall a b. (a -> b) -> a -> b
$ forall as. TypeBase Size as -> Set VName
freeInType StructType
st
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeExp Info VName
te', [VName]
svars, forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
dims StructType
st)
  where
    observeDim :: VName -> TermTypeM ()
observeDim VName
v =
      Ident -> TermTypeM ()
observe forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
vn -> f PatType -> SrcLoc -> IdentBase f vn
Ident VName
v (forall a. a -> Info a
Info 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
Int64) forall a. Monoid a => a
mempty

checkTypeExpNonrigid :: TypeExp NoInfo Name -> TermTypeM (TypeExp Info VName, StructType, [VName])
checkTypeExpNonrigid :: TypeExp NoInfo Name
-> TermTypeM (TypeExp Info VName, StructType, [VName])
checkTypeExpNonrigid TypeExp NoInfo Name
te = do
  (TypeExp Info VName
te', [VName]
svars, RetType [VName]
dims StructType
st) <- TypeExp NoInfo Name
-> TermTypeM (TypeExp Info VName, [VName], RetTypeBase Size ())
termCheckTypeExp TypeExp NoInfo Name
te
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ([VName]
svars forall a. [a] -> [a] -> [a]
++ [VName]
dims) forall a b. (a -> b) -> a -> b
$ \VName
v ->
    VName -> Constraint -> TermTypeM ()
constrain VName
v forall a b. (a -> b) -> a -> b
$ Maybe Size -> Usage -> Constraint
Size forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ SrcLoc -> Text -> Usage
mkUsage (forall a. Located a => a -> SrcLoc
srclocOf TypeExp NoInfo Name
te) Text
"anonymous size in type expression"
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeExp Info VName
te', StructType
st, [VName]
svars forall a. [a] -> [a] -> [a]
++ [VName]
dims)

checkTypeExpRigid ::
  TypeExp NoInfo Name ->
  RigidSource ->
  TermTypeM (TypeExp Info VName, StructType, [VName])
checkTypeExpRigid :: TypeExp NoInfo Name
-> RigidSource
-> TermTypeM (TypeExp Info VName, StructType, [VName])
checkTypeExpRigid TypeExp NoInfo Name
te RigidSource
rsrc = do
  (TypeExp Info VName
te', [VName]
svars, RetType [VName]
dims StructType
st) <- TypeExp NoInfo Name
-> TermTypeM (TypeExp Info VName, [VName], RetTypeBase Size ())
termCheckTypeExp TypeExp NoInfo Name
te
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ([VName]
svars forall a. [a] -> [a] -> [a]
++ [VName]
dims) forall a b. (a -> b) -> a -> b
$ \VName
v ->
    VName -> Constraint -> TermTypeM ()
constrain VName
v forall a b. (a -> b) -> a -> b
$ SrcLoc -> RigidSource -> Constraint
UnknowableSize (forall a. Located a => a -> SrcLoc
srclocOf TypeExp NoInfo Name
te) RigidSource
rsrc
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeExp Info VName
te', StructType
st, [VName]
svars forall a. [a] -> [a] -> [a]
++ [VName]
dims)

--- Sizes

isInt64 :: Exp -> Maybe Int64
isInt64 :: Exp -> Maybe Int64
isInt64 (Literal (SignedValue (Int64Value Int64
k')) SrcLoc
_) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a b. (Integral a, Num b) => a -> b
fromIntegral Int64
k'
isInt64 (IntLit Integer
k' Info PatType
_ SrcLoc
_) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. Num a => Integer -> a
fromInteger Integer
k'
isInt64 (Negate Exp
x SrcLoc
_) = forall a. Num a => a -> a
negate forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp -> Maybe Int64
isInt64 Exp
x
isInt64 Exp
_ = forall a. Maybe a
Nothing

maybeDimFromExp :: Exp -> Maybe Size
maybeDimFromExp :: Exp -> Maybe Size
maybeDimFromExp (Var QualName VName
v Info PatType
_ SrcLoc
_) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ QualName VName -> Size
NamedSize QualName VName
v
maybeDimFromExp (Parens Exp
e SrcLoc
_) = Exp -> Maybe Size
maybeDimFromExp Exp
e
maybeDimFromExp (QualParens (QualName VName, SrcLoc)
_ Exp
e SrcLoc
_) = Exp -> Maybe Size
maybeDimFromExp Exp
e
maybeDimFromExp Exp
e = Int64 -> Size
ConstSize forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
fromIntegral forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp -> Maybe Int64
isInt64 Exp
e

dimFromExp :: (Exp -> SizeSource) -> Exp -> TermTypeM (Size, Maybe VName)
dimFromExp :: (Exp -> SizeSource) -> Exp -> TermTypeM (Size, Maybe VName)
dimFromExp Exp -> SizeSource
rf (Attr AttrInfo VName
_ Exp
e SrcLoc
_) = (Exp -> SizeSource) -> Exp -> TermTypeM (Size, Maybe VName)
dimFromExp Exp -> SizeSource
rf Exp
e
dimFromExp Exp -> SizeSource
rf (Assert Exp
_ Exp
e Info Text
_ SrcLoc
_) = (Exp -> SizeSource) -> Exp -> TermTypeM (Size, Maybe VName)
dimFromExp Exp -> SizeSource
rf Exp
e
dimFromExp Exp -> SizeSource
rf (Parens Exp
e SrcLoc
_) = (Exp -> SizeSource) -> Exp -> TermTypeM (Size, Maybe VName)
dimFromExp Exp -> SizeSource
rf Exp
e
dimFromExp Exp -> SizeSource
rf (QualParens (QualName VName, SrcLoc)
_ Exp
e SrcLoc
_) = (Exp -> SizeSource) -> Exp -> TermTypeM (Size, Maybe VName)
dimFromExp Exp -> SizeSource
rf Exp
e
dimFromExp Exp -> SizeSource
rf Exp
e
  | Just Size
d <- Exp -> Maybe Size
maybeDimFromExp Exp
e =
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (Size
d, forall a. Maybe a
Nothing)
  | Bool
otherwise =
      SrcLoc -> SizeSource -> TermTypeM (Size, Maybe VName)
extSize (forall a. Located a => a -> SrcLoc
srclocOf Exp
e) forall a b. (a -> b) -> a -> b
$ Exp -> SizeSource
rf Exp
e

sizeFromArg :: Maybe (QualName VName) -> Exp -> TermTypeM (Size, Maybe VName)
sizeFromArg :: Maybe (QualName VName) -> Exp -> TermTypeM (Size, Maybe VName)
sizeFromArg Maybe (QualName VName)
fname = (Exp -> SizeSource) -> Exp -> TermTypeM (Size, Maybe VName)
dimFromExp forall a b. (a -> b) -> a -> b
$ FName -> ExpBase NoInfo VName -> SizeSource
SourceArg (Maybe (QualName VName) -> FName
FName Maybe (QualName VName)
fname) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Exp -> ExpBase NoInfo VName
bareExp

-- | Any argument sizes created with 'extSize' inside the given action
-- will be removed once the action finishes.  This is to ensure that
-- just because e.g. @n+1@ appears as a size in one branch of a
-- conditional, that doesn't mean it's also available in the other
-- branch.
noSizeEscape :: TermTypeM a -> TermTypeM a
noSizeEscape :: forall a. TermTypeM a -> TermTypeM a
noSizeEscape TermTypeM a
m = do
  Map SizeSource VName
dimtable <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TermTypeState -> Map SizeSource VName
stateDimTable
  a
x <- TermTypeM a
m
  forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \TermTypeState
s -> TermTypeState
s {stateDimTable :: Map SizeSource VName
stateDimTable = Map SizeSource VName
dimtable}
  forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x

--- Control flow

tapOccurrences :: TermTypeM a -> TermTypeM (a, Occurrences)
tapOccurrences :: forall a. TermTypeM a -> TermTypeM (a, Occurrences)
tapOccurrences TermTypeM a
m = do
  (a
x, Occurrences
occs) <- forall a. TermTypeM a -> TermTypeM (a, Occurrences)
collectOccurrences TermTypeM a
m
  Occurrences -> TermTypeM ()
occur Occurrences
occs
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
x, Occurrences
occs)

collectOccurrences :: TermTypeM a -> TermTypeM (a, Occurrences)
collectOccurrences :: forall a. TermTypeM a -> TermTypeM (a, Occurrences)
collectOccurrences TermTypeM a
m = do
  Occurrences
old <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TermTypeState -> Occurrences
stateOccs
  forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \TermTypeState
s -> TermTypeState
s {stateOccs :: Occurrences
stateOccs = forall a. Monoid a => a
mempty}
  a
x <- TermTypeM a
m
  Occurrences
new <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TermTypeState -> Occurrences
stateOccs
  forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \TermTypeState
s -> TermTypeState
s {stateOccs :: Occurrences
stateOccs = Occurrences
old}
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
x, Occurrences
new)

alternative :: TermTypeM a -> TermTypeM b -> TermTypeM (a, b)
alternative :: forall a b. TermTypeM a -> TermTypeM b -> TermTypeM (a, b)
alternative TermTypeM a
m1 TermTypeM b
m2 = do
  (a
x, Occurrences
occurs1) <- forall a. TermTypeM a -> TermTypeM (a, Occurrences)
collectOccurrences forall a b. (a -> b) -> a -> b
$ forall a. TermTypeM a -> TermTypeM a
noSizeEscape TermTypeM a
m1
  (b
y, Occurrences
occurs2) <- forall a. TermTypeM a -> TermTypeM (a, Occurrences)
collectOccurrences forall a b. (a -> b) -> a -> b
$ forall a. TermTypeM a -> TermTypeM a
noSizeEscape TermTypeM b
m2
  Occurrences -> TermTypeM ()
checkOccurrences Occurrences
occurs1
  Occurrences -> TermTypeM ()
checkOccurrences Occurrences
occurs2
  Occurrences -> TermTypeM ()
occur forall a b. (a -> b) -> a -> b
$ Occurrences
occurs1 Occurrences -> Occurrences -> Occurrences
`altOccurrences` Occurrences
occurs2
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
x, b
y)

sequentially :: TermTypeM a -> (a -> Occurrences -> TermTypeM b) -> TermTypeM b
sequentially :: forall a b.
TermTypeM a -> (a -> Occurrences -> TermTypeM b) -> TermTypeM b
sequentially TermTypeM a
m1 a -> Occurrences -> TermTypeM b
m2 = do
  (a
a, Occurrences
m1flow) <- forall a. TermTypeM a -> TermTypeM (a, Occurrences)
collectOccurrences TermTypeM a
m1
  (b
b, Occurrences
m2flow) <- forall a. TermTypeM a -> TermTypeM (a, Occurrences)
collectOccurrences forall a b. (a -> b) -> a -> b
$ a -> Occurrences -> TermTypeM b
m2 a
a Occurrences
m1flow
  Occurrences -> TermTypeM ()
occur forall a b. (a -> b) -> a -> b
$ Occurrences
m1flow Occurrences -> Occurrences -> Occurrences
`seqOccurrences` Occurrences
m2flow
  forall (f :: * -> *) a. Applicative f => a -> f a
pure b
b

--- Consumption

occur :: Occurrences -> TermTypeM ()
occur :: Occurrences -> TermTypeM ()
occur Occurrences
occs = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \TermTypeState
s -> TermTypeState
s {stateOccs :: Occurrences
stateOccs = TermTypeState -> Occurrences
stateOccs TermTypeState
s forall a. Semigroup a => a -> a -> a
<> Occurrences
occs}

-- | Proclaim that we have made read-only use of the given variable.
observe :: Ident -> TermTypeM ()
observe :: Ident -> TermTypeM ()
observe (Ident VName
nm (Info PatType
t) SrcLoc
loc) =
  let als :: Aliasing
als = VName -> Alias
AliasBound VName
nm forall a. Ord a => a -> Set a -> Set a
`S.insert` forall as shape. Monoid as => TypeBase shape as -> as
aliases PatType
t
   in Occurrences -> TermTypeM ()
occur [Aliasing -> SrcLoc -> Occurrence
observation Aliasing
als SrcLoc
loc]

-- | Enter a context where nothing outside can be consumed (i.e. the
-- body of a function definition).
noUnique :: TermTypeM a -> TermTypeM a
noUnique :: forall a. TermTypeM a -> TermTypeM a
noUnique TermTypeM a
m = do
  (a
x, Occurrences
occs) <- forall a. TermTypeM a -> TermTypeM (a, Occurrences)
collectOccurrences forall a b. (a -> b) -> a -> b
$ forall a. (TermScope -> TermScope) -> TermTypeM a -> TermTypeM a
localScope TermScope -> TermScope
f TermTypeM a
m
  Occurrences -> TermTypeM ()
checkOccurrences Occurrences
occs
  Occurrences -> TermTypeM ()
occur forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ Occurrences -> (Occurrences, Occurrences)
split Occurrences
occs
  forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x
  where
    f :: TermScope -> TermScope
f TermScope
scope = TermScope
scope {scopeVtable :: Map VName ValBinding
scopeVtable = forall a b k. (a -> b) -> Map k a -> Map k b
M.map ValBinding -> ValBinding
set forall a b. (a -> b) -> a -> b
$ TermScope -> Map VName ValBinding
scopeVtable TermScope
scope}

    set :: ValBinding -> ValBinding
set (BoundV Locality
l [TypeParam]
tparams PatType
t) = Locality -> [TypeParam] -> PatType -> ValBinding
BoundV (forall a. Ord a => a -> a -> a
max Locality
l Locality
Nonlocal) [TypeParam]
tparams PatType
t
    set (OverloadedF [PrimType]
ts [Maybe PrimType]
pts Maybe PrimType
rt) = [PrimType] -> [Maybe PrimType] -> Maybe PrimType -> ValBinding
OverloadedF [PrimType]
ts [Maybe PrimType]
pts Maybe PrimType
rt
    set ValBinding
EqualityF = ValBinding
EqualityF
    set (WasConsumed SrcLoc
loc) = SrcLoc -> ValBinding
WasConsumed SrcLoc
loc

    split :: Occurrences -> (Occurrences, Occurrences)
split = forall a b. [(a, b)] -> ([a], [b])
unzip forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (\Occurrence
occ -> (Occurrence
occ {consumed :: Maybe (Set VName)
consumed = forall a. Monoid a => a
mempty}, Occurrence
occ {observed :: Set VName
observed = forall a. Monoid a => a
mempty}))

removeSeminullOccurrences :: TermTypeM a -> TermTypeM a
removeSeminullOccurrences :: forall a. TermTypeM a -> TermTypeM a
removeSeminullOccurrences TermTypeM a
m = do
  (a
x, Occurrences
occs) <- forall a. TermTypeM a -> TermTypeM (a, Occurrences)
collectOccurrences TermTypeM a
m
  Occurrences -> TermTypeM ()
occur forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Occurrence -> Bool
seminullOccurrence) Occurrences
occs
  forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x

checkIfConsumable :: SrcLoc -> Aliasing -> TermTypeM ()
checkIfConsumable :: SrcLoc -> Aliasing -> TermTypeM ()
checkIfConsumable SrcLoc
loc Aliasing
als = 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 boundAlias :: Alias -> Maybe VName
boundAlias (AliasBound VName
v) = forall a. a -> Maybe a
Just VName
v
      boundAlias (AliasFree VName
_) = forall a. Maybe a
Nothing
      consumable :: VName -> Bool
consumable VName
v = case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
v Map VName ValBinding
vtable of
        Just (BoundV Locality
Local [TypeParam]
_ PatType
t)
          | Scalar Arrow {} <- PatType
t -> Bool
False
          | Bool
otherwise -> Bool
True
        Just (BoundV Locality
l [TypeParam]
_ PatType
_) -> Locality
l forall a. Eq a => a -> a -> Bool
== Locality
Local
        Maybe ValBinding
_ -> Bool
False -- Implies name from module.
  case forall a. Ord a => [a] -> [a]
sort forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. VName -> Bool
consumable) forall a b. (a -> b) -> a -> b
$ forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Alias -> Maybe VName
boundAlias forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
S.toList Aliasing
als of
    VName
v : [VName]
_ -> forall (m :: * -> *) b.
MonadTypeChecker m =>
SrcLoc -> Doc () -> m b
notConsumable SrcLoc
loc forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a. SrcLoc -> VName -> TermTypeM (Doc a)
describeVar SrcLoc
loc VName
v
    [] -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- | Proclaim that we have written to the given variable.
consume :: SrcLoc -> Aliasing -> TermTypeM ()
consume :: SrcLoc -> Aliasing -> TermTypeM ()
consume SrcLoc
loc Aliasing
als = do
  SrcLoc -> Aliasing -> TermTypeM ()
checkIfConsumable SrcLoc
loc Aliasing
als
  Occurrences -> TermTypeM ()
occur [Aliasing -> SrcLoc -> Occurrence
consumption Aliasing
als SrcLoc
loc]

-- | Proclaim that we have written to the given variable, and mark
-- accesses to it and all of its aliases as invalid inside the given
-- computation.
consuming :: Ident -> TermTypeM a -> TermTypeM a
consuming :: forall a. Ident -> TermTypeM a -> TermTypeM a
consuming (Ident VName
name (Info PatType
t) SrcLoc
loc) TermTypeM a
m = do
  PatType
t' <- forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully PatType
t
  SrcLoc -> Aliasing -> TermTypeM ()
consume SrcLoc
loc forall a b. (a -> b) -> a -> b
$ VName -> Alias
AliasBound VName
name forall a. Ord a => a -> Set a -> Set a
`S.insert` forall as shape. Monoid as => TypeBase shape as -> as
aliases PatType
t'
  forall a. (TermScope -> TermScope) -> TermTypeM a -> TermTypeM a
localScope TermScope -> TermScope
consume' TermTypeM a
m
  where
    consume' :: TermScope -> TermScope
consume' 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 (SrcLoc -> ValBinding
WasConsumed SrcLoc
loc) forall a b. (a -> b) -> a -> b
$ TermScope -> Map VName ValBinding
scopeVtable TermScope
scope}

-- Running

initialTermScope :: TermScope
initialTermScope :: TermScope
initialTermScope =
  TermScope
    { scopeVtable :: Map VName ValBinding
scopeVtable = Map VName ValBinding
initialVtable,
      scopeTypeTable :: Map VName TypeBinding
scopeTypeTable = forall a. Monoid a => a
mempty,
      scopeNameMap :: NameMap
scopeNameMap = NameMap
topLevelNameMap,
      scopeModTable :: Map VName Mod
scopeModTable = forall a. Monoid a => a
mempty
    }
  where
    initialVtable :: Map VName ValBinding
initialVtable = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe forall {a}. (a, Intrinsic) -> Maybe (a, ValBinding)
addIntrinsicF forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
M.toList Map VName Intrinsic
intrinsics

    prim :: PrimType -> TypeBase dim as
prim = forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall dim as. PrimType -> ScalarTypeBase dim as
Prim
    arrow :: TypeBase dim () -> RetTypeBase dim as -> TypeBase dim as
arrow TypeBase dim ()
x RetTypeBase dim as
y = forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as.
as
-> PName
-> Diet
-> TypeBase dim ()
-> RetTypeBase dim as
-> ScalarTypeBase dim as
Arrow forall a. Monoid a => a
mempty PName
Unnamed Diet
Observe TypeBase dim ()
x RetTypeBase dim as
y

    addIntrinsicF :: (a, Intrinsic) -> Maybe (a, ValBinding)
addIntrinsicF (a
name, IntrinsicMonoFun [PrimType]
pts PrimType
t) =
      forall a. a -> Maybe a
Just (a
name, Locality -> [TypeParam] -> PatType -> ValBinding
BoundV Locality
Global [] forall a b. (a -> b) -> a -> b
$ forall {as} {dim}.
Monoid as =>
TypeBase dim () -> RetTypeBase dim as -> TypeBase dim as
arrow forall {dim} {as}. TypeBase dim as
pts' 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}. PrimType -> TypeBase dim as
prim PrimType
t)
      where
        pts' :: TypeBase dim as
pts' = case [PrimType]
pts of
          [PrimType
pt] -> forall {dim} {as}. PrimType -> TypeBase dim as
prim PrimType
pt
          [PrimType]
_ -> 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 a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall {dim} {as}. PrimType -> TypeBase dim as
prim [PrimType]
pts
    addIntrinsicF (a
name, IntrinsicOverloadedFun [PrimType]
ts [Maybe PrimType]
pts Maybe PrimType
rts) =
      forall a. a -> Maybe a
Just (a
name, [PrimType] -> [Maybe PrimType] -> Maybe PrimType -> ValBinding
OverloadedF [PrimType]
ts [Maybe PrimType]
pts Maybe PrimType
rts)
    addIntrinsicF (a
name, IntrinsicPolyFun [TypeParam]
tvs [(Diet, StructType)]
pts RetTypeBase Size ()
rt) =
      forall a. a -> Maybe a
Just
        ( a
name,
          Locality -> [TypeParam] -> PatType -> ValBinding
BoundV Locality
Global [TypeParam]
tvs forall a b. (a -> b) -> a -> b
$ forall dim as. TypeBase dim as -> TypeBase dim Aliasing
fromStruct forall a b. (a -> b) -> a -> b
$ forall as dim pas.
Monoid as =>
[(Diet, TypeBase dim pas)] -> RetTypeBase dim as -> TypeBase dim as
foldFunType [(Diet, StructType)]
pts RetTypeBase Size ()
rt
        )
    addIntrinsicF (a
name, Intrinsic
IntrinsicEquality) =
      forall a. a -> Maybe a
Just (a
name, ValBinding
EqualityF)
    addIntrinsicF (a, Intrinsic)
_ = forall a. Maybe a
Nothing

runTermTypeM :: TermTypeM a -> TypeM (a, Occurrences)
runTermTypeM :: forall a. TermTypeM a -> TypeM (a, Occurrences)
runTermTypeM (TermTypeM ReaderT TermEnv (StateT TermTypeState TypeM) a
m) = do
  TermScope
initial_scope <- (TermScope
initialTermScope <>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> TermScope
envToTermScope forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeM Env
askEnv
  let initial_tenv :: TermEnv
initial_tenv =
        TermEnv
          { termScope :: TermScope
termScope = TermScope
initial_scope,
            termChecking :: Maybe Checking
termChecking = forall a. Maybe a
Nothing,
            termLevel :: Int
termLevel = Int
0
          }
  forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second TermTypeState -> Occurrences
stateOccs
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT
      (forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT TermEnv (StateT TermTypeState TypeM) a
m TermEnv
initial_tenv)
      (Constraints
-> Int
-> Map SizeSource VName
-> Map VName NameReason
-> Occurrences
-> TermTypeState
TermTypeState forall a. Monoid a => a
mempty Int
0 forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty)