-- | 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)