    -- | The type checker checks whether the program is type-consistent
    -- and adds type annotations and various other elaborations.  The
    -- program does not need to have any particular properties for the
    -- type checker to function; in particular it does not need unique
    -- names.
    module Language.Futhark.TypeChecker
      ( checkProg,
        checkExp,
        checkDec,
        checkModExp,
        Notes,
        TypeError (..),
        prettyTypeError,
        prettyTypeErrorNoLoc,
        Warnings,
        initialEnv,
        envWithImports,
      )
    where

    import Control.Monad
    import Data.Bifunctor
    import Data.Either
    import Data.List qualified as L
    import Data.Map.Strict qualified as M
    import Data.Maybe
    import Data.Ord
    import Data.Set qualified as S
    import Futhark.FreshNames hiding (newName)
    import Futhark.Util.Pretty hiding (space)
    import Language.Futhark
    import Language.Futhark.Semantic
    import Language.Futhark.TypeChecker.Modules
    import Language.Futhark.TypeChecker.Monad
    import Language.Futhark.TypeChecker.Names
    import Language.Futhark.TypeChecker.Terms
    import Language.Futhark.TypeChecker.Types
    import Prelude hiding (abs, mod)

    --- The main checker

    -- | Type check a program containing no type information, yielding
    -- either a type error or a program with complete type information.
    -- Accepts a mapping from file names (excluding extension) to
    -- previously type checked results.  The 'ImportName' is used to resolve
    -- relative @import@s.
    checkProg ::
      Imports ->
      VNameSource ->
      ImportName ->
      UncheckedProg ->
      (Warnings, Either TypeError (FileModule, VNameSource))
    checkProg :: Imports
    -> VNameSource
    -> ImportName
    -> UncheckedProg
    -> (Warnings, Either TypeError (FileModule, VNameSource))
    checkProg Imports
    files VNameSource
    src ImportName
    name UncheckedProg
    prog =
      Env
    -> ImportTable
    -> ImportName
    -> VNameSource
    -> TypeM FileModule
    -> (Warnings, Either TypeError (FileModule, VNameSource))
    forall a.
    Env
    -> ImportTable
    -> ImportName
    -> VNameSource
    -> TypeM a
    -> (Warnings, Either TypeError (a, VNameSource))
    runTypeM Env
    initialEnv ImportTable
    files' ImportName
    name VNameSource
    src (TypeM FileModule
     -> (Warnings, Either TypeError (FileModule, VNameSource)))
    -> TypeM FileModule
    -> (Warnings, Either TypeError (FileModule, VNameSource))
    forall a b. (a -> b) -> a -> b
    $ UncheckedProg -> TypeM FileModule
    checkProgM UncheckedProg
    prog
      where
        files' :: ImportTable
    files' = (FileModule -> Env) -> Map ImportName FileModule -> ImportTable
    forall a b k. (a -> b) -> Map k a -> Map k b
    M.map FileModule -> Env
    fileEnv (Map ImportName FileModule -> ImportTable)
    -> Map ImportName FileModule -> ImportTable
    forall a b. (a -> b) -> a -> b
    $ Imports -> Map ImportName FileModule
    forall k a. Ord k => [(k, a)] -> Map k a
    M.fromList Imports
    files

    -- | Type check a single expression containing no type information,
    -- yielding either a type error or the same expression annotated with
    -- type information.  Also returns a list of type parameters, which
    -- will be nonempty if the expression is polymorphic.  See also
    -- 'checkProg'.
    checkExp ::
      Imports ->
      VNameSource ->
      Env ->
      UncheckedExp ->
      (Warnings, Either TypeError ([TypeParam], Exp))
    checkExp :: Imports
    -> VNameSource
    -> Env
    -> ExpBase NoInfo Name
    -> (Warnings, Either TypeError ([TypeParamBase VName], Exp))
    checkExp Imports
    files VNameSource
    src Env
    env ExpBase NoInfo Name
    e =
      (Either TypeError (([TypeParamBase VName], Exp), VNameSource)
     -> Either TypeError ([TypeParamBase VName], Exp))
    -> (Warnings,
        Either TypeError (([TypeParamBase VName], Exp), VNameSource))
    -> (Warnings, Either TypeError ([TypeParamBase VName], Exp))
    forall b c a. (b -> c) -> (a, b) -> (a, c)
    forall (p :: * -> * -> *) b c a.
    Bifunctor p =>
    (b -> c) -> p a b -> p a c
    second (((([TypeParamBase VName], Exp), VNameSource)
     -> ([TypeParamBase VName], Exp))
    -> Either TypeError (([TypeParamBase VName], Exp), VNameSource)
    -> Either TypeError ([TypeParamBase VName], Exp)
    forall a b. (a -> b) -> Either TypeError a -> Either TypeError b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (([TypeParamBase VName], Exp), VNameSource)
    -> ([TypeParamBase VName], Exp)
    forall a b. (a, b) -> a
    fst) ((Warnings,
      Either TypeError (([TypeParamBase VName], Exp), VNameSource))
     -> (Warnings, Either TypeError ([TypeParamBase VName], Exp)))
    -> (Warnings,
        Either TypeError (([TypeParamBase VName], Exp), VNameSource))
    -> (Warnings, Either TypeError ([TypeParamBase VName], Exp))
    forall a b. (a -> b) -> a -> b
    $
        Env
    -> ImportTable
    -> ImportName
    -> VNameSource
    -> TypeM ([TypeParamBase VName], Exp)
    -> (Warnings,
        Either TypeError (([TypeParamBase VName], Exp), VNameSource))
    forall a.
    Env
    -> ImportTable
    -> ImportName
    -> VNameSource
    -> TypeM a
    -> (Warnings, Either TypeError (a, VNameSource))
    runTypeM
          Env
    env
          ImportTable
    files'
          (FilePath -> ImportName
    mkInitialImport FilePath
    "")
          VNameSource
    src
          (ExpBase NoInfo VName -> TypeM ([TypeParamBase VName], Exp)
    checkOneExp (ExpBase NoInfo VName -> TypeM ([TypeParamBase VName], Exp))
    -> TypeM (ExpBase NoInfo VName)
    -> TypeM ([TypeParamBase VName], Exp)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ExpBase NoInfo Name -> TypeM (ExpBase NoInfo VName)
    resolveExp ExpBase NoInfo Name
    e)
      where
        files' :: ImportTable
    files' = (FileModule -> Env) -> Map ImportName FileModule -> ImportTable
    forall a b k. (a -> b) -> Map k a -> Map k b
    M.map FileModule -> Env
    fileEnv (Map ImportName FileModule -> ImportTable)
    -> Map ImportName FileModule -> ImportTable
    forall a b. (a -> b) -> a -> b
    $ Imports -> Map ImportName FileModule
    forall k a. Ord k => [(k, a)] -> Map k a
    M.fromList Imports
    files

    -- | Type check a single declaration containing no type information,
    -- yielding either a type error or the same declaration annotated with
    -- type information along the Env produced by that declaration.  See
    -- also 'checkProg'.
    checkDec ::
      Imports ->
      VNameSource ->
      Env ->
      ImportName ->
      UncheckedDec ->
      (Warnings, Either TypeError (Env, Dec, VNameSource))
    checkDec :: Imports
    -> VNameSource
    -> Env
    -> ImportName
    -> UncheckedDec
    -> (Warnings, Either TypeError (Env, Dec, VNameSource))
    checkDec Imports
    files VNameSource
    src Env
    env ImportName
    name UncheckedDec
    d =
      (Either TypeError ((Env, Dec), VNameSource)
     -> Either TypeError (Env, Dec, VNameSource))
    -> (Warnings, Either TypeError ((Env, Dec), VNameSource))
    -> (Warnings, Either TypeError (Env, Dec, VNameSource))
    forall b c a. (b -> c) -> (a, b) -> (a, c)
    forall (p :: * -> * -> *) b c a.
    Bifunctor p =>
    (b -> c) -> p a b -> p a c
    second ((((Env, Dec), VNameSource) -> (Env, Dec, VNameSource))
    -> Either TypeError ((Env, Dec), VNameSource)
    -> Either TypeError (Env, Dec, VNameSource)
    forall a b. (a -> b) -> Either TypeError a -> Either TypeError b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Env, Dec), VNameSource) -> (Env, Dec, VNameSource)
    forall {a} {b} {c}. ((a, b), c) -> (a, b, c)
    massage) ((Warnings, Either TypeError ((Env, Dec), VNameSource))
     -> (Warnings, Either TypeError (Env, Dec, VNameSource)))
    -> (Warnings, Either TypeError ((Env, Dec), VNameSource))
    -> (Warnings, Either TypeError (Env, Dec, VNameSource))
    forall a b. (a -> b) -> a -> b
    $
        Env
    -> ImportTable
    -> ImportName
    -> VNameSource
    -> TypeM (Env, Dec)
    -> (Warnings, Either TypeError ((Env, Dec), VNameSource))
    forall a.
    Env
    -> ImportTable
    -> ImportName
    -> VNameSource
    -> TypeM a
    -> (Warnings, Either TypeError (a, VNameSource))
    runTypeM Env
    env ImportTable
    files' ImportName
    name VNameSource
    src (TypeM (Env, Dec)
     -> (Warnings, Either TypeError ((Env, Dec), VNameSource)))
    -> TypeM (Env, Dec)
    -> (Warnings, Either TypeError ((Env, Dec), VNameSource))
    forall a b. (a -> b) -> a -> b
    $ do
          (_, env', d') <- UncheckedDec -> TypeM (TySet, Env, Dec)
    checkOneDec UncheckedDec
    d
          pure (env' <> env, d')
      where
        massage :: ((a, b), c) -> (a, b, c)
    massage ((a
    env', b
    d'), c
    src') =
          (a
    env', b
    d', c
    src')
        files' :: ImportTable
    files' = (FileModule -> Env) -> Map ImportName FileModule -> ImportTable
    forall a b k. (a -> b) -> Map k a -> Map k b
    M.map FileModule -> Env
    fileEnv (Map ImportName FileModule -> ImportTable)
    -> Map ImportName FileModule -> ImportTable
    forall a b. (a -> b) -> a -> b
    $ Imports -> Map ImportName FileModule
    forall k a. Ord k => [(k, a)] -> Map k a
    M.fromList Imports
    files

    -- | Type check a single module expression containing no type information,
    -- yielding either a type error or the same expression annotated with
    -- type information along the Env produced by that declaration.  See
    -- also 'checkProg'.
    checkModExp ::
      Imports ->
      VNameSource ->
      Env ->
      ModExpBase NoInfo Name ->
      (Warnings, Either TypeError (MTy, ModExpBase Info VName))
    checkModExp :: Imports
    -> VNameSource
    -> Env
    -> ModExpBase NoInfo Name
    -> (Warnings, Either TypeError (MTy, ModExpBase Info VName))
    checkModExp Imports
    files VNameSource
    src Env
    env ModExpBase NoInfo Name
    me =
      (Either TypeError ((MTy, ModExpBase Info VName), VNameSource)
     -> Either TypeError (MTy, ModExpBase Info VName))
    -> (Warnings,
        Either TypeError ((MTy, ModExpBase Info VName), VNameSource))
    -> (Warnings, Either TypeError (MTy, ModExpBase Info VName))
    forall b c a. (b -> c) -> (a, b) -> (a, c)
    forall (p :: * -> * -> *) b c a.
    Bifunctor p =>
    (b -> c) -> p a b -> p a c
    second ((((MTy, ModExpBase Info VName), VNameSource)
     -> (MTy, ModExpBase Info VName))
    -> Either TypeError ((MTy, ModExpBase Info VName), VNameSource)
    -> Either TypeError (MTy, ModExpBase Info VName)
    forall a b. (a -> b) -> Either TypeError a -> Either TypeError b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((MTy, ModExpBase Info VName), VNameSource)
    -> (MTy, ModExpBase Info VName)
    forall a b. (a, b) -> a
    fst) ((Warnings,
      Either TypeError ((MTy, ModExpBase Info VName), VNameSource))
     -> (Warnings, Either TypeError (MTy, ModExpBase Info VName)))
    -> (TypeM (MTy, ModExpBase Info VName)
        -> (Warnings,
            Either TypeError ((MTy, ModExpBase Info VName), VNameSource)))
    -> TypeM (MTy, ModExpBase Info VName)
    -> (Warnings, Either TypeError (MTy, ModExpBase Info VName))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Env
    -> ImportTable
    -> ImportName
    -> VNameSource
    -> TypeM (MTy, ModExpBase Info VName)
    -> (Warnings,
        Either TypeError ((MTy, ModExpBase Info VName), VNameSource))
    forall a.
    Env
    -> ImportTable
    -> ImportName
    -> VNameSource
    -> TypeM a
    -> (Warnings, Either TypeError (a, VNameSource))
    runTypeM Env
    env ImportTable
    files' (FilePath -> ImportName
    mkInitialImport FilePath
    "") VNameSource
    src (TypeM (MTy, ModExpBase Info VName)
     -> (Warnings, Either TypeError (MTy, ModExpBase Info VName)))
    -> TypeM (MTy, ModExpBase Info VName)
    -> (Warnings, Either TypeError (MTy, ModExpBase Info VName))
    forall a b. (a -> b) -> a -> b
    $ do
        (_abs, mty, me') <- ModExpBase NoInfo Name -> TypeM (TySet, MTy, ModExpBase Info VName)
    checkOneModExp ModExpBase NoInfo Name
    me
        pure (mty, me')
      where
        files' :: ImportTable
    files' = (FileModule -> Env) -> Map ImportName FileModule -> ImportTable
    forall a b k. (a -> b) -> Map k a -> Map k b
    M.map FileModule -> Env
    fileEnv (Map ImportName FileModule -> ImportTable)
    -> Map ImportName FileModule -> ImportTable
    forall a b. (a -> b) -> a -> b
    $ Imports -> Map ImportName FileModule
    forall k a. Ord k => [(k, a)] -> Map k a
    M.fromList Imports
    files

    -- | An initial environment for the type checker, containing
    -- intrinsics and such.
    initialEnv :: Env
    initialEnv :: Env
    initialEnv =
      Env
    intrinsicsModule
        { envModTable = initialModTable,
          envNameMap =
            M.insert
              (Term, nameFromString "intrinsics")
              (qualName intrinsics_v)
              topLevelNameMap
        }
      where
        initialTypeTable :: Map VName TypeBinding
    initialTypeTable = [(VName, TypeBinding)] -> Map VName TypeBinding
    forall k a. Ord k => [(k, a)] -> Map k a
    M.fromList ([(VName, TypeBinding)] -> Map VName TypeBinding)
    -> [(VName, TypeBinding)] -> Map VName TypeBinding
    forall a b. (a -> b) -> a -> b
    $ ((VName, Intrinsic) -> Maybe (VName, TypeBinding))
    -> [(VName, Intrinsic)] -> [(VName, TypeBinding)]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe (VName, Intrinsic) -> Maybe (VName, TypeBinding)
    forall {a}. (a, Intrinsic) -> Maybe (a, TypeBinding)
    addIntrinsicT ([(VName, Intrinsic)] -> [(VName, TypeBinding)])
    -> [(VName, Intrinsic)] -> [(VName, TypeBinding)]
    forall a b. (a -> b) -> a -> b
    $ Map VName Intrinsic -> [(VName, Intrinsic)]
    forall k a. Map k a -> [(k, a)]
    M.toList Map VName Intrinsic
    intrinsics
        initialModTable :: Map VName Mod
    initialModTable = VName -> Mod -> Map VName Mod
    forall k a. k -> a -> Map k a
    M.singleton VName
    intrinsics_v (Env -> Mod
    ModEnv Env
    intrinsicsModule)

        intrinsics_v :: VName
    intrinsics_v = Name -> Int -> VName
    VName (FilePath -> Name
    nameFromString FilePath
    "intrinsics") Int
    0

        intrinsicsModule :: Env
    intrinsicsModule = Map VName BoundV
    -> Map VName TypeBinding
    -> Map VName MTy
    -> Map VName Mod
    -> Map (Namespace, Name) (QualName VName)
    -> Env
    Env Map VName BoundV
    forall a. Monoid a => a
    mempty Map VName TypeBinding
    initialTypeTable Map VName MTy
    forall a. Monoid a => a
    mempty Map VName Mod
    forall a. Monoid a => a
    mempty Map (Namespace, Name) (QualName VName)
    intrinsicsNameMap

        addIntrinsicT :: (a, Intrinsic) -> Maybe (a, TypeBinding)
    addIntrinsicT (a
    name, IntrinsicType Liftedness
    l [TypeParamBase VName]
    ps StructType
    t) =
          (a, TypeBinding) -> Maybe (a, TypeBinding)
    forall a. a -> Maybe a
    Just (a
    name, Liftedness -> [TypeParamBase VName] -> StructRetType -> TypeBinding
    TypeAbbr Liftedness
    l [TypeParamBase VName]
    ps (StructRetType -> TypeBinding) -> StructRetType -> TypeBinding
    forall a b. (a -> b) -> a -> b
    $ [VName] -> StructType -> StructRetType
    forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
    RetType [] StructType
    t)
        addIntrinsicT (a, Intrinsic)
    _ =
          Maybe (a, TypeBinding)
    forall a. Maybe a
    Nothing

    -- | Produce an environment, based on the one passed in, where all of
    -- the provided imports have been @open@ened in order.  This could in principle
    -- also be done with 'checkDec', but this is more precise.
    envWithImports :: Imports -> Env -> Env
    envWithImports :: Imports -> Env -> Env
    envWithImports Imports
    imports Env
    env =
      [Env] -> Env
    forall a. Monoid a => [a] -> a
    mconcat (((ImportName, FileModule) -> Env) -> Imports -> [Env]
    forall a b. (a -> b) -> [a] -> [b]
    map (FileModule -> Env
    fileEnv (FileModule -> Env)
    -> ((ImportName, FileModule) -> FileModule)
    -> (ImportName, FileModule)
    -> Env
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (ImportName, FileModule) -> FileModule
    forall a b. (a, b) -> b
    snd) (Imports -> Imports
    forall a. [a] -> [a]
    reverse Imports
    imports)) Env -> Env -> Env
    forall a. Semigroup a => a -> a -> a
    <> Env
    env

    checkProgM :: UncheckedProg -> TypeM FileModule
    checkProgM :: UncheckedProg -> TypeM FileModule
    checkProgM (Prog Maybe DocComment
    doc [UncheckedDec]
    decs) = do
      [UncheckedDec] -> TypeM ()
    checkForDuplicateDecs [UncheckedDec]
    decs
      (abs, env, decs', full_env) <- [UncheckedDec] -> TypeM (TySet, Env, [Dec], Env)
    checkDecs [UncheckedDec]
    decs
      pure (FileModule abs env (Prog doc decs') full_env)

    dupDefinitionError ::
      (MonadTypeChecker m) =>
      Namespace ->
      Name ->
      SrcLoc ->
      SrcLoc ->
      m a
    dupDefinitionError :: forall (m :: * -> *) a.
    MonadTypeChecker m =>
    Namespace -> Name -> SrcLoc -> SrcLoc -> m a
    dupDefinitionError Namespace
    space Name
    name SrcLoc
    loc1 SrcLoc
    loc2 =
      SrcLoc -> 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 SrcLoc
    loc1 Notes
    forall a. Monoid a => a
    mempty (Doc () -> m a) -> Doc () -> m a
    forall a b. (a -> b) -> a -> b
    $
        Doc ()
    "Duplicate definition of"
          Doc () -> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> Namespace -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. Namespace -> Doc ann
    pretty Namespace
    space
          Doc () -> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> Name -> Doc ()
    forall a. Name -> Doc a
    forall v a. IsName v => v -> Doc a
    prettyName Name
    name
          Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Doc ()
    "."
            Doc () -> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann -> Doc ann
    </> Doc ()
    "Previously defined at"
            Doc () -> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> FilePath -> Doc ()
    forall ann. FilePath -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty (SrcLoc -> FilePath
    forall a. Located a => a -> FilePath
    locStr SrcLoc
    loc2)
          Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Doc ()
    "."

    checkForDuplicateDecs :: [DecBase NoInfo Name] -> TypeM ()
    checkForDuplicateDecs :: [UncheckedDec] -> TypeM ()
    checkForDuplicateDecs =
      (Map (Namespace, Name) SrcLoc
     -> UncheckedDec -> TypeM (Map (Namespace, Name) SrcLoc))
    -> Map (Namespace, Name) SrcLoc -> [UncheckedDec] -> TypeM ()
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Monad m) =>
    (b -> a -> m b) -> b -> t a -> m ()
    foldM_ ((UncheckedDec
     -> Map (Namespace, Name) SrcLoc
     -> TypeM (Map (Namespace, Name) SrcLoc))
    -> Map (Namespace, Name) SrcLoc
    -> UncheckedDec
    -> TypeM (Map (Namespace, Name) SrcLoc)
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip UncheckedDec
    -> Map (Namespace, Name) SrcLoc
    -> TypeM (Map (Namespace, Name) SrcLoc)
    forall {m :: * -> *} {f :: * -> *}.
    MonadTypeChecker m =>
    DecBase f Name
    -> Map (Namespace, Name) SrcLoc -> m (Map (Namespace, Name) SrcLoc)
    f) Map (Namespace, Name) SrcLoc
    forall a. Monoid a => a
    mempty
      where
        check :: Namespace
    -> Name
    -> SrcLoc
    -> Map (Namespace, Name) SrcLoc
    -> m (Map (Namespace, Name) SrcLoc)
    check Namespace
    namespace Name
    name SrcLoc
    loc Map (Namespace, Name) SrcLoc
    known =
          case (Namespace, Name) -> Map (Namespace, Name) SrcLoc -> Maybe SrcLoc
    forall k a. Ord k => k -> Map k a -> Maybe a
    M.lookup (Namespace
    namespace, Name
    name) Map (Namespace, Name) SrcLoc
    known of
            Just SrcLoc
    loc' ->
              Namespace
    -> Name -> SrcLoc -> SrcLoc -> m (Map (Namespace, Name) SrcLoc)
    forall (m :: * -> *) a.
    MonadTypeChecker m =>
    Namespace -> Name -> SrcLoc -> SrcLoc -> m a
    dupDefinitionError Namespace
    namespace Name
    name SrcLoc
    loc SrcLoc
    loc'
            Maybe SrcLoc
    _ -> Map (Namespace, Name) SrcLoc -> m (Map (Namespace, Name) SrcLoc)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Map (Namespace, Name) SrcLoc -> m (Map (Namespace, Name) SrcLoc))
    -> Map (Namespace, Name) SrcLoc -> m (Map (Namespace, Name) SrcLoc)
    forall a b. (a -> b) -> a -> b
    $ (Namespace, Name)
    -> SrcLoc
    -> Map (Namespace, Name) SrcLoc
    -> Map (Namespace, Name) SrcLoc
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    M.insert (Namespace
    namespace, Name
    name) SrcLoc
    loc Map (Namespace, Name) SrcLoc
    known

        f :: DecBase f Name
    -> Map (Namespace, Name) SrcLoc -> m (Map (Namespace, Name) SrcLoc)
    f (ValDec ValBindBase f Name
    vb) =
          Namespace
    -> Name
    -> SrcLoc
    -> Map (Namespace, Name) SrcLoc
    -> m (Map (Namespace, Name) SrcLoc)
    forall {m :: * -> *}.
    MonadTypeChecker m =>
    Namespace
    -> Name
    -> SrcLoc
    -> Map (Namespace, Name) SrcLoc
    -> m (Map (Namespace, Name) SrcLoc)
    check Namespace
    Term (ValBindBase f Name -> Name
    forall (f :: * -> *) vn. ValBindBase f vn -> vn
    valBindName ValBindBase f Name
    vb) (ValBindBase f Name -> SrcLoc
    forall a. Located a => a -> SrcLoc
    srclocOf ValBindBase f Name
    vb)
        f (TypeDec (TypeBind Name
    name Liftedness
    _ [TypeParamBase Name]
    _ TypeExp (ExpBase f Name) Name
    _ f StructRetType
    _ Maybe DocComment
    _ SrcLoc
    loc)) =
          Namespace
    -> Name
    -> SrcLoc
    -> Map (Namespace, Name) SrcLoc
    -> m (Map (Namespace, Name) SrcLoc)
    forall {m :: * -> *}.
    MonadTypeChecker m =>
    Namespace
    -> Name
    -> SrcLoc
    -> Map (Namespace, Name) SrcLoc
    -> m (Map (Namespace, Name) SrcLoc)
    check Namespace
    Type Name
    name SrcLoc
    loc
        f (ModTypeDec (ModTypeBind Name
    name ModTypeExpBase f Name
    _ Maybe DocComment
    _ SrcLoc
    loc)) =
          Namespace
    -> Name
    -> SrcLoc
    -> Map (Namespace, Name) SrcLoc
    -> m (Map (Namespace, Name) SrcLoc)
    forall {m :: * -> *}.
    MonadTypeChecker m =>
    Namespace
    -> Name
    -> SrcLoc
    -> Map (Namespace, Name) SrcLoc
    -> m (Map (Namespace, Name) SrcLoc)
    check Namespace
    Signature Name
    name SrcLoc
    loc
        f (ModDec (ModBind Name
    name [ModParamBase f Name]
    _ Maybe (ModTypeExpBase f Name, f (Map VName VName))
    _ ModExpBase f Name
    _ Maybe DocComment
    _ SrcLoc
    loc)) =
          Namespace
    -> Name
    -> SrcLoc
    -> Map (Namespace, Name) SrcLoc
    -> m (Map (Namespace, Name) SrcLoc)
    forall {m :: * -> *}.
    MonadTypeChecker m =>
    Namespace
    -> Name
    -> SrcLoc
    -> Map (Namespace, Name) SrcLoc
    -> m (Map (Namespace, Name) SrcLoc)
    check Namespace
    Term Name
    name SrcLoc
    loc
        f OpenDec {} = Map (Namespace, Name) SrcLoc -> m (Map (Namespace, Name) SrcLoc)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure
        f LocalDec {} = Map (Namespace, Name) SrcLoc -> m (Map (Namespace, Name) SrcLoc)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure
        f ImportDec {} = Map (Namespace, Name) SrcLoc -> m (Map (Namespace, Name) SrcLoc)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure

    bindingTypeParams :: [TypeParam] -> TypeM a -> TypeM a
    bindingTypeParams :: forall a. [TypeParamBase VName] -> TypeM a -> TypeM a
    bindingTypeParams [TypeParamBase VName]
    tparams = Env -> TypeM a -> TypeM a
    forall a. Env -> TypeM a -> TypeM a
    localEnv Env
    env
      where
        env :: Env
    env = [Env] -> Env
    forall a. Monoid a => [a] -> a
    mconcat ([Env] -> Env) -> [Env] -> Env
    forall a b. (a -> b) -> a -> b
    $ (TypeParamBase VName -> Env) -> [TypeParamBase VName] -> [Env]
    forall a b. (a -> b) -> [a] -> [b]
    map TypeParamBase VName -> Env
    typeParamEnv [TypeParamBase VName]
    tparams

        typeParamEnv :: TypeParamBase VName -> Env
    typeParamEnv (TypeParamDim VName
    v SrcLoc
    _) =
          Env
    forall a. Monoid a => a
    mempty
            { envVtable =
                M.singleton v $ BoundV [] (Scalar $ Prim $ Signed Int64)
            }
        typeParamEnv (TypeParamType Liftedness
    l VName
    v SrcLoc
    _) =
          Env
    forall a. Monoid a => a
    mempty
            { envTypeTable =
                M.singleton v $
                  TypeAbbr l [] . RetType [] . Scalar $
                    TypeVar mempty (qualName v) []
            }

    checkTypeDecl ::
      UncheckedTypeExp ->
      TypeM ([VName], TypeExp Exp VName, StructType, Liftedness)
    checkTypeDecl :: TypeExp (ExpBase NoInfo Name) Name
    -> TypeM ([VName], TypeExp Exp VName, StructType, Liftedness)
    checkTypeDecl TypeExp (ExpBase NoInfo Name) Name
    te = do
      (te', svars, RetType dims st, l) <- (ExpBase NoInfo VName -> TypeM Exp)
    -> TypeExp (ExpBase NoInfo VName) VName
    -> TypeM (TypeExp Exp VName, [VName], ResRetType, Liftedness)
    forall (m :: * -> *) df.
    (MonadTypeChecker m, Pretty df) =>
    (df -> m Exp)
    -> TypeExp df VName
    -> m (TypeExp Exp VName, [VName], ResRetType, Liftedness)
    checkTypeExp ExpBase NoInfo VName -> TypeM Exp
    checkSizeExp (TypeExp (ExpBase NoInfo VName) VName
     -> TypeM (TypeExp Exp VName, [VName], ResRetType, Liftedness))
    -> TypeM (TypeExp (ExpBase NoInfo VName) VName)
    -> TypeM (TypeExp Exp VName, [VName], ResRetType, Liftedness)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TypeExp (ExpBase NoInfo Name) Name
    -> TypeM (TypeExp (ExpBase NoInfo VName) VName)
    resolveTypeExp TypeExp (ExpBase NoInfo Name) Name
    te
      pure (svars ++ dims, te', toStruct st, l)

    -- In this function, after the recursion, we add the Env of the
    -- current Spec *after* the one that is returned from the recursive
    -- call.  This implements the behaviour that specs later in a module
    -- type can override those earlier (it rarely matters, but it affects
    -- the specific structure of substitutions in case some module type is
    -- redundantly imported multiple times).
    checkSpecs :: [SpecBase NoInfo Name] -> TypeM (TySet, Env, [SpecBase Info VName])
    checkSpecs :: [SpecBase NoInfo Name] -> TypeM (TySet, Env, [SpecBase Info VName])
    checkSpecs [] = (TySet, Env, [SpecBase Info VName])
    -> TypeM (TySet, Env, [SpecBase Info VName])
    forall a. a -> TypeM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (TySet
    forall a. Monoid a => a
    mempty, Env
    forall a. Monoid a => a
    mempty, [])
    checkSpecs (ValSpec Name
    name [TypeParamBase Name]
    tparams TypeExp (ExpBase NoInfo Name) Name
    vtype NoInfo StructType
    NoInfo Maybe DocComment
    doc SrcLoc
    loc : [SpecBase NoInfo Name]
    specs) = do
      (tparams', vtype', vtype_t) <-
        [TypeParamBase Name]
    -> ([TypeParamBase VName]
        -> TypeM ([TypeParamBase VName], TypeExp Exp VName, StructType))
    -> TypeM ([TypeParamBase VName], TypeExp Exp VName, StructType)
    forall a.
    [TypeParamBase Name]
    -> ([TypeParamBase VName] -> TypeM a) -> TypeM a
    resolveTypeParams [TypeParamBase Name]
    tparams (([TypeParamBase VName]
      -> TypeM ([TypeParamBase VName], TypeExp Exp VName, StructType))
     -> TypeM ([TypeParamBase VName], TypeExp Exp VName, StructType))
    -> ([TypeParamBase VName]
        -> TypeM ([TypeParamBase VName], TypeExp Exp VName, StructType))
    -> TypeM ([TypeParamBase VName], TypeExp Exp VName, StructType)
    forall a b. (a -> b) -> a -> b
    $ \[TypeParamBase VName]
    tparams' -> [TypeParamBase VName]
    -> TypeM ([TypeParamBase VName], TypeExp Exp VName, StructType)
    -> TypeM ([TypeParamBase VName], TypeExp Exp VName, StructType)
    forall a. [TypeParamBase VName] -> TypeM a -> TypeM a
    bindingTypeParams [TypeParamBase VName]
    tparams' (TypeM ([TypeParamBase VName], TypeExp Exp VName, StructType)
     -> TypeM ([TypeParamBase VName], TypeExp Exp VName, StructType))
    -> TypeM ([TypeParamBase VName], TypeExp Exp VName, StructType)
    -> TypeM ([TypeParamBase VName], TypeExp Exp VName, StructType)
    forall a b. (a -> b) -> a -> b
    $ do
          (ext, vtype', vtype_t, _) <- TypeExp (ExpBase NoInfo Name) Name
    -> TypeM ([VName], TypeExp Exp VName, StructType, Liftedness)
    checkTypeDecl TypeExp (ExpBase NoInfo Name) Name
    vtype

          unless (null ext) $
            typeError loc mempty $
              "All function parameters must have non-anonymous sizes."
                </> "Hint: add size parameters to"
                <+> dquotes (pretty name)
                <> "."

          pure (tparams', vtype', vtype_t)

      bindSpaced1 Term name loc $ \VName
    name' -> do
        let valenv :: Env
    valenv =
              Env
    forall a. Monoid a => a
    mempty
                { envVtable = M.singleton name' $ BoundV tparams' vtype_t,
                  envNameMap = M.singleton (Term, name) $ qualName name'
                }
        VName -> TypeM ()
    usedName VName
    name'
        (abstypes, env, specs') <- Env
    -> TypeM (TySet, Env, [SpecBase Info VName])
    -> TypeM (TySet, Env, [SpecBase Info VName])
    forall a. Env -> TypeM a -> TypeM a
    localEnv Env
    valenv (TypeM (TySet, Env, [SpecBase Info VName])
     -> TypeM (TySet, Env, [SpecBase Info VName]))
    -> TypeM (TySet, Env, [SpecBase Info VName])
    -> TypeM (TySet, Env, [SpecBase Info VName])
    forall a b. (a -> b) -> a -> b
    $ [SpecBase NoInfo Name] -> TypeM (TySet, Env, [SpecBase Info VName])
    checkSpecs [SpecBase NoInfo Name]
    specs
        pure
          ( abstypes,
            env <> valenv,
            ValSpec name' tparams' vtype' (Info vtype_t) doc loc : specs'
          )
    checkSpecs (TypeAbbrSpec TypeBindBase NoInfo Name
    tdec : [SpecBase NoInfo Name]
    specs) = do
      (tenv, tdec') <- TypeBindBase NoInfo Name -> TypeM (Env, TypeBindBase Info VName)
    checkTypeBind TypeBindBase NoInfo Name
    tdec
      bindSpaced1 Type (typeAlias tdec) (srclocOf tdec) $ \VName
    name' -> do
        VName -> TypeM ()
    usedName VName
    name'
        (abstypes, env, specs') <- Env
    -> TypeM (TySet, Env, [SpecBase Info VName])
    -> TypeM (TySet, Env, [SpecBase Info VName])
    forall a. Env -> TypeM a -> TypeM a
    localEnv Env
    tenv (TypeM (TySet, Env, [SpecBase Info VName])
     -> TypeM (TySet, Env, [SpecBase Info VName]))
    -> TypeM (TySet, Env, [SpecBase Info VName])
    -> TypeM (TySet, Env, [SpecBase Info VName])
    forall a b. (a -> b) -> a -> b
    $ [SpecBase NoInfo Name] -> TypeM (TySet, Env, [SpecBase Info VName])
    checkSpecs [SpecBase NoInfo Name]
    specs
        pure
          ( abstypes,
            env <> tenv,
            TypeAbbrSpec tdec' : specs'
          )
    checkSpecs (TypeSpec Liftedness
    l Name
    name [TypeParamBase Name]
    ps Maybe DocComment
    doc SrcLoc
    loc : [SpecBase NoInfo Name]
    specs) = do
      ps' <- [TypeParamBase Name]
    -> ([TypeParamBase VName] -> TypeM [TypeParamBase VName])
    -> TypeM [TypeParamBase VName]
    forall a.
    [TypeParamBase Name]
    -> ([TypeParamBase VName] -> TypeM a) -> TypeM a
    resolveTypeParams [TypeParamBase Name]
    ps [TypeParamBase VName] -> TypeM [TypeParamBase VName]
    forall a. a -> TypeM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure
      bindSpaced1 Type name loc $ \VName
    name' -> do
        VName -> TypeM ()
    usedName VName
    name'
        let tenv :: Env
    tenv =
              Env
    forall a. Monoid a => a
    mempty
                { envNameMap =
                    M.singleton (Type, name) $ qualName name',
                  envTypeTable =
                    M.singleton name' $
                      TypeAbbr l ps' . RetType [] . Scalar $
                        TypeVar mempty (qualName name') $
                          map typeParamToArg ps'
                }
        (abstypes, env, specs') <- Env
    -> TypeM (TySet, Env, [SpecBase Info VName])
    -> TypeM (TySet, Env, [SpecBase Info VName])
    forall a. Env -> TypeM a -> TypeM a
    localEnv Env
    tenv (TypeM (TySet, Env, [SpecBase Info VName])
     -> TypeM (TySet, Env, [SpecBase Info VName]))
    -> TypeM (TySet, Env, [SpecBase Info VName])
    -> TypeM (TySet, Env, [SpecBase Info VName])
    forall a b. (a -> b) -> a -> b
    $ [SpecBase NoInfo Name] -> TypeM (TySet, Env, [SpecBase Info VName])
    checkSpecs [SpecBase NoInfo Name]
    specs
        pure
          ( M.insert (qualName name') l abstypes,
            env <> tenv,
            TypeSpec l name' ps' doc loc : specs'
          )
    checkSpecs (ModSpec Name
    name ModTypeExpBase NoInfo Name
    sig Maybe DocComment
    doc SrcLoc
    loc : [SpecBase NoInfo Name]
    specs) = do
      (_sig_abs, mty, sig') <- ModTypeExpBase NoInfo Name
    -> TypeM (TySet, MTy, ModTypeExpBase Info VName)
    checkModTypeExp ModTypeExpBase NoInfo Name
    sig
      bindSpaced1 Term name loc $ \VName
    name' -> do
        VName -> TypeM ()
    usedName VName
    name'
        let senv :: Env
    senv =
              Env
    forall a. Monoid a => a
    mempty
                { envNameMap = M.singleton (Term, name) $ qualName name',
                  envModTable = M.singleton name' $ mtyMod mty
                }
        (abstypes, env, specs') <- Env
    -> TypeM (TySet, Env, [SpecBase Info VName])
    -> TypeM (TySet, Env, [SpecBase Info VName])
    forall a. Env -> TypeM a -> TypeM a
    localEnv Env
    senv (TypeM (TySet, Env, [SpecBase Info VName])
     -> TypeM (TySet, Env, [SpecBase Info VName]))
    -> TypeM (TySet, Env, [SpecBase Info VName])
    -> TypeM (TySet, Env, [SpecBase Info VName])
    forall a b. (a -> b) -> a -> b
    $ [SpecBase NoInfo Name] -> TypeM (TySet, Env, [SpecBase Info VName])
    checkSpecs [SpecBase NoInfo Name]
    specs
        pure
          ( M.mapKeys (qualify name') (mtyAbs mty) <> abstypes,
            env <> senv,
            ModSpec name' sig' doc loc : specs'
          )
    checkSpecs (IncludeSpec ModTypeExpBase NoInfo Name
    e SrcLoc
    loc : [SpecBase NoInfo Name]
    specs) = do
      (e_abs, env_abs, e_env, e') <- ModTypeExpBase NoInfo Name
    -> TypeM (TySet, TySet, Env, ModTypeExpBase Info VName)
    checkModTypeExpToEnv ModTypeExpBase NoInfo Name
    e

      mapM_ warnIfShadowing $ M.keys env_abs

      (abstypes, env, specs') <- localEnv e_env $ checkSpecs specs
      pure
        ( e_abs <> env_abs <> abstypes,
          env <> e_env,
          IncludeSpec e' loc : specs'
        )
      where
        warnIfShadowing :: QualName VName -> TypeM ()
    warnIfShadowing QualName VName
    qn = do
          known <- QualName VName -> TypeM Bool
    isKnownType QualName VName
    qn
          when known $ warnAbout qn
        warnAbout :: a -> m ()
    warnAbout a
    qn =
          SrcLoc -> Doc () -> m ()
    forall loc. Located loc => loc -> Doc () -> m ()
    forall (m :: * -> *) loc.
    (MonadTypeChecker m, Located loc) =>
    loc -> Doc () -> m ()
    warn SrcLoc
    loc (Doc () -> m ()) -> Doc () -> m ()
    forall a b. (a -> b) -> a -> b
    $ Doc ()
    "Inclusion shadows type" Doc () -> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann
    dquotes (a -> Doc ()
    forall ann. a -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty a
    qn) Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Doc ()
    "."

    checkModTypeExp :: ModTypeExpBase NoInfo Name -> TypeM (TySet, MTy, ModTypeExpBase Info VName)
    checkModTypeExp :: ModTypeExpBase NoInfo Name
    -> TypeM (TySet, MTy, ModTypeExpBase Info VName)
    checkModTypeExp (ModTypeParens ModTypeExpBase NoInfo Name
    e SrcLoc
    loc) = do
      (abs, mty, e') <- ModTypeExpBase NoInfo Name
    -> TypeM (TySet, MTy, ModTypeExpBase Info VName)
    checkModTypeExp ModTypeExpBase NoInfo Name
    e
      pure (abs, mty, ModTypeParens e' loc)
    checkModTypeExp (ModTypeVar QualName Name
    name NoInfo (Map VName VName)
    NoInfo SrcLoc
    loc) = do
      (name', mty) <- SrcLoc -> QualName Name -> TypeM (QualName VName, MTy)
    lookupMTy SrcLoc
    loc QualName Name
    name
      (mty', substs) <- newNamesForMTy mty
      pure (mtyAbs mty', mty', ModTypeVar name' (Info substs) loc)
    checkModTypeExp (ModTypeSpecs [SpecBase NoInfo Name]
    specs SrcLoc
    loc) = do
      [SpecBase NoInfo Name] -> TypeM ()
    checkForDuplicateSpecs [SpecBase NoInfo Name]
    specs
      (abstypes, env, specs') <- [SpecBase NoInfo Name] -> TypeM (TySet, Env, [SpecBase Info VName])
    checkSpecs [SpecBase NoInfo Name]
    specs
      pure (abstypes, MTy abstypes $ ModEnv env, ModTypeSpecs specs' loc)
    checkModTypeExp (ModTypeWith ModTypeExpBase NoInfo Name
    s (TypeRef QualName Name
    tname [TypeParamBase Name]
    ps TypeExp (ExpBase NoInfo Name) Name
    te SrcLoc
    trloc) SrcLoc
    loc) = do
      (abs, s_abs, s_env, s') <- ModTypeExpBase NoInfo Name
    -> TypeM (TySet, TySet, Env, ModTypeExpBase Info VName)
    checkModTypeExpToEnv ModTypeExpBase NoInfo Name
    s
      resolveTypeParams ps $ \[TypeParamBase VName]
    ps' -> do
        (ext, te', te_t, _) <- [TypeParamBase VName]
    -> TypeM ([VName], TypeExp Exp VName, StructType, Liftedness)
    -> TypeM ([VName], TypeExp Exp VName, StructType, Liftedness)
    forall a. [TypeParamBase VName] -> TypeM a -> TypeM a
    bindingTypeParams [TypeParamBase VName]
    ps' (TypeM ([VName], TypeExp Exp VName, StructType, Liftedness)
     -> TypeM ([VName], TypeExp Exp VName, StructType, Liftedness))
    -> TypeM ([VName], TypeExp Exp VName, StructType, Liftedness)
    -> TypeM ([VName], TypeExp Exp VName, StructType, Liftedness)
    forall a b. (a -> b) -> a -> b
    $ TypeExp (ExpBase NoInfo Name) Name
    -> TypeM ([VName], TypeExp Exp VName, StructType, Liftedness)
    checkTypeDecl TypeExp (ExpBase NoInfo Name) Name
    te
        (tname', s_abs', s_env') <-
          refineEnv loc s_abs s_env tname ps' $ RetType ext te_t
        pure (abs, MTy s_abs' $ ModEnv s_env', ModTypeWith s' (TypeRef tname' ps' te' trloc) loc)
    checkModTypeExp (ModTypeArrow Maybe Name
    maybe_pname ModTypeExpBase NoInfo Name
    e1 ModTypeExpBase NoInfo Name
    e2 SrcLoc
    loc) = do
      (e1_abs, MTy s_abs e1_mod, e1') <- ModTypeExpBase NoInfo Name
    -> TypeM (TySet, MTy, ModTypeExpBase Info VName)
    checkModTypeExp ModTypeExpBase NoInfo Name
    e1
      (maybe_pname', (e2_abs, e2_mod, e2')) <-
        case maybe_pname of
          Just Name
    pname -> Namespace
    -> Name
    -> SrcLoc
    -> (VName
        -> TypeM (Maybe VName, (TySet, MTy, ModTypeExpBase Info VName)))
    -> TypeM (Maybe VName, (TySet, MTy, ModTypeExpBase Info VName))
    forall a.
    Namespace -> Name -> SrcLoc -> (VName -> TypeM a) -> TypeM a
    bindSpaced1 Namespace
    Term Name
    pname SrcLoc
    loc ((VName
      -> TypeM (Maybe VName, (TySet, MTy, ModTypeExpBase Info VName)))
     -> TypeM (Maybe VName, (TySet, MTy, ModTypeExpBase Info VName)))
    -> (VName
        -> TypeM (Maybe VName, (TySet, MTy, ModTypeExpBase Info VName)))
    -> TypeM (Maybe VName, (TySet, MTy, ModTypeExpBase Info VName))
    forall a b. (a -> b) -> a -> b
    $ \VName
    pname' ->
            Env
    -> TypeM (Maybe VName, (TySet, MTy, ModTypeExpBase Info VName))
    -> TypeM (Maybe VName, (TySet, MTy, ModTypeExpBase Info VName))
    forall a. Env -> TypeM a -> TypeM a
    localEnv (Env
    forall a. Monoid a => a
    mempty {envModTable = M.singleton pname' e1_mod}) (TypeM (Maybe VName, (TySet, MTy, ModTypeExpBase Info VName))
     -> TypeM (Maybe VName, (TySet, MTy, ModTypeExpBase Info VName)))
    -> TypeM (Maybe VName, (TySet, MTy, ModTypeExpBase Info VName))
    -> TypeM (Maybe VName, (TySet, MTy, ModTypeExpBase Info VName))
    forall a b. (a -> b) -> a -> b
    $
              (VName -> Maybe VName
    forall a. a -> Maybe a
    Just VName
    pname',) ((TySet, MTy, ModTypeExpBase Info VName)
     -> (Maybe VName, (TySet, MTy, ModTypeExpBase Info VName)))
    -> TypeM (TySet, MTy, ModTypeExpBase Info VName)
    -> TypeM (Maybe VName, (TySet, MTy, ModTypeExpBase Info VName))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ModTypeExpBase NoInfo Name
    -> TypeM (TySet, MTy, ModTypeExpBase Info VName)
    checkModTypeExp ModTypeExpBase NoInfo Name
    e2
          Maybe Name
    Nothing ->
            (Maybe VName
    forall a. Maybe a
    Nothing,) ((TySet, MTy, ModTypeExpBase Info VName)
     -> (Maybe VName, (TySet, MTy, ModTypeExpBase Info VName)))
    -> TypeM (TySet, MTy, ModTypeExpBase Info VName)
    -> TypeM (Maybe VName, (TySet, MTy, ModTypeExpBase Info VName))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ModTypeExpBase NoInfo Name
    -> TypeM (TySet, MTy, ModTypeExpBase Info VName)
    checkModTypeExp ModTypeExpBase NoInfo Name
    e2
      pure
        ( e1_abs <> e2_abs,
          MTy mempty $ ModFun $ FunModType s_abs e1_mod e2_mod,
          ModTypeArrow maybe_pname' e1' e2' loc
        )

    checkModTypeExpToEnv ::
      ModTypeExpBase NoInfo Name ->
      TypeM (TySet, TySet, Env, ModTypeExpBase Info VName)
    checkModTypeExpToEnv :: ModTypeExpBase NoInfo Name
    -> TypeM (TySet, TySet, Env, ModTypeExpBase Info VName)
    checkModTypeExpToEnv ModTypeExpBase NoInfo Name
    e = do
      (abs, MTy mod_abs mod, e') <- ModTypeExpBase NoInfo Name
    -> TypeM (TySet, MTy, ModTypeExpBase Info VName)
    checkModTypeExp ModTypeExpBase NoInfo Name
    e
      case mod of
        ModEnv Env
    env -> (TySet, TySet, Env, ModTypeExpBase Info VName)
    -> TypeM (TySet, TySet, Env, ModTypeExpBase Info VName)
    forall a. a -> TypeM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (TySet
    abs, TySet
    mod_abs, Env
    env, ModTypeExpBase Info VName
    e')
        ModFun {} -> SrcLoc -> TypeM (TySet, TySet, Env, ModTypeExpBase Info VName)
    forall (m :: * -> *) a. MonadTypeChecker m => SrcLoc -> m a
    unappliedFunctor (SrcLoc -> TypeM (TySet, TySet, Env, ModTypeExpBase Info VName))
    -> SrcLoc -> TypeM (TySet, TySet, Env, ModTypeExpBase Info VName)
    forall a b. (a -> b) -> a -> b
    $ ModTypeExpBase NoInfo Name -> SrcLoc
    forall a. Located a => a -> SrcLoc
    srclocOf ModTypeExpBase NoInfo Name
    e

    checkModTypeBind :: ModTypeBindBase NoInfo Name -> TypeM (TySet, Env, ModTypeBindBase Info VName)
    checkModTypeBind :: ModTypeBindBase NoInfo Name
    -> TypeM (TySet, Env, ModTypeBindBase Info VName)
    checkModTypeBind (ModTypeBind Name
    name ModTypeExpBase NoInfo Name
    e Maybe DocComment
    doc SrcLoc
    loc) = do
      (abs, env, e') <- ModTypeExpBase NoInfo Name
    -> TypeM (TySet, MTy, ModTypeExpBase Info VName)
    checkModTypeExp ModTypeExpBase NoInfo Name
    e
      bindSpaced1 Signature name loc $ \VName
    name' -> do
        VName -> TypeM ()
    usedName VName
    name'
        (TySet, Env, ModTypeBindBase Info VName)
    -> TypeM (TySet, Env, ModTypeBindBase Info VName)
    forall a. a -> TypeM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure
          ( TySet
    abs,
            Env
    forall a. Monoid a => a
    mempty
              { envModTypeTable = M.singleton name' env,
                envNameMap = M.singleton (Signature, name) (qualName name')
              },
            VName
    -> ModTypeExpBase Info VName
    -> Maybe DocComment
    -> SrcLoc
    -> ModTypeBindBase Info VName
    forall (f :: * -> *) vn.
    vn
    -> ModTypeExpBase f vn
    -> Maybe DocComment
    -> SrcLoc
    -> ModTypeBindBase f vn
    ModTypeBind VName
    name' ModTypeExpBase Info VName
    e' Maybe DocComment
    doc SrcLoc
    loc
          )

    checkOneModExp ::
      ModExpBase NoInfo Name ->
      TypeM (TySet, MTy, ModExpBase Info VName)
    checkOneModExp :: ModExpBase NoInfo Name -> TypeM (TySet, MTy, ModExpBase Info VName)
    checkOneModExp (ModParens ModExpBase NoInfo Name
    e SrcLoc
    loc) = do
      (abs, mty, e') <- ModExpBase NoInfo Name -> TypeM (TySet, MTy, ModExpBase Info VName)
    checkOneModExp ModExpBase NoInfo Name
    e
      pure (abs, mty, ModParens e' loc)
    checkOneModExp (ModDecs [UncheckedDec]
    decs SrcLoc
    loc) = do
      [UncheckedDec] -> TypeM ()
    checkForDuplicateDecs [UncheckedDec]
    decs
      (abstypes, env, decs', _) <- [UncheckedDec] -> TypeM (TySet, Env, [Dec], Env)
    checkDecs [UncheckedDec]
    decs
      pure
        ( abstypes,
          MTy abstypes $ ModEnv env,
          ModDecs decs' loc
        )
    checkOneModExp (ModVar QualName Name
    v SrcLoc
    loc) = do
      (v', env) <- SrcLoc -> QualName Name -> TypeM (QualName VName, Mod)
    lookupMod SrcLoc
    loc QualName Name
    v
      when
        ( baseName (qualLeaf v') == nameFromString "intrinsics"
            && baseTag (qualLeaf v') <= maxIntrinsicTag
        )
        $ typeError loc mempty "The 'intrinsics' module may not be used in module expressions."
      pure (mempty, MTy mempty env, ModVar v' loc)
    checkOneModExp (ModImport FilePath
    name NoInfo ImportName
    NoInfo SrcLoc
    loc) = do
      (name', env) <- SrcLoc -> FilePath -> TypeM (ImportName, Env)
    lookupImport SrcLoc
    loc FilePath
    name
      pure
        ( mempty,
          MTy mempty $ ModEnv env,
          ModImport name (Info name') loc
        )
    checkOneModExp (ModApply ModExpBase NoInfo Name
    f ModExpBase NoInfo Name
    e NoInfo (Map VName VName)
    NoInfo NoInfo (Map VName VName)
    NoInfo SrcLoc
    loc) = do
      (f_abs, f_mty, f') <- ModExpBase NoInfo Name -> TypeM (TySet, MTy, ModExpBase Info VName)
    checkOneModExp ModExpBase NoInfo Name
    f
      case mtyMod f_mty of
        ModFun FunModType
    functor -> do
          (e_abs, e_mty, e') <- ModExpBase NoInfo Name -> TypeM (TySet, MTy, ModExpBase Info VName)
    checkOneModExp ModExpBase NoInfo Name
    e
          (mty, psubsts, rsubsts) <- applyFunctor (locOf loc) functor e_mty
          pure
            ( mtyAbs mty <> f_abs <> e_abs,
              mty,
              ModApply f' e' (Info psubsts) (Info rsubsts) loc
            )
        Mod
    _ ->
          SrcLoc
    -> Notes -> Doc () -> TypeM (TySet, MTy, ModExpBase Info VName)
    forall loc a. Located loc => loc -> Notes -> Doc () -> TypeM a
    forall (m :: * -> *) loc a.
    (MonadTypeChecker m, Located loc) =>
    loc -> Notes -> Doc () -> m a
    typeError SrcLoc
    loc Notes
    forall a. Monoid a => a
    mempty Doc ()
    "Cannot apply non-parametric module."
    checkOneModExp (ModAscript ModExpBase NoInfo Name
    me ModTypeExpBase NoInfo Name
    se NoInfo (Map VName VName)
    NoInfo SrcLoc
    loc) = do
      (me_abs, me_mod, me') <- ModExpBase NoInfo Name -> TypeM (TySet, MTy, ModExpBase Info VName)
    checkOneModExp ModExpBase NoInfo Name
    me
      (se_abs, se_mty, se') <- checkModTypeExp se
      match_subst <- badOnLeft $ matchMTys me_mod se_mty (locOf loc)
      pure (se_abs <> me_abs, se_mty, ModAscript me' se' (Info match_subst) loc)
    checkOneModExp (ModLambda ModParamBase NoInfo Name
    param Maybe (ModTypeExpBase NoInfo Name, NoInfo (Map VName VName))
    maybe_fsig_e ModExpBase NoInfo Name
    body_e SrcLoc
    loc) =
      ModParamBase NoInfo Name
    -> (ModParamBase Info VName
        -> TySet -> Mod -> TypeM (TySet, MTy, ModExpBase Info VName))
    -> TypeM (TySet, MTy, ModExpBase Info VName)
    forall a.
    ModParamBase NoInfo Name
    -> (ModParamBase Info VName -> TySet -> Mod -> TypeM a) -> TypeM a
    withModParam ModParamBase NoInfo Name
    param ((ModParamBase Info VName
      -> TySet -> Mod -> TypeM (TySet, MTy, ModExpBase Info VName))
     -> TypeM (TySet, MTy, ModExpBase Info VName))
    -> (ModParamBase Info VName
        -> TySet -> Mod -> TypeM (TySet, MTy, ModExpBase Info VName))
    -> TypeM (TySet, MTy, ModExpBase Info VName)
    forall a b. (a -> b) -> a -> b
    $ \ModParamBase Info VName
    param' TySet
    param_abs Mod
    param_mod -> do
        (abs, maybe_fsig_e', body_e', mty) <-
          Maybe (ModTypeExpBase NoInfo Name)
    -> ModExpBase NoInfo Name
    -> SrcLoc
    -> TypeM
         (TySet, Maybe (ModTypeExpBase Info VName, Info (Map VName VName)),
          ModExpBase Info VName, MTy)
    checkModBody ((ModTypeExpBase NoInfo Name, NoInfo (Map VName VName))
    -> ModTypeExpBase NoInfo Name
    forall a b. (a, b) -> a
    fst ((ModTypeExpBase NoInfo Name, NoInfo (Map VName VName))
     -> ModTypeExpBase NoInfo Name)
    -> Maybe (ModTypeExpBase NoInfo Name, NoInfo (Map VName VName))
    -> Maybe (ModTypeExpBase NoInfo Name)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe (ModTypeExpBase NoInfo Name, NoInfo (Map VName VName))
    maybe_fsig_e) ModExpBase NoInfo Name
    body_e SrcLoc
    loc
        pure
          ( abs,
            MTy mempty $ ModFun $ FunModType param_abs param_mod mty,
            ModLambda param' maybe_fsig_e' body_e' loc
          )

    checkOneModExpToEnv :: ModExpBase NoInfo Name -> TypeM (TySet, Env, ModExpBase Info VName)
    checkOneModExpToEnv :: ModExpBase NoInfo Name -> TypeM (TySet, Env, ModExpBase Info VName)
    checkOneModExpToEnv ModExpBase NoInfo Name
    e = do
      (e_abs, MTy abs mod, e') <- ModExpBase NoInfo Name -> TypeM (TySet, MTy, ModExpBase Info VName)
    checkOneModExp ModExpBase NoInfo Name
    e
      case mod of
        ModEnv Env
    env -> (TySet, Env, ModExpBase Info VName)
    -> TypeM (TySet, Env, ModExpBase Info VName)
    forall a. a -> TypeM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (TySet
    e_abs TySet -> TySet -> TySet
    forall a. Semigroup a => a -> a -> a
    <> TySet
    abs, Env
    env, ModExpBase Info VName
    e')
        ModFun {} -> SrcLoc -> TypeM (TySet, Env, ModExpBase Info VName)
    forall (m :: * -> *) a. MonadTypeChecker m => SrcLoc -> m a
    unappliedFunctor (SrcLoc -> TypeM (TySet, Env, ModExpBase Info VName))
    -> SrcLoc -> TypeM (TySet, Env, ModExpBase Info VName)
    forall a b. (a -> b) -> a -> b
    $ ModExpBase NoInfo Name -> SrcLoc
    forall a. Located a => a -> SrcLoc
    srclocOf ModExpBase NoInfo Name
    e

    withModParam ::
      ModParamBase NoInfo Name ->
      (ModParamBase Info VName -> TySet -> Mod -> TypeM a) ->
      TypeM a
    withModParam :: forall a.
    ModParamBase NoInfo Name
    -> (ModParamBase Info VName -> TySet -> Mod -> TypeM a) -> TypeM a
    withModParam (ModParam Name
    pname ModTypeExpBase NoInfo Name
    psig_e NoInfo [VName]
    NoInfo SrcLoc
    loc) ModParamBase Info VName -> TySet -> Mod -> TypeM a
    m = do
      (_abs, MTy p_abs p_mod, psig_e') <- ModTypeExpBase NoInfo Name
    -> TypeM (TySet, MTy, ModTypeExpBase Info VName)
    checkModTypeExp ModTypeExpBase NoInfo Name
    psig_e
      bindSpaced1 Term pname loc $ \VName
    pname' -> do
        let in_body_env :: Env
    in_body_env = Env
    forall a. Monoid a => a
    mempty {envModTable = M.singleton pname' p_mod}
        Env -> TypeM a -> TypeM a
    forall a. Env -> TypeM a -> TypeM a
    localEnv Env
    in_body_env (TypeM a -> TypeM a) -> TypeM a -> TypeM a
    forall a b. (a -> b) -> a -> b
    $
          ModParamBase Info VName -> TySet -> Mod -> TypeM a
    m (VName
    -> ModTypeExpBase Info VName
    -> Info [VName]
    -> SrcLoc
    -> ModParamBase Info VName
    forall (f :: * -> *) vn.
    vn
    -> ModTypeExpBase f vn -> f [VName] -> SrcLoc -> ModParamBase f vn
    ModParam VName
    pname' ModTypeExpBase Info VName
    psig_e' ([VName] -> Info [VName]
    forall a. a -> Info a
    Info ([VName] -> Info [VName]) -> [VName] -> Info [VName]
    forall a b. (a -> b) -> a -> b
    $ (QualName VName -> VName) -> [QualName VName] -> [VName]
    forall a b. (a -> b) -> [a] -> [b]
    map QualName VName -> VName
    forall vn. QualName vn -> vn
    qualLeaf ([QualName VName] -> [VName]) -> [QualName VName] -> [VName]
    forall a b. (a -> b) -> a -> b
    $ TySet -> [QualName VName]
    forall k a. Map k a -> [k]
    M.keys TySet
    p_abs) SrcLoc
    loc) TySet
    p_abs Mod
    p_mod

    withModParams ::
      [ModParamBase NoInfo Name] ->
      ([(ModParamBase Info VName, TySet, Mod)] -> TypeM a) ->
      TypeM a
    withModParams :: forall a.
    [ModParamBase NoInfo Name]
    -> ([(ModParamBase Info VName, TySet, Mod)] -> TypeM a) -> TypeM a
    withModParams [] [(ModParamBase Info VName, TySet, Mod)] -> TypeM a
    m = [(ModParamBase Info VName, TySet, Mod)] -> TypeM a
    m []
    withModParams (ModParamBase NoInfo Name
    p : [ModParamBase NoInfo Name]
    ps) [(ModParamBase Info VName, TySet, Mod)] -> TypeM a
    m =
      ModParamBase NoInfo Name
    -> (ModParamBase Info VName -> TySet -> Mod -> TypeM a) -> TypeM a
    forall a.
    ModParamBase NoInfo Name
    -> (ModParamBase Info VName -> TySet -> Mod -> TypeM a) -> TypeM a
    withModParam ModParamBase NoInfo Name
    p ((ModParamBase Info VName -> TySet -> Mod -> TypeM a) -> TypeM a)
    -> (ModParamBase Info VName -> TySet -> Mod -> TypeM a) -> TypeM a
    forall a b. (a -> b) -> a -> b
    $ \ModParamBase Info VName
    p' TySet
    pabs Mod
    pmod ->
        [ModParamBase NoInfo Name]
    -> ([(ModParamBase Info VName, TySet, Mod)] -> TypeM a) -> TypeM a
    forall a.
    [ModParamBase NoInfo Name]
    -> ([(ModParamBase Info VName, TySet, Mod)] -> TypeM a) -> TypeM a
    withModParams [ModParamBase NoInfo Name]
    ps (([(ModParamBase Info VName, TySet, Mod)] -> TypeM a) -> TypeM a)
    -> ([(ModParamBase Info VName, TySet, Mod)] -> TypeM a) -> TypeM a
    forall a b. (a -> b) -> a -> b
    $ \[(ModParamBase Info VName, TySet, Mod)]
    ps' -> [(ModParamBase Info VName, TySet, Mod)] -> TypeM a
    m ([(ModParamBase Info VName, TySet, Mod)] -> TypeM a)
    -> [(ModParamBase Info VName, TySet, Mod)] -> TypeM a
    forall a b. (a -> b) -> a -> b
    $ (ModParamBase Info VName
    p', TySet
    pabs, Mod
    pmod) (ModParamBase Info VName, TySet, Mod)
    -> [(ModParamBase Info VName, TySet, Mod)]
    -> [(ModParamBase Info VName, TySet, Mod)]
    forall a. a -> [a] -> [a]
    : [(ModParamBase Info VName, TySet, Mod)]
    ps'

    checkModBody ::
      Maybe (ModTypeExpBase NoInfo Name) ->
      ModExpBase NoInfo Name ->
      SrcLoc ->
      TypeM
        ( TySet,
          Maybe (ModTypeExp, Info (M.Map VName VName)),
          ModExp,
          MTy
        )
    checkModBody :: Maybe (ModTypeExpBase NoInfo Name)
    -> ModExpBase NoInfo Name
    -> SrcLoc
    -> TypeM
         (TySet, Maybe (ModTypeExpBase Info VName, Info (Map VName VName)),
          ModExpBase Info VName, MTy)
    checkModBody Maybe (ModTypeExpBase NoInfo Name)
    maybe_fsig_e ModExpBase NoInfo Name
    body_e SrcLoc
    loc = TypeM
      (TySet, Maybe (ModTypeExpBase Info VName, Info (Map VName VName)),
       ModExpBase Info VName, MTy)
    -> TypeM
         (TySet, Maybe (ModTypeExpBase Info VName, Info (Map VName VName)),
          ModExpBase Info VName, MTy)
    forall a. TypeM a -> TypeM a
    enteringModule (TypeM
       (TySet, Maybe (ModTypeExpBase Info VName, Info (Map VName VName)),
        ModExpBase Info VName, MTy)
     -> TypeM
          (TySet, Maybe (ModTypeExpBase Info VName, Info (Map VName VName)),
           ModExpBase Info VName, MTy))
    -> TypeM
         (TySet, Maybe (ModTypeExpBase Info VName, Info (Map VName VName)),
          ModExpBase Info VName, MTy)
    -> TypeM
         (TySet, Maybe (ModTypeExpBase Info VName, Info (Map VName VName)),
          ModExpBase Info VName, MTy)
    forall a b. (a -> b) -> a -> b
    $ do
      (body_e_abs, body_mty, body_e') <- ModExpBase NoInfo Name -> TypeM (TySet, MTy, ModExpBase Info VName)
    checkOneModExp ModExpBase NoInfo Name
    body_e
      case maybe_fsig_e of
        Maybe (ModTypeExpBase NoInfo Name)
    Nothing ->
          (TySet, Maybe (ModTypeExpBase Info VName, Info (Map VName VName)),
     ModExpBase Info VName, MTy)
    -> TypeM
         (TySet, Maybe (ModTypeExpBase Info VName, Info (Map VName VName)),
          ModExpBase Info VName, MTy)
    forall a. a -> TypeM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure
            ( MTy -> TySet
    mtyAbs MTy
    body_mty TySet -> TySet -> TySet
    forall a. Semigroup a => a -> a -> a
    <> TySet
    body_e_abs,
              Maybe (ModTypeExpBase Info VName, Info (Map VName VName))
    forall a. Maybe a
    Nothing,
              ModExpBase Info VName
    body_e',
              MTy
    body_mty
            )
        Just ModTypeExpBase NoInfo Name
    fsig_e -> do
          (fsig_abs, fsig_mty, fsig_e') <- ModTypeExpBase NoInfo Name
    -> TypeM (TySet, MTy, ModTypeExpBase Info VName)
    checkModTypeExp ModTypeExpBase NoInfo Name
    fsig_e
          fsig_subst <- badOnLeft $ matchMTys body_mty fsig_mty (locOf loc)
          pure
            ( fsig_abs <> body_e_abs,
              Just (fsig_e', Info fsig_subst),
              body_e',
              fsig_mty
            )

    checkModBind :: ModBindBase NoInfo Name -> TypeM (TySet, Env, ModBindBase Info VName)
    checkModBind :: ModBindBase NoInfo Name
    -> TypeM (TySet, Env, ModBindBase Info VName)
    checkModBind (ModBind Name
    name [] Maybe (ModTypeExpBase NoInfo Name, NoInfo (Map VName VName))
    maybe_fsig_e ModExpBase NoInfo Name
    e Maybe DocComment
    doc SrcLoc
    loc) = do
      (e_abs, maybe_fsig_e', e', mty) <- Maybe (ModTypeExpBase NoInfo Name)
    -> ModExpBase NoInfo Name
    -> SrcLoc
    -> TypeM
         (TySet, Maybe (ModTypeExpBase Info VName, Info (Map VName VName)),
          ModExpBase Info VName, MTy)
    checkModBody ((ModTypeExpBase NoInfo Name, NoInfo (Map VName VName))
    -> ModTypeExpBase NoInfo Name
    forall a b. (a, b) -> a
    fst ((ModTypeExpBase NoInfo Name, NoInfo (Map VName VName))
     -> ModTypeExpBase NoInfo Name)
    -> Maybe (ModTypeExpBase NoInfo Name, NoInfo (Map VName VName))
    -> Maybe (ModTypeExpBase NoInfo Name)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe (ModTypeExpBase NoInfo Name, NoInfo (Map VName VName))
    maybe_fsig_e) ModExpBase NoInfo Name
    e SrcLoc
    loc
      bindSpaced1 Term name loc $ \VName
    name' -> do
        VName -> TypeM ()
    usedName VName
    name'
        (TySet, Env, ModBindBase Info VName)
    -> TypeM (TySet, Env, ModBindBase Info VName)
    forall a. a -> TypeM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure
          ( TySet
    e_abs,
            Env
    forall a. Monoid a => a
    mempty
              { envModTable = M.singleton name' $ mtyMod mty,
                envNameMap = M.singleton (Term, name) $ qualName name'
              },
            VName
    -> [ModParamBase Info VName]
    -> Maybe (ModTypeExpBase Info VName, Info (Map VName VName))
    -> ModExpBase Info VName
    -> Maybe DocComment
    -> SrcLoc
    -> ModBindBase Info VName
    forall (f :: * -> *) vn.
    vn
    -> [ModParamBase f vn]
    -> Maybe (ModTypeExpBase f vn, f (Map VName VName))
    -> ModExpBase f vn
    -> Maybe DocComment
    -> SrcLoc
    -> ModBindBase f vn
    ModBind VName
    name' [] Maybe (ModTypeExpBase Info VName, Info (Map VName VName))
    maybe_fsig_e' ModExpBase Info VName
    e' Maybe DocComment
    doc SrcLoc
    loc
          )
    checkModBind (ModBind Name
    name (ModParamBase NoInfo Name
    p : [ModParamBase NoInfo Name]
    ps) Maybe (ModTypeExpBase NoInfo Name, NoInfo (Map VName VName))
    maybe_fsig_e ModExpBase NoInfo Name
    body_e Maybe DocComment
    doc SrcLoc
    loc) = do
      (abs, params', maybe_fsig_e', body_e', funsig) <-
        ModParamBase NoInfo Name
    -> (ModParamBase Info VName
        -> TySet
        -> Mod
        -> TypeM
             (TySet, [ModParamBase Info VName],
              Maybe (ModTypeExpBase Info VName, Info (Map VName VName)),
              ModExpBase Info VName, FunModType))
    -> TypeM
         (TySet, [ModParamBase Info VName],
          Maybe (ModTypeExpBase Info VName, Info (Map VName VName)),
          ModExpBase Info VName, FunModType)
    forall a.
    ModParamBase NoInfo Name
    -> (ModParamBase Info VName -> TySet -> Mod -> TypeM a) -> TypeM a
    withModParam ModParamBase NoInfo Name
    p ((ModParamBase Info VName
      -> TySet
      -> Mod
      -> TypeM
           (TySet, [ModParamBase Info VName],
            Maybe (ModTypeExpBase Info VName, Info (Map VName VName)),
            ModExpBase Info VName, FunModType))
     -> TypeM
          (TySet, [ModParamBase Info VName],
           Maybe (ModTypeExpBase Info VName, Info (Map VName VName)),
           ModExpBase Info VName, FunModType))
    -> (ModParamBase Info VName
        -> TySet
        -> Mod
        -> TypeM
             (TySet, [ModParamBase Info VName],
              Maybe (ModTypeExpBase Info VName, Info (Map VName VName)),
              ModExpBase Info VName, FunModType))
    -> TypeM
         (TySet, [ModParamBase Info VName],
          Maybe (ModTypeExpBase Info VName, Info (Map VName VName)),
          ModExpBase Info VName, FunModType)
    forall a b. (a -> b) -> a -> b
    $ \ModParamBase Info VName
    p' TySet
    p_abs Mod
    p_mod ->
          [ModParamBase NoInfo Name]
    -> ([(ModParamBase Info VName, TySet, Mod)]
        -> TypeM
             (TySet, [ModParamBase Info VName],
              Maybe (ModTypeExpBase Info VName, Info (Map VName VName)),
              ModExpBase Info VName, FunModType))
    -> TypeM
         (TySet, [ModParamBase Info VName],
          Maybe (ModTypeExpBase Info VName, Info (Map VName VName)),
          ModExpBase Info VName, FunModType)
    forall a.
    [ModParamBase NoInfo Name]
    -> ([(ModParamBase Info VName, TySet, Mod)] -> TypeM a) -> TypeM a
    withModParams [ModParamBase NoInfo Name]
    ps (([(ModParamBase Info VName, TySet, Mod)]
      -> TypeM
           (TySet, [ModParamBase Info VName],
            Maybe (ModTypeExpBase Info VName, Info (Map VName VName)),
            ModExpBase Info VName, FunModType))
     -> TypeM
          (TySet, [ModParamBase Info VName],
           Maybe (ModTypeExpBase Info VName, Info (Map VName VName)),
           ModExpBase Info VName, FunModType))
    -> ([(ModParamBase Info VName, TySet, Mod)]
        -> TypeM
             (TySet, [ModParamBase Info VName],
              Maybe (ModTypeExpBase Info VName, Info (Map VName VName)),
              ModExpBase Info VName, FunModType))
    -> TypeM
         (TySet, [ModParamBase Info VName],
          Maybe (ModTypeExpBase Info VName, Info (Map VName VName)),
          ModExpBase Info VName, FunModType)
    forall a b. (a -> b) -> a -> b
    $ \[(ModParamBase Info VName, TySet, Mod)]
    params_stuff -> do
            let ([ModParamBase Info VName]
    ps', [TySet]
    ps_abs, [Mod]
    ps_mod) = [(ModParamBase Info VName, TySet, Mod)]
    -> ([ModParamBase Info VName], [TySet], [Mod])
    forall a b c. [(a, b, c)] -> ([a], [b], [c])
    unzip3 [(ModParamBase Info VName, TySet, Mod)]
    params_stuff
            (abs, maybe_fsig_e', body_e', mty) <- Maybe (ModTypeExpBase NoInfo Name)
    -> ModExpBase NoInfo Name
    -> SrcLoc
    -> TypeM
         (TySet, Maybe (ModTypeExpBase Info VName, Info (Map VName VName)),
          ModExpBase Info VName, MTy)
    checkModBody ((ModTypeExpBase NoInfo Name, NoInfo (Map VName VName))
    -> ModTypeExpBase NoInfo Name
    forall a b. (a, b) -> a
    fst ((ModTypeExpBase NoInfo Name, NoInfo (Map VName VName))
     -> ModTypeExpBase NoInfo Name)
    -> Maybe (ModTypeExpBase NoInfo Name, NoInfo (Map VName VName))
    -> Maybe (ModTypeExpBase NoInfo Name)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe (ModTypeExpBase NoInfo Name, NoInfo (Map VName VName))
    maybe_fsig_e) ModExpBase NoInfo Name
    body_e SrcLoc
    loc
            let addParam (TySet
    x, Mod
    y) MTy
    mty' = TySet -> Mod -> MTy
    MTy TySet
    forall a. Monoid a => a
    mempty (Mod -> MTy) -> Mod -> MTy
    forall a b. (a -> b) -> a -> b
    $ FunModType -> Mod
    ModFun (FunModType -> Mod) -> FunModType -> Mod
    forall a b. (a -> b) -> a -> b
    $ TySet -> Mod -> MTy -> FunModType
    FunModType TySet
    x Mod
    y MTy
    mty'
            pure
              ( abs,
                p' : ps',
                maybe_fsig_e',
                body_e',
                FunModType p_abs p_mod $ foldr addParam mty $ zip ps_abs ps_mod
              )
      bindSpaced1 Term name loc $ \VName
    name' -> do
        VName -> TypeM ()
    usedName VName
    name'
        (TySet, Env, ModBindBase Info VName)
    -> TypeM (TySet, Env, ModBindBase Info VName)
    forall a. a -> TypeM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure
          ( TySet
    abs,
            Env
    forall a. Monoid a => a
    mempty
              { envModTable =
                  M.singleton name' $ ModFun funsig,
                envNameMap =
                  M.singleton (Term, name) $ qualName name'
              },
            VName
    -> [ModParamBase Info VName]
    -> Maybe (ModTypeExpBase Info VName, Info (Map VName VName))
    -> ModExpBase Info VName
    -> Maybe DocComment
    -> SrcLoc
    -> ModBindBase Info VName
    forall (f :: * -> *) vn.
    vn
    -> [ModParamBase f vn]
    -> Maybe (ModTypeExpBase f vn, f (Map VName VName))
    -> ModExpBase f vn
    -> Maybe DocComment
    -> SrcLoc
    -> ModBindBase f vn
    ModBind VName
    name' [ModParamBase Info VName]
    params' Maybe (ModTypeExpBase Info VName, Info (Map VName VName))
    maybe_fsig_e' ModExpBase Info VName
    body_e' Maybe DocComment
    doc SrcLoc
    loc
          )

    checkForDuplicateSpecs :: [SpecBase NoInfo Name] -> TypeM ()
    checkForDuplicateSpecs :: [SpecBase NoInfo Name] -> TypeM ()
    checkForDuplicateSpecs =
      (Map (Namespace, Name) SrcLoc
     -> SpecBase NoInfo Name -> TypeM (Map (Namespace, Name) SrcLoc))
    -> Map (Namespace, Name) SrcLoc
    -> [SpecBase NoInfo Name]
    -> TypeM ()
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Monad m) =>
    (b -> a -> m b) -> b -> t a -> m ()
    foldM_ ((SpecBase NoInfo Name
     -> Map (Namespace, Name) SrcLoc
     -> TypeM (Map (Namespace, Name) SrcLoc))
    -> Map (Namespace, Name) SrcLoc
    -> SpecBase NoInfo Name
    -> TypeM (Map (Namespace, Name) SrcLoc)
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip SpecBase NoInfo Name
    -> Map (Namespace, Name) SrcLoc
    -> TypeM (Map (Namespace, Name) SrcLoc)
    forall {m :: * -> *} {f :: * -> *}.
    MonadTypeChecker m =>
    SpecBase f Name
    -> Map (Namespace, Name) SrcLoc -> m (Map (Namespace, Name) SrcLoc)
    f) Map (Namespace, Name) SrcLoc
    forall a. Monoid a => a
    mempty
      where
        check :: Namespace
    -> Name
    -> SrcLoc
    -> Map (Namespace, Name) SrcLoc
    -> m (Map (Namespace, Name) SrcLoc)
    check Namespace
    namespace Name
    name SrcLoc
    loc Map (Namespace, Name) SrcLoc
    known =
          case (Namespace, Name) -> Map (Namespace, Name) SrcLoc -> Maybe SrcLoc
    forall k a. Ord k => k -> Map k a -> Maybe a
    M.lookup (Namespace
    namespace, Name
    name) Map (Namespace, Name) SrcLoc
    known of
            Just SrcLoc
    loc' ->
              Namespace
    -> Name -> SrcLoc -> SrcLoc -> m (Map (Namespace, Name) SrcLoc)
    forall (m :: * -> *) a.
    MonadTypeChecker m =>
    Namespace -> Name -> SrcLoc -> SrcLoc -> m a
    dupDefinitionError Namespace
    namespace Name
    name SrcLoc
    loc SrcLoc
    loc'
            Maybe SrcLoc
    _ -> Map (Namespace, Name) SrcLoc -> m (Map (Namespace, Name) SrcLoc)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Map (Namespace, Name) SrcLoc -> m (Map (Namespace, Name) SrcLoc))
    -> Map (Namespace, Name) SrcLoc -> m (Map (Namespace, Name) SrcLoc)
    forall a b. (a -> b) -> a -> b
    $ (Namespace, Name)
    -> SrcLoc
    -> Map (Namespace, Name) SrcLoc
    -> Map (Namespace, Name) SrcLoc
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    M.insert (Namespace
    namespace, Name
    name) SrcLoc
    loc Map (Namespace, Name) SrcLoc
    known

        f :: SpecBase f Name
    -> Map (Namespace, Name) SrcLoc -> m (Map (Namespace, Name) SrcLoc)
    f (ValSpec Name
    name [TypeParamBase Name]
    _ TypeExp (ExpBase f Name) Name
    _ f StructType
    _ Maybe DocComment
    _ SrcLoc
    loc) =
          Namespace
    -> Name
    -> SrcLoc
    -> Map (Namespace, Name) SrcLoc
    -> m (Map (Namespace, Name) SrcLoc)
    forall {m :: * -> *}.
    MonadTypeChecker m =>
    Namespace
    -> Name
    -> SrcLoc
    -> Map (Namespace, Name) SrcLoc
    -> m (Map (Namespace, Name) SrcLoc)
    check Namespace
    Term Name
    name SrcLoc
    loc
        f (TypeAbbrSpec (TypeBind Name
    name Liftedness
    _ [TypeParamBase Name]
    _ TypeExp (ExpBase f Name) Name
    _ f StructRetType
    _ Maybe DocComment
    _ SrcLoc
    loc)) =
          Namespace
    -> Name
    -> SrcLoc
    -> Map (Namespace, Name) SrcLoc
    -> m (Map (Namespace, Name) SrcLoc)
    forall {m :: * -> *}.
    MonadTypeChecker m =>
    Namespace
    -> Name
    -> SrcLoc
    -> Map (Namespace, Name) SrcLoc
    -> m (Map (Namespace, Name) SrcLoc)
    check Namespace
    Type Name
    name SrcLoc
    loc
        f (TypeSpec Liftedness
    _ Name
    name [TypeParamBase Name]
    _ Maybe DocComment
    _ SrcLoc
    loc) =
          Namespace
    -> Name
    -> SrcLoc
    -> Map (Namespace, Name) SrcLoc
    -> m (Map (Namespace, Name) SrcLoc)
    forall {m :: * -> *}.
    MonadTypeChecker m =>
    Namespace
    -> Name
    -> SrcLoc
    -> Map (Namespace, Name) SrcLoc
    -> m (Map (Namespace, Name) SrcLoc)
    check Namespace
    Type Name
    name SrcLoc
    loc
        f (ModSpec Name
    name ModTypeExpBase f Name
    _ Maybe DocComment
    _ SrcLoc
    loc) =
          Namespace
    -> Name
    -> SrcLoc
    -> Map (Namespace, Name) SrcLoc
    -> m (Map (Namespace, Name) SrcLoc)
    forall {m :: * -> *}.
    MonadTypeChecker m =>
    Namespace
    -> Name
    -> SrcLoc
    -> Map (Namespace, Name) SrcLoc
    -> m (Map (Namespace, Name) SrcLoc)
    check Namespace
    Term Name
    name SrcLoc
    loc
        f IncludeSpec {} =
          Map (Namespace, Name) SrcLoc -> m (Map (Namespace, Name) SrcLoc)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure

    checkTypeBind ::
      TypeBindBase NoInfo Name ->
      TypeM (Env, TypeBindBase Info VName)
    checkTypeBind :: TypeBindBase NoInfo Name -> TypeM (Env, TypeBindBase Info VName)
    checkTypeBind (TypeBind Name
    name Liftedness
    l [TypeParamBase Name]
    tps TypeExp (ExpBase NoInfo Name) Name
    te NoInfo StructRetType
    NoInfo Maybe DocComment
    doc SrcLoc
    loc) =
      [TypeParamBase Name]
    -> ([TypeParamBase VName] -> TypeM (Env, TypeBindBase Info VName))
    -> TypeM (Env, TypeBindBase Info VName)
    forall a.
    [TypeParamBase Name]
    -> ([TypeParamBase VName] -> TypeM a) -> TypeM a
    resolveTypeParams [TypeParamBase Name]
    tps (([TypeParamBase VName] -> TypeM (Env, TypeBindBase Info VName))
     -> TypeM (Env, TypeBindBase Info VName))
    -> ([TypeParamBase VName] -> TypeM (Env, TypeBindBase Info VName))
    -> TypeM (Env, TypeBindBase Info VName)
    forall a b. (a -> b) -> a -> b
    $ \[TypeParamBase VName]
    tps' -> do
        (te', svars, RetType dims t, l') <-
          [TypeParamBase VName]
    -> TypeM (TypeExp Exp VName, [VName], ResRetType, Liftedness)
    -> TypeM (TypeExp Exp VName, [VName], ResRetType, Liftedness)
    forall a. [TypeParamBase VName] -> TypeM a -> TypeM a
    bindingTypeParams [TypeParamBase VName]
    tps' (TypeM (TypeExp Exp VName, [VName], ResRetType, Liftedness)
     -> TypeM (TypeExp Exp VName, [VName], ResRetType, Liftedness))
    -> TypeM (TypeExp Exp VName, [VName], ResRetType, Liftedness)
    -> TypeM (TypeExp Exp VName, [VName], ResRetType, Liftedness)
    forall a b. (a -> b) -> a -> b
    $ (ExpBase NoInfo VName -> TypeM Exp)
    -> TypeExp (ExpBase NoInfo VName) VName
    -> TypeM (TypeExp Exp VName, [VName], ResRetType, Liftedness)
    forall (m :: * -> *) df.
    (MonadTypeChecker m, Pretty df) =>
    (df -> m Exp)
    -> TypeExp df VName
    -> m (TypeExp Exp VName, [VName], ResRetType, Liftedness)
    checkTypeExp ExpBase NoInfo VName -> TypeM Exp
    checkSizeExp (TypeExp (ExpBase NoInfo VName) VName
     -> TypeM (TypeExp Exp VName, [VName], ResRetType, Liftedness))
    -> TypeM (TypeExp (ExpBase NoInfo VName) VName)
    -> TypeM (TypeExp Exp VName, [VName], ResRetType, Liftedness)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TypeExp (ExpBase NoInfo Name) Name
    -> TypeM (TypeExp (ExpBase NoInfo VName) VName)
    resolveTypeExp TypeExp (ExpBase NoInfo Name) Name
    te

        let (witnessed, _) = determineSizeWitnesses $ toStruct t
        case L.find (`S.notMember` witnessed) svars of
          Just VName
    _ ->
            Loc -> Notes -> Doc () -> TypeM ()
    forall loc a. Located loc => loc -> Notes -> Doc () -> TypeM a
    forall (m :: * -> *) loc a.
    (MonadTypeChecker m, Located loc) =>
    loc -> Notes -> Doc () -> m a
    typeError (TypeExp (ExpBase NoInfo Name) Name -> Loc
    forall a. Located a => a -> Loc
    locOf TypeExp (ExpBase NoInfo Name) Name
    te) Notes
    forall a. Monoid a => a
    mempty (Doc () -> TypeM ()) -> (Doc () -> Doc ()) -> Doc () -> TypeM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc () -> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann -> Doc ann
    withIndexLink Doc ()
    "anonymous-nonconstructive" (Doc () -> TypeM ()) -> Doc () -> TypeM ()
    forall a b. (a -> b) -> a -> b
    $
              Doc ()
    "Type abbreviation contains an anonymous size not used constructively as an array size."
          Maybe VName
    Nothing ->
            () -> TypeM ()
    forall a. a -> TypeM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()

        let elab_t = [VName] -> StructType -> StructRetType
    forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
    RetType ([VName]
    svars [VName] -> [VName] -> [VName]
    forall a. [a] -> [a] -> [a]
    ++ [VName]
    dims) (StructType -> StructRetType) -> StructType -> StructRetType
    forall a b. (a -> b) -> a -> b
    $ TypeBase Exp Uniqueness -> StructType
    forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
    toStruct TypeBase Exp Uniqueness
    t

        let used_dims = FV -> Set VName
    fvVars (FV -> Set VName) -> FV -> Set VName
    forall a b. (a -> b) -> a -> b
    $ TypeBase Exp Uniqueness -> FV
    forall u. TypeBase Exp u -> FV
    freeInType TypeBase Exp Uniqueness
    t
        case filter ((`S.notMember` used_dims) . typeParamName) $
          filter isSizeParam tps' of
          [] -> () -> TypeM ()
    forall a. a -> TypeM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()
          TypeParamBase VName
    tp : [TypeParamBase VName]
    _ ->
            SrcLoc -> Notes -> Doc () -> TypeM ()
    forall loc a. Located loc => loc -> Notes -> Doc () -> TypeM a
    forall (m :: * -> *) loc a.
    (MonadTypeChecker m, Located loc) =>
    loc -> Notes -> Doc () -> m a
    typeError SrcLoc
    loc Notes
    forall a. Monoid a => a
    mempty (Doc () -> TypeM ()) -> Doc () -> TypeM ()
    forall a b. (a -> b) -> a -> b
    $
              Doc ()
    "Size parameter" Doc () -> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann
    dquotes (TypeParamBase VName -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. TypeParamBase VName -> Doc ann
    pretty TypeParamBase VName
    tp) Doc () -> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> Doc ()
    "unused."

        case (l, l') of
          (Liftedness
    _, Liftedness
    Lifted)
            | Liftedness
    l Liftedness -> Liftedness -> Bool
    forall a. Ord a => a -> a -> Bool
    < Liftedness
    Lifted ->
                SrcLoc -> Notes -> Doc () -> TypeM ()
    forall loc a. Located loc => loc -> Notes -> Doc () -> TypeM a
    forall (m :: * -> *) loc a.
    (MonadTypeChecker m, Located loc) =>
    loc -> Notes -> Doc () -> m a
    typeError SrcLoc
    loc Notes
    forall a. Monoid a => a
    mempty (Doc () -> TypeM ()) -> Doc () -> TypeM ()
    forall a b. (a -> b) -> a -> b
    $
                  Doc ()
    "Non-lifted type abbreviations may not contain functions."
                    Doc () -> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann -> Doc ann
    </> Doc ()
    "Hint: consider using 'type^'."
          (Liftedness
    _, Liftedness
    SizeLifted)
            | Liftedness
    l Liftedness -> Liftedness -> Bool
    forall a. Ord a => a -> a -> Bool
    < Liftedness
    SizeLifted ->
                SrcLoc -> Notes -> Doc () -> TypeM ()
    forall loc a. Located loc => loc -> Notes -> Doc () -> TypeM a
    forall (m :: * -> *) loc a.
    (MonadTypeChecker m, Located loc) =>
    loc -> Notes -> Doc () -> m a
    typeError SrcLoc
    loc Notes
    forall a. Monoid a => a
    mempty (Doc () -> TypeM ()) -> Doc () -> TypeM ()
    forall a b. (a -> b) -> a -> b
    $
                  Doc ()
    "Non-size-lifted type abbreviations may not contain size-lifted types."
                    Doc () -> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann -> Doc ann
    </> Doc ()
    "Hint: consider using 'type~'."
          (Liftedness
    Unlifted, Liftedness
    _)
            | Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ [VName] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null ([VName] -> Bool) -> [VName] -> Bool
    forall a b. (a -> b) -> a -> b
    $ [VName]
    svars [VName] -> [VName] -> [VName]
    forall a. [a] -> [a] -> [a]
    ++ [VName]
    dims ->
                SrcLoc -> Notes -> Doc () -> TypeM ()
    forall loc a. Located loc => loc -> Notes -> Doc () -> TypeM a
    forall (m :: * -> *) loc a.
    (MonadTypeChecker m, Located loc) =>
    loc -> Notes -> Doc () -> m a
    typeError SrcLoc
    loc Notes
    forall a. Monoid a => a
    mempty (Doc () -> TypeM ()) -> Doc () -> TypeM ()
    forall a b. (a -> b) -> a -> b
    $
                  Doc ()
    "Non-lifted type abbreviations may not use existential sizes in their definition."
                    Doc () -> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann -> Doc ann
    </> Doc ()
    "Hint: use 'type~' or add size parameters to"
                    Doc () -> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann
    dquotes (Name -> Doc ()
    forall a. Name -> Doc a
    forall v a. IsName v => v -> Doc a
    prettyName Name
    name)
                    Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Doc ()
    "."
          (Liftedness, Liftedness)
    _ -> () -> TypeM ()
    forall a. a -> TypeM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()

        bindSpaced1 Type name loc $ \VName
    name' -> do
          VName -> TypeM ()
    usedName VName
    name'
          (Env, TypeBindBase Info VName)
    -> TypeM (Env, TypeBindBase Info VName)
    forall a. a -> TypeM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure
            ( Env
    forall a. Monoid a => a
    mempty
                { envTypeTable =
                    M.singleton name' $ TypeAbbr l tps' elab_t,
                  envNameMap =
                    M.singleton (Type, name) $ qualName name'
                },
              VName
    -> Liftedness
    -> [TypeParamBase VName]
    -> TypeExp Exp VName
    -> Info StructRetType
    -> Maybe DocComment
    -> SrcLoc
    -> TypeBindBase Info VName
    forall (f :: * -> *) vn.
    vn
    -> Liftedness
    -> [TypeParamBase vn]
    -> TypeExp (ExpBase f vn) vn
    -> f StructRetType
    -> Maybe DocComment
    -> SrcLoc
    -> TypeBindBase f vn
    TypeBind VName
    name' Liftedness
    l [TypeParamBase VName]
    tps' TypeExp Exp VName
    te' (StructRetType -> Info StructRetType
    forall a. a -> Info a
    Info StructRetType
    elab_t) Maybe DocComment
    doc SrcLoc
    loc
            )

    entryPoint :: [Pat ParamType] -> Maybe (TypeExp Exp VName) -> ResRetType -> EntryPoint
    entryPoint :: [Pat ParamType]
    -> Maybe (TypeExp Exp VName) -> ResRetType -> EntryPoint
    entryPoint [Pat ParamType]
    params Maybe (TypeExp Exp VName)
    orig_ret_te (RetType [VName]
    _ret TypeBase Exp Uniqueness
    orig_ret) =
      [EntryParam] -> EntryType -> EntryPoint
    EntryPoint ((Pat ParamType -> EntryParam) -> [Pat ParamType] -> [EntryParam]
    forall a b. (a -> b) -> [a] -> [b]
    map Pat ParamType -> EntryParam
    forall {u}. PatBase Info VName (TypeBase Exp u) -> EntryParam
    patternEntry [Pat ParamType]
    params [EntryParam] -> [EntryParam] -> [EntryParam]
    forall a. [a] -> [a] -> [a]
    ++ [EntryParam]
    more_params) EntryType
    rettype'
      where
        ([EntryParam]
    more_params, EntryType
    rettype') = Maybe (TypeExp Exp VName)
    -> StructType -> ([EntryParam], EntryType)
    onRetType Maybe (TypeExp Exp VName)
    orig_ret_te (StructType -> ([EntryParam], EntryType))
    -> StructType -> ([EntryParam], EntryType)
    forall a b. (a -> b) -> a -> b
    $ TypeBase Exp Uniqueness -> StructType
    forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
    toStruct TypeBase Exp Uniqueness
    orig_ret

        patternEntry :: PatBase Info VName (TypeBase Exp u) -> EntryParam
    patternEntry (PatParens PatBase Info VName (TypeBase Exp u)
    p SrcLoc
    _) =
          PatBase Info VName (TypeBase Exp u) -> EntryParam
    patternEntry PatBase Info VName (TypeBase Exp u)
    p
        patternEntry (PatAscription PatBase Info VName (TypeBase Exp u)
    p TypeExp Exp VName
    te SrcLoc
    _) =
          Name -> EntryType -> EntryParam
    EntryParam (PatBase Info VName (TypeBase Exp u) -> Name
    forall {f :: * -> *} {t}. PatBase f VName t -> Name
    patternName PatBase Info VName (TypeBase Exp u)
    p) (EntryType -> EntryParam) -> EntryType -> EntryParam
    forall a b. (a -> b) -> a -> b
    $ StructType -> Maybe (TypeExp Exp VName) -> EntryType
    EntryType (PatBase Info VName (TypeBase Exp u) -> StructType
    forall u. Pat (TypeBase Exp u) -> StructType
    patternStructType PatBase Info VName (TypeBase Exp u)
    p) (TypeExp Exp VName -> Maybe (TypeExp Exp VName)
    forall a. a -> Maybe a
    Just TypeExp Exp VName
    te)
        patternEntry PatBase Info VName (TypeBase Exp u)
    p =
          Name -> EntryType -> EntryParam
    EntryParam (PatBase Info VName (TypeBase Exp u) -> Name
    forall {f :: * -> *} {t}. PatBase f VName t -> Name
    patternName PatBase Info VName (TypeBase Exp u)
    p) (EntryType -> EntryParam) -> EntryType -> EntryParam
    forall a b. (a -> b) -> a -> b
    $ StructType -> Maybe (TypeExp Exp VName) -> EntryType
    EntryType (PatBase Info VName (TypeBase Exp u) -> StructType
    forall u. Pat (TypeBase Exp u) -> StructType
    patternStructType PatBase Info VName (TypeBase Exp u)
    p) Maybe (TypeExp Exp VName)
    forall a. Maybe a
    Nothing

        patternName :: PatBase f VName t -> Name
    patternName (Id VName
    x f t
    _ SrcLoc
    _) = VName -> Name
    baseName VName
    x
        patternName (PatParens PatBase f VName t
    p SrcLoc
    _) = PatBase f VName t -> Name
    patternName PatBase f VName t
    p
        patternName PatBase f VName t
    _ = Name
    "_"

        pname :: PName -> Name
    pname (Named VName
    v) = VName -> Name
    baseName VName
    v
        pname PName
    Unnamed = Name
    "_"
        onRetType :: Maybe (TypeExp Exp VName)
    -> StructType -> ([EntryParam], EntryType)
    onRetType (Just (TEArrow Maybe VName
    p TypeExp Exp VName
    t1_te TypeExp Exp VName
    t2_te SrcLoc
    _)) (Scalar (Arrow NoUniqueness
    _ PName
    _ Diet
    _ StructType
    t1 (RetType [VName]
    _ TypeBase Exp Uniqueness
    t2))) =
          let ([EntryParam]
    xs, EntryType
    y) = Maybe (TypeExp Exp VName)
    -> StructType -> ([EntryParam], EntryType)
    onRetType (TypeExp Exp VName -> Maybe (TypeExp Exp VName)
    forall a. a -> Maybe a
    Just TypeExp Exp VName
    t2_te) (StructType -> ([EntryParam], EntryType))
    -> StructType -> ([EntryParam], EntryType)
    forall a b. (a -> b) -> a -> b
    $ TypeBase Exp Uniqueness -> StructType
    forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
    toStruct TypeBase Exp Uniqueness
    t2
           in (Name -> EntryType -> EntryParam
    EntryParam (Name -> (VName -> Name) -> Maybe VName -> Name
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Name
    "_" VName -> Name
    baseName Maybe VName
    p) (StructType -> Maybe (TypeExp Exp VName) -> EntryType
    EntryType StructType
    t1 (TypeExp Exp VName -> Maybe (TypeExp Exp VName)
    forall a. a -> Maybe a
    Just TypeExp Exp VName
    t1_te)) EntryParam -> [EntryParam] -> [EntryParam]
    forall a. a -> [a] -> [a]
    : [EntryParam]
    xs, EntryType
    y)
        onRetType Maybe (TypeExp Exp VName)
    _ (Scalar (Arrow NoUniqueness
    _ PName
    p Diet
    _ StructType
    t1 (RetType [VName]
    _ TypeBase Exp Uniqueness
    t2))) =
          let ([EntryParam]
    xs, EntryType
    y) = Maybe (TypeExp Exp VName)
    -> StructType -> ([EntryParam], EntryType)
    onRetType Maybe (TypeExp Exp VName)
    forall a. Maybe a
    Nothing (StructType -> ([EntryParam], EntryType))
    -> StructType -> ([EntryParam], EntryType)
    forall a b. (a -> b) -> a -> b
    $ TypeBase Exp Uniqueness -> StructType
    forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
    toStruct TypeBase Exp Uniqueness
    t2
           in (Name -> EntryType -> EntryParam
    EntryParam (PName -> Name
    pname PName
    p) (StructType -> Maybe (TypeExp Exp VName) -> EntryType
    EntryType StructType
    t1 Maybe (TypeExp Exp VName)
    forall a. Maybe a
    Nothing) EntryParam -> [EntryParam] -> [EntryParam]
    forall a. a -> [a] -> [a]
    : [EntryParam]
    xs, EntryType
    y)
        onRetType Maybe (TypeExp Exp VName)
    te StructType
    t =
          ([], StructType -> Maybe (TypeExp Exp VName) -> EntryType
    EntryType StructType
    t Maybe (TypeExp Exp VName)
    te)

    checkEntryPoint ::
      SrcLoc ->
      [TypeParam] ->
      [Pat ParamType] ->
      ResRetType ->
      TypeM ()
    checkEntryPoint :: SrcLoc
    -> [TypeParamBase VName]
    -> [Pat ParamType]
    -> ResRetType
    -> TypeM ()
    checkEntryPoint SrcLoc
    loc [TypeParamBase VName]
    tparams [Pat ParamType]
    params ResRetType
    rettype
      | (TypeParamBase VName -> Bool) -> [TypeParamBase VName] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any TypeParamBase VName -> Bool
    forall vn. TypeParamBase vn -> Bool
    isTypeParam [TypeParamBase VName]
    tparams =
          SrcLoc -> Notes -> Doc () -> TypeM ()
    forall loc a. Located loc => loc -> Notes -> Doc () -> TypeM a
    forall (m :: * -> *) loc a.
    (MonadTypeChecker m, Located loc) =>
    loc -> Notes -> Doc () -> m a
    typeError SrcLoc
    loc Notes
    forall a. Monoid a => a
    mempty (Doc () -> TypeM ()) -> Doc () -> TypeM ()
    forall a b. (a -> b) -> a -> b
    $
            Doc () -> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann -> Doc ann
    withIndexLink
              Doc ()
    "polymorphic-entry"
              Doc ()
    "Entry point functions may not be polymorphic."
      | Bool -> Bool
    not ((ParamType -> Bool) -> [ParamType] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all ParamType -> Bool
    forall dim as. TypeBase dim as -> Bool
    orderZero [ParamType]
    param_ts)
          Bool -> Bool -> Bool
    || Bool -> Bool
    not (StructType -> Bool
    forall dim as. TypeBase dim as -> Bool
    orderZero StructType
    rettype') =
          SrcLoc -> Notes -> Doc () -> TypeM ()
    forall loc a. Located loc => loc -> Notes -> Doc () -> TypeM a
    forall (m :: * -> *) loc a.
    (MonadTypeChecker m, Located loc) =>
    loc -> Notes -> Doc () -> m a
    typeError SrcLoc
    loc Notes
    forall a. Monoid a => a
    mempty (Doc () -> TypeM ()) -> Doc () -> TypeM ()
    forall a b. (a -> b) -> a -> b
    $
            Doc () -> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann -> Doc ann
    withIndexLink
              Doc ()
    "higher-order-entry"
              Doc ()
    "Entry point functions may not be higher-order."
      | Set VName
    sizes_only_in_ret <-
          [VName] -> Set VName
    forall a. Ord a => [a] -> Set a
    S.fromList ((TypeParamBase VName -> VName) -> [TypeParamBase VName] -> [VName]
    forall a b. (a -> b) -> [a] -> [b]
    map TypeParamBase VName -> VName
    forall vn. TypeParamBase vn -> vn
    typeParamName [TypeParamBase VName]
    tparams)
            Set VName -> Set VName -> Set VName
    forall a. Ord a => Set a -> Set a -> Set a
    `S.intersection` FV -> Set VName
    fvVars (StructType -> FV
    forall u. TypeBase Exp u -> FV
    freeInType StructType
    rettype')
            Set VName -> Set VName -> Set VName
    forall a. Ord a => Set a -> Set a -> Set a
    `S.difference` (ParamType -> Set VName) -> [ParamType] -> Set VName
    forall m a. Monoid m => (a -> m) -> [a] -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap (FV -> Set VName
    fvVars (FV -> Set VName) -> (ParamType -> FV) -> ParamType -> Set VName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ParamType -> FV
    forall u. TypeBase Exp u -> FV
    freeInType) [ParamType]
    param_ts,
        Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ Set VName -> Bool
    forall a. Set a -> Bool
    S.null Set VName
    sizes_only_in_ret =
          SrcLoc -> Notes -> Doc () -> TypeM ()
    forall loc a. Located loc => loc -> Notes -> Doc () -> TypeM a
    forall (m :: * -> *) loc a.
    (MonadTypeChecker m, Located loc) =>
    loc -> Notes -> Doc () -> m a
    typeError SrcLoc
    loc Notes
    forall a. Monoid a => a
    mempty (Doc () -> TypeM ()) -> Doc () -> TypeM ()
    forall a b. (a -> b) -> a -> b
    $
            Doc () -> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann -> Doc ann
    withIndexLink
              Doc ()
    "size-polymorphic-entry"
              Doc ()
    "Entry point functions must not be size-polymorphic in their return type."
      | (Set VName
    constructive, Set VName
    _) <- (ParamType -> (Set VName, Set VName))
    -> [ParamType] -> (Set VName, Set VName)
    forall m a. Monoid m => (a -> m) -> [a] -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap (StructType -> (Set VName, Set VName)
    determineSizeWitnesses (StructType -> (Set VName, Set VName))
    -> (ParamType -> StructType) -> ParamType -> (Set VName, Set VName)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ParamType -> StructType
    forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
    toStruct) [ParamType]
    param_ts,
        Just TypeParamBase VName
    p <- (TypeParamBase VName -> Bool)
    -> [TypeParamBase VName] -> Maybe (TypeParamBase VName)
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
    L.find ((VName -> Set VName -> Bool) -> Set VName -> VName -> Bool
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip VName -> Set VName -> Bool
    forall a. Ord a => a -> Set a -> Bool
    S.notMember Set VName
    constructive (VName -> Bool)
    -> (TypeParamBase VName -> VName) -> TypeParamBase VName -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TypeParamBase VName -> VName
    forall vn. TypeParamBase vn -> vn
    typeParamName) [TypeParamBase VName]
    tparams =
          TypeParamBase VName -> Notes -> Doc () -> TypeM ()
    forall loc a. Located loc => loc -> Notes -> Doc () -> TypeM a
    forall (m :: * -> *) loc a.
    (MonadTypeChecker m, Located loc) =>
    loc -> Notes -> Doc () -> m a
    typeError TypeParamBase VName
    p Notes
    forall a. Monoid a => a
    mempty (Doc () -> TypeM ()) -> (Doc () -> Doc ()) -> Doc () -> TypeM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc () -> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann -> Doc ann
    withIndexLink Doc ()
    "nonconstructive-entry" (Doc () -> TypeM ()) -> Doc () -> TypeM ()
    forall a b. (a -> b) -> a -> b
    $
            Doc ()
    "Entry point size parameter "
              Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> TypeParamBase VName -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. TypeParamBase VName -> Doc ann
    pretty TypeParamBase VName
    p
              Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Doc ()
    " only used non-constructively."
      | Bool
    otherwise =
          () -> TypeM ()
    forall a. a -> TypeM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()
      where
        (RetType [VName]
    _ TypeBase Exp Uniqueness
    rettype_t) = ResRetType
    rettype
        ([ParamType]
    rettype_params, StructType
    rettype') = TypeBase Exp Uniqueness -> ([ParamType], StructType)
    forall dim as.
    TypeBase dim as -> ([TypeBase dim Diet], TypeBase dim NoUniqueness)
    unfoldFunType TypeBase Exp Uniqueness
    rettype_t
        param_ts :: [ParamType]
    param_ts = (Pat ParamType -> ParamType) -> [Pat ParamType] -> [ParamType]
    forall a b. (a -> b) -> [a] -> [b]
    map Pat ParamType -> ParamType
    forall d u. Pat (TypeBase d u) -> TypeBase d u
    patternType [Pat ParamType]
    params [ParamType] -> [ParamType] -> [ParamType]
    forall a. [a] -> [a] -> [a]
    ++ [ParamType]
    rettype_params

    checkValBind :: ValBindBase NoInfo Name -> TypeM (Env, ValBind)
    checkValBind :: ValBindBase NoInfo Name -> TypeM (Env, ValBind)
    checkValBind ValBindBase NoInfo Name
    vb = do
      (ValBind entry fname maybe_tdecl NoInfo tparams params body doc attrs loc) <-
        ValBindBase NoInfo Name -> TypeM (ValBindBase NoInfo VName)
    resolveValBind ValBindBase NoInfo Name
    vb

      top_level <- atTopLevel
      when (not top_level && isJust entry) $
        typeError loc mempty $
          withIndexLink "nested-entry" "Entry points may not be declared inside modules."

      attrs' <- mapM checkAttr attrs

      (tparams', params', maybe_tdecl', rettype, body') <-
        checkFunDef (fname, maybe_tdecl, tparams, params, body, loc)

      let entry' = EntryPoint -> Info EntryPoint
    forall a. a -> Info a
    Info ([Pat ParamType]
    -> Maybe (TypeExp Exp VName) -> ResRetType -> EntryPoint
    entryPoint [Pat ParamType]
    params' Maybe (TypeExp Exp VName)
    maybe_tdecl' ResRetType
    rettype) Info EntryPoint
    -> Maybe (NoInfo EntryPoint) -> Maybe (Info EntryPoint)
    forall a b. a -> Maybe b -> Maybe a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Maybe (NoInfo EntryPoint)
    entry
      case entry' of
        Just Info EntryPoint
    _ -> SrcLoc
    -> [TypeParamBase VName]
    -> [Pat ParamType]
    -> ResRetType
    -> TypeM ()
    checkEntryPoint SrcLoc
    loc [TypeParamBase VName]
    tparams' [Pat ParamType]
    params' ResRetType
    rettype
        Maybe (Info EntryPoint)
    _ -> () -> TypeM ()
    forall a. a -> TypeM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()

      let vb' = Maybe (Info EntryPoint)
    -> VName
    -> Maybe (TypeExp Exp VName)
    -> Info ResRetType
    -> [TypeParamBase VName]
    -> [Pat ParamType]
    -> Exp
    -> Maybe DocComment
    -> [AttrInfo VName]
    -> SrcLoc
    -> ValBind
    forall (f :: * -> *) vn.
    Maybe (f EntryPoint)
    -> vn
    -> Maybe (TypeExp (ExpBase f vn) vn)
    -> f ResRetType
    -> [TypeParamBase vn]
    -> [PatBase f vn ParamType]
    -> ExpBase f vn
    -> Maybe DocComment
    -> [AttrInfo vn]
    -> SrcLoc
    -> ValBindBase f vn
    ValBind Maybe (Info EntryPoint)
    entry' VName
    fname Maybe (TypeExp Exp VName)
    maybe_tdecl' (ResRetType -> Info ResRetType
    forall a. a -> Info a
    Info ResRetType
    rettype) [TypeParamBase VName]
    tparams' [Pat ParamType]
    params' Exp
    body' Maybe DocComment
    doc [AttrInfo VName]
    attrs' SrcLoc
    loc
      pure
        ( mempty
            { envVtable =
                M.singleton fname $ uncurry BoundV $ valBindTypeScheme vb',
              envNameMap =
                M.singleton (Term, baseName fname) $ qualName fname
            },
          vb'
        )

    checkOneDec :: DecBase NoInfo Name -> TypeM (TySet, Env, DecBase Info VName)
    checkOneDec :: UncheckedDec -> TypeM (TySet, Env, Dec)
    checkOneDec (ModDec ModBindBase NoInfo Name
    struct) = do
      (abs, modenv, struct') <- ModBindBase NoInfo Name
    -> TypeM (TySet, Env, ModBindBase Info VName)
    checkModBind ModBindBase NoInfo Name
    struct
      pure (abs, modenv, ModDec struct')
    checkOneDec (ModTypeDec ModTypeBindBase NoInfo Name
    sig) = do
      (abs, sigenv, sig') <- ModTypeBindBase NoInfo Name
    -> TypeM (TySet, Env, ModTypeBindBase Info VName)
    checkModTypeBind ModTypeBindBase NoInfo Name
    sig
      pure (abs, sigenv, ModTypeDec sig')
    checkOneDec (TypeDec TypeBindBase NoInfo Name
    tdec) = do
      (tenv, tdec') <- TypeBindBase NoInfo Name -> TypeM (Env, TypeBindBase Info VName)
    checkTypeBind TypeBindBase NoInfo Name
    tdec
      pure (mempty, tenv, TypeDec tdec')
    checkOneDec (OpenDec ModExpBase NoInfo Name
    x SrcLoc
    loc) = do
      (x_abs, x_env, x') <- ModExpBase NoInfo Name -> TypeM (TySet, Env, ModExpBase Info VName)
    checkOneModExpToEnv ModExpBase NoInfo Name
    x
      pure (x_abs, x_env, OpenDec x' loc)
    checkOneDec (LocalDec UncheckedDec
    d SrcLoc
    loc) = do
      (abstypes, env, d') <- UncheckedDec -> TypeM (TySet, Env, Dec)
    checkOneDec UncheckedDec
    d
      pure (abstypes, env, LocalDec d' loc)
    checkOneDec (ImportDec FilePath
    name NoInfo ImportName
    NoInfo SrcLoc
    loc) = do
      (name', env) <- SrcLoc -> FilePath -> TypeM (ImportName, Env)
    lookupImport SrcLoc
    loc FilePath
    name
      when (isBuiltin name) $
        typeError loc mempty $
          pretty name <+> "may not be explicitly imported."
      pure (mempty, env, ImportDec name (Info name') loc)
    checkOneDec (ValDec ValBindBase NoInfo Name
    vb) = do
      (env, vb') <- ValBindBase NoInfo Name -> TypeM (Env, ValBind)
    checkValBind ValBindBase NoInfo Name
    vb
      pure (mempty, env, ValDec vb')

    checkDecs :: [DecBase NoInfo Name] -> TypeM (TySet, Env, [DecBase Info VName], Env)
    checkDecs :: [UncheckedDec] -> TypeM (TySet, Env, [Dec], Env)
    checkDecs (UncheckedDec
    d : [UncheckedDec]
    ds) = do
      (d_abstypes, d_env, d') <- UncheckedDec -> TypeM (TySet, Env, Dec)
    checkOneDec UncheckedDec
    d
      (ds_abstypes, ds_env, ds', full_env) <- localEnv d_env $ checkDecs ds
      pure
        ( d_abstypes <> ds_abstypes,
          case d' of
            LocalDec {} -> Env
    ds_env
            ImportDec {} -> Env
    ds_env
            Dec
    _ -> Env
    ds_env Env -> Env -> Env
    forall a. Semigroup a => a -> a -> a
    <> Env
    d_env,
          d' : ds',
          full_env
        )
    checkDecs [] = do
      full_env <- TypeM Env
    askEnv
      pure (mempty, mempty, [], full_env)