{-# LANGUAGE Strict #-}

-- | 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,
    ValBinding (..),
    SizeSource (SourceSlice),
    Inferred (..),
    Checking (..),
    withEnv,
    localScope,
    TermEnv (..),
    TermScope (..),
    TermTypeState (..),
    onFailure,
    extSize,
    expType,
    expTypeFully,
    constrain,
    instTyVars,
    replaceTyVars,
    replaceTyVarsAbsorbable,
    updateTypes,
    Names,

    -- * Primitive checking
    unifies,
    checkTypeExpNonrigid,
    lookupVar,
    lookupMod,
    typeSchemes,
    lookupAbsTy,

    -- * Sizes
    isInt64,

    -- * Control flow
    incLevel,

    -- * Errors
    unusedSize,
  )
where

import Control.Monad
import Control.Monad.Except
import Control.Monad.Reader
import Control.Monad.State.Strict
import Data.Bifunctor
import Data.Bitraversable
import Data.Foldable
import Data.Map.Strict qualified as M
import Data.Maybe
import Data.Set qualified as S
import Data.Text qualified as T
import Futhark.FreshNames hiding (newName)
import Futhark.FreshNames qualified
import Futhark.Util.Pretty hiding (space)
import Language.Futhark
import Language.Futhark.Traversals
import Language.Futhark.TypeChecker.Constraints (TyVar)
import Language.Futhark.TypeChecker.Error
import Language.Futhark.TypeChecker.Monad hiding (BoundV, lookupAbsTy, lookupMod, stateNameSource)
import Language.Futhark.TypeChecker.Monad qualified as TypeM
import Language.Futhark.TypeChecker.Terms.Scope hiding (envToTermScope, initialTermScope, lookupQualNameEnv)
import Language.Futhark.TypeChecker.Terms.Scope qualified as Scope
import Language.Futhark.TypeChecker.Types
import Language.Futhark.TypeChecker.Unify
import Prelude hiding (abs, mod)

type Names = S.Set VName

unusedSize :: (MonadTypeChecker m) => SizeBinder VName -> m a
unusedSize :: forall (m :: * -> *) a.
MonadTypeChecker m =>
SizeBinder VName -> m a
unusedSize SizeBinder VName
p =
  SizeBinder VName -> Notes -> Doc () -> m a
forall loc a. Located loc => loc -> Notes -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SizeBinder VName
p Notes
forall a. Monoid a => a
mempty (Doc () -> m a) -> (Doc () -> Doc ()) -> Doc () -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
withIndexLink Doc ()
"unused-size" (Doc () -> m a) -> Doc () -> m a
forall a b. (a -> b) -> a -> b
$
    Doc ()
"Size" Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> SizeBinder VName -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. SizeBinder VName -> Doc ann
pretty SizeBinder VName
p Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"unused in pattern."

data Checking
  = CheckingApply (Maybe (QualName VName)) Exp StructType StructType
  | CheckingReturn ResType StructType
  | CheckingAscription StructType StructType
  | CheckingLetGeneralise Name
  | CheckingParams (Maybe Name)
  | CheckingPat (PatBase Info VName StructType) (Inferred StructType)
  | CheckingLoopBody StructType StructType
  | CheckingLoopInitial StructType StructType
  | CheckingRecordUpdate [Name] 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) =
    Doc ann
forall {ann}. Doc ann
header
      Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
</> Doc ann
"Expected:"
      Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
align (StructType -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. StructType -> Doc ann
pretty StructType
expected)
      Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
</> Doc ann
"Actual:  "
      Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
align (StructType -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. StructType -> 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"
              Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
dquotes (Doc (ZonkAny 1) -> Doc ann
forall a b. Doc a -> Doc b
shorten (Doc (ZonkAny 1) -> Doc ann) -> Doc (ZonkAny 1) -> Doc ann
forall a b. (a -> b) -> a -> b
$ Doc (ZonkAny 1) -> Doc (ZonkAny 1)
forall ann. Doc ann -> Doc ann
group (Doc (ZonkAny 1) -> Doc (ZonkAny 1))
-> Doc (ZonkAny 1) -> Doc (ZonkAny 1)
forall a b. (a -> b) -> a -> b
$ Exp -> Doc (ZonkAny 1)
forall a ann. Pretty a => a -> Doc ann
forall ann. Exp -> Doc ann
pretty Exp
e)
              Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
" (invalid type)."
          Just QualName VName
fname ->
            Doc ann
"Cannot apply"
              Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
dquotes (QualName VName -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. QualName VName -> Doc ann
pretty QualName VName
fname)
              Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
<+> Doc ann
"to"
              Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
dquotes (Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
align (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Doc (ZonkAny 2) -> Doc ann
forall a b. Doc a -> Doc b
shorten (Doc (ZonkAny 2) -> Doc ann) -> Doc (ZonkAny 2) -> Doc ann
forall a b. (a -> b) -> a -> b
$ Doc (ZonkAny 2) -> Doc (ZonkAny 2)
forall ann. Doc ann -> Doc ann
group (Doc (ZonkAny 2) -> Doc (ZonkAny 2))
-> Doc (ZonkAny 2) -> Doc (ZonkAny 2)
forall a b. (a -> b) -> a -> b
$ Exp -> Doc (ZonkAny 2)
forall a ann. Pretty a => a -> Doc ann
forall ann. Exp -> Doc ann
pretty Exp
e)
              Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
" (invalid type)."
  pretty (CheckingReturn ResType
expected StructType
actual) =
    Doc ann
"Function body does not have expected type."
      Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
</> Doc ann
"Expected:"
      Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
align (ResType -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. ResType -> Doc ann
pretty ResType
expected)
      Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
</> Doc ann
"Actual:  "
      Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
align (StructType -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. StructType -> Doc ann
pretty StructType
actual)
  pretty (CheckingAscription StructType
expected StructType
actual) =
    Doc ann
"Expression does not have expected type from explicit ascription."
      Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
</> Doc ann
"Expected:"
      Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
align (StructType -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. StructType -> Doc ann
pretty StructType
expected)
      Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
</> Doc ann
"Actual:  "
      Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
align (StructType -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. StructType -> Doc ann
pretty StructType
actual)
  pretty (CheckingLetGeneralise Name
fname) =
    Doc ann
"Cannot generalise type of" Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
dquotes (Name -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Name -> Doc ann
pretty Name
fname) Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"."
  pretty (CheckingParams Maybe Name
fname) =
    Doc ann
"Invalid use of parameters in" Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
dquotes Doc ann
forall {ann}. Doc ann
fname' Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"."
    where
      fname' :: Doc ann
fname' = Doc ann -> (Name -> Doc ann) -> Maybe Name -> Doc ann
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc ann
"anonymous function" Name -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Name -> Doc ann
pretty Maybe Name
fname
  pretty (CheckingPat PatBase Info VName StructType
pat Inferred StructType
NoneInferred) =
    Doc ann
"Invalid pattern" Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
dquotes (PatBase Info VName StructType -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. PatBase Info VName StructType -> Doc ann
pretty PatBase Info VName StructType
pat) Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"."
  pretty (CheckingPat PatBase Info VName StructType
pat (Ascribed StructType
t)) =
    Doc ann
"Pattern"
      Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
</> Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (PatBase Info VName StructType -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. PatBase Info VName StructType -> Doc ann
pretty PatBase Info VName StructType
pat)
      Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
</> Doc ann
"cannot match value of type"
      Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
</> Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (StructType -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. StructType -> Doc ann
pretty StructType
t)
  pretty (CheckingLoopBody StructType
expected StructType
actual) =
    Doc ann
"Loop body does not have expected type."
      Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
</> Doc ann
"Expected:"
      Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
align (StructType -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. StructType -> Doc ann
pretty StructType
expected)
      Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
</> Doc ann
"Actual:  "
      Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
align (StructType -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. StructType -> Doc ann
pretty StructType
actual)
  pretty (CheckingLoopInitial StructType
expected StructType
actual) =
    Doc ann
"Initial loop values do not have expected type."
      Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
</> Doc ann
"Expected:"
      Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
align (StructType -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. StructType -> Doc ann
pretty StructType
expected)
      Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
</> Doc ann
"Actual:  "
      Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
align (StructType -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. StructType -> Doc ann
pretty StructType
actual)
  pretty (CheckingRecordUpdate [Name]
fs StructType
expected StructType
actual) =
    Doc ann
"Type mismatch when updating record field"
      Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
dquotes Doc ann
forall {ann}. Doc ann
fs'
      Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"."
        Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
</> Doc ann
"Existing:"
        Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
align (StructType -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. StructType -> Doc ann
pretty StructType
expected)
        Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
</> Doc ann
"New:     "
        Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
align (StructType -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. StructType -> Doc ann
pretty StructType
actual)
    where
      fs' :: Doc ann
fs' = [Doc ann] -> Doc ann
forall a. Monoid a => [a] -> a
mconcat ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$ Doc ann -> [Doc ann] -> [Doc ann]
forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate Doc ann
"." ([Doc ann] -> [Doc ann]) -> [Doc ann] -> [Doc ann]
forall a b. (a -> b) -> a -> b
$ (Name -> Doc ann) -> [Name] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Name -> Doc ann
pretty [Name]
fs
  pretty (CheckingBranches StructType
t1 StructType
t2) =
    Doc ann
"Branches differ in type."
      Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
</> Doc ann
"Former:"
      Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
<+> StructType -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. StructType -> Doc ann
pretty StructType
t1
      Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
</> Doc ann
"Latter:"
      Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
<+> StructType -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. StructType -> 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 Exp
termScope :: TermScope Size,
    TermEnv -> Maybe Checking
termChecking :: Maybe Checking,
    TermEnv -> Int
termLevel :: Level,
    TermEnv -> Exp -> TermTypeM Exp
termCheckExp :: ExpBase Info VName -> TermTypeM Exp,
    TermEnv -> Env
termOuterEnv :: Env,
    TermEnv -> TySet
termTySet :: TySet,
    TermEnv -> Map VName (TypeBase () NoMode)
termTyVars :: M.Map TyVar (TypeBase () NoMode),
    TermEnv -> ImportName
termImportName :: ImportName
  }

-- | The scope, with sized types. See
-- "Language.Futhark.TypeChecker.Terms.Scope".
envToTermScope :: Env -> TermScope Size
envToTermScope :: Env -> TermScope Exp
envToTermScope = (StructType -> StructType) -> Env -> TermScope Exp
forall dim.
(StructType -> TypeBase dim NoMode) -> Env -> TermScope dim
Scope.envToTermScope StructType -> StructType
forall a. a -> a
id

withEnv :: TermEnv -> Env -> TermEnv
withEnv :: TermEnv -> Env -> TermEnv
withEnv TermEnv
tenv Env
env = TermEnv
tenv {termScope = termScope tenv <> envToTermScope 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
(Int -> FName -> ShowS)
-> (FName -> String) -> ([FName] -> ShowS) -> Show FName
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> FName -> ShowS
showsPrec :: Int -> FName -> ShowS
$cshow :: FName -> String
show :: FName -> String
$cshowList :: [FName] -> ShowS
showList :: [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)
  | SourceSlice
      (Maybe Size)
      (Maybe (ExpBase NoInfo VName))
      (Maybe (ExpBase NoInfo VName))
      (Maybe (ExpBase NoInfo VName))
  deriving (SizeSource -> SizeSource -> Bool
(SizeSource -> SizeSource -> Bool)
-> (SizeSource -> SizeSource -> Bool) -> Eq SizeSource
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SizeSource -> SizeSource -> Bool
== :: SizeSource -> SizeSource -> Bool
$c/= :: SizeSource -> SizeSource -> Bool
/= :: SizeSource -> SizeSource -> Bool
Eq, Eq SizeSource
Eq SizeSource =>
(SizeSource -> SizeSource -> Ordering)
-> (SizeSource -> SizeSource -> Bool)
-> (SizeSource -> SizeSource -> Bool)
-> (SizeSource -> SizeSource -> Bool)
-> (SizeSource -> SizeSource -> Bool)
-> (SizeSource -> SizeSource -> SizeSource)
-> (SizeSource -> SizeSource -> SizeSource)
-> Ord 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
$ccompare :: SizeSource -> SizeSource -> Ordering
compare :: SizeSource -> SizeSource -> Ordering
$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
>= :: SizeSource -> SizeSource -> Bool
$cmax :: SizeSource -> SizeSource -> SizeSource
max :: SizeSource -> SizeSource -> SizeSource
$cmin :: SizeSource -> SizeSource -> SizeSource
min :: SizeSource -> SizeSource -> SizeSource
Ord, Int -> SizeSource -> ShowS
[SizeSource] -> ShowS
SizeSource -> String
(Int -> SizeSource -> ShowS)
-> (SizeSource -> String)
-> ([SizeSource] -> ShowS)
-> Show SizeSource
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SizeSource -> ShowS
showsPrec :: Int -> SizeSource -> ShowS
$cshow :: SizeSource -> String
show :: SizeSource -> String
$cshowList :: [SizeSource] -> ShowS
showList :: [SizeSource] -> ShowS
Show)

-- | 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,
    TermTypeState -> Warnings
stateWarnings :: Warnings,
    TermTypeState -> VNameSource
stateNameSource :: VNameSource
  }

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

instance MonadError TypeError TermTypeM where
  throwError :: forall a. TypeError -> TermTypeM a
throwError TypeError
e = ReaderT
  TermEnv (StateT TermTypeState (Except (Warnings, TypeError))) a
-> TermTypeM a
forall a.
ReaderT
  TermEnv (StateT TermTypeState (Except (Warnings, TypeError))) a
-> TermTypeM a
TermTypeM (ReaderT
   TermEnv (StateT TermTypeState (Except (Warnings, TypeError))) a
 -> TermTypeM a)
-> ReaderT
     TermEnv (StateT TermTypeState (Except (Warnings, TypeError))) a
-> TermTypeM a
forall a b. (a -> b) -> a -> b
$ do
    ws <- (TermTypeState -> Warnings)
-> ReaderT
     TermEnv
     (StateT TermTypeState (Except (Warnings, TypeError)))
     Warnings
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TermTypeState -> Warnings
stateWarnings
    throwError (ws, e)

  catchError :: forall a. TermTypeM a -> (TypeError -> TermTypeM a) -> TermTypeM a
catchError (TermTypeM ReaderT
  TermEnv (StateT TermTypeState (Except (Warnings, TypeError))) a
m) TypeError -> TermTypeM a
f =
    ReaderT
  TermEnv (StateT TermTypeState (Except (Warnings, TypeError))) a
-> TermTypeM a
forall a.
ReaderT
  TermEnv (StateT TermTypeState (Except (Warnings, TypeError))) a
-> TermTypeM a
TermTypeM (ReaderT
   TermEnv (StateT TermTypeState (Except (Warnings, TypeError))) a
 -> TermTypeM a)
-> ReaderT
     TermEnv (StateT TermTypeState (Except (Warnings, TypeError))) a
-> TermTypeM a
forall a b. (a -> b) -> a -> b
$ ReaderT
  TermEnv (StateT TermTypeState (Except (Warnings, TypeError))) a
m ReaderT
  TermEnv (StateT TermTypeState (Except (Warnings, TypeError))) a
-> ((Warnings, TypeError)
    -> ReaderT
         TermEnv (StateT TermTypeState (Except (Warnings, TypeError))) a)
-> ReaderT
     TermEnv (StateT TermTypeState (Except (Warnings, TypeError))) a
forall a.
ReaderT
  TermEnv (StateT TermTypeState (Except (Warnings, TypeError))) a
-> ((Warnings, TypeError)
    -> ReaderT
         TermEnv (StateT TermTypeState (Except (Warnings, TypeError))) a)
-> ReaderT
     TermEnv (StateT TermTypeState (Except (Warnings, TypeError))) a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` (Warnings, TypeError)
-> ReaderT
     TermEnv (StateT TermTypeState (Except (Warnings, TypeError))) a
forall {a}.
(a, TypeError)
-> ReaderT
     TermEnv (StateT TermTypeState (Except (Warnings, TypeError))) a
f'
    where
      f' :: (a, TypeError)
-> ReaderT
     TermEnv (StateT TermTypeState (Except (Warnings, TypeError))) a
f' (a
_, TypeError
e) = let TermTypeM ReaderT
  TermEnv (StateT TermTypeState (Except (Warnings, TypeError))) a
m' = TypeError -> TermTypeM a
f TypeError
e in ReaderT
  TermEnv (StateT TermTypeState (Except (Warnings, TypeError))) a
m'

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

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

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

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

  newDimVar :: Usage -> Rigidity -> Name -> TermTypeM VName
newDimVar Usage
usage Rigidity
rigidity Name
name = do
    dim <- Name -> TermTypeM VName
forall (m :: * -> *). MonadTypeChecker m => Name -> m VName
newTypeName Name
name
    case rigidity of
      Rigid RigidSource
rsrc -> VName -> Constraint -> TermTypeM ()
constrain VName
dim (Constraint -> TermTypeM ()) -> Constraint -> TermTypeM ()
forall a b. (a -> b) -> a -> b
$ Loc -> RigidSource -> Constraint
UnknownSize (Usage -> Loc
forall a. Located a => a -> Loc
locOf Usage
usage) RigidSource
rsrc
      Rigidity
Nonrigid -> VName -> Constraint -> TermTypeM ()
constrain VName
dim (Constraint -> TermTypeM ()) -> Constraint -> TermTypeM ()
forall a b. (a -> b) -> a -> b
$ Maybe Exp -> Usage -> Constraint
Size Maybe Exp
forall a. Maybe a
Nothing Usage
usage
    pure dim

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

-- | Register the named parameters of arrows within a type as size parameters
-- ('ParamSize'), so that unification can reconstruct dependent function types
-- by linking instantiated sizes to them (the connection between a binder and
-- its uses is erased by the unsized pass). See Note [Size Inference] in
-- Language.Futhark.TypeChecker.Terms.
registerBinders :: Loc -> TypeBase Size o -> TermTypeM ()
registerBinders :: forall o. Loc -> TypeBase Exp o -> TermTypeM ()
registerBinders Loc
loc (Scalar (Arrow o
_ PName
pn Diet
_ StructType
ta (RetType [VName]
_ ResType
tr))) = do
  case PName
pn of
    Named VName
pv -> VName -> Constraint -> TermTypeM ()
constrain VName
pv (Constraint -> TermTypeM ()) -> Constraint -> TermTypeM ()
forall a b. (a -> b) -> a -> b
$ Loc -> Constraint
ParamSize Loc
loc
    PName
Unnamed -> () -> TermTypeM ()
forall a. a -> TermTypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  Loc -> StructType -> TermTypeM ()
forall o. Loc -> TypeBase Exp o -> TermTypeM ()
registerBinders Loc
loc StructType
ta
  Loc -> ResType -> TermTypeM ()
forall o. Loc -> TypeBase Exp o -> TermTypeM ()
registerBinders Loc
loc ResType
tr
registerBinders Loc
loc (Scalar (Record Map Name (TypeBase Exp o)
fs)) =
  (TypeBase Exp o -> TermTypeM ())
-> Map Name (TypeBase Exp o) -> TermTypeM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Loc -> TypeBase Exp o -> TermTypeM ()
forall o. Loc -> TypeBase Exp o -> TermTypeM ()
registerBinders Loc
loc) Map Name (TypeBase Exp o)
fs
registerBinders Loc
loc (Scalar (Sum Map Name [TypeBase Exp o]
cs)) =
  ([TypeBase Exp o] -> TermTypeM ())
-> Map Name [TypeBase Exp o] -> TermTypeM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((TypeBase Exp o -> TermTypeM ())
-> [TypeBase Exp o] -> TermTypeM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Loc -> TypeBase Exp o -> TermTypeM ()
forall o. Loc -> TypeBase Exp o -> TermTypeM ()
registerBinders Loc
loc)) Map Name [TypeBase Exp o]
cs
registerBinders Loc
loc (Scalar (TypeVar o
_ QualName VName
_ [TypeArg Exp]
targs)) =
  (TypeArg Exp -> TermTypeM ()) -> [TypeArg Exp] -> TermTypeM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ TypeArg Exp -> TermTypeM ()
onTArg [TypeArg Exp]
targs
  where
    onTArg :: TypeArg Exp -> TermTypeM ()
onTArg (TypeArgType StructType
ta) = Loc -> StructType -> TermTypeM ()
forall o. Loc -> TypeBase Exp o -> TermTypeM ()
registerBinders Loc
loc StructType
ta
    onTArg TypeArgDim {} = () -> TermTypeM ()
forall a. a -> TermTypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
registerBinders Loc
_ (Scalar Prim {}) = () -> TermTypeM ()
forall a. a -> TermTypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
registerBinders Loc
loc (Array o
_ Shape Exp
_ ScalarTypeBase Exp NoMode
et) = Loc -> StructType -> TermTypeM ()
forall o. Loc -> TypeBase Exp o -> TermTypeM ()
registerBinders Loc
loc (ScalarTypeBase Exp NoMode -> StructType
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar ScalarTypeBase Exp NoMode
et)

-- | Replace type variables inferred by the unsized type checker
-- with their solutions, instantiating their sizes with fresh
-- (non-absorbable) size variables. See Note [Size Inference] in
-- Language.Futhark.TypeChecker.Terms.
replaceTyVars :: SrcLoc -> TypeBase Size o -> TermTypeM (TypeBase Size o)
replaceTyVars :: forall o. SrcLoc -> TypeBase Exp o -> TermTypeM (TypeBase Exp o)
replaceTyVars = Bool -> SrcLoc -> TypeBase Exp o -> TermTypeM (TypeBase Exp o)
forall o.
Bool -> SrcLoc -> TypeBase Exp o -> TermTypeM (TypeBase Exp o)
replaceTyVarsWith Bool
False

-- | Like 'replaceTyVars', but the fresh sizes may be determined to
-- be existential by unification, like instantiated sizes. This is
-- used for holes, which adopt whatever type the context provides.
-- See Note [Size Inference] in Language.Futhark.TypeChecker.Terms.
replaceTyVarsAbsorbable :: SrcLoc -> TypeBase Size o -> TermTypeM (TypeBase Size o)
replaceTyVarsAbsorbable :: forall o. SrcLoc -> TypeBase Exp o -> TermTypeM (TypeBase Exp o)
replaceTyVarsAbsorbable = Bool -> SrcLoc -> TypeBase Exp o -> TermTypeM (TypeBase Exp o)
forall o.
Bool -> SrcLoc -> TypeBase Exp o -> TermTypeM (TypeBase Exp o)
replaceTyVarsWith Bool
True

replaceTyVarsWith :: Bool -> SrcLoc -> TypeBase Size o -> TermTypeM (TypeBase Size o)
replaceTyVarsWith :: forall o.
Bool -> SrcLoc -> TypeBase Exp o -> TermTypeM (TypeBase Exp o)
replaceTyVarsWith Bool
absorbable SrcLoc
loc TypeBase Exp o
orig_t = do
  tyvars <- (TermEnv -> Map VName (TypeBase () NoMode))
-> TermTypeM (Map VName (TypeBase () NoMode))
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks TermEnv -> Map VName (TypeBase () NoMode)
termTyVars
  let f ::
        TypeBase Size o ->
        StateT (M.Map VName (TypeBase Size NoMode)) TermTypeM (TypeBase Size o)
      f (Scalar (Prim PrimType
t)) = TypeBase Exp o
-> StateT (Map VName StructType) TermTypeM (TypeBase Exp o)
forall a. a -> StateT (Map VName StructType) TermTypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeBase Exp o
 -> StateT (Map VName StructType) TermTypeM (TypeBase Exp o))
-> TypeBase Exp o
-> StateT (Map VName StructType) TermTypeM (TypeBase Exp o)
forall a b. (a -> b) -> a -> b
$ ScalarTypeBase Exp o -> TypeBase Exp o
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (ScalarTypeBase Exp o -> TypeBase Exp o)
-> ScalarTypeBase Exp o -> TypeBase Exp o
forall a b. (a -> b) -> a -> b
$ PrimType -> ScalarTypeBase Exp o
forall dim o. PrimType -> ScalarTypeBase dim o
Prim PrimType
t
      f
        (Scalar (TypeVar o
o (QualName [] VName
v) []))
          | Just TypeBase () NoMode
t <- VName
-> Map VName (TypeBase () NoMode) -> Maybe (TypeBase () NoMode)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
v Map VName (TypeBase () NoMode)
tyvars = do
              -- Multiple occurrences of the same type variable must
              -- be given the same sizes.
              seen <- StateT (Map VName StructType) TermTypeM (Map VName StructType)
forall s (m :: * -> *). MonadState s m => m s
get
              case M.lookup v seen of
                Just StructType
t' -> TypeBase Exp o
-> StateT (Map VName StructType) TermTypeM (TypeBase Exp o)
forall a. a -> StateT (Map VName StructType) TermTypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeBase Exp o
 -> StateT (Map VName StructType) TermTypeM (TypeBase Exp o))
-> TypeBase Exp o
-> StateT (Map VName StructType) TermTypeM (TypeBase Exp o)
forall a b. (a -> b) -> a -> b
$ (NoMode -> o) -> StructType -> TypeBase Exp o
forall b c a. (b -> c) -> TypeBase a b -> TypeBase a c
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (o -> NoMode -> o
forall a b. a -> b -> a
const o
o) StructType
t'
                Maybe StructType
Nothing -> do
                  let usage :: Usage
usage = SrcLoc -> Text -> Usage
forall a. Located a => a -> Text -> Usage
mkUsage SrcLoc
loc Text
"replaceTyVars"
                  (t', drepl) <-
                    TermTypeM (TypeBase Exp o, Map VName ())
-> StateT
     (Map VName StructType) TermTypeM (TypeBase Exp o, Map VName ())
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (Map VName StructType) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TermTypeM (TypeBase Exp o, Map VName ())
 -> StateT
      (Map VName StructType) TermTypeM (TypeBase Exp o, Map VName ()))
-> TermTypeM (TypeBase Exp o, Map VName ())
-> StateT
     (Map VName StructType) TermTypeM (TypeBase Exp o, Map VName ())
forall a b. (a -> b) -> a -> b
$ Usage
-> Rigidity
-> Name
-> TypeBase () o
-> TermTypeM (TypeBase Exp o, Map VName ())
forall (m :: * -> *) d o.
MonadUnify m =>
Usage
-> Rigidity
-> Name
-> TypeBase d o
-> m (TypeBase Exp o, Map VName d)
allDimsFreshInType Usage
usage Rigidity
Nonrigid Name
"dv" ((NoMode -> o) -> TypeBase () NoMode -> TypeBase () o
forall b c a. (b -> c) -> TypeBase a b -> TypeBase a c
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (o -> NoMode -> o
forall a b. a -> b -> a
const o
o) TypeBase () NoMode
t)
                  -- The sizes are instantiated sizes: 'Unlifted' unless
                  -- absorbable, so they can be linked to binders of the
                  -- type itself (reconstructing dependent function
                  -- types) but only absorb existentials when absorbable.
                  -- See Note [Size Inference].
                  lift . forM_ (M.keys drepl) $ \VName
d ->
                    VName -> Constraint -> TermTypeM ()
constrain VName
d (Constraint -> TermTypeM ()) -> Constraint -> TermTypeM ()
forall a b. (a -> b) -> a -> b
$ Liftedness -> Usage -> Constraint
InstSize (if Bool
absorbable then Liftedness
Lifted else Liftedness
Unlifted) Usage
usage
                  lift $ registerBinders (locOf loc) t'
                  modify $ M.insert v $ second (const NoMode) t'
                  pure t'
          | Bool
otherwise =
              TypeBase Exp o
-> StateT (Map VName StructType) TermTypeM (TypeBase Exp o)
forall a. a -> StateT (Map VName StructType) TermTypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeBase Exp o
 -> StateT (Map VName StructType) TermTypeM (TypeBase Exp o))
-> TypeBase Exp o
-> StateT (Map VName StructType) TermTypeM (TypeBase Exp o)
forall a b. (a -> b) -> a -> b
$ ScalarTypeBase Exp o -> TypeBase Exp o
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (o -> QualName VName -> [TypeArg Exp] -> ScalarTypeBase Exp o
forall dim o.
o -> QualName VName -> [TypeArg dim] -> ScalarTypeBase dim o
TypeVar o
o ([VName] -> VName -> QualName VName
forall vn. [vn] -> vn -> QualName vn
QualName [] VName
v) [])
      f (Scalar (TypeVar o
o QualName VName
qn [TypeArg Exp]
targs)) =
        ScalarTypeBase Exp o -> TypeBase Exp o
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (ScalarTypeBase Exp o -> TypeBase Exp o)
-> ([TypeArg Exp] -> ScalarTypeBase Exp o)
-> [TypeArg Exp]
-> TypeBase Exp o
forall b c a. (b -> c) -> (a -> b) -> a -> c
. o -> QualName VName -> [TypeArg Exp] -> ScalarTypeBase Exp o
forall dim o.
o -> QualName VName -> [TypeArg dim] -> ScalarTypeBase dim o
TypeVar o
o QualName VName
qn ([TypeArg Exp] -> TypeBase Exp o)
-> StateT (Map VName StructType) TermTypeM [TypeArg Exp]
-> StateT (Map VName StructType) TermTypeM (TypeBase Exp o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TypeArg Exp
 -> StateT (Map VName StructType) TermTypeM (TypeArg Exp))
-> [TypeArg Exp]
-> StateT (Map VName StructType) TermTypeM [TypeArg Exp]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM TypeArg Exp
-> StateT (Map VName StructType) TermTypeM (TypeArg Exp)
onTyArg [TypeArg Exp]
targs
        where
          onTyArg :: TypeArg Exp
-> StateT (Map VName StructType) TermTypeM (TypeArg Exp)
onTyArg (TypeArgDim Exp
e) = TypeArg Exp
-> StateT (Map VName StructType) TermTypeM (TypeArg Exp)
forall a. a -> StateT (Map VName StructType) TermTypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeArg Exp
 -> StateT (Map VName StructType) TermTypeM (TypeArg Exp))
-> TypeArg Exp
-> StateT (Map VName StructType) TermTypeM (TypeArg Exp)
forall a b. (a -> b) -> a -> b
$ Exp -> TypeArg Exp
forall dim. dim -> TypeArg dim
TypeArgDim Exp
e
          onTyArg (TypeArgType StructType
t) = StructType -> TypeArg Exp
forall dim. TypeBase dim NoMode -> TypeArg dim
TypeArgType (StructType -> TypeArg Exp)
-> StateT (Map VName StructType) TermTypeM StructType
-> StateT (Map VName StructType) TermTypeM (TypeArg Exp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StructType -> StateT (Map VName StructType) TermTypeM StructType
forall o.
TypeBase Exp o
-> StateT (Map VName StructType) TermTypeM (TypeBase Exp o)
f StructType
t
      f (Scalar (Record Map Name (TypeBase Exp o)
fs)) =
        ScalarTypeBase Exp o -> TypeBase Exp o
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (ScalarTypeBase Exp o -> TypeBase Exp o)
-> (Map Name (TypeBase Exp o) -> ScalarTypeBase Exp o)
-> Map Name (TypeBase Exp o)
-> TypeBase Exp o
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Name (TypeBase Exp o) -> ScalarTypeBase Exp o
forall dim o. Map Name (TypeBase dim o) -> ScalarTypeBase dim o
Record (Map Name (TypeBase Exp o) -> TypeBase Exp o)
-> StateT
     (Map VName StructType) TermTypeM (Map Name (TypeBase Exp o))
-> StateT (Map VName StructType) TermTypeM (TypeBase Exp o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TypeBase Exp o
 -> StateT (Map VName StructType) TermTypeM (TypeBase Exp o))
-> Map Name (TypeBase Exp o)
-> StateT
     (Map VName StructType) TermTypeM (Map Name (TypeBase Exp o))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Map Name a -> f (Map Name b)
traverse TypeBase Exp o
-> StateT (Map VName StructType) TermTypeM (TypeBase Exp o)
forall o.
TypeBase Exp o
-> StateT (Map VName StructType) TermTypeM (TypeBase Exp o)
f Map Name (TypeBase Exp o)
fs
      f (Scalar (Sum Map Name [TypeBase Exp o]
fs)) =
        ScalarTypeBase Exp o -> TypeBase Exp o
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (ScalarTypeBase Exp o -> TypeBase Exp o)
-> (Map Name [TypeBase Exp o] -> ScalarTypeBase Exp o)
-> Map Name [TypeBase Exp o]
-> TypeBase Exp o
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Name [TypeBase Exp o] -> ScalarTypeBase Exp o
forall dim o. Map Name [TypeBase dim o] -> ScalarTypeBase dim o
Sum (Map Name [TypeBase Exp o] -> TypeBase Exp o)
-> StateT
     (Map VName StructType) TermTypeM (Map Name [TypeBase Exp o])
-> StateT (Map VName StructType) TermTypeM (TypeBase Exp o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([TypeBase Exp o]
 -> StateT (Map VName StructType) TermTypeM [TypeBase Exp o])
-> Map Name [TypeBase Exp o]
-> StateT
     (Map VName StructType) TermTypeM (Map Name [TypeBase Exp o])
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Map Name a -> f (Map Name b)
traverse ((TypeBase Exp o
 -> StateT (Map VName StructType) TermTypeM (TypeBase Exp o))
-> [TypeBase Exp o]
-> StateT (Map VName StructType) TermTypeM [TypeBase Exp o]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM TypeBase Exp o
-> StateT (Map VName StructType) TermTypeM (TypeBase Exp o)
forall o.
TypeBase Exp o
-> StateT (Map VName StructType) TermTypeM (TypeBase Exp o)
f) Map Name [TypeBase Exp o]
fs
      f (Scalar (Arrow o
o PName
pname Diet
d StructType
ta (RetType [VName]
ext ResType
tr))) = do
        ta' <- StructType -> StateT (Map VName StructType) TermTypeM StructType
forall o.
TypeBase Exp o
-> StateT (Map VName StructType) TermTypeM (TypeBase Exp o)
f StructType
ta
        tr' <- f tr
        pure $ Scalar $ Arrow o pname d ta' $ RetType ext tr'
      f (Array o
o Shape Exp
shape ScalarTypeBase Exp NoMode
t) =
        o -> Shape Exp -> StructType -> TypeBase Exp o
forall o dim o'.
o -> Shape dim -> TypeBase dim o' -> TypeBase dim o
arrayOfWithAliases o
o Shape Exp
shape (StructType -> TypeBase Exp o)
-> StateT (Map VName StructType) TermTypeM StructType
-> StateT (Map VName StructType) TermTypeM (TypeBase Exp o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StructType -> StateT (Map VName StructType) TermTypeM StructType
forall o.
TypeBase Exp o
-> StateT (Map VName StructType) TermTypeM (TypeBase Exp o)
f (ScalarTypeBase Exp NoMode -> StructType
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar ScalarTypeBase Exp NoMode
t)

  evalStateT (f orig_t) mempty

-- | Instantiate the type parameters of a type scheme with the types
-- inferred by the unsized type checker, creating fresh variables for
-- their sizes. See Note [Size Inference] in
-- Language.Futhark.TypeChecker.Terms.
instTyVars ::
  (Substitutable (TypeBase Size o)) =>
  SrcLoc ->
  -- | The type parameters being instantiated, along with their
  -- liftedness.
  M.Map VName Liftedness ->
  TypeBase () o ->
  TypeBase Size o ->
  TermTypeM (TypeBase Size o)
instTyVars :: forall o.
Substitutable (TypeBase Exp o) =>
SrcLoc
-> Map VName Liftedness
-> TypeBase () o
-> TypeBase Exp o
-> TermTypeM (TypeBase Exp o)
instTyVars SrcLoc
loc Map VName Liftedness
names TypeBase () o
orig_t1 TypeBase Exp o
orig_t2 = do
  tyvars <- (TermEnv -> Map VName (TypeBase () NoMode))
-> TermTypeM (Map VName (TypeBase () NoMode))
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks TermEnv -> Map VName (TypeBase () NoMode)
termTyVars
  let f ::
        TypeBase d o ->
        TypeBase Size o ->
        StateT (M.Map VName (TypeBase Size NoMode)) TermTypeM (TypeBase Size o)
      f
        (Scalar (TypeVar o
o (QualName [] VName
v1) []))
        TypeBase Exp o
t2
          | Just TypeBase () NoMode
t <- VName
-> Map VName (TypeBase () NoMode) -> Maybe (TypeBase () NoMode)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
v1 Map VName (TypeBase () NoMode)
tyvars =
              TypeBase () o
-> TypeBase Exp o
-> StateT (Map VName StructType) TermTypeM (TypeBase Exp o)
forall d o.
TypeBase d o
-> TypeBase Exp o
-> StateT (Map VName StructType) TermTypeM (TypeBase Exp o)
f ((NoMode -> o) -> TypeBase () NoMode -> TypeBase () o
forall b c a. (b -> c) -> TypeBase a b -> TypeBase a c
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (o -> NoMode -> o
forall a b. a -> b -> a
const o
o) TypeBase () NoMode
t) TypeBase Exp o
t2
      f (Scalar (Record Map Name (TypeBase d o)
fs1)) (Scalar (Record Map Name (TypeBase Exp o)
fs2)) =
        ScalarTypeBase Exp o -> TypeBase Exp o
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (ScalarTypeBase Exp o -> TypeBase Exp o)
-> (Map Name (TypeBase Exp o) -> ScalarTypeBase Exp o)
-> Map Name (TypeBase Exp o)
-> TypeBase Exp o
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Name (TypeBase Exp o) -> ScalarTypeBase Exp o
forall dim o. Map Name (TypeBase dim o) -> ScalarTypeBase dim o
Record (Map Name (TypeBase Exp o) -> TypeBase Exp o)
-> StateT
     (Map VName StructType) TermTypeM (Map Name (TypeBase Exp o))
-> StateT (Map VName StructType) TermTypeM (TypeBase Exp o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Name (StateT (Map VName StructType) TermTypeM (TypeBase Exp o))
-> StateT
     (Map VName StructType) TermTypeM (Map Name (TypeBase Exp o))
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => Map Name (m a) -> m (Map Name a)
sequence ((TypeBase d o
 -> TypeBase Exp o
 -> StateT (Map VName StructType) TermTypeM (TypeBase Exp o))
-> Map Name (TypeBase d o)
-> Map Name (TypeBase Exp o)
-> Map
     Name (StateT (Map VName StructType) TermTypeM (TypeBase Exp o))
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith TypeBase d o
-> TypeBase Exp o
-> StateT (Map VName StructType) TermTypeM (TypeBase Exp o)
forall d o.
TypeBase d o
-> TypeBase Exp o
-> StateT (Map VName StructType) TermTypeM (TypeBase Exp o)
f Map Name (TypeBase d o)
fs1 Map Name (TypeBase Exp o)
fs2)
      f (Scalar (Sum Map Name [TypeBase d o]
fs1)) (Scalar (Sum Map Name [TypeBase Exp o]
fs2)) =
        ScalarTypeBase Exp o -> TypeBase Exp o
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (ScalarTypeBase Exp o -> TypeBase Exp o)
-> (Map Name [TypeBase Exp o] -> ScalarTypeBase Exp o)
-> Map Name [TypeBase Exp o]
-> TypeBase Exp o
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Name [TypeBase Exp o] -> ScalarTypeBase Exp o
forall dim o. Map Name [TypeBase dim o] -> ScalarTypeBase dim o
Sum (Map Name [TypeBase Exp o] -> TypeBase Exp o)
-> StateT
     (Map VName StructType) TermTypeM (Map Name [TypeBase Exp o])
-> StateT (Map VName StructType) TermTypeM (TypeBase Exp o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Name (StateT (Map VName StructType) TermTypeM [TypeBase Exp o])
-> StateT
     (Map VName StructType) TermTypeM (Map Name [TypeBase Exp o])
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => Map Name (m a) -> m (Map Name a)
sequence (([TypeBase d o]
 -> [TypeBase Exp o]
 -> StateT (Map VName StructType) TermTypeM [TypeBase Exp o])
-> Map Name [TypeBase d o]
-> Map Name [TypeBase Exp o]
-> Map
     Name (StateT (Map VName StructType) TermTypeM [TypeBase Exp o])
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith ((TypeBase d o
 -> TypeBase Exp o
 -> StateT (Map VName StructType) TermTypeM (TypeBase Exp o))
-> [TypeBase d o]
-> [TypeBase Exp o]
-> StateT (Map VName StructType) TermTypeM [TypeBase Exp o]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM TypeBase d o
-> TypeBase Exp o
-> StateT (Map VName StructType) TermTypeM (TypeBase Exp o)
forall d o.
TypeBase d o
-> TypeBase Exp o
-> StateT (Map VName StructType) TermTypeM (TypeBase Exp o)
f) Map Name [TypeBase d o]
fs1 Map Name [TypeBase Exp o]
fs2)
      -- Note: annotations are always taken from the second type, as
      -- the first (inferred) type comes from the unsized type
      -- checker, which does not track them.
      f
        (Scalar (Arrow o
_ PName
_ Diet
_ TypeBase d NoMode
t1a (RetType [VName]
_ TypeBase d Freshness
t1r)))
        (Scalar (Arrow o
o PName
pname Diet
d StructType
t2a (RetType [VName]
ext ResType
t2r))) = do
          ta <- TypeBase d NoMode
-> StructType -> StateT (Map VName StructType) TermTypeM StructType
forall d o.
TypeBase d o
-> TypeBase Exp o
-> StateT (Map VName StructType) TermTypeM (TypeBase Exp o)
f TypeBase d NoMode
t1a StructType
t2a
          tr <- f t1r t2r
          pure $ Scalar $ Arrow o pname d ta $ RetType ext tr
      f
        (Array o
_ (Shape (d
_ : [d]
ds1)) ScalarTypeBase d NoMode
t1)
        (Array o
o (Shape (Exp
d : [Exp]
ds2)) ScalarTypeBase Exp NoMode
t2) =
          o -> Shape Exp -> StructType -> TypeBase Exp o
forall o dim o'.
o -> Shape dim -> TypeBase dim o' -> TypeBase dim o
arrayOfWithAliases o
o ([Exp] -> Shape Exp
forall dim. [dim] -> Shape dim
Shape [Exp
d])
            (StructType -> TypeBase Exp o)
-> StateT (Map VName StructType) TermTypeM StructType
-> StateT (Map VName StructType) TermTypeM (TypeBase Exp o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeBase d NoMode
-> StructType -> StateT (Map VName StructType) TermTypeM StructType
forall d o.
TypeBase d o
-> TypeBase Exp o
-> StateT (Map VName StructType) TermTypeM (TypeBase Exp o)
f (Shape d -> TypeBase d NoMode -> TypeBase d NoMode
forall dim. Shape dim -> TypeBase dim NoMode -> TypeBase dim NoMode
arrayOf ([d] -> Shape d
forall dim. [dim] -> Shape dim
Shape [d]
ds1) (ScalarTypeBase d NoMode -> TypeBase d NoMode
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar ScalarTypeBase d NoMode
t1)) (Shape Exp -> StructType -> StructType
forall dim. Shape dim -> TypeBase dim NoMode -> TypeBase dim NoMode
arrayOf ([Exp] -> Shape Exp
forall dim. [dim] -> Shape dim
Shape [Exp]
ds2) (ScalarTypeBase Exp NoMode -> StructType
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar ScalarTypeBase Exp NoMode
t2))
      f
        (Scalar (TypeVar o
_ QualName VName
v1 [TypeArg d]
targs1))
        (Scalar (TypeVar o
o QualName VName
v2 [TypeArg Exp]
targs2))
          -- If v2 is a type parameter being instantiated, it must be
          -- handled by the general case below.
          | QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
v2 VName -> Map VName Liftedness -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`M.notMember` Map VName Liftedness
names,
            [TypeArg d] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeArg d]
targs1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [TypeArg Exp] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeArg Exp]
targs2 =
              ScalarTypeBase Exp o -> TypeBase Exp o
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (ScalarTypeBase Exp o -> TypeBase Exp o)
-> ([TypeArg Exp] -> ScalarTypeBase Exp o)
-> [TypeArg Exp]
-> TypeBase Exp o
forall b c a. (b -> c) -> (a -> b) -> a -> c
. o -> QualName VName -> [TypeArg Exp] -> ScalarTypeBase Exp o
forall dim o.
o -> QualName VName -> [TypeArg dim] -> ScalarTypeBase dim o
TypeVar o
o QualName VName
v1 ([TypeArg Exp] -> TypeBase Exp o)
-> StateT (Map VName StructType) TermTypeM [TypeArg Exp]
-> StateT (Map VName StructType) TermTypeM (TypeBase Exp o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TypeArg d
 -> TypeArg Exp
 -> StateT (Map VName StructType) TermTypeM (TypeArg Exp))
-> [TypeArg d]
-> [TypeArg Exp]
-> StateT (Map VName StructType) TermTypeM [TypeArg Exp]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM TypeArg d
-> TypeArg Exp
-> StateT (Map VName StructType) TermTypeM (TypeArg Exp)
forall {d}.
TypeArg d
-> TypeArg Exp
-> StateT (Map VName StructType) TermTypeM (TypeArg Exp)
g [TypeArg d]
targs1 [TypeArg Exp]
targs2
          where
            g :: TypeArg d
-> TypeArg Exp
-> StateT (Map VName StructType) TermTypeM (TypeArg Exp)
g (TypeArgType TypeBase d NoMode
t1) (TypeArgType StructType
t2) =
              StructType -> TypeArg Exp
forall dim. TypeBase dim NoMode -> TypeArg dim
TypeArgType (StructType -> TypeArg Exp)
-> StateT (Map VName StructType) TermTypeM StructType
-> StateT (Map VName StructType) TermTypeM (TypeArg Exp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeBase d NoMode
-> StructType -> StateT (Map VName StructType) TermTypeM StructType
forall d o.
TypeBase d o
-> TypeBase Exp o
-> StateT (Map VName StructType) TermTypeM (TypeBase Exp o)
f TypeBase d NoMode
t1 StructType
t2
            g TypeArg d
_ TypeArg Exp
targ = TypeArg Exp
-> StateT (Map VName StructType) TermTypeM (TypeArg Exp)
forall a. a -> StateT (Map VName StructType) TermTypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TypeArg Exp
targ
      f TypeBase d o
t1 TypeBase Exp o
t2 = do
        let usage :: Usage
usage = SrcLoc -> Text -> Usage
forall a. Located a => a -> Text -> Usage
mkUsage SrcLoc
loc Text
"instantiation"
            mkNew :: StateT (Map VName StructType) TermTypeM (TypeBase Exp o)
mkNew = (TypeBase Exp o, Map VName d) -> TypeBase Exp o
forall a b. (a, b) -> a
fst ((TypeBase Exp o, Map VName d) -> TypeBase Exp o)
-> StateT
     (Map VName StructType) TermTypeM (TypeBase Exp o, Map VName d)
-> StateT (Map VName StructType) TermTypeM (TypeBase Exp o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TermTypeM (TypeBase Exp o, Map VName d)
-> StateT
     (Map VName StructType) TermTypeM (TypeBase Exp o, Map VName d)
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (Map VName StructType) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Usage
-> Rigidity
-> Name
-> TypeBase d o
-> TermTypeM (TypeBase Exp o, Map VName d)
forall (m :: * -> *) d o.
MonadUnify m =>
Usage
-> Rigidity
-> Name
-> TypeBase d o
-> m (TypeBase Exp o, Map VName d)
allDimsFreshInType Usage
usage Rigidity
Nonrigid Name
"dv" TypeBase d o
t1)
        case TypeBase Exp o
t2 of
          Scalar (TypeVar o
o (QualName [] VName
v2) [])
            | Just Liftedness
l <- VName -> Map VName Liftedness -> Maybe Liftedness
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
v2 Map VName Liftedness
names -> do
                seen <- StateT (Map VName StructType) TermTypeM (Map VName StructType)
forall s (m :: * -> *). MonadState s m => m s
get
                case M.lookup v2 seen of
                  Maybe StructType
Nothing -> do
                    (t, drepl) <- TermTypeM (TypeBase Exp o, Map VName d)
-> StateT
     (Map VName StructType) TermTypeM (TypeBase Exp o, Map VName d)
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (Map VName StructType) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TermTypeM (TypeBase Exp o, Map VName d)
 -> StateT
      (Map VName StructType) TermTypeM (TypeBase Exp o, Map VName d))
-> TermTypeM (TypeBase Exp o, Map VName d)
-> StateT
     (Map VName StructType) TermTypeM (TypeBase Exp o, Map VName d)
forall a b. (a -> b) -> a -> b
$ Usage
-> Rigidity
-> Name
-> TypeBase d o
-> TermTypeM (TypeBase Exp o, Map VName d)
forall (m :: * -> *) d o.
MonadUnify m =>
Usage
-> Rigidity
-> Name
-> TypeBase d o
-> m (TypeBase Exp o, Map VName d)
allDimsFreshInType Usage
usage Rigidity
Nonrigid Name
"dv" TypeBase d o
t1
                    -- These are canonical instantiated sizes, which
                    -- unification may determine to be existential.
                    lift $ forM_ (M.keys drepl) $ \VName
d ->
                      VName -> Constraint -> TermTypeM ()
constrain VName
d (Constraint -> TermTypeM ()) -> Constraint -> TermTypeM ()
forall a b. (a -> b) -> a -> b
$ Liftedness -> Usage -> Constraint
InstSize Liftedness
l Usage
usage
                    -- Named parameters of arrows inside the instantiated type
                    -- are registered as size parameters, such that unification
                    -- can reconstruct dependent function types by linking
                    -- instantiated sizes to them.
                    unless (null drepl) $ lift $ registerBinders (locOf loc) t
                    modify $ M.insert v2 $ second (const NoMode) t
                    pure t
                  Just StructType
t -> do
                    -- Another occurrence of an already instantiated
                    -- type parameter. The sizes must be given
                    -- distinct names, as each occurrence denotes a
                    -- distinct existential size if the instantiated
                    -- size turns out to be existential.
                    occ <- TermTypeM Int -> StateT (Map VName StructType) TermTypeM Int
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (Map VName StructType) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift TermTypeM Int
incCounter
                    let onDim (Var (QualName [VName]
_ VName
c) f StructType
info SrcLoc
dloc) = do
                          d <- TermTypeM VName -> t TermTypeM VName
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TermTypeM VName -> t TermTypeM VName)
-> TermTypeM VName -> t TermTypeM VName
forall a b. (a -> b) -> a -> b
$ Usage -> Rigidity -> Name -> TermTypeM VName
forall (m :: * -> *).
MonadUnify m =>
Usage -> Rigidity -> Name -> m VName
newDimVar Usage
usage Rigidity
Nonrigid Name
"dv"
                          lift $ constrain d $ CopySize c occ usage
                          pure $ Var (qualName d) info dloc
                        onDim ExpBase f VName
d = ExpBase f VName -> t TermTypeM (ExpBase f VName)
forall a. a -> t TermTypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ExpBase f VName
d
                    second (const o) <$> bitraverse onDim pure t
          TypeBase Exp o
_ -> StateT (Map VName StructType) TermTypeM (TypeBase Exp o)
mkNew

  (t, seen) <- runStateT (f orig_t1 orig_t2) mempty
  -- The walk above replaces occurrences of the type parameters at the type
  -- level, but the types of expressions that occur as *sizes* in the original
  -- type may also refer to the type parameters (e.g. a size 'length s - k'
  -- where 's' has a parametric type). An ordinary substitution fixes those, as
  -- substitution on expressions descends into their types.
  let substs = (StructType -> Subst (RetTypeBase Exp NoMode))
-> Map VName StructType
-> Map VName (Subst (RetTypeBase Exp NoMode))
forall a b k. (a -> b) -> Map k a -> Map k b
M.map ([TypeParam]
-> RetTypeBase Exp NoMode -> Subst (RetTypeBase Exp NoMode)
forall t. [TypeParam] -> t -> Subst t
Subst [] (RetTypeBase Exp NoMode -> Subst (RetTypeBase Exp NoMode))
-> (StructType -> RetTypeBase Exp NoMode)
-> StructType
-> Subst (RetTypeBase Exp NoMode)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [VName] -> StructType -> RetTypeBase Exp NoMode
forall dim o. [VName] -> TypeBase dim o -> RetTypeBase dim o
RetType []) Map VName StructType
seen
  pure $ applySubst (`M.lookup` substs) t

-- | Instantiate a type scheme with fresh variables for its size and
-- type parameters. Returns the names of the fresh size and type
-- variables and the instantiated type.
instTypeScheme ::
  QualName VName ->
  SrcLoc ->
  [TypeParam] ->
  StructType ->
  TypeBase () NoMode ->
  TermTypeM ([VName], StructType)
instTypeScheme :: QualName VName
-> SrcLoc
-> [TypeParam]
-> StructType
-> TypeBase () NoMode
-> TermTypeM ([VName], StructType)
instTypeScheme QualName VName
qn SrcLoc
loc [TypeParam]
tparams StructType
scheme_t TypeBase () NoMode
inferred = do
  (names, substs) <- ([Maybe (VName, (VName, Subst (RetTypeBase Exp NoMode)))]
 -> ([VName], [(VName, Subst (RetTypeBase Exp NoMode))]))
-> TermTypeM
     [Maybe (VName, (VName, Subst (RetTypeBase Exp NoMode)))]
-> TermTypeM ([VName], [(VName, Subst (RetTypeBase Exp NoMode))])
forall a b. (a -> b) -> TermTypeM a -> TermTypeM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(VName, (VName, Subst (RetTypeBase Exp NoMode)))]
-> ([VName], [(VName, Subst (RetTypeBase Exp NoMode))])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(VName, (VName, Subst (RetTypeBase Exp NoMode)))]
 -> ([VName], [(VName, Subst (RetTypeBase Exp NoMode))]))
-> ([Maybe (VName, (VName, Subst (RetTypeBase Exp NoMode)))]
    -> [(VName, (VName, Subst (RetTypeBase Exp NoMode)))])
-> [Maybe (VName, (VName, Subst (RetTypeBase Exp NoMode)))]
-> ([VName], [(VName, Subst (RetTypeBase Exp NoMode))])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Maybe (VName, (VName, Subst (RetTypeBase Exp NoMode)))]
-> [(VName, (VName, Subst (RetTypeBase Exp NoMode)))]
forall a. [Maybe a] -> [a]
catMaybes) (TermTypeM [Maybe (VName, (VName, Subst (RetTypeBase Exp NoMode)))]
 -> TermTypeM ([VName], [(VName, Subst (RetTypeBase Exp NoMode))]))
-> ((TypeParam
     -> TermTypeM
          (Maybe (VName, (VName, Subst (RetTypeBase Exp NoMode)))))
    -> TermTypeM
         [Maybe (VName, (VName, Subst (RetTypeBase Exp NoMode)))])
-> (TypeParam
    -> TermTypeM
         (Maybe (VName, (VName, Subst (RetTypeBase Exp NoMode)))))
-> TermTypeM ([VName], [(VName, Subst (RetTypeBase Exp NoMode))])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TypeParam]
-> (TypeParam
    -> TermTypeM
         (Maybe (VName, (VName, Subst (RetTypeBase Exp NoMode)))))
-> TermTypeM
     [Maybe (VName, (VName, Subst (RetTypeBase Exp NoMode)))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [TypeParam]
tparams ((TypeParam
  -> TermTypeM
       (Maybe (VName, (VName, Subst (RetTypeBase Exp NoMode)))))
 -> TermTypeM ([VName], [(VName, Subst (RetTypeBase Exp NoMode))]))
-> (TypeParam
    -> TermTypeM
         (Maybe (VName, (VName, Subst (RetTypeBase Exp NoMode)))))
-> TermTypeM ([VName], [(VName, Subst (RetTypeBase Exp NoMode))])
forall a b. (a -> b) -> a -> b
$ \TypeParam
tparam -> do
    case TypeParam
tparam of
      TypeParamType {} -> Maybe (VName, (VName, Subst (RetTypeBase Exp NoMode)))
-> TermTypeM
     (Maybe (VName, (VName, Subst (RetTypeBase Exp NoMode))))
forall a. a -> TermTypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (VName, (VName, Subst (RetTypeBase Exp NoMode)))
forall a. Maybe a
Nothing
      TypeParamDim VName
v SrcLoc
_ -> do
        i <- TermTypeM Int
incCounter
        v' <- newID $ mkTypeVarName (baseName v) i
        -- The instantiation of a size parameter may turn out to be
        -- an existential size, when the value whose type contains it
        -- is returned from a function argument.
        constrain v' . InstSize Lifted . mkUsage loc . docText $
          "instantiated size parameter of " <> dquotes (pretty qn)
        pure $ Just (v', (v, ExpSubst $ sizeFromName (qualName v') loc))

  let tp_names = [(VName, Liftedness)] -> Map VName Liftedness
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(VName, Liftedness)] -> Map VName Liftedness)
-> [(VName, Liftedness)] -> Map VName Liftedness
forall a b. (a -> b) -> a -> b
$ (TypeParam -> Maybe (VName, Liftedness))
-> [TypeParam] -> [(VName, Liftedness)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe TypeParam -> Maybe (VName, Liftedness)
forall {a}. TypeParamBase a -> Maybe (a, Liftedness)
tpName [TypeParam]
tparams
      tpName (TypeParamType Liftedness
l a
v SrcLoc
_) = (a, Liftedness) -> Maybe (a, Liftedness)
forall a. a -> Maybe a
Just (a
v, Liftedness
l)
      tpName TypeParamDim {} = Maybe (a, Liftedness)
forall a. Maybe a
Nothing
  t' <- instTyVars loc tp_names inferred $ applySubst (`lookup` substs) scheme_t
  pure (names, t')

lookupQualNameEnv :: QualName VName -> TermTypeM (TermScope Size)
lookupQualNameEnv :: QualName VName -> TermTypeM (TermScope Exp)
lookupQualNameEnv QualName VName
qn = (TermEnv -> TermScope Exp) -> TermTypeM (TermScope Exp)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ((TermEnv -> TermScope Exp) -> TermTypeM (TermScope Exp))
-> (TermEnv -> TermScope Exp) -> TermTypeM (TermScope Exp)
forall a b. (a -> b) -> a -> b
$ \TermEnv
tenv -> (StructType -> StructType)
-> TermScope Exp -> QualName VName -> TermScope Exp
forall dim.
(StructType -> TypeBase dim NoMode)
-> TermScope dim -> QualName VName -> TermScope dim
Scope.lookupQualNameEnv StructType -> StructType
forall a. a -> a
id (TermEnv -> TermScope Exp
termScope TermEnv
tenv) QualName VName
qn

lookupMod :: QualName VName -> TermTypeM Mod
lookupMod :: QualName VName -> TermTypeM Mod
lookupMod qn :: QualName VName
qn@(QualName [VName]
_ VName
name) = do
  scope <- QualName VName -> TermTypeM (TermScope Exp)
lookupQualNameEnv QualName VName
qn
  case M.lookup name $ scopeModTable scope of
    Maybe Mod
Nothing -> String -> TermTypeM Mod
forall a. HasCallStack => String -> a
error (String -> TermTypeM Mod) -> String -> TermTypeM Mod
forall a b. (a -> b) -> a -> b
$ String
"lookupMod: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> QualName VName -> String
forall a. Show a => a -> String
show QualName VName
qn
    Just Mod
m -> Mod -> TermTypeM Mod
forall a. a -> TermTypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Mod
m

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

instance MonadTypeChecker TermTypeM where
  warnings :: Warnings -> TermTypeM ()
warnings Warnings
ws =
    (TermTypeState -> TermTypeState) -> TermTypeM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((TermTypeState -> TermTypeState) -> TermTypeM ())
-> (TermTypeState -> TermTypeState) -> TermTypeM ()
forall a b. (a -> b) -> a -> b
$ \TermTypeState
s -> TermTypeState
s {stateWarnings = stateWarnings s <> ws}

  warn :: forall loc. Located loc => loc -> Doc () -> TermTypeM ()
warn loc
loc Doc ()
problem = Warnings -> TermTypeM ()
forall (m :: * -> *). MonadTypeChecker m => Warnings -> m ()
warnings (Warnings -> TermTypeM ()) -> Warnings -> TermTypeM ()
forall a b. (a -> b) -> a -> b
$ Loc -> Doc () -> Warnings
singleWarning (loc -> Loc
forall a. Located a => a -> Loc
locOf loc
loc) Doc ()
problem

  newName :: VName -> TermTypeM VName
newName VName
v = do
    s <- TermTypeM TermTypeState
forall s (m :: * -> *). MonadState s m => m s
get
    let (v', src') = Futhark.FreshNames.newName (stateNameSource s) v
    put $ s {stateNameSource = src'}
    pure v'

  newTypeName :: Name -> TermTypeM VName
newTypeName Name
name = do
    i <- TermTypeM Int
incCounter
    newID $ mkTypeVarName name i

  bindVal :: forall a. VName -> BoundV -> TermTypeM a -> TermTypeM a
bindVal VName
v (TypeM.BoundV [TypeParam]
tps StructType
t) = (TermScope Exp -> TermScope Exp) -> TermTypeM a -> TermTypeM a
forall a.
(TermScope Exp -> TermScope Exp) -> TermTypeM a -> TermTypeM a
localScope ((TermScope Exp -> TermScope Exp) -> TermTypeM a -> TermTypeM a)
-> (TermScope Exp -> TermScope Exp) -> TermTypeM a -> TermTypeM a
forall a b. (a -> b) -> a -> b
$ \TermScope Exp
scope ->
    TermScope Exp
scope {scopeVtable = M.insert v (BoundV tps t) $ scopeVtable scope}

  lookupType :: QualName VName
-> TermTypeM ([TypeParam], RetTypeBase Exp NoMode, Liftedness)
lookupType QualName VName
qn = do
    outer_env <- (TermEnv -> Env) -> TermTypeM Env
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks TermEnv -> Env
termOuterEnv
    scope <- lookupQualNameEnv qn
    case M.lookup (qualLeaf qn) $ scopeTypeTable scope of
      Maybe TypeBinding
Nothing -> String
-> TermTypeM ([TypeParam], RetTypeBase Exp NoMode, Liftedness)
forall a. HasCallStack => String -> a
error (String
 -> TermTypeM ([TypeParam], RetTypeBase Exp NoMode, Liftedness))
-> String
-> TermTypeM ([TypeParam], RetTypeBase Exp NoMode, Liftedness)
forall a b. (a -> b) -> a -> b
$ String
"lookupType: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> QualName VName -> String
forall a. Show a => a -> String
show QualName VName
qn
      Just (TypeAbbr Liftedness
l [TypeParam]
ps (RetType [VName]
dims StructType
def)) ->
        ([TypeParam], RetTypeBase Exp NoMode, Liftedness)
-> TermTypeM ([TypeParam], RetTypeBase Exp NoMode, Liftedness)
forall a. a -> TermTypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
          ( [TypeParam]
ps,
            [VName] -> StructType -> RetTypeBase Exp NoMode
forall dim o. [VName] -> TypeBase dim o -> RetTypeBase dim o
RetType [VName]
dims (StructType -> RetTypeBase Exp NoMode)
-> StructType -> RetTypeBase Exp NoMode
forall a b. (a -> b) -> a -> b
$ Env -> [VName] -> [VName] -> StructType -> StructType
forall o.
Env -> [VName] -> [VName] -> TypeBase Exp o -> TypeBase Exp o
qualifyTypeVars Env
outer_env ((TypeParam -> VName) -> [TypeParam] -> [VName]
forall a b. (a -> b) -> [a] -> [b]
map TypeParam -> VName
forall vn. TypeParamBase vn -> vn
typeParamName [TypeParam]
ps) (QualName VName -> [VName]
forall vn. QualName vn -> [vn]
qualQuals QualName VName
qn) StructType
def,
            Liftedness
l
          )

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

lookupVar :: SrcLoc -> QualName VName -> StructType -> TermTypeM StructType
lookupVar :: SrcLoc -> QualName VName -> StructType -> TermTypeM StructType
lookupVar SrcLoc
loc qn :: QualName VName
qn@(QualName [VName]
qs VName
name) StructType
inst_t = do
  scope <- QualName VName -> TermTypeM (TermScope Exp)
lookupQualNameEnv QualName VName
qn
  outer_env <- asks termOuterEnv
  -- Top-level value bindings are not in the term scope (see
  -- 'envToTermScopeNoVals'); look them up on demand in the outer
  -- environment.
  case M.lookup name (scopeVtable scope)
    `mplus` Scope.lookupOuterVal id outer_env name of
    Maybe (ValBinding Exp)
Nothing ->
      String -> TermTypeM StructType
forall a. HasCallStack => String -> a
error (String -> TermTypeM StructType) -> String -> TermTypeM StructType
forall a b. (a -> b) -> a -> b
$ String
"lookupVar: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> QualName VName -> String
forall a. Show a => a -> String
show QualName VName
qn
    Just (BoundV [TypeParam]
tparams StructType
bound_t) ->
      if [TypeParam] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TypeParam]
tparams Bool -> Bool -> Bool
&& [VName] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [VName]
qs
        then StructType -> TermTypeM StructType
forall a. a -> TermTypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure StructType
bound_t
        else do
          (tnames, t) <- QualName VName
-> SrcLoc
-> [TypeParam]
-> StructType
-> TypeBase () NoMode
-> TermTypeM ([VName], StructType)
instTypeScheme QualName VName
qn SrcLoc
loc [TypeParam]
tparams StructType
bound_t (TypeBase () NoMode -> TermTypeM ([VName], StructType))
-> TypeBase () NoMode -> TermTypeM ([VName], StructType)
forall a b. (a -> b) -> a -> b
$ (Exp -> ()) -> StructType -> TypeBase () NoMode
forall a b c. (a -> b) -> TypeBase a c -> TypeBase b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (() -> Exp -> ()
forall a b. a -> b -> a
const ()) StructType
inst_t
          pure $ qualifyTypeVars outer_env tnames qs t
    Just ValBinding Exp
EqualityF ->
      SrcLoc -> StructType -> TermTypeM StructType
forall o. SrcLoc -> TypeBase Exp o -> TermTypeM (TypeBase Exp o)
replaceTyVars SrcLoc
loc StructType
inst_t
    Just OverloadedF {} ->
      SrcLoc -> StructType -> TermTypeM StructType
forall o. SrcLoc -> TypeBase Exp o -> TermTypeM (TypeBase Exp o)
replaceTyVars SrcLoc
loc StructType
inst_t
    -- See Note [Checking recursive functions] in
    -- Language.Futhark.TypeChecker.Terms.
    Just ValBinding Exp
RecursiveV -> do
      (ext, t) <- StructType -> ([VName], StructType)
forall o. TypeBase Exp o -> ([VName], TypeBase Exp o)
existentialResult (StructType -> ([VName], StructType))
-> TermTypeM StructType -> TermTypeM ([VName], StructType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SrcLoc -> StructType -> TermTypeM StructType
forall o. SrcLoc -> TypeBase Exp o -> TermTypeM (TypeBase Exp o)
replaceTyVars SrcLoc
loc StructType
inst_t
      -- The sizes are now bound by the type, so they are not size variables
      -- to be solved.
      modifyConstraints (`M.withoutKeys` S.fromList ext)
      pure t

-- | Make the sizes of the final result of a function type existential, unless
-- a parameter mentions them, and return them. Each application of the function
-- may then return a different size, as each call of a recursive function may.
existentialResult :: TypeBase Size o -> ([VName], TypeBase Size o)
existentialResult :: forall o. TypeBase Exp o -> ([VName], TypeBase Exp o)
existentialResult = Set VName -> TypeBase Exp o -> ([VName], TypeBase Exp o)
forall u. Set VName -> TypeBase Exp u -> ([VName], TypeBase Exp u)
go Set VName
forall a. Monoid a => a
mempty
  where
    go :: S.Set VName -> TypeBase Size u -> ([VName], TypeBase Size u)
    go :: forall u. Set VName -> TypeBase Exp u -> ([VName], TypeBase Exp u)
go Set VName
bound (Scalar (Arrow u
o PName
pn Diet
d StructType
ta (RetType [VName]
ext ResType
tr))) =
      let bound' :: Set VName
bound' = Set VName
bound Set VName -> Set VName -> Set VName
forall a. Semigroup a => a -> a -> a
<> FV -> Set VName
fvVars (StructType -> FV
forall o. TypeBase Exp o -> FV
freeInType StructType
ta)
       in case ResType
tr of
            Scalar Arrow {} ->
              ScalarTypeBase Exp u -> TypeBase Exp u
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (ScalarTypeBase Exp u -> TypeBase Exp u)
-> (ResType -> ScalarTypeBase Exp u) -> ResType -> TypeBase Exp u
forall b c a. (b -> c) -> (a -> b) -> a -> c
. u
-> PName
-> Diet
-> StructType
-> RetTypeBase Exp Freshness
-> ScalarTypeBase Exp u
forall dim o.
o
-> PName
-> Diet
-> TypeBase dim NoMode
-> RetTypeBase dim Freshness
-> ScalarTypeBase dim o
Arrow u
o PName
pn Diet
d StructType
ta (RetTypeBase Exp Freshness -> ScalarTypeBase Exp u)
-> (ResType -> RetTypeBase Exp Freshness)
-> ResType
-> ScalarTypeBase Exp u
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [VName] -> ResType -> RetTypeBase Exp Freshness
forall dim o. [VName] -> TypeBase dim o -> RetTypeBase dim o
RetType [VName]
ext (ResType -> TypeBase Exp u)
-> ([VName], ResType) -> ([VName], TypeBase Exp u)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set VName -> ResType -> ([VName], ResType)
forall u. Set VName -> TypeBase Exp u -> ([VName], TypeBase Exp u)
go Set VName
bound' ResType
tr
            ResType
_ ->
              let new :: [VName]
new = (VName -> Bool) -> [VName] -> [VName]
forall a. (a -> Bool) -> [a] -> [a]
filter (VName -> Set VName -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.notMember` Set VName
bound') ([VName] -> [VName]) -> [VName] -> [VName]
forall a b. (a -> b) -> a -> b
$ Set VName -> [VName]
forall a. Set a -> [a]
S.toList (Set VName -> [VName]) -> Set VName -> [VName]
forall a b. (a -> b) -> a -> b
$ FV -> Set VName
fvVars (FV -> Set VName) -> FV -> Set VName
forall a b. (a -> b) -> a -> b
$ ResType -> FV
forall o. TypeBase Exp o -> FV
freeInType ResType
tr
               in ([VName]
new, ScalarTypeBase Exp u -> TypeBase Exp u
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (ScalarTypeBase Exp u -> TypeBase Exp u)
-> ScalarTypeBase Exp u -> TypeBase Exp u
forall a b. (a -> b) -> a -> b
$ u
-> PName
-> Diet
-> StructType
-> RetTypeBase Exp Freshness
-> ScalarTypeBase Exp u
forall dim o.
o
-> PName
-> Diet
-> TypeBase dim NoMode
-> RetTypeBase dim Freshness
-> ScalarTypeBase dim o
Arrow u
o PName
pn Diet
d StructType
ta (RetTypeBase Exp Freshness -> ScalarTypeBase Exp u)
-> RetTypeBase Exp Freshness -> ScalarTypeBase Exp u
forall a b. (a -> b) -> a -> b
$ [VName] -> ResType -> RetTypeBase Exp Freshness
forall dim o. [VName] -> TypeBase dim o -> RetTypeBase dim o
RetType ([VName]
ext [VName] -> [VName] -> [VName]
forall a. Semigroup a => a -> a -> a
<> [VName]
new) ResType
tr)
    go Set VName
_ TypeBase Exp u
t = ([], TypeBase Exp u
t)

-- | A pure function for looking up the type scheme of a global name. Used by
-- consumption checking to exploit parametricity; see Note [Parametric results]
-- in "Language.Futhark.TypeChecker.Consumption".
typeSchemes :: TermTypeM (QualName VName -> Maybe TypeM.BoundV)
typeSchemes :: TermTypeM (QualName VName -> Maybe BoundV)
typeSchemes = do
  scope <- (TermEnv -> TermScope Exp) -> TermTypeM (TermScope Exp)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks TermEnv -> TermScope Exp
termScope
  outer_env <- asks termOuterEnv
  pure $ \qn :: QualName VName
qn@(QualName [VName]
_ VName
name) ->
    case (VName -> Map VName (ValBinding Exp) -> Maybe (ValBinding Exp)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
name (Map VName (ValBinding Exp) -> Maybe (ValBinding Exp))
-> (TermScope Exp -> Map VName (ValBinding Exp))
-> TermScope Exp
-> Maybe (ValBinding Exp)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermScope Exp -> Map VName (ValBinding Exp)
forall dim. TermScope dim -> Map VName (ValBinding dim)
scopeVtable (TermScope Exp -> Maybe (ValBinding Exp))
-> Maybe (TermScope Exp) -> Maybe (ValBinding Exp)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (StructType -> StructType)
-> TermScope Exp -> QualName VName -> Maybe (TermScope Exp)
forall dim.
(StructType -> TypeBase dim NoMode)
-> TermScope dim -> QualName VName -> Maybe (TermScope dim)
Scope.lookupQualNameEnvMaybe StructType -> StructType
forall a. a -> a
id TermScope Exp
scope QualName VName
qn)
      Maybe (ValBinding Exp)
-> Maybe (ValBinding Exp) -> Maybe (ValBinding Exp)
forall a. Maybe a -> Maybe a -> Maybe a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` (StructType -> StructType)
-> Env -> VName -> Maybe (ValBinding Exp)
forall dim.
(StructType -> TypeBase dim NoMode)
-> Env -> VName -> Maybe (ValBinding dim)
Scope.lookupOuterVal StructType -> StructType
forall a. a -> a
id Env
outer_env VName
name of
      Just (BoundV [TypeParam]
tparams StructType
t) -> BoundV -> Maybe BoundV
forall a. a -> Maybe a
Just ([TypeParam] -> StructType -> BoundV
TypeM.BoundV [TypeParam]
tparams StructType
t)
      Maybe (ValBinding Exp)
_ -> Maybe BoundV
forall a. Maybe a
Nothing

-- | Look up the liftedness of an abstract type.
lookupAbsTy :: QualName VName -> TermTypeM Liftedness
lookupAbsTy :: QualName VName -> TermTypeM Liftedness
lookupAbsTy QualName VName
v | VName -> Bool
isIntrinsic (QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
v) = Liftedness -> TermTypeM Liftedness
forall a. a -> TermTypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Liftedness
Unlifted
lookupAbsTy QualName VName
v = do
  abs <- (TermEnv -> TySet) -> TermTypeM TySet
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks TermEnv -> TySet
termTySet
  case M.lookup v abs of
    Just Liftedness
l -> Liftedness -> TermTypeM Liftedness
forall a. a -> TermTypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Liftedness
l
    Maybe Liftedness
Nothing ->
      String -> TermTypeM Liftedness
forall a. HasCallStack => String -> a
error (String -> TermTypeM Liftedness) -> String -> TermTypeM Liftedness
forall a b. (a -> b) -> a -> b
$
        [String] -> String
unlines
          [ String
"lookupAbsTy: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> QualName VName -> String
forall a. Pretty a => a -> String
prettyString QualName VName
v,
            String
"known: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> TySet -> String
forall a. Show a => a -> String
show TySet
abs
          ]

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

extSize :: SrcLoc -> SizeSource -> TermTypeM (Size, Maybe VName)
extSize :: SrcLoc -> SizeSource -> TermTypeM (Exp, Maybe VName)
extSize SrcLoc
loc SizeSource
e = 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 (Text -> RigidSource) -> Text -> RigidSource
forall a b. (a -> b) -> a -> b
$ ExpBase NoInfo VName -> Text
forall a. Pretty a => a -> Text
prettyTextOneLine ExpBase NoInfo VName
e'
        SourceSlice Maybe Exp
d Maybe (ExpBase NoInfo VName)
i Maybe (ExpBase NoInfo VName)
j Maybe (ExpBase NoInfo VName)
s ->
          Maybe Exp -> Text -> RigidSource
RigidSlice Maybe Exp
d (Text -> RigidSource) -> Text -> RigidSource
forall a b. (a -> b) -> a -> b
$ DimIndexBase NoInfo VName -> Text
forall a. Pretty a => a -> Text
prettyTextOneLine (DimIndexBase NoInfo VName -> Text)
-> DimIndexBase NoInfo VName -> Text
forall a b. (a -> b) -> a -> b
$ Maybe (ExpBase NoInfo VName)
-> Maybe (ExpBase NoInfo VName)
-> Maybe (ExpBase NoInfo VName)
-> DimIndexBase NoInfo VName
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
  d <- SrcLoc -> RigidSource -> Name -> TermTypeM VName
forall a. Located a => a -> RigidSource -> Name -> TermTypeM VName
forall (m :: * -> *) a.
(MonadUnify m, Located a) =>
a -> RigidSource -> Name -> m VName
newRigidDim SrcLoc
loc RigidSource
rsrc Name
"n"
  pure
    ( sizeFromName (qualName d) loc,
      Just d
    )

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

-- | Get the type of an expression. Currently no different from
-- 'typeOf', but kept as the counterpart of 'expTypeFully'.
expType :: Exp -> TermTypeM StructType
expType :: Exp -> TermTypeM StructType
expType = StructType -> TermTypeM StructType
forall a. a -> TermTypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StructType -> TermTypeM StructType)
-> (Exp -> StructType) -> Exp -> TermTypeM StructType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Exp -> StructType
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 StructType
expTypeFully :: Exp -> TermTypeM StructType
expTypeFully = StructType -> TermTypeM StructType
forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully (StructType -> TermTypeM StructType)
-> (Exp -> StructType) -> Exp -> TermTypeM StructType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Exp -> StructType
typeOf

-- | Replace all type variables with their concrete types.
updateTypes :: (ASTMappable e) => e -> TermTypeM e
updateTypes :: forall e. ASTMappable e => e -> TermTypeM e
updateTypes = ASTMapper TermTypeM -> e -> TermTypeM e
forall x (m :: * -> *).
(ASTMappable x, Monad m) =>
ASTMapper m -> x -> m x
forall (m :: * -> *). Monad m => ASTMapper m -> e -> m e
astMap ASTMapper TermTypeM
tv
  where
    tv :: ASTMapper TermTypeM
tv =
      ASTMapper
        { mapOnExp :: Exp -> TermTypeM Exp
mapOnExp = ASTMapper TermTypeM -> Exp -> TermTypeM Exp
forall x (m :: * -> *).
(ASTMappable x, Monad m) =>
ASTMapper m -> x -> m x
forall (m :: * -> *). Monad m => ASTMapper m -> Exp -> m Exp
astMap ASTMapper TermTypeM
tv,
          mapOnName :: QualName VName -> TermTypeM (QualName VName)
mapOnName = QualName VName -> TermTypeM (QualName VName)
forall a. a -> TermTypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure,
          mapOnStructType :: StructType -> TermTypeM StructType
mapOnStructType = StructType -> TermTypeM StructType
forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully,
          mapOnParamType :: ParamType -> TermTypeM ParamType
mapOnParamType = ParamType -> TermTypeM ParamType
forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully,
          mapOnResRetType :: RetTypeBase Exp Freshness -> TermTypeM (RetTypeBase Exp Freshness)
mapOnResRetType = RetTypeBase Exp Freshness -> TermTypeM (RetTypeBase Exp Freshness)
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
  Usage -> StructType -> StructType -> TermTypeM ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify (SrcLoc -> Text -> Usage
forall a. Located a => a -> Text -> Usage
mkUsage (Exp -> SrcLoc
forall a. Located a => a -> SrcLoc
srclocOf Exp
e) Text
why) StructType
t (StructType -> TermTypeM ())
-> (StructType -> StructType) -> StructType -> TermTypeM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StructType -> StructType
forall dim o. TypeBase dim o -> TypeBase dim NoMode
toStruct (StructType -> TermTypeM ())
-> TermTypeM StructType -> TermTypeM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Exp -> TermTypeM StructType
expType Exp
e
  Exp -> TermTypeM Exp
forall a. a -> TermTypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Exp
e

checkExpForSize :: ExpBase Info VName -> TermTypeM Exp
checkExpForSize :: Exp -> TermTypeM Exp
checkExpForSize Exp
e = do
  checker <- (TermEnv -> Exp -> TermTypeM Exp)
-> TermTypeM (Exp -> TermTypeM Exp)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks TermEnv -> Exp -> TermTypeM Exp
termCheckExp
  e' <- checker e
  let t = StructType -> StructType
forall dim o. TypeBase dim o -> TypeBase dim NoMode
toStruct (StructType -> StructType) -> StructType -> StructType
forall a b. (a -> b) -> a -> b
$ Exp -> StructType
typeOf Exp
e'
  unify (mkUsage (locOf e') "Size expression") t (Scalar (Prim (Signed Int64)))
  updateTypes e'

checkTypeExpNonrigid :: TypeExp Exp VName -> TermTypeM (TypeExp Exp VName, ResType, [VName])
checkTypeExpNonrigid :: TypeExp Exp VName
-> TermTypeM (TypeExp Exp VName, ResType, [VName])
checkTypeExpNonrigid TypeExp Exp VName
te = do
  (te', svars, rettype, _l) <- (Exp -> TermTypeM Exp)
-> TypeExp Exp VName
-> TermTypeM
     (TypeExp Exp VName, [VName], RetTypeBase Exp Freshness, Liftedness)
forall (m :: * -> *) df.
(MonadTypeChecker m, Pretty df) =>
(df -> m Exp)
-> TypeExp df VName
-> m (TypeExp Exp VName, [VName], RetTypeBase Exp Freshness,
      Liftedness)
checkTypeExp Exp -> TermTypeM Exp
checkExpForSize TypeExp Exp VName
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.
  RetType dims st <- renameRetType rettype

  forM_ (svars ++ dims) $ \VName
v ->
    VName -> Constraint -> TermTypeM ()
constrain VName
v (Constraint -> TermTypeM ()) -> Constraint -> TermTypeM ()
forall a b. (a -> b) -> a -> b
$ Maybe Exp -> Usage -> Constraint
Size Maybe Exp
forall a. Maybe a
Nothing (Usage -> Constraint) -> Usage -> Constraint
forall a b. (a -> b) -> a -> b
$ SrcLoc -> Text -> Usage
forall a. Located a => a -> Text -> Usage
mkUsage (TypeExp Exp VName -> SrcLoc
forall a. Located a => a -> SrcLoc
srclocOf TypeExp Exp VName
te) Text
"anonymous size in type expression"
  pure (te', st, svars ++ dims)

--- Sizes

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

-- Running

initialTermScope :: TermScope Size
initialTermScope :: TermScope Exp
initialTermScope = (StructType -> StructType) -> TermScope Exp
forall dim. (StructType -> TypeBase dim NoMode) -> TermScope dim
Scope.initialTermScope StructType -> StructType
forall a. a -> a
id

runTermTypeM :: (ExpBase Info VName -> TermTypeM Exp) -> M.Map TyVar (TypeBase () NoMode) -> TermTypeM a -> TypeM a
runTermTypeM :: forall a.
(Exp -> TermTypeM Exp)
-> Map VName (TypeBase () NoMode) -> TermTypeM a -> TypeM a
runTermTypeM Exp -> TermTypeM Exp
checker Map VName (TypeBase () NoMode)
tyvars (TermTypeM ReaderT
  TermEnv (StateT TermTypeState (Except (Warnings, TypeError))) a
m) = do
  initial_scope <- (TermScope Exp
initialTermScope TermScope Exp -> TermScope Exp -> TermScope Exp
forall a. Semigroup a => a -> a -> a
<>) (TermScope Exp -> TermScope Exp)
-> (Env -> TermScope Exp) -> Env -> TermScope Exp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> TermScope Exp
forall dim. Env -> TermScope dim
Scope.envToTermScopeNoVals (Env -> TermScope Exp) -> TypeM Env -> TypeM (TermScope Exp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeM Env
askEnv
  name <- askImportName
  outer_env <- askEnv
  src <- gets TypeM.stateNameSource
  abs <- getTySet
  let initial_tenv =
        TermEnv
          { termScope :: TermScope Exp
termScope = TermScope Exp
initial_scope,
            termChecking :: Maybe Checking
termChecking = Maybe Checking
forall a. Maybe a
Nothing,
            termLevel :: Int
termLevel = Int
0,
            termCheckExp :: Exp -> TermTypeM Exp
termCheckExp = Exp -> TermTypeM Exp
checker,
            termImportName :: ImportName
termImportName = ImportName
name,
            termOuterEnv :: Env
termOuterEnv = Env
outer_env,
            termTySet :: TySet
termTySet = TySet
abs,
            termTyVars :: Map VName (TypeBase () NoMode)
termTyVars = Map VName (TypeBase () NoMode)
tyvars
          }
      initial_state =
        TermTypeState
          { stateConstraints :: Constraints
stateConstraints = Constraints
forall a. Monoid a => a
mempty,
            stateCounter :: Int
stateCounter = Int
0,
            stateWarnings :: Warnings
stateWarnings = Warnings
forall a. Monoid a => a
mempty,
            stateNameSource :: VNameSource
stateNameSource = VNameSource
src
          }
  case runExcept (runStateT (runReaderT m initial_tenv) initial_state) of
    Left (Warnings
ws, TypeError
e) -> do
      Warnings -> TypeM ()
forall (m :: * -> *). MonadTypeChecker m => Warnings -> m ()
warnings Warnings
ws
      TypeError -> TypeM a
forall a. TypeError -> TypeM a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TypeError
e
    Right (a
a, TermTypeState {VNameSource
stateNameSource :: TermTypeState -> VNameSource
stateNameSource :: VNameSource
stateNameSource, Warnings
stateWarnings :: TermTypeState -> Warnings
stateWarnings :: Warnings
stateWarnings}) -> do
      Warnings -> TypeM ()
forall (m :: * -> *). MonadTypeChecker m => Warnings -> m ()
warnings Warnings
stateWarnings
      (TypeState -> TypeState) -> TypeM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((TypeState -> TypeState) -> TypeM ())
-> (TypeState -> TypeState) -> TypeM ()
forall a b. (a -> b) -> a -> b
$ \TypeState
s -> TypeState
s {TypeM.stateNameSource = stateNameSource}
      a -> TypeM a
forall a. a -> TypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a