-- | 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 Control.Monad.Except
import Data.Bifunctor (first, second)
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.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 =
  forall a.
Env
-> ImportTable
-> ImportName
-> VNameSource
-> TypeM a
-> (Warnings, Either TypeError (a, VNameSource))
runTypeM Env
initialEnv ImportTable
files' ImportName
name VNameSource
src forall a b. (a -> b) -> a -> b
$ UncheckedProg -> TypeM FileModule
checkProgM UncheckedProg
prog
  where
    files' :: ImportTable
files' = forall a b k. (a -> b) -> Map k a -> Map k b
M.map FileModule -> Env
fileEnv forall a b. (a -> b) -> a -> b
$ 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
-> UncheckedExp
-> (Warnings, Either TypeError ([TypeParamBase VName], Exp))
checkExp Imports
files VNameSource
src Env
env UncheckedExp
e =
  forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst) forall a b. (a -> b) -> a -> b
$ forall a.
Env
-> ImportTable
-> ImportName
-> VNameSource
-> TypeM a
-> (Warnings, Either TypeError (a, VNameSource))
runTypeM Env
env ImportTable
files' (FilePath -> ImportName
mkInitialImport FilePath
"") VNameSource
src forall a b. (a -> b) -> a -> b
$ UncheckedExp -> TypeM ([TypeParamBase VName], Exp)
checkOneExp UncheckedExp
e
  where
    files' :: ImportTable
files' = forall a b k. (a -> b) -> Map k a -> Map k b
M.map FileModule -> Env
fileEnv forall a b. (a -> b) -> a -> b
$ 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 =
  forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {a} {b} {c}. ((a, b), c) -> (a, b, c)
massage) forall a b. (a -> b) -> a -> b
$
    forall a.
Env
-> ImportTable
-> ImportName
-> VNameSource
-> TypeM a
-> (Warnings, Either TypeError (a, VNameSource))
runTypeM Env
env ImportTable
files' ImportName
name VNameSource
src forall a b. (a -> b) -> a -> b
$ do
      (TySet
_, Env
env', Dec
d') <- UncheckedDec -> TypeM (TySet, Env, Dec)
checkOneDec UncheckedDec
d
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (Env
env' forall a. Semigroup a => a -> a -> a
<> Env
env, Dec
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' = forall a b k. (a -> b) -> Map k a -> Map k b
M.map FileModule -> Env
fileEnv forall a b. (a -> b) -> a -> b
$ 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 =
  forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
Env
-> ImportTable
-> ImportName
-> VNameSource
-> TypeM a
-> (Warnings, Either TypeError (a, VNameSource))
runTypeM Env
env ImportTable
files' (FilePath -> ImportName
mkInitialImport FilePath
"") VNameSource
src forall a b. (a -> b) -> a -> b
$ do
    (TySet
_abs, MTy
mty, ModExpBase Info VName
me') <- ModExpBase NoInfo Name -> TypeM (TySet, MTy, ModExpBase Info VName)
checkOneModExp ModExpBase NoInfo Name
me
    forall (f :: * -> *) a. Applicative f => a -> f a
pure (MTy
mty, ModExpBase Info VName
me')
  where
    files' :: ImportTable
files' = forall a b k. (a -> b) -> Map k a -> Map k b
M.map FileModule -> Env
fileEnv forall a b. (a -> b) -> a -> b
$ 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 :: Map VName Mod
envModTable = Map VName Mod
initialModTable,
      envNameMap :: NameMap
envNameMap =
        forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert
          (Namespace
Term, FilePath -> Name
nameFromString FilePath
"intrinsics")
          (forall v. v -> QualName v
qualName VName
intrinsics_v)
          NameMap
topLevelNameMap
    }
  where
    initialTypeTable :: Map VName TypeBinding
initialTypeTable = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe forall {a}. (a, Intrinsic) -> Maybe (a, TypeBinding)
addIntrinsicT forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
M.toList Map VName Intrinsic
intrinsics
    initialModTable :: Map VName Mod
initialModTable = 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
-> NameMap
-> Env
Env forall a. Monoid a => a
mempty Map VName TypeBinding
initialTypeTable forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty NameMap
intrinsicsNameMap

    addIntrinsicT :: (a, Intrinsic) -> Maybe (a, TypeBinding)
addIntrinsicT (a
name, IntrinsicType Liftedness
l [TypeParamBase VName]
ps StructType
t) =
      forall a. a -> Maybe a
Just (a
name, Liftedness -> [TypeParamBase VName] -> StructRetType -> TypeBinding
TypeAbbr Liftedness
l [TypeParamBase VName]
ps forall a b. (a -> b) -> a -> b
$ forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [] StructType
t)
    addIntrinsicT (a, Intrinsic)
_ =
      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 =
  forall a. Monoid a => [a] -> a
mconcat (forall a b. (a -> b) -> [a] -> [b]
map (FileModule -> Env
fileEnv forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) (forall a. [a] -> [a]
reverse Imports
imports)) 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
  (TySet
abs, Env
env, [Dec]
decs', Env
full_env) <- [UncheckedDec] -> TypeM (TySet, Env, [Dec], Env)
checkDecs [UncheckedDec]
decs
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (TySet -> Env -> Prog -> Env -> FileModule
FileModule TySet
abs Env
env (forall (f :: * -> *) vn.
Maybe DocComment -> [DecBase f vn] -> ProgBase f vn
Prog Maybe DocComment
doc [Dec]
decs') Env
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 =
  forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc1 forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
    Doc ()
"Duplicate definition of"
      forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty Namespace
space
      forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall v a. IsName v => v -> Doc a
prettyName Name
name forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
      forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"Previously defined at"
      forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall a. Located a => a -> FilePath
locStr SrcLoc
loc2) forall a. Semigroup a => a -> a -> a
<> Doc ()
"."

checkForDuplicateDecs :: [DecBase NoInfo Name] -> TypeM ()
checkForDuplicateDecs :: [UncheckedDec] -> TypeM ()
checkForDuplicateDecs =
  forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m ()
foldM_ (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall {m :: * -> *} {f :: * -> *}.
MonadTypeChecker m =>
DecBase f Name
-> Map (Namespace, Name) SrcLoc -> m (Map (Namespace, Name) SrcLoc)
f) 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 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' ->
          forall (m :: * -> *) a.
MonadTypeChecker m =>
Namespace -> Name -> SrcLoc -> SrcLoc -> m a
dupDefinitionError Namespace
namespace Name
name SrcLoc
loc SrcLoc
loc'
        Maybe SrcLoc
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ 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) =
      forall {m :: * -> *}.
MonadTypeChecker m =>
Namespace
-> Name
-> SrcLoc
-> Map (Namespace, Name) SrcLoc
-> m (Map (Namespace, Name) SrcLoc)
check Namespace
Term (forall (f :: * -> *) vn. ValBindBase f vn -> vn
valBindName ValBindBase f Name
vb) (forall a. Located a => a -> SrcLoc
srclocOf ValBindBase f Name
vb)
    f (TypeDec (TypeBind Name
name Liftedness
_ [TypeParamBase Name]
_ TypeExp f Name
_ f StructRetType
_ Maybe DocComment
_ SrcLoc
loc)) =
      forall {m :: * -> *}.
MonadTypeChecker m =>
Namespace
-> Name
-> SrcLoc
-> Map (Namespace, Name) SrcLoc
-> m (Map (Namespace, Name) SrcLoc)
check Namespace
Type Name
name SrcLoc
loc
    f (SigDec (SigBind Name
name SigExpBase f Name
_ Maybe DocComment
_ SrcLoc
loc)) =
      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 (SigExpBase f Name, f (Map VName VName))
_ ModExpBase f Name
_ Maybe DocComment
_ SrcLoc
loc)) =
      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 {} = forall (f :: * -> *) a. Applicative f => a -> f a
pure
    f LocalDec {} = forall (f :: * -> *) a. Applicative f => a -> f a
pure
    f ImportDec {} = 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 = forall a. Env -> TypeM a -> TypeM a
localEnv Env
env
  where
    env :: Env
env = forall a. Monoid a => [a] -> a
mconcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map TypeParamBase VName -> Env
typeParamEnv [TypeParamBase VName]
tparams

    typeParamEnv :: TypeParamBase VName -> Env
typeParamEnv (TypeParamDim VName
v SrcLoc
_) =
      forall a. Monoid a => a
mempty
        { envVtable :: Map VName BoundV
envVtable =
            forall k a. k -> a -> Map k a
M.singleton VName
v forall a b. (a -> b) -> a -> b
$ [TypeParamBase VName] -> StructType -> BoundV
BoundV [] (forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as. PrimType -> ScalarTypeBase dim as
Prim forall a b. (a -> b) -> a -> b
$ IntType -> PrimType
Signed IntType
Int64)
        }
    typeParamEnv (TypeParamType Liftedness
l VName
v SrcLoc
_) =
      forall a. Monoid a => a
mempty
        { envTypeTable :: Map VName TypeBinding
envTypeTable =
            forall k a. k -> a -> Map k a
M.singleton VName
v forall a b. (a -> b) -> a -> b
$
              Liftedness -> [TypeParamBase VName] -> StructRetType -> TypeBinding
TypeAbbr Liftedness
l [] forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [] forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$
                forall dim as.
as
-> Uniqueness
-> QualName VName
-> [TypeArg dim]
-> ScalarTypeBase dim as
TypeVar () Uniqueness
Nonunique (forall v. v -> QualName v
qualName VName
v) []
        }

checkTypeDecl ::
  UncheckedTypeExp ->
  TypeM ([VName], TypeExp Info VName, StructType, Liftedness)
checkTypeDecl :: TypeExp NoInfo Name
-> TypeM ([VName], TypeExp Info VName, StructType, Liftedness)
checkTypeDecl TypeExp NoInfo Name
te = do
  (TypeExp Info VName
te', [VName]
svars, RetType [VName]
dims StructType
st, Liftedness
l) <- forall (m :: * -> *).
MonadTypeChecker m =>
TypeExp NoInfo Name
-> m (TypeExp Info VName, [VName], StructRetType, Liftedness)
checkTypeExp TypeExp NoInfo Name
te
  forall (f :: * -> *) a. Applicative f => a -> f a
pure ([VName]
svars forall a. [a] -> [a] -> [a]
++ [VName]
dims, TypeExp Info VName
te', StructType
st, Liftedness
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 [] = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Monoid a => a
mempty, forall a. Monoid a => a
mempty, [])
checkSpecs (ValSpec Name
name [TypeParamBase Name]
tparams TypeExp NoInfo Name
vtype NoInfo StructType
NoInfo Maybe DocComment
doc SrcLoc
loc : [SpecBase NoInfo Name]
specs) =
  forall (m :: * -> *) a.
MonadTypeChecker m =>
[(Namespace, Name)] -> m a -> m a
bindSpaced [(Namespace
Term, Name
name)] forall a b. (a -> b) -> a -> b
$ do
    VName
name' <- forall (m :: * -> *).
MonadTypeChecker m =>
Namespace -> Name -> SrcLoc -> m VName
checkName Namespace
Term Name
name SrcLoc
loc
    ([TypeParamBase VName]
tparams', TypeExp Info VName
vtype', StructType
vtype_t) <-
      forall (m :: * -> *) a.
MonadTypeChecker m =>
[TypeParamBase Name] -> ([TypeParamBase VName] -> m a) -> m a
checkTypeParams [TypeParamBase Name]
tparams forall a b. (a -> b) -> a -> b
$ \[TypeParamBase VName]
tparams' -> forall a. [TypeParamBase VName] -> TypeM a -> TypeM a
bindingTypeParams [TypeParamBase VName]
tparams' forall a b. (a -> b) -> a -> b
$ do
        ([VName]
ext, TypeExp Info VName
vtype', StructType
vtype_t, Liftedness
_) <- TypeExp NoInfo Name
-> TypeM ([VName], TypeExp Info VName, StructType, Liftedness)
checkTypeDecl TypeExp NoInfo Name
vtype

        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [VName]
ext) forall a b. (a -> b) -> a -> b
$
          forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
            Doc ()
"All function parameters must have non-anonymous sizes."
              forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"Hint: add size parameters to"
              forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName VName
name') forall a. Semigroup a => a -> a -> a
<> Doc ()
"."

        forall (f :: * -> *) a. Applicative f => a -> f a
pure ([TypeParamBase VName]
tparams', TypeExp Info VName
vtype', StructType
vtype_t)

    let binding :: BoundV
binding = [TypeParamBase VName] -> StructType -> BoundV
BoundV [TypeParamBase VName]
tparams' StructType
vtype_t
        valenv :: Env
valenv =
          forall a. Monoid a => a
mempty
            { envVtable :: Map VName BoundV
envVtable = forall k a. k -> a -> Map k a
M.singleton VName
name' BoundV
binding,
              envNameMap :: NameMap
envNameMap = forall k a. k -> a -> Map k a
M.singleton (Namespace
Term, Name
name) forall a b. (a -> b) -> a -> b
$ forall v. v -> QualName v
qualName VName
name'
            }
    (TySet
abstypes, Env
env, [SpecBase Info VName]
specs') <- forall a. Env -> TypeM a -> TypeM a
localEnv Env
valenv forall a b. (a -> b) -> a -> b
$ [SpecBase NoInfo Name] -> TypeM (TySet, Env, [SpecBase Info VName])
checkSpecs [SpecBase NoInfo Name]
specs
    forall (f :: * -> *) a. Applicative f => a -> f a
pure
      ( TySet
abstypes,
        Env
env forall a. Semigroup a => a -> a -> a
<> Env
valenv,
        forall (f :: * -> *) vn.
vn
-> [TypeParamBase vn]
-> TypeExp f vn
-> f StructType
-> Maybe DocComment
-> SrcLoc
-> SpecBase f vn
ValSpec VName
name' [TypeParamBase VName]
tparams' TypeExp Info VName
vtype' (forall a. a -> Info a
Info StructType
vtype_t) Maybe DocComment
doc SrcLoc
loc forall a. a -> [a] -> [a]
: [SpecBase Info VName]
specs'
      )
checkSpecs (TypeAbbrSpec TypeBindBase NoInfo Name
tdec : [SpecBase NoInfo Name]
specs) =
  forall (m :: * -> *) a.
MonadTypeChecker m =>
[(Namespace, Name)] -> m a -> m a
bindSpaced [(Namespace
Type, forall (f :: * -> *) vn. TypeBindBase f vn -> vn
typeAlias TypeBindBase NoInfo Name
tdec)] forall a b. (a -> b) -> a -> b
$ do
    (Env
tenv, TypeBindBase Info VName
tdec') <- TypeBindBase NoInfo Name -> TypeM (Env, TypeBindBase Info VName)
checkTypeBind TypeBindBase NoInfo Name
tdec
    (TySet
abstypes, Env
env, [SpecBase Info VName]
specs') <- forall a. Env -> TypeM a -> TypeM a
localEnv Env
tenv forall a b. (a -> b) -> a -> b
$ [SpecBase NoInfo Name] -> TypeM (TySet, Env, [SpecBase Info VName])
checkSpecs [SpecBase NoInfo Name]
specs
    forall (f :: * -> *) a. Applicative f => a -> f a
pure
      ( TySet
abstypes,
        Env
env forall a. Semigroup a => a -> a -> a
<> Env
tenv,
        forall (f :: * -> *) vn. TypeBindBase f vn -> SpecBase f vn
TypeAbbrSpec TypeBindBase Info VName
tdec' forall a. a -> [a] -> [a]
: [SpecBase Info VName]
specs'
      )
checkSpecs (TypeSpec Liftedness
l Name
name [TypeParamBase Name]
ps Maybe DocComment
doc SrcLoc
loc : [SpecBase NoInfo Name]
specs) =
  forall (m :: * -> *) a.
MonadTypeChecker m =>
[TypeParamBase Name] -> ([TypeParamBase VName] -> m a) -> m a
checkTypeParams [TypeParamBase Name]
ps forall a b. (a -> b) -> a -> b
$ \[TypeParamBase VName]
ps' ->
    forall (m :: * -> *) a.
MonadTypeChecker m =>
[(Namespace, Name)] -> m a -> m a
bindSpaced [(Namespace
Type, Name
name)] forall a b. (a -> b) -> a -> b
$ do
      VName
name' <- forall (m :: * -> *).
MonadTypeChecker m =>
Namespace -> Name -> SrcLoc -> m VName
checkName Namespace
Type Name
name SrcLoc
loc
      let tenv :: Env
tenv =
            forall a. Monoid a => a
mempty
              { envNameMap :: NameMap
envNameMap =
                  forall k a. k -> a -> Map k a
M.singleton (Namespace
Type, Name
name) forall a b. (a -> b) -> a -> b
$ forall v. v -> QualName v
qualName VName
name',
                envTypeTable :: Map VName TypeBinding
envTypeTable =
                  forall k a. k -> a -> Map k a
M.singleton VName
name' forall a b. (a -> b) -> a -> b
$
                    Liftedness -> [TypeParamBase VName] -> StructRetType -> TypeBinding
TypeAbbr Liftedness
l [TypeParamBase VName]
ps' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [] forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$
                      forall dim as.
as
-> Uniqueness
-> QualName VName
-> [TypeArg dim]
-> ScalarTypeBase dim as
TypeVar () Uniqueness
Nonunique (forall v. v -> QualName v
qualName VName
name') forall a b. (a -> b) -> a -> b
$
                        forall a b. (a -> b) -> [a] -> [b]
map TypeParamBase VName -> StructTypeArg
typeParamToArg [TypeParamBase VName]
ps'
              }
      (TySet
abstypes, Env
env, [SpecBase Info VName]
specs') <- forall a. Env -> TypeM a -> TypeM a
localEnv Env
tenv forall a b. (a -> b) -> a -> b
$ [SpecBase NoInfo Name] -> TypeM (TySet, Env, [SpecBase Info VName])
checkSpecs [SpecBase NoInfo Name]
specs
      forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (forall v. v -> QualName v
qualName VName
name') Liftedness
l TySet
abstypes,
          Env
env forall a. Semigroup a => a -> a -> a
<> Env
tenv,
          forall (f :: * -> *) vn.
Liftedness
-> vn
-> [TypeParamBase vn]
-> Maybe DocComment
-> SrcLoc
-> SpecBase f vn
TypeSpec Liftedness
l VName
name' [TypeParamBase VName]
ps' Maybe DocComment
doc SrcLoc
loc forall a. a -> [a] -> [a]
: [SpecBase Info VName]
specs'
        )
checkSpecs (ModSpec Name
name SigExpBase NoInfo Name
sig Maybe DocComment
doc SrcLoc
loc : [SpecBase NoInfo Name]
specs) =
  forall (m :: * -> *) a.
MonadTypeChecker m =>
[(Namespace, Name)] -> m a -> m a
bindSpaced [(Namespace
Term, Name
name)] forall a b. (a -> b) -> a -> b
$ do
    VName
name' <- forall (m :: * -> *).
MonadTypeChecker m =>
Namespace -> Name -> SrcLoc -> m VName
checkName Namespace
Term Name
name SrcLoc
loc
    (TySet
_sig_abs, MTy
mty, SigExpBase Info VName
sig') <- SigExpBase NoInfo Name -> TypeM (TySet, MTy, SigExpBase Info VName)
checkSigExp SigExpBase NoInfo Name
sig
    let senv :: Env
senv =
          forall a. Monoid a => a
mempty
            { envNameMap :: NameMap
envNameMap = forall k a. k -> a -> Map k a
M.singleton (Namespace
Term, Name
name) forall a b. (a -> b) -> a -> b
$ forall v. v -> QualName v
qualName VName
name',
              envModTable :: Map VName Mod
envModTable = forall k a. k -> a -> Map k a
M.singleton VName
name' forall a b. (a -> b) -> a -> b
$ MTy -> Mod
mtyMod MTy
mty
            }
    (TySet
abstypes, Env
env, [SpecBase Info VName]
specs') <- forall a. Env -> TypeM a -> TypeM a
localEnv Env
senv forall a b. (a -> b) -> a -> b
$ [SpecBase NoInfo Name] -> TypeM (TySet, Env, [SpecBase Info VName])
checkSpecs [SpecBase NoInfo Name]
specs
    forall (f :: * -> *) a. Applicative f => a -> f a
pure
      ( forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
M.mapKeys (forall v. v -> QualName v -> QualName v
qualify VName
name') (MTy -> TySet
mtyAbs MTy
mty) forall a. Semigroup a => a -> a -> a
<> TySet
abstypes,
        Env
env forall a. Semigroup a => a -> a -> a
<> Env
senv,
        forall (f :: * -> *) vn.
vn
-> SigExpBase f vn -> Maybe DocComment -> SrcLoc -> SpecBase f vn
ModSpec VName
name' SigExpBase Info VName
sig' Maybe DocComment
doc SrcLoc
loc forall a. a -> [a] -> [a]
: [SpecBase Info VName]
specs'
      )
checkSpecs (IncludeSpec SigExpBase NoInfo Name
e SrcLoc
loc : [SpecBase NoInfo Name]
specs) = do
  (TySet
e_abs, TySet
env_abs, Env
e_env, SigExpBase Info VName
e') <- SigExpBase NoInfo Name
-> TypeM (TySet, TySet, Env, SigExpBase Info VName)
checkSigExpToEnv SigExpBase NoInfo Name
e

  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall {e} {m :: * -> *}.
(MonadError e m, MonadTypeChecker m) =>
QualName Name -> m ()
warnIfShadowing forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap VName -> Name
baseName) forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [k]
M.keys TySet
env_abs

  (TySet
abstypes, Env
env, [SpecBase Info VName]
specs') <- forall a. Env -> TypeM a -> TypeM a
localEnv Env
e_env forall a b. (a -> b) -> a -> b
$ [SpecBase NoInfo Name] -> TypeM (TySet, Env, [SpecBase Info VName])
checkSpecs [SpecBase NoInfo Name]
specs
  forall (f :: * -> *) a. Applicative f => a -> f a
pure
    ( TySet
e_abs forall a. Semigroup a => a -> a -> a
<> TySet
env_abs forall a. Semigroup a => a -> a -> a
<> TySet
abstypes,
      Env
env forall a. Semigroup a => a -> a -> a
<> Env
e_env,
      forall (f :: * -> *) vn. SigExpBase f vn -> SrcLoc -> SpecBase f vn
IncludeSpec SigExpBase Info VName
e' SrcLoc
loc forall a. a -> [a] -> [a]
: [SpecBase Info VName]
specs'
    )
  where
    warnIfShadowing :: QualName Name -> m ()
warnIfShadowing QualName Name
qn =
      (forall (m :: * -> *).
MonadTypeChecker m =>
SrcLoc
-> QualName Name
-> m (QualName VName, [TypeParamBase VName], StructRetType,
      Liftedness)
lookupType SrcLoc
loc QualName Name
qn forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall {m :: * -> *} {a}.
(MonadTypeChecker m, Pretty a) =>
a -> m ()
warnAbout QualName Name
qn)
        forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \e
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    warnAbout :: a -> m ()
warnAbout a
qn =
      forall (m :: * -> *) loc.
(MonadTypeChecker m, Located loc) =>
loc -> Doc () -> m ()
warn SrcLoc
loc forall a b. (a -> b) -> a -> b
$ Doc ()
"Inclusion shadows type" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty a
qn) forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"."

checkSigExp :: SigExpBase NoInfo Name -> TypeM (TySet, MTy, SigExpBase Info VName)
checkSigExp :: SigExpBase NoInfo Name -> TypeM (TySet, MTy, SigExpBase Info VName)
checkSigExp (SigParens SigExpBase NoInfo Name
e SrcLoc
loc) = do
  (TySet
abs, MTy
mty, SigExpBase Info VName
e') <- SigExpBase NoInfo Name -> TypeM (TySet, MTy, SigExpBase Info VName)
checkSigExp SigExpBase NoInfo Name
e
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (TySet
abs, MTy
mty, forall (f :: * -> *) vn.
SigExpBase f vn -> SrcLoc -> SigExpBase f vn
SigParens SigExpBase Info VName
e' SrcLoc
loc)
checkSigExp (SigVar QualName Name
name NoInfo (Map VName VName)
NoInfo SrcLoc
loc) = do
  (QualName VName
name', MTy
mty) <- SrcLoc -> QualName Name -> TypeM (QualName VName, MTy)
lookupMTy SrcLoc
loc QualName Name
name
  (MTy
mty', Map VName VName
substs) <- MTy -> TypeM (MTy, Map VName VName)
newNamesForMTy MTy
mty
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (MTy -> TySet
mtyAbs MTy
mty', MTy
mty', forall (f :: * -> *) vn.
QualName vn -> f (Map VName VName) -> SrcLoc -> SigExpBase f vn
SigVar QualName VName
name' (forall a. a -> Info a
Info Map VName VName
substs) SrcLoc
loc)
checkSigExp (SigSpecs [SpecBase NoInfo Name]
specs SrcLoc
loc) = do
  [SpecBase NoInfo Name] -> TypeM ()
checkForDuplicateSpecs [SpecBase NoInfo Name]
specs
  (TySet
abstypes, Env
env, [SpecBase Info VName]
specs') <- [SpecBase NoInfo Name] -> TypeM (TySet, Env, [SpecBase Info VName])
checkSpecs [SpecBase NoInfo Name]
specs
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (TySet
abstypes, TySet -> Mod -> MTy
MTy TySet
abstypes forall a b. (a -> b) -> a -> b
$ Env -> Mod
ModEnv Env
env, forall (f :: * -> *) vn.
[SpecBase f vn] -> SrcLoc -> SigExpBase f vn
SigSpecs [SpecBase Info VName]
specs' SrcLoc
loc)
checkSigExp (SigWith SigExpBase NoInfo Name
s (TypeRef QualName Name
tname [TypeParamBase Name]
ps TypeExp NoInfo Name
te SrcLoc
trloc) SrcLoc
loc) = do
  (TySet
abs, TySet
s_abs, Env
s_env, SigExpBase Info VName
s') <- SigExpBase NoInfo Name
-> TypeM (TySet, TySet, Env, SigExpBase Info VName)
checkSigExpToEnv SigExpBase NoInfo Name
s
  forall (m :: * -> *) a.
MonadTypeChecker m =>
[TypeParamBase Name] -> ([TypeParamBase VName] -> m a) -> m a
checkTypeParams [TypeParamBase Name]
ps forall a b. (a -> b) -> a -> b
$ \[TypeParamBase VName]
ps' -> do
    ([VName]
ext, TypeExp Info VName
te', StructType
te_t, Liftedness
_) <- forall a. [TypeParamBase VName] -> TypeM a -> TypeM a
bindingTypeParams [TypeParamBase VName]
ps' forall a b. (a -> b) -> a -> b
$ TypeExp NoInfo Name
-> TypeM ([VName], TypeExp Info VName, StructType, Liftedness)
checkTypeDecl TypeExp NoInfo Name
te
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [VName]
ext) forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError TypeExp Info VName
te' forall a. Monoid a => a
mempty Doc ()
"Anonymous dimensions are not allowed here."
    (QualName VName
tname', TySet
s_abs', Env
s_env') <- SrcLoc
-> TySet
-> Env
-> QualName Name
-> [TypeParamBase VName]
-> StructType
-> TypeM (QualName VName, TySet, Env)
refineEnv SrcLoc
loc TySet
s_abs Env
s_env QualName Name
tname [TypeParamBase VName]
ps' StructType
te_t
    forall (f :: * -> *) a. Applicative f => a -> f a
pure (TySet
abs, TySet -> Mod -> MTy
MTy TySet
s_abs' forall a b. (a -> b) -> a -> b
$ Env -> Mod
ModEnv Env
s_env', forall (f :: * -> *) vn.
SigExpBase f vn -> TypeRefBase f vn -> SrcLoc -> SigExpBase f vn
SigWith SigExpBase Info VName
s' (forall (f :: * -> *) vn.
QualName vn
-> [TypeParamBase vn] -> TypeExp f vn -> SrcLoc -> TypeRefBase f vn
TypeRef QualName VName
tname' [TypeParamBase VName]
ps' TypeExp Info VName
te' SrcLoc
trloc) SrcLoc
loc)
checkSigExp (SigArrow Maybe Name
maybe_pname SigExpBase NoInfo Name
e1 SigExpBase NoInfo Name
e2 SrcLoc
loc) = do
  (TySet
e1_abs, MTy TySet
s_abs Mod
e1_mod, SigExpBase Info VName
e1') <- SigExpBase NoInfo Name -> TypeM (TySet, MTy, SigExpBase Info VName)
checkSigExp SigExpBase NoInfo Name
e1
  (Env
env_for_e2, Maybe VName
maybe_pname') <-
    case Maybe Name
maybe_pname of
      Just Name
pname -> forall (m :: * -> *) a.
MonadTypeChecker m =>
[(Namespace, Name)] -> m a -> m a
bindSpaced [(Namespace
Term, Name
pname)] forall a b. (a -> b) -> a -> b
$ do
        VName
pname' <- forall (m :: * -> *).
MonadTypeChecker m =>
Namespace -> Name -> SrcLoc -> m VName
checkName Namespace
Term Name
pname SrcLoc
loc
        forall (f :: * -> *) a. Applicative f => a -> f a
pure
          ( forall a. Monoid a => a
mempty
              { envNameMap :: NameMap
envNameMap = forall k a. k -> a -> Map k a
M.singleton (Namespace
Term, Name
pname) forall a b. (a -> b) -> a -> b
$ forall v. v -> QualName v
qualName VName
pname',
                envModTable :: Map VName Mod
envModTable = forall k a. k -> a -> Map k a
M.singleton VName
pname' Mod
e1_mod
              },
            forall a. a -> Maybe a
Just VName
pname'
          )
      Maybe Name
Nothing ->
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Monoid a => a
mempty, forall a. Maybe a
Nothing)
  (TySet
e2_abs, MTy
e2_mod, SigExpBase Info VName
e2') <- forall a. Env -> TypeM a -> TypeM a
localEnv Env
env_for_e2 forall a b. (a -> b) -> a -> b
$ SigExpBase NoInfo Name -> TypeM (TySet, MTy, SigExpBase Info VName)
checkSigExp SigExpBase NoInfo Name
e2
  forall (f :: * -> *) a. Applicative f => a -> f a
pure
    ( TySet
e1_abs forall a. Semigroup a => a -> a -> a
<> TySet
e2_abs,
      TySet -> Mod -> MTy
MTy forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$ FunSig -> Mod
ModFun forall a b. (a -> b) -> a -> b
$ TySet -> Mod -> MTy -> FunSig
FunSig TySet
s_abs Mod
e1_mod MTy
e2_mod,
      forall (f :: * -> *) vn.
Maybe vn
-> SigExpBase f vn -> SigExpBase f vn -> SrcLoc -> SigExpBase f vn
SigArrow Maybe VName
maybe_pname' SigExpBase Info VName
e1' SigExpBase Info VName
e2' SrcLoc
loc
    )

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

checkSigBind :: SigBindBase NoInfo Name -> TypeM (TySet, Env, SigBindBase Info VName)
checkSigBind :: SigBindBase NoInfo Name
-> TypeM (TySet, Env, SigBindBase Info VName)
checkSigBind (SigBind Name
name SigExpBase NoInfo Name
e Maybe DocComment
doc SrcLoc
loc) = do
  (TySet
abs, MTy
env, SigExpBase Info VName
e') <- SigExpBase NoInfo Name -> TypeM (TySet, MTy, SigExpBase Info VName)
checkSigExp SigExpBase NoInfo Name
e
  forall (m :: * -> *) a.
MonadTypeChecker m =>
[(Namespace, Name)] -> m a -> m a
bindSpaced [(Namespace
Signature, Name
name)] forall a b. (a -> b) -> a -> b
$ do
    VName
name' <- forall (m :: * -> *).
MonadTypeChecker m =>
Namespace -> Name -> SrcLoc -> m VName
checkName Namespace
Signature Name
name SrcLoc
loc
    forall (f :: * -> *) a. Applicative f => a -> f a
pure
      ( TySet
abs,
        forall a. Monoid a => a
mempty
          { envSigTable :: Map VName MTy
envSigTable = forall k a. k -> a -> Map k a
M.singleton VName
name' MTy
env,
            envNameMap :: NameMap
envNameMap = forall k a. k -> a -> Map k a
M.singleton (Namespace
Signature, Name
name) (forall v. v -> QualName v
qualName VName
name')
          },
        forall (f :: * -> *) vn.
vn
-> SigExpBase f vn
-> Maybe DocComment
-> SrcLoc
-> SigBindBase f vn
SigBind VName
name' SigExpBase 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
  (TySet
abs, MTy
mty, ModExpBase Info VName
e') <- ModExpBase NoInfo Name -> TypeM (TySet, MTy, ModExpBase Info VName)
checkOneModExp ModExpBase NoInfo Name
e
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (TySet
abs, MTy
mty, forall (f :: * -> *) vn.
ModExpBase f vn -> SrcLoc -> ModExpBase f vn
ModParens ModExpBase Info VName
e' SrcLoc
loc)
checkOneModExp (ModDecs [UncheckedDec]
decs SrcLoc
loc) = do
  [UncheckedDec] -> TypeM ()
checkForDuplicateDecs [UncheckedDec]
decs
  (TySet
abstypes, Env
env, [Dec]
decs', Env
_) <- [UncheckedDec] -> TypeM (TySet, Env, [Dec], Env)
checkDecs [UncheckedDec]
decs
  forall (f :: * -> *) a. Applicative f => a -> f a
pure
    ( TySet
abstypes,
      TySet -> Mod -> MTy
MTy TySet
abstypes forall a b. (a -> b) -> a -> b
$ Env -> Mod
ModEnv Env
env,
      forall (f :: * -> *) vn.
[DecBase f vn] -> SrcLoc -> ModExpBase f vn
ModDecs [Dec]
decs' SrcLoc
loc
    )
checkOneModExp (ModVar QualName Name
v SrcLoc
loc) = do
  (QualName VName
v', Mod
env) <- forall (m :: * -> *).
MonadTypeChecker m =>
SrcLoc -> QualName Name -> m (QualName VName, Mod)
lookupMod SrcLoc
loc QualName Name
v
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when
    ( VName -> Name
baseName (forall vn. QualName vn -> vn
qualLeaf QualName VName
v') forall a. Eq a => a -> a -> Bool
== FilePath -> Name
nameFromString FilePath
"intrinsics"
        Bool -> Bool -> Bool
&& VName -> Int
baseTag (forall vn. QualName vn -> vn
qualLeaf QualName VName
v') forall a. Ord a => a -> a -> Bool
<= Int
maxIntrinsicTag
    )
    forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc forall a. Monoid a => a
mempty Doc ()
"The 'intrinsics' module may not be used in module expressions."
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Monoid a => a
mempty, TySet -> Mod -> MTy
MTy forall a. Monoid a => a
mempty Mod
env, forall (f :: * -> *) vn. QualName vn -> SrcLoc -> ModExpBase f vn
ModVar QualName VName
v' SrcLoc
loc)
checkOneModExp (ModImport FilePath
name NoInfo ImportName
NoInfo SrcLoc
loc) = do
  (ImportName
name', Env
env) <- SrcLoc -> FilePath -> TypeM (ImportName, Env)
lookupImport SrcLoc
loc FilePath
name
  forall (f :: * -> *) a. Applicative f => a -> f a
pure
    ( forall a. Monoid a => a
mempty,
      TySet -> Mod -> MTy
MTy forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$ Env -> Mod
ModEnv Env
env,
      forall (f :: * -> *) vn.
FilePath -> f ImportName -> SrcLoc -> ModExpBase f vn
ModImport FilePath
name (forall a. a -> Info a
Info ImportName
name') SrcLoc
loc
    )
checkOneModExp (ModApply ModExpBase NoInfo Name
f ModExpBase NoInfo Name
e NoInfo (Map VName VName)
NoInfo NoInfo (Map VName VName)
NoInfo SrcLoc
loc) = do
  (TySet
f_abs, MTy
f_mty, ModExpBase Info VName
f') <- ModExpBase NoInfo Name -> TypeM (TySet, MTy, ModExpBase Info VName)
checkOneModExp ModExpBase NoInfo Name
f
  case MTy -> Mod
mtyMod MTy
f_mty of
    ModFun FunSig
functor -> do
      (TySet
e_abs, MTy
e_mty, ModExpBase Info VName
e') <- ModExpBase NoInfo Name -> TypeM (TySet, MTy, ModExpBase Info VName)
checkOneModExp ModExpBase NoInfo Name
e
      (MTy
mty, Map VName VName
psubsts, Map VName VName
rsubsts) <- Loc
-> FunSig -> MTy -> TypeM (MTy, Map VName VName, Map VName VName)
applyFunctor (forall a. Located a => a -> Loc
locOf SrcLoc
loc) FunSig
functor MTy
e_mty
      forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( MTy -> TySet
mtyAbs MTy
mty forall a. Semigroup a => a -> a -> a
<> TySet
f_abs forall a. Semigroup a => a -> a -> a
<> TySet
e_abs,
          MTy
mty,
          forall (f :: * -> *) vn.
ModExpBase f vn
-> ModExpBase f vn
-> f (Map VName VName)
-> f (Map VName VName)
-> SrcLoc
-> ModExpBase f vn
ModApply ModExpBase Info VName
f' ModExpBase Info VName
e' (forall a. a -> Info a
Info Map VName VName
psubsts) (forall a. a -> Info a
Info Map VName VName
rsubsts) SrcLoc
loc
        )
    Mod
_ ->
      forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc forall a. Monoid a => a
mempty Doc ()
"Cannot apply non-parametric module."
checkOneModExp (ModAscript ModExpBase NoInfo Name
me SigExpBase NoInfo Name
se NoInfo (Map VName VName)
NoInfo SrcLoc
loc) = do
  (TySet
me_abs, MTy
me_mod, ModExpBase Info VName
me') <- ModExpBase NoInfo Name -> TypeM (TySet, MTy, ModExpBase Info VName)
checkOneModExp ModExpBase NoInfo Name
me
  (TySet
se_abs, MTy
se_mty, SigExpBase Info VName
se') <- SigExpBase NoInfo Name -> TypeM (TySet, MTy, SigExpBase Info VName)
checkSigExp SigExpBase NoInfo Name
se
  Map VName VName
match_subst <- forall a. Either TypeError a -> TypeM a
badOnLeft forall a b. (a -> b) -> a -> b
$ MTy -> MTy -> Loc -> Either TypeError (Map VName VName)
matchMTys MTy
me_mod MTy
se_mty (forall a. Located a => a -> Loc
locOf SrcLoc
loc)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (TySet
se_abs forall a. Semigroup a => a -> a -> a
<> TySet
me_abs, MTy
se_mty, forall (f :: * -> *) vn.
ModExpBase f vn
-> SigExpBase f vn
-> f (Map VName VName)
-> SrcLoc
-> ModExpBase f vn
ModAscript ModExpBase Info VName
me' SigExpBase Info VName
se' (forall a. a -> Info a
Info Map VName VName
match_subst) SrcLoc
loc)
checkOneModExp (ModLambda ModParamBase NoInfo Name
param Maybe (SigExpBase NoInfo Name, NoInfo (Map VName VName))
maybe_fsig_e ModExpBase NoInfo Name
body_e SrcLoc
loc) =
  forall a.
ModParamBase NoInfo Name
-> (ModParamBase Info VName -> TySet -> Mod -> TypeM a) -> TypeM a
withModParam ModParamBase NoInfo Name
param forall a b. (a -> b) -> a -> b
$ \ModParamBase Info VName
param' TySet
param_abs Mod
param_mod -> do
    (TySet
abs, Maybe (SigExpBase Info VName, Info (Map VName VName))
maybe_fsig_e', ModExpBase Info VName
body_e', MTy
mty) <-
      Maybe (SigExpBase NoInfo Name)
-> ModExpBase NoInfo Name
-> SrcLoc
-> TypeM
     (TySet, Maybe (SigExpBase Info VName, Info (Map VName VName)),
      ModExpBase Info VName, MTy)
checkModBody (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (SigExpBase NoInfo Name, NoInfo (Map VName VName))
maybe_fsig_e) ModExpBase NoInfo Name
body_e SrcLoc
loc
    forall (f :: * -> *) a. Applicative f => a -> f a
pure
      ( TySet
abs,
        TySet -> Mod -> MTy
MTy forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$ FunSig -> Mod
ModFun forall a b. (a -> b) -> a -> b
$ TySet -> Mod -> MTy -> FunSig
FunSig TySet
param_abs Mod
param_mod MTy
mty,
        forall (f :: * -> *) vn.
ModParamBase f vn
-> Maybe (SigExpBase f vn, f (Map VName VName))
-> ModExpBase f vn
-> SrcLoc
-> ModExpBase f vn
ModLambda ModParamBase Info VName
param' Maybe (SigExpBase Info VName, Info (Map VName VName))
maybe_fsig_e' ModExpBase Info VName
body_e' SrcLoc
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
  (TySet
e_abs, MTy TySet
abs Mod
mod, ModExpBase Info VName
e') <- ModExpBase NoInfo Name -> TypeM (TySet, MTy, ModExpBase Info VName)
checkOneModExp ModExpBase NoInfo Name
e
  case Mod
mod of
    ModEnv Env
env -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (TySet
e_abs forall a. Semigroup a => a -> a -> a
<> TySet
abs, Env
env, ModExpBase Info VName
e')
    ModFun {} -> forall (m :: * -> *) a. MonadTypeChecker m => SrcLoc -> m a
unappliedFunctor forall a b. (a -> b) -> a -> b
$ 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 SigExpBase NoInfo Name
psig_e NoInfo [VName]
NoInfo SrcLoc
loc) ModParamBase Info VName -> TySet -> Mod -> TypeM a
m = do
  (TySet
_abs, MTy TySet
p_abs Mod
p_mod, SigExpBase Info VName
psig_e') <- SigExpBase NoInfo Name -> TypeM (TySet, MTy, SigExpBase Info VName)
checkSigExp SigExpBase NoInfo Name
psig_e
  forall (m :: * -> *) a.
MonadTypeChecker m =>
[(Namespace, Name)] -> m a -> m a
bindSpaced [(Namespace
Term, Name
pname)] forall a b. (a -> b) -> a -> b
$ do
    VName
pname' <- forall (m :: * -> *).
MonadTypeChecker m =>
Namespace -> Name -> SrcLoc -> m VName
checkName Namespace
Term Name
pname SrcLoc
loc
    let in_body_env :: Env
in_body_env = forall a. Monoid a => a
mempty {envModTable :: Map VName Mod
envModTable = forall k a. k -> a -> Map k a
M.singleton VName
pname' Mod
p_mod}
    forall a. Env -> TypeM a -> TypeM a
localEnv Env
in_body_env forall a b. (a -> b) -> a -> b
$
      ModParamBase Info VName -> TySet -> Mod -> TypeM a
m (forall (f :: * -> *) vn.
vn -> SigExpBase f vn -> f [VName] -> SrcLoc -> ModParamBase f vn
ModParam VName
pname' SigExpBase Info VName
psig_e' (forall a. a -> Info a
Info forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall vn. QualName vn -> vn
qualLeaf forall a b. (a -> b) -> a -> b
$ 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 =
  forall a.
ModParamBase NoInfo Name
-> (ModParamBase Info VName -> TySet -> Mod -> TypeM a) -> TypeM a
withModParam ModParamBase NoInfo Name
p forall a b. (a -> b) -> a -> b
$ \ModParamBase Info VName
p' TySet
pabs Mod
pmod ->
    forall a.
[ModParamBase NoInfo Name]
-> ([(ModParamBase Info VName, TySet, Mod)] -> TypeM a) -> TypeM a
withModParams [ModParamBase NoInfo Name]
ps forall a b. (a -> b) -> a -> b
$ \[(ModParamBase Info VName, TySet, Mod)]
ps' -> [(ModParamBase Info VName, TySet, Mod)] -> TypeM a
m forall a b. (a -> b) -> a -> b
$ (ModParamBase Info VName
p', TySet
pabs, Mod
pmod) forall a. a -> [a] -> [a]
: [(ModParamBase Info VName, TySet, Mod)]
ps'

checkModBody ::
  Maybe (SigExpBase NoInfo Name) ->
  ModExpBase NoInfo Name ->
  SrcLoc ->
  TypeM
    ( TySet,
      Maybe (SigExp, Info (M.Map VName VName)),
      ModExp,
      MTy
    )
checkModBody :: Maybe (SigExpBase NoInfo Name)
-> ModExpBase NoInfo Name
-> SrcLoc
-> TypeM
     (TySet, Maybe (SigExpBase Info VName, Info (Map VName VName)),
      ModExpBase Info VName, MTy)
checkModBody Maybe (SigExpBase NoInfo Name)
maybe_fsig_e ModExpBase NoInfo Name
body_e SrcLoc
loc = forall a. TypeM a -> TypeM a
enteringModule forall a b. (a -> b) -> a -> b
$ do
  (TySet
body_e_abs, MTy
body_mty, ModExpBase Info VName
body_e') <- ModExpBase NoInfo Name -> TypeM (TySet, MTy, ModExpBase Info VName)
checkOneModExp ModExpBase NoInfo Name
body_e
  case Maybe (SigExpBase NoInfo Name)
maybe_fsig_e of
    Maybe (SigExpBase NoInfo Name)
Nothing ->
      forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( MTy -> TySet
mtyAbs MTy
body_mty forall a. Semigroup a => a -> a -> a
<> TySet
body_e_abs,
          forall a. Maybe a
Nothing,
          ModExpBase Info VName
body_e',
          MTy
body_mty
        )
    Just SigExpBase NoInfo Name
fsig_e -> do
      (TySet
fsig_abs, MTy
fsig_mty, SigExpBase Info VName
fsig_e') <- SigExpBase NoInfo Name -> TypeM (TySet, MTy, SigExpBase Info VName)
checkSigExp SigExpBase NoInfo Name
fsig_e
      Map VName VName
fsig_subst <- forall a. Either TypeError a -> TypeM a
badOnLeft forall a b. (a -> b) -> a -> b
$ MTy -> MTy -> Loc -> Either TypeError (Map VName VName)
matchMTys MTy
body_mty MTy
fsig_mty (forall a. Located a => a -> Loc
locOf SrcLoc
loc)
      forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( TySet
fsig_abs forall a. Semigroup a => a -> a -> a
<> TySet
body_e_abs,
          forall a. a -> Maybe a
Just (SigExpBase Info VName
fsig_e', forall a. a -> Info a
Info Map VName VName
fsig_subst),
          ModExpBase Info VName
body_e',
          MTy
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 (SigExpBase NoInfo Name, NoInfo (Map VName VName))
maybe_fsig_e ModExpBase NoInfo Name
e Maybe DocComment
doc SrcLoc
loc) = do
  (TySet
e_abs, Maybe (SigExpBase Info VName, Info (Map VName VName))
maybe_fsig_e', ModExpBase Info VName
e', MTy
mty) <- Maybe (SigExpBase NoInfo Name)
-> ModExpBase NoInfo Name
-> SrcLoc
-> TypeM
     (TySet, Maybe (SigExpBase Info VName, Info (Map VName VName)),
      ModExpBase Info VName, MTy)
checkModBody (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (SigExpBase NoInfo Name, NoInfo (Map VName VName))
maybe_fsig_e) ModExpBase NoInfo Name
e SrcLoc
loc
  forall (m :: * -> *) a.
MonadTypeChecker m =>
[(Namespace, Name)] -> m a -> m a
bindSpaced [(Namespace
Term, Name
name)] forall a b. (a -> b) -> a -> b
$ do
    VName
name' <- forall (m :: * -> *).
MonadTypeChecker m =>
Namespace -> Name -> SrcLoc -> m VName
checkName Namespace
Term Name
name SrcLoc
loc
    forall (f :: * -> *) a. Applicative f => a -> f a
pure
      ( TySet
e_abs,
        forall a. Monoid a => a
mempty
          { envModTable :: Map VName Mod
envModTable = forall k a. k -> a -> Map k a
M.singleton VName
name' forall a b. (a -> b) -> a -> b
$ MTy -> Mod
mtyMod MTy
mty,
            envNameMap :: NameMap
envNameMap = forall k a. k -> a -> Map k a
M.singleton (Namespace
Term, Name
name) forall a b. (a -> b) -> a -> b
$ forall v. v -> QualName v
qualName VName
name'
          },
        forall (f :: * -> *) vn.
vn
-> [ModParamBase f vn]
-> Maybe (SigExpBase f vn, f (Map VName VName))
-> ModExpBase f vn
-> Maybe DocComment
-> SrcLoc
-> ModBindBase f vn
ModBind VName
name' [] Maybe (SigExpBase 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 (SigExpBase NoInfo Name, NoInfo (Map VName VName))
maybe_fsig_e ModExpBase NoInfo Name
body_e Maybe DocComment
doc SrcLoc
loc) = do
  (TySet
abs, [ModParamBase Info VName]
params', Maybe (SigExpBase Info VName, Info (Map VName VName))
maybe_fsig_e', ModExpBase Info VName
body_e', FunSig
funsig) <-
    forall a.
ModParamBase NoInfo Name
-> (ModParamBase Info VName -> TySet -> Mod -> TypeM a) -> TypeM a
withModParam ModParamBase NoInfo Name
p forall a b. (a -> b) -> a -> b
$ \ModParamBase Info VName
p' TySet
p_abs Mod
p_mod ->
      forall a.
[ModParamBase NoInfo Name]
-> ([(ModParamBase Info VName, TySet, Mod)] -> TypeM a) -> TypeM a
withModParams [ModParamBase NoInfo Name]
ps 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) = forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 [(ModParamBase Info VName, TySet, Mod)]
params_stuff
        (TySet
abs, Maybe (SigExpBase Info VName, Info (Map VName VName))
maybe_fsig_e', ModExpBase Info VName
body_e', MTy
mty) <- Maybe (SigExpBase NoInfo Name)
-> ModExpBase NoInfo Name
-> SrcLoc
-> TypeM
     (TySet, Maybe (SigExpBase Info VName, Info (Map VName VName)),
      ModExpBase Info VName, MTy)
checkModBody (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (SigExpBase NoInfo Name, NoInfo (Map VName VName))
maybe_fsig_e) ModExpBase NoInfo Name
body_e SrcLoc
loc
        let addParam :: (TySet, Mod) -> MTy -> MTy
addParam (TySet
x, Mod
y) MTy
mty' = TySet -> Mod -> MTy
MTy forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$ FunSig -> Mod
ModFun forall a b. (a -> b) -> a -> b
$ TySet -> Mod -> MTy -> FunSig
FunSig TySet
x Mod
y MTy
mty'
        forall (f :: * -> *) a. Applicative f => a -> f a
pure
          ( TySet
abs,
            ModParamBase Info VName
p' forall a. a -> [a] -> [a]
: [ModParamBase Info VName]
ps',
            Maybe (SigExpBase Info VName, Info (Map VName VName))
maybe_fsig_e',
            ModExpBase Info VName
body_e',
            TySet -> Mod -> MTy -> FunSig
FunSig TySet
p_abs Mod
p_mod forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (TySet, Mod) -> MTy -> MTy
addParam MTy
mty forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [TySet]
ps_abs [Mod]
ps_mod
          )
  forall (m :: * -> *) a.
MonadTypeChecker m =>
[(Namespace, Name)] -> m a -> m a
bindSpaced [(Namespace
Term, Name
name)] forall a b. (a -> b) -> a -> b
$ do
    VName
name' <- forall (m :: * -> *).
MonadTypeChecker m =>
Namespace -> Name -> SrcLoc -> m VName
checkName Namespace
Term Name
name SrcLoc
loc
    forall (f :: * -> *) a. Applicative f => a -> f a
pure
      ( TySet
abs,
        forall a. Monoid a => a
mempty
          { envModTable :: Map VName Mod
envModTable =
              forall k a. k -> a -> Map k a
M.singleton VName
name' forall a b. (a -> b) -> a -> b
$ FunSig -> Mod
ModFun FunSig
funsig,
            envNameMap :: NameMap
envNameMap =
              forall k a. k -> a -> Map k a
M.singleton (Namespace
Term, Name
name) forall a b. (a -> b) -> a -> b
$ forall v. v -> QualName v
qualName VName
name'
          },
        forall (f :: * -> *) vn.
vn
-> [ModParamBase f vn]
-> Maybe (SigExpBase f vn, f (Map VName VName))
-> ModExpBase f vn
-> Maybe DocComment
-> SrcLoc
-> ModBindBase f vn
ModBind VName
name' [ModParamBase Info VName]
params' Maybe (SigExpBase 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 =
  forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m ()
foldM_ (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall {m :: * -> *} {f :: * -> *}.
MonadTypeChecker m =>
SpecBase f Name
-> Map (Namespace, Name) SrcLoc -> m (Map (Namespace, Name) SrcLoc)
f) 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 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' ->
          forall (m :: * -> *) a.
MonadTypeChecker m =>
Namespace -> Name -> SrcLoc -> SrcLoc -> m a
dupDefinitionError Namespace
namespace Name
name SrcLoc
loc SrcLoc
loc'
        Maybe SrcLoc
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ 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 f Name
_ f StructType
_ Maybe DocComment
_ SrcLoc
loc) =
      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 f Name
_ f StructRetType
_ Maybe DocComment
_ SrcLoc
loc)) =
      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) =
      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 SigExpBase f Name
_ Maybe DocComment
_ SrcLoc
loc) =
      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 {} =
      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 NoInfo Name
te NoInfo StructRetType
NoInfo Maybe DocComment
doc SrcLoc
loc) =
  forall (m :: * -> *) a.
MonadTypeChecker m =>
[TypeParamBase Name] -> ([TypeParamBase VName] -> m a) -> m a
checkTypeParams [TypeParamBase Name]
tps forall a b. (a -> b) -> a -> b
$ \[TypeParamBase VName]
tps' -> do
    (TypeExp Info VName
te', [VName]
svars, RetType [VName]
dims StructType
t, Liftedness
l') <- forall a. [TypeParamBase VName] -> TypeM a -> TypeM a
bindingTypeParams [TypeParamBase VName]
tps' forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadTypeChecker m =>
TypeExp NoInfo Name
-> m (TypeExp Info VName, [VName], StructRetType, Liftedness)
checkTypeExp TypeExp NoInfo Name
te

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

    let elab_t :: StructRetType
elab_t = forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType ([VName]
svars forall a. [a] -> [a] -> [a]
++ [VName]
dims) StructType
t

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

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

    forall (m :: * -> *) a.
MonadTypeChecker m =>
[(Namespace, Name)] -> m a -> m a
bindSpaced [(Namespace
Type, Name
name)] forall a b. (a -> b) -> a -> b
$ do
      VName
name' <- forall (m :: * -> *).
MonadTypeChecker m =>
Namespace -> Name -> SrcLoc -> m VName
checkName Namespace
Type Name
name SrcLoc
loc
      forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( forall a. Monoid a => a
mempty
            { envTypeTable :: Map VName TypeBinding
envTypeTable =
                forall k a. k -> a -> Map k a
M.singleton VName
name' forall a b. (a -> b) -> a -> b
$ Liftedness -> [TypeParamBase VName] -> StructRetType -> TypeBinding
TypeAbbr Liftedness
l [TypeParamBase VName]
tps' StructRetType
elab_t,
              envNameMap :: NameMap
envNameMap =
                forall k a. k -> a -> Map k a
M.singleton (Namespace
Type, Name
name) forall a b. (a -> b) -> a -> b
$ forall v. v -> QualName v
qualName VName
name'
            },
          forall (f :: * -> *) vn.
vn
-> Liftedness
-> [TypeParamBase vn]
-> TypeExp f vn
-> f StructRetType
-> Maybe DocComment
-> SrcLoc
-> TypeBindBase f vn
TypeBind VName
name' Liftedness
l [TypeParamBase VName]
tps' TypeExp Info VName
te' (forall a. a -> Info a
Info StructRetType
elab_t) Maybe DocComment
doc SrcLoc
loc
        )

entryPoint :: [Pat] -> Maybe (TypeExp Info VName) -> StructRetType -> EntryPoint
entryPoint :: [Pat] -> Maybe (TypeExp Info VName) -> StructRetType -> EntryPoint
entryPoint [Pat]
params Maybe (TypeExp Info VName)
orig_ret_te (RetType [VName]
ret StructType
orig_ret) =
  [EntryParam] -> EntryType -> EntryPoint
EntryPoint (forall a b. (a -> b) -> [a] -> [b]
map Pat -> EntryParam
patternEntry [Pat]
params forall a. [a] -> [a] -> [a]
++ [EntryParam]
more_params) EntryType
rettype'
  where
    ([EntryParam]
more_params, EntryType
rettype') = Maybe (TypeExp Info VName)
-> StructType -> ([EntryParam], EntryType)
onRetType Maybe (TypeExp Info VName)
orig_ret_te forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Size -> Size
extToAny StructType
orig_ret

    -- Since the entry point type is not a RetType but just a plain
    -- StructType, we have to remove any existentially bound sizes.
    extToAny :: Size -> Size
extToAny (NamedSize QualName VName
v) | forall vn. QualName vn -> vn
qualLeaf QualName VName
v forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [VName]
ret = Maybe VName -> Size
AnySize forall a. Maybe a
Nothing
    extToAny Size
d = Size
d

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

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

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

checkEntryPoint ::
  SrcLoc ->
  [TypeParam] ->
  [Pat] ->
  Maybe (TypeExp Info VName) ->
  StructRetType ->
  TypeM ()
checkEntryPoint :: SrcLoc
-> [TypeParamBase VName]
-> [Pat]
-> Maybe (TypeExp Info VName)
-> StructRetType
-> TypeM ()
checkEntryPoint SrcLoc
loc [TypeParamBase VName]
tparams [Pat]
params Maybe (TypeExp Info VName)
maybe_tdecl StructRetType
rettype
  | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall vn. TypeParamBase vn -> Bool
isTypeParam [TypeParamBase VName]
tparams =
      forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
        forall ann. Doc ann -> Doc ann -> Doc ann
withIndexLink
          Doc ()
"polymorphic-entry"
          Doc ()
"Entry point functions may not be polymorphic."
  | Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall dim as. TypeBase dim as -> Bool
orderZero [StructType]
param_ts)
      Bool -> Bool -> Bool
|| Bool -> Bool
not (forall dim as. TypeBase dim as -> Bool
orderZero StructType
rettype') =
      forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
        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 <-
      forall a. Ord a => [a] -> Set a
S.fromList (forall a b. (a -> b) -> [a] -> [b]
map forall vn. TypeParamBase vn -> vn
typeParamName [TypeParamBase VName]
tparams)
        forall a. Ord a => Set a -> Set a -> Set a
`S.intersection` forall as. TypeBase Size as -> Set VName
freeInType StructType
rettype'
        forall a. Ord a => Set a -> Set a -> Set a
`S.difference` forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall as. TypeBase Size as -> Set VName
freeInType [StructType]
param_ts,
    Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. Set a -> Bool
S.null Set VName
sizes_only_in_ret =
      forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
        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."
  | Pat
p : [Pat]
_ <- forall a. (a -> Bool) -> [a] -> [a]
filter Pat -> Bool
nastyParameter [Pat]
params =
      forall (m :: * -> *) loc.
(MonadTypeChecker m, Located loc) =>
loc -> Doc () -> m ()
warn SrcLoc
loc forall a b. (a -> b) -> a -> b
$
        Doc ()
"Entry point parameter\n"
          forall ann. Doc ann -> Doc ann -> Doc ann
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a ann. Pretty a => a -> Doc ann
pretty Pat
p)
          forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"\nwill have an opaque type, so the entry point will likely not be callable."
  | forall als dim.
Monoid als =>
Maybe (TypeExp Info VName) -> TypeBase dim als -> Bool
nastyReturnType Maybe (TypeExp Info VName)
maybe_tdecl StructType
rettype_t =
      forall (m :: * -> *) loc.
(MonadTypeChecker m, Located loc) =>
loc -> Doc () -> m ()
warn SrcLoc
loc forall a b. (a -> b) -> a -> b
$
        Doc ()
"Entry point return type\n"
          forall ann. Doc ann -> Doc ann -> Doc ann
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a ann. Pretty a => a -> Doc ann
pretty StructRetType
rettype)
          forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"\nwill have an opaque type, so the result will likely not be usable."
  | Bool
otherwise =
      forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  where
    (RetType [VName]
_ StructType
rettype_t) = StructRetType
rettype
    ([(Diet, StructType)]
rettype_params, StructType
rettype') = forall dim as.
TypeBase dim as -> ([(Diet, TypeBase dim ())], TypeBase dim ())
unfoldFunType StructType
rettype_t
    param_ts :: [StructType]
param_ts = forall a b. (a -> b) -> [a] -> [b]
map Pat -> StructType
patternStructType [Pat]
params forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(Diet, StructType)]
rettype_params

checkValBind :: ValBindBase NoInfo Name -> TypeM (Env, ValBind)
checkValBind :: ValBindBase NoInfo Name -> TypeM (Env, ValBind)
checkValBind (ValBind Maybe (NoInfo EntryPoint)
entry Name
fname Maybe (TypeExp NoInfo Name)
maybe_tdecl NoInfo StructRetType
NoInfo [TypeParamBase Name]
tparams [PatBase NoInfo Name]
params UncheckedExp
body Maybe DocComment
doc [AttrInfo Name]
attrs SrcLoc
loc) = do
  Bool
top_level <- TypeM Bool
atTopLevel
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not Bool
top_level Bool -> Bool -> Bool
&& forall a. Maybe a -> Bool
isJust Maybe (NoInfo EntryPoint)
entry) forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
      forall ann. Doc ann -> Doc ann -> Doc ann
withIndexLink Doc ()
"nested-entry" Doc ()
"Entry points may not be declared inside modules."

  (VName
fname', [TypeParamBase VName]
tparams', [Pat]
params', Maybe (TypeExp Info VName)
maybe_tdecl', StructRetType
rettype, Exp
body') <-
    (Name, Maybe (TypeExp NoInfo Name), [TypeParamBase Name],
 [PatBase NoInfo Name], UncheckedExp, SrcLoc)
-> TypeM
     (VName, [TypeParamBase VName], [Pat], Maybe (TypeExp Info VName),
      StructRetType, Exp)
checkFunDef (Name
fname, Maybe (TypeExp NoInfo Name)
maybe_tdecl, [TypeParamBase Name]
tparams, [PatBase NoInfo Name]
params, UncheckedExp
body, SrcLoc
loc)

  let entry' :: Maybe (Info EntryPoint)
entry' = forall a. a -> Info a
Info ([Pat] -> Maybe (TypeExp Info VName) -> StructRetType -> EntryPoint
entryPoint [Pat]
params' Maybe (TypeExp Info VName)
maybe_tdecl' StructRetType
rettype) forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Maybe (NoInfo EntryPoint)
entry

  case Maybe (Info EntryPoint)
entry' of
    Just Info EntryPoint
_ -> SrcLoc
-> [TypeParamBase VName]
-> [Pat]
-> Maybe (TypeExp Info VName)
-> StructRetType
-> TypeM ()
checkEntryPoint SrcLoc
loc [TypeParamBase VName]
tparams' [Pat]
params' Maybe (TypeExp Info VName)
maybe_tdecl' StructRetType
rettype
    Maybe (Info EntryPoint)
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

  [AttrInfo VName]
attrs' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *).
MonadTypeChecker m =>
AttrInfo Name -> m (AttrInfo VName)
checkAttr [AttrInfo Name]
attrs
  let vb :: ValBind
vb = forall (f :: * -> *) vn.
Maybe (f EntryPoint)
-> vn
-> Maybe (TypeExp f vn)
-> f StructRetType
-> [TypeParamBase vn]
-> [PatBase f vn]
-> ExpBase f vn
-> Maybe DocComment
-> [AttrInfo vn]
-> SrcLoc
-> ValBindBase f vn
ValBind Maybe (Info EntryPoint)
entry' VName
fname' Maybe (TypeExp Info VName)
maybe_tdecl' (forall a. a -> Info a
Info StructRetType
rettype) [TypeParamBase VName]
tparams' [Pat]
params' Exp
body' Maybe DocComment
doc [AttrInfo VName]
attrs' SrcLoc
loc
  forall (f :: * -> *) a. Applicative f => a -> f a
pure
    ( forall a. Monoid a => a
mempty
        { envVtable :: Map VName BoundV
envVtable =
            forall k a. k -> a -> Map k a
M.singleton VName
fname' forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [TypeParamBase VName] -> StructType -> BoundV
BoundV forall a b. (a -> b) -> a -> b
$ ValBind -> ([TypeParamBase VName], StructType)
valBindTypeScheme ValBind
vb,
          envNameMap :: NameMap
envNameMap =
            forall k a. k -> a -> Map k a
M.singleton (Namespace
Term, Name
fname) forall a b. (a -> b) -> a -> b
$ forall v. v -> QualName v
qualName VName
fname'
        },
      ValBind
vb
    )

nastyType :: Monoid als => TypeBase dim als -> Bool
nastyType :: forall als dim. Monoid als => TypeBase dim als -> Bool
nastyType (Scalar Prim {}) = Bool
False
nastyType t :: TypeBase dim als
t@Array {} = forall als dim. Monoid als => TypeBase dim als -> Bool
nastyType forall a b. (a -> b) -> a -> b
$ forall dim as. Int -> TypeBase dim as -> TypeBase dim as
stripArray Int
1 TypeBase dim als
t
nastyType TypeBase dim als
_ = Bool
True

nastyReturnType :: Monoid als => Maybe (TypeExp Info VName) -> TypeBase dim als -> Bool
nastyReturnType :: forall als dim.
Monoid als =>
Maybe (TypeExp Info VName) -> TypeBase dim als -> Bool
nastyReturnType Maybe (TypeExp Info VName)
Nothing (Scalar (Arrow als
_ PName
_ Diet
_ TypeBase dim ()
t1 (RetType [VName]
_ TypeBase dim als
t2))) =
  forall als dim. Monoid als => TypeBase dim als -> Bool
nastyType TypeBase dim ()
t1 Bool -> Bool -> Bool
|| forall als dim.
Monoid als =>
Maybe (TypeExp Info VName) -> TypeBase dim als -> Bool
nastyReturnType forall a. Maybe a
Nothing TypeBase dim als
t2
nastyReturnType (Just (TEArrow Maybe VName
_ TypeExp Info VName
te1 TypeExp Info VName
te2 SrcLoc
_)) (Scalar (Arrow als
_ PName
_ Diet
_ TypeBase dim ()
t1 (RetType [VName]
_ TypeBase dim als
t2))) =
  (Bool -> Bool
not (TypeExp Info VName -> Bool
niceTypeExp TypeExp Info VName
te1) Bool -> Bool -> Bool
&& forall als dim. Monoid als => TypeBase dim als -> Bool
nastyType TypeBase dim ()
t1)
    Bool -> Bool -> Bool
|| forall als dim.
Monoid als =>
Maybe (TypeExp Info VName) -> TypeBase dim als -> Bool
nastyReturnType (forall a. a -> Maybe a
Just TypeExp Info VName
te2) TypeBase dim als
t2
nastyReturnType (Just TypeExp Info VName
te) TypeBase dim als
_
  | TypeExp Info VName -> Bool
niceTypeExp TypeExp Info VName
te = Bool
False
nastyReturnType Maybe (TypeExp Info VName)
te TypeBase dim als
t
  | Just [TypeBase dim als]
ts <- forall dim as. TypeBase dim as -> Maybe [TypeBase dim as]
isTupleRecord TypeBase dim als
t =
      case Maybe (TypeExp Info VName)
te of
        Just (TETuple [TypeExp Info VName]
tes SrcLoc
_) -> forall (t :: * -> *). Foldable t => t Bool -> Bool
or forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall als dim.
Monoid als =>
Maybe (TypeExp Info VName) -> TypeBase dim als -> Bool
nastyType' (forall a b. (a -> b) -> [a] -> [b]
map forall a. a -> Maybe a
Just [TypeExp Info VName]
tes) [TypeBase dim als]
ts
        Maybe (TypeExp Info VName)
_ -> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall als dim. Monoid als => TypeBase dim als -> Bool
nastyType [TypeBase dim als]
ts
  | Bool
otherwise = forall als dim.
Monoid als =>
Maybe (TypeExp Info VName) -> TypeBase dim als -> Bool
nastyType' Maybe (TypeExp Info VName)
te TypeBase dim als
t
  where
    nastyType' :: Maybe (TypeExp Info VName) -> TypeBase dim als -> Bool
nastyType' (Just TypeExp Info VName
te') TypeBase dim als
_ | TypeExp Info VName -> Bool
niceTypeExp TypeExp Info VName
te' = Bool
False
    nastyType' Maybe (TypeExp Info VName)
_ TypeBase dim als
t' = forall als dim. Monoid als => TypeBase dim als -> Bool
nastyType TypeBase dim als
t'

nastyParameter :: Pat -> Bool
nastyParameter :: Pat -> Bool
nastyParameter Pat
p = forall als dim. Monoid als => TypeBase dim als -> Bool
nastyType (Pat -> PatType
patternType Pat
p) Bool -> Bool -> Bool
&& Bool -> Bool
not (Pat -> Bool
ascripted Pat
p)
  where
    ascripted :: Pat -> Bool
ascripted (PatAscription Pat
_ TypeExp Info VName
te SrcLoc
_) = TypeExp Info VName -> Bool
niceTypeExp TypeExp Info VName
te
    ascripted (PatParens Pat
p' SrcLoc
_) = Pat -> Bool
ascripted Pat
p'
    ascripted Pat
_ = Bool
False

niceTypeExp :: TypeExp Info VName -> Bool
niceTypeExp :: TypeExp Info VName -> Bool
niceTypeExp (TEVar (QualName [] VName
_) SrcLoc
_) = Bool
True
niceTypeExp (TEApply TypeExp Info VName
te TypeArgExpSize {} SrcLoc
_) = TypeExp Info VName -> Bool
niceTypeExp TypeExp Info VName
te
niceTypeExp (TEArray SizeExp Info VName
_ TypeExp Info VName
te SrcLoc
_) = TypeExp Info VName -> Bool
niceTypeExp TypeExp Info VName
te
niceTypeExp (TEUnique TypeExp Info VName
te SrcLoc
_) = TypeExp Info VName -> Bool
niceTypeExp TypeExp Info VName
te
niceTypeExp TypeExp Info VName
_ = Bool
False

checkOneDec :: DecBase NoInfo Name -> TypeM (TySet, Env, DecBase Info VName)
checkOneDec :: UncheckedDec -> TypeM (TySet, Env, Dec)
checkOneDec (ModDec ModBindBase NoInfo Name
struct) = do
  (TySet
abs, Env
modenv, ModBindBase Info VName
struct') <- ModBindBase NoInfo Name
-> TypeM (TySet, Env, ModBindBase Info VName)
checkModBind ModBindBase NoInfo Name
struct
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (TySet
abs, Env
modenv, forall (f :: * -> *) vn. ModBindBase f vn -> DecBase f vn
ModDec ModBindBase Info VName
struct')
checkOneDec (SigDec SigBindBase NoInfo Name
sig) = do
  (TySet
abs, Env
sigenv, SigBindBase Info VName
sig') <- SigBindBase NoInfo Name
-> TypeM (TySet, Env, SigBindBase Info VName)
checkSigBind SigBindBase NoInfo Name
sig
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (TySet
abs, Env
sigenv, forall (f :: * -> *) vn. SigBindBase f vn -> DecBase f vn
SigDec SigBindBase Info VName
sig')
checkOneDec (TypeDec TypeBindBase NoInfo Name
tdec) = do
  (Env
tenv, TypeBindBase Info VName
tdec') <- TypeBindBase NoInfo Name -> TypeM (Env, TypeBindBase Info VName)
checkTypeBind TypeBindBase NoInfo Name
tdec
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Monoid a => a
mempty, Env
tenv, forall (f :: * -> *) vn. TypeBindBase f vn -> DecBase f vn
TypeDec TypeBindBase Info VName
tdec')
checkOneDec (OpenDec ModExpBase NoInfo Name
x SrcLoc
loc) = do
  (TySet
x_abs, Env
x_env, ModExpBase Info VName
x') <- ModExpBase NoInfo Name -> TypeM (TySet, Env, ModExpBase Info VName)
checkOneModExpToEnv ModExpBase NoInfo Name
x
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (TySet
x_abs, Env
x_env, forall (f :: * -> *) vn. ModExpBase f vn -> SrcLoc -> DecBase f vn
OpenDec ModExpBase Info VName
x' SrcLoc
loc)
checkOneDec (LocalDec UncheckedDec
d SrcLoc
loc) = do
  (TySet
abstypes, Env
env, Dec
d') <- UncheckedDec -> TypeM (TySet, Env, Dec)
checkOneDec UncheckedDec
d
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (TySet
abstypes, Env
env, forall (f :: * -> *) vn. DecBase f vn -> SrcLoc -> DecBase f vn
LocalDec Dec
d' SrcLoc
loc)
checkOneDec (ImportDec FilePath
name NoInfo ImportName
NoInfo SrcLoc
loc) = do
  (ImportName
name', Env
env) <- SrcLoc -> FilePath -> TypeM (ImportName, Env)
lookupImport SrcLoc
loc FilePath
name
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (FilePath -> Bool
isBuiltin FilePath
name) forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
      forall a ann. Pretty a => a -> Doc ann
pretty FilePath
name forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"may not be explicitly imported."
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Monoid a => a
mempty, Env
env, forall (f :: * -> *) vn.
FilePath -> f ImportName -> SrcLoc -> DecBase f vn
ImportDec FilePath
name (forall a. a -> Info a
Info ImportName
name') SrcLoc
loc)
checkOneDec (ValDec ValBindBase NoInfo Name
vb) = do
  (Env
env, ValBind
vb') <- ValBindBase NoInfo Name -> TypeM (Env, ValBind)
checkValBind ValBindBase NoInfo Name
vb
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Monoid a => a
mempty, Env
env, forall (f :: * -> *) vn. ValBindBase f vn -> DecBase f vn
ValDec ValBind
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
  (TySet
d_abstypes, Env
d_env, Dec
d') <- UncheckedDec -> TypeM (TySet, Env, Dec)
checkOneDec UncheckedDec
d
  (TySet
ds_abstypes, Env
ds_env, [Dec]
ds', Env
full_env) <- forall a. Env -> TypeM a -> TypeM a
localEnv Env
d_env forall a b. (a -> b) -> a -> b
$ [UncheckedDec] -> TypeM (TySet, Env, [Dec], Env)
checkDecs [UncheckedDec]
ds
  forall (f :: * -> *) a. Applicative f => a -> f a
pure
    ( TySet
d_abstypes forall a. Semigroup a => a -> a -> a
<> TySet
ds_abstypes,
      case Dec
d' of
        LocalDec {} -> Env
ds_env
        ImportDec {} -> Env
ds_env
        Dec
_ -> Env
ds_env forall a. Semigroup a => a -> a -> a
<> Env
d_env,
      Dec
d' forall a. a -> [a] -> [a]
: [Dec]
ds',
      Env
full_env
    )
checkDecs [] = do
  Env
full_env <- TypeM Env
askEnv
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Monoid a => a
mempty, forall a. Monoid a => a
mempty, [], Env
full_env)