{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedStrings #-}

-- | 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,
    TypeError,
    Warnings,
    initialEnv,
  )
where

import Control.Monad.Except
import Control.Monad.Writer hiding (Sum)
import Data.Bifunctor (second)
import Data.Char (isAlpha, isAlphaNum)
import Data.Either
import Data.List (isPrefixOf)
import qualified Data.Map.Strict as M
import Data.Maybe
import Data.Ord
import qualified Data.Set 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 =
  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 String FileModule -> ImportTable
forall a b k. (a -> b) -> Map k a -> Map k b
M.map FileModule -> Env
fileEnv (Map String FileModule -> ImportTable)
-> Map String FileModule -> ImportTable
forall a b. (a -> b) -> a -> b
$ Imports -> Map String 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
-> UncheckedExp
-> (Warnings, Either TypeError ([TypeParam], Exp))
checkExp Imports
files VNameSource
src Env
env UncheckedExp
e =
  (Either TypeError (([TypeParam], Exp), VNameSource)
 -> Either TypeError ([TypeParam], Exp))
-> (Warnings, Either TypeError (([TypeParam], Exp), VNameSource))
-> (Warnings, Either TypeError ([TypeParam], Exp))
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (((([TypeParam], Exp), VNameSource) -> ([TypeParam], Exp))
-> Either TypeError (([TypeParam], Exp), VNameSource)
-> Either TypeError ([TypeParam], Exp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([TypeParam], Exp), VNameSource) -> ([TypeParam], Exp)
forall a b. (a, b) -> a
fst) ((Warnings, Either TypeError (([TypeParam], Exp), VNameSource))
 -> (Warnings, Either TypeError ([TypeParam], Exp)))
-> (Warnings, Either TypeError (([TypeParam], Exp), VNameSource))
-> (Warnings, Either TypeError ([TypeParam], Exp))
forall a b. (a -> b) -> a -> b
$ Env
-> ImportTable
-> ImportName
-> VNameSource
-> TypeM ([TypeParam], Exp)
-> (Warnings, Either TypeError (([TypeParam], Exp), VNameSource))
forall a.
Env
-> ImportTable
-> ImportName
-> VNameSource
-> TypeM a
-> (Warnings, Either TypeError (a, VNameSource))
runTypeM Env
env ImportTable
files' (String -> ImportName
mkInitialImport String
"") VNameSource
src (TypeM ([TypeParam], Exp)
 -> (Warnings, Either TypeError (([TypeParam], Exp), VNameSource)))
-> TypeM ([TypeParam], Exp)
-> (Warnings, Either TypeError (([TypeParam], Exp), VNameSource))
forall a b. (a -> b) -> a -> b
$ UncheckedExp -> TypeM ([TypeParam], Exp)
checkOneExp UncheckedExp
e
  where
    files' :: ImportTable
files' = (FileModule -> Env) -> Map String FileModule -> ImportTable
forall a b k. (a -> b) -> Map k a -> Map k b
M.map FileModule -> Env
fileEnv (Map String FileModule -> ImportTable)
-> Map String FileModule -> ImportTable
forall a b. (a -> b) -> a -> b
$ Imports -> Map String 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 (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 (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
      (TySet
_, Env
env', Dec
d') <- UncheckedDec -> TypeM (TySet, Env, Dec)
checkOneDec UncheckedDec
d
      (Env, Dec) -> TypeM (Env, Dec)
forall (m :: * -> *) a. Monad m => a -> m a
return (Env
env' Env -> 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' = (FileModule -> Env) -> Map String FileModule -> ImportTable
forall a b k. (a -> b) -> Map k a -> Map k b
M.map FileModule -> Env
fileEnv (Map String FileModule -> ImportTable)
-> Map String FileModule -> ImportTable
forall a b. (a -> b) -> a -> b
$ Imports -> Map String 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 (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 (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)))
-> (Warnings,
    Either TypeError ((MTy, ModExpBase Info VName), VNameSource))
-> (Warnings, Either TypeError (MTy, ModExpBase Info VName))
forall a b. (a -> b) -> a -> b
$ 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' (String -> ImportName
mkInitialImport String
"") VNameSource
src (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), VNameSource))
forall a b. (a -> b) -> a -> b
$ ModExpBase NoInfo Name -> TypeM (MTy, ModExpBase Info VName)
checkOneModExp ModExpBase NoInfo Name
me
  where
    files' :: ImportTable
files' = (FileModule -> Env) -> Map String FileModule -> ImportTable
forall a b k. (a -> b) -> Map k a -> Map k b
M.map FileModule -> Env
fileEnv (Map String FileModule -> ImportTable)
-> Map String FileModule -> ImportTable
forall a b. (a -> b) -> a -> b
$ Imports -> Map String 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 :: Map VName Mod
envModTable = Map VName Mod
initialModTable,
      envNameMap :: NameMap
envNameMap =
        (Namespace, Name) -> QualName VName -> NameMap -> NameMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert
          (Namespace
Term, String -> Name
nameFromString String
"intrinsics")
          (VName -> QualName VName
forall v. v -> QualName v
qualName VName
intrinsics_v)
          NameMap
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 (String -> Name
nameFromString String
"intrinsics") Int
0

    intrinsicsModule :: Env
intrinsicsModule = Map VName BoundV
-> Map VName TypeBinding
-> Map VName MTy
-> Map VName Mod
-> NameMap
-> 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 NameMap
intrinsicsNameMap

    addIntrinsicT :: (a, Intrinsic) -> Maybe (a, TypeBinding)
addIntrinsicT (a
name, IntrinsicType PrimType
t) =
      (a, TypeBinding) -> Maybe (a, TypeBinding)
forall a. a -> Maybe a
Just (a
name, Liftedness -> [TypeParam] -> StructType -> TypeBinding
TypeAbbr Liftedness
Unlifted [] (StructType -> TypeBinding) -> StructType -> TypeBinding
forall a b. (a -> b) -> a -> b
$ ScalarTypeBase (DimDecl VName) () -> StructType
forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar (ScalarTypeBase (DimDecl VName) () -> StructType)
-> ScalarTypeBase (DimDecl VName) () -> StructType
forall a b. (a -> b) -> a -> b
$ PrimType -> ScalarTypeBase (DimDecl VName) ()
forall dim as. PrimType -> ScalarTypeBase dim as
Prim PrimType
t)
    addIntrinsicT (a, Intrinsic)
_ =
      Maybe (a, TypeBinding)
forall a. Maybe a
Nothing

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') <- [UncheckedDec] -> TypeM (TySet, Env, [Dec])
checkDecs [UncheckedDec]
decs
  FileModule -> TypeM FileModule
forall (m :: * -> *) a. Monad m => a -> m a
return (TySet -> Env -> Prog -> FileModule
FileModule TySet
abs Env
env (Prog -> FileModule) -> Prog -> FileModule
forall a b. (a -> b) -> a -> b
$ Maybe DocComment -> [Dec] -> Prog
forall (f :: * -> *) vn.
Maybe DocComment -> [DecBase f vn] -> ProgBase f vn
Prog Maybe DocComment
doc [Dec]
decs')

dupDefinitionError ::
  MonadTypeChecker m =>
  Namespace ->
  Name ->
  SrcLoc ->
  SrcLoc ->
  m a
dupDefinitionError :: Namespace -> Name -> SrcLoc -> SrcLoc -> m a
dupDefinitionError Namespace
space Name
name SrcLoc
loc1 SrcLoc
loc2 =
  SrcLoc -> 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
<+> Namespace -> Doc
forall a. Pretty a => a -> Doc
ppr Namespace
space
      Doc -> Doc -> Doc
<+> Name -> Doc
forall v. IsName v => v -> Doc
pprName Name
name Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
".  Previously defined at"
      Doc -> Doc -> Doc
<+> String -> Doc
text (SrcLoc -> String
forall a. Located a => a -> String
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 (m :: * -> *) a. Monad m => a -> m a
return (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]
_ TypeDeclBase 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
Type Name
name SrcLoc
loc
    f (SigDec (SigBind Name
name SigExpBase 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 (SigExpBase 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 (m :: * -> *) a. Monad m => a -> m a
return
    f LocalDec {} = Map (Namespace, Name) SrcLoc -> m (Map (Namespace, Name) SrcLoc)
forall (m :: * -> *) a. Monad m => a -> m a
return
    f ImportDec {} = Map (Namespace, Name) SrcLoc -> m (Map (Namespace, Name) SrcLoc)
forall (m :: * -> *) a. Monad m => a -> m a
return

bindingTypeParams :: [TypeParam] -> TypeM a -> TypeM a
bindingTypeParams :: [TypeParam] -> TypeM a -> TypeM a
bindingTypeParams [TypeParam]
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
$ (TypeParam -> Env) -> [TypeParam] -> [Env]
forall a b. (a -> b) -> [a] -> [b]
map TypeParam -> Env
typeParamEnv [TypeParam]
tparams

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

emptyDimParam :: StructType -> Bool
emptyDimParam :: StructType -> Bool
emptyDimParam = Maybe StructType -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe StructType -> Bool)
-> (StructType -> Maybe StructType) -> StructType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set VName -> DimPos -> DimDecl VName -> Maybe (DimDecl VName))
-> StructType -> Maybe StructType
forall (f :: * -> *) fdim tdim als.
Applicative f =>
(Set VName -> DimPos -> fdim -> f tdim)
-> TypeBase fdim als -> f (TypeBase tdim als)
traverseDims Set VName -> DimPos -> DimDecl VName -> Maybe (DimDecl VName)
forall p vn. p -> DimPos -> DimDecl vn -> Maybe (DimDecl vn)
onDim
  where
    onDim :: p -> DimPos -> DimDecl vn -> Maybe (DimDecl vn)
onDim p
_ DimPos
pos DimDecl vn
AnyDim | DimPos
pos DimPos -> [DimPos] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [DimPos
PosImmediate, DimPos
PosParam] = Maybe (DimDecl vn)
forall a. Maybe a
Nothing
    onDim p
_ DimPos
_ DimDecl vn
d = DimDecl vn -> Maybe (DimDecl vn)
forall a. a -> Maybe a
Just DimDecl vn
d

-- 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 (m :: * -> *) a. Monad m => a -> m a
return (TySet
forall a. Monoid a => a
mempty, Env
forall a. Monoid a => a
mempty, [])
checkSpecs (ValSpec Name
name [TypeParamBase Name]
tparams TypeDeclBase NoInfo Name
vtype Maybe DocComment
doc SrcLoc
loc : [SpecBase NoInfo Name]
specs) =
  [(Namespace, Name)]
-> TypeM (TySet, Env, [SpecBase Info VName])
-> TypeM (TySet, Env, [SpecBase Info VName])
forall (m :: * -> *) a.
MonadTypeChecker m =>
[(Namespace, Name)] -> m a -> m a
bindSpaced [(Namespace
Term, Name
name)] (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
$ do
    VName
name' <- Namespace -> Name -> SrcLoc -> TypeM VName
forall (m :: * -> *).
MonadTypeChecker m =>
Namespace -> Name -> SrcLoc -> m VName
checkName Namespace
Term Name
name SrcLoc
loc
    ([TypeParam]
tparams', TypeDeclBase Info VName
vtype') <-
      [TypeParamBase Name]
-> ([TypeParam] -> TypeM ([TypeParam], TypeDeclBase Info VName))
-> TypeM ([TypeParam], TypeDeclBase Info VName)
forall (m :: * -> *) a.
MonadTypeChecker m =>
[TypeParamBase Name] -> ([TypeParam] -> m a) -> m a
checkTypeParams [TypeParamBase Name]
tparams (([TypeParam] -> TypeM ([TypeParam], TypeDeclBase Info VName))
 -> TypeM ([TypeParam], TypeDeclBase Info VName))
-> ([TypeParam] -> TypeM ([TypeParam], TypeDeclBase Info VName))
-> TypeM ([TypeParam], TypeDeclBase Info VName)
forall a b. (a -> b) -> a -> b
$ \[TypeParam]
tparams' -> [TypeParam]
-> TypeM ([TypeParam], TypeDeclBase Info VName)
-> TypeM ([TypeParam], TypeDeclBase Info VName)
forall a. [TypeParam] -> TypeM a -> TypeM a
bindingTypeParams [TypeParam]
tparams' (TypeM ([TypeParam], TypeDeclBase Info VName)
 -> TypeM ([TypeParam], TypeDeclBase Info VName))
-> TypeM ([TypeParam], TypeDeclBase Info VName)
-> TypeM ([TypeParam], TypeDeclBase Info VName)
forall a b. (a -> b) -> a -> b
$ do
        (TypeDeclBase Info VName
vtype', Liftedness
_) <- TypeDeclBase NoInfo Name
-> TypeM (TypeDeclBase Info VName, Liftedness)
forall (m :: * -> *).
MonadTypeChecker m =>
TypeDeclBase NoInfo Name -> m (TypeDeclBase Info VName, Liftedness)
checkTypeDecl TypeDeclBase NoInfo Name
vtype
        ([TypeParam], TypeDeclBase Info VName)
-> TypeM ([TypeParam], TypeDeclBase Info VName)
forall (m :: * -> *) a. Monad m => a -> m a
return ([TypeParam]
tparams', TypeDeclBase Info VName
vtype')

    Bool -> TypeM () -> TypeM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (StructType -> Bool
emptyDimParam (StructType -> Bool) -> StructType -> Bool
forall a b. (a -> b) -> a -> b
$ Info StructType -> StructType
forall a. Info a -> a
unInfo (Info StructType -> StructType) -> Info StructType -> StructType
forall a b. (a -> b) -> a -> b
$ TypeDeclBase Info VName -> Info StructType
forall (f :: * -> *) vn. TypeDeclBase f vn -> f StructType
expandedType TypeDeclBase Info VName
vtype') (TypeM () -> TypeM ()) -> TypeM () -> TypeM ()
forall a b. (a -> b) -> a -> b
$
      SrcLoc -> Notes -> Doc -> TypeM ()
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
"All function parameters must have non-anonymous sizes."
          Doc -> Doc -> Doc
</> Doc
"Hint: add size parameters to" Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (VName -> Doc
forall v. IsName v => v -> Doc
pprName VName
name') Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."

    let ([StructType]
params, StructType
_) = StructType -> ([StructType], StructType)
forall dim as.
TypeBase dim as -> ([TypeBase dim as], TypeBase dim as)
unfoldFunType (StructType -> ([StructType], StructType))
-> StructType -> ([StructType], StructType)
forall a b. (a -> b) -> a -> b
$ Info StructType -> StructType
forall a. Info a -> a
unInfo (Info StructType -> StructType) -> Info StructType -> StructType
forall a b. (a -> b) -> a -> b
$ TypeDeclBase Info VName -> Info StructType
forall (f :: * -> *) vn. TypeDeclBase f vn -> f StructType
expandedType TypeDeclBase Info VName
vtype'
    Bool -> TypeM () -> TypeM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([StructType] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [StructType]
params Bool -> Bool -> Bool
&& (TypeParamBase Name -> Bool) -> [TypeParamBase Name] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any TypeParamBase Name -> Bool
forall vn. TypeParamBase vn -> Bool
isSizeParam [TypeParamBase Name]
tparams) (TypeM () -> TypeM ()) -> TypeM () -> TypeM ()
forall a b. (a -> b) -> a -> b
$
      SrcLoc -> Notes -> Doc -> TypeM ()
forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc -> m a
typeError
        SrcLoc
loc
        Notes
forall a. Monoid a => a
mempty
        Doc
"Size parameters are only allowed on bindings that also have value parameters."

    let binding :: BoundV
binding = [TypeParam] -> StructType -> BoundV
BoundV [TypeParam]
tparams' (StructType -> BoundV) -> StructType -> BoundV
forall a b. (a -> b) -> a -> b
$ Info StructType -> StructType
forall a. Info a -> a
unInfo (Info StructType -> StructType) -> Info StructType -> StructType
forall a b. (a -> b) -> a -> b
$ TypeDeclBase Info VName -> Info StructType
forall (f :: * -> *) vn. TypeDeclBase f vn -> f StructType
expandedType TypeDeclBase Info VName
vtype'
        valenv :: Env
valenv =
          Env
forall a. Monoid a => a
mempty
            { envVtable :: Map VName BoundV
envVtable = VName -> BoundV -> Map VName BoundV
forall k a. k -> a -> Map k a
M.singleton VName
name' BoundV
binding,
              envNameMap :: NameMap
envNameMap = (Namespace, Name) -> QualName VName -> NameMap
forall k a. k -> a -> Map k a
M.singleton (Namespace
Term, Name
name) (QualName VName -> NameMap) -> QualName VName -> NameMap
forall a b. (a -> b) -> a -> b
$ VName -> QualName VName
forall v. v -> QualName v
qualName VName
name'
            }
    (TySet
abstypes, Env
env, [SpecBase Info VName]
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
    (TySet, Env, [SpecBase Info VName])
-> TypeM (TySet, Env, [SpecBase Info VName])
forall (m :: * -> *) a. Monad m => a -> m a
return
      ( TySet
abstypes,
        Env
env Env -> Env -> Env
forall a. Semigroup a => a -> a -> a
<> Env
valenv,
        VName
-> [TypeParam]
-> TypeDeclBase Info VName
-> Maybe DocComment
-> SrcLoc
-> SpecBase Info VName
forall (f :: * -> *) vn.
vn
-> [TypeParamBase vn]
-> TypeDeclBase f vn
-> Maybe DocComment
-> SrcLoc
-> SpecBase f vn
ValSpec VName
name' [TypeParam]
tparams' TypeDeclBase Info VName
vtype' Maybe DocComment
doc SrcLoc
loc SpecBase Info VName
-> [SpecBase Info VName] -> [SpecBase Info VName]
forall a. a -> [a] -> [a]
: [SpecBase Info VName]
specs'
      )
checkSpecs (TypeAbbrSpec TypeBindBase NoInfo Name
tdec : [SpecBase NoInfo Name]
specs) =
  [(Namespace, Name)]
-> TypeM (TySet, Env, [SpecBase Info VName])
-> TypeM (TySet, Env, [SpecBase Info VName])
forall (m :: * -> *) a.
MonadTypeChecker m =>
[(Namespace, Name)] -> m a -> m a
bindSpaced [(Namespace
Type, TypeBindBase NoInfo Name -> Name
forall (f :: * -> *) vn. TypeBindBase f vn -> vn
typeAlias TypeBindBase NoInfo Name
tdec)] (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
$ 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') <- 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
    (TySet, Env, [SpecBase Info VName])
-> TypeM (TySet, Env, [SpecBase Info VName])
forall (m :: * -> *) a. Monad m => a -> m a
return
      ( TySet
abstypes,
        Env
env Env -> Env -> Env
forall a. Semigroup a => a -> a -> a
<> Env
tenv,
        TypeBindBase Info VName -> SpecBase Info VName
forall (f :: * -> *) vn. TypeBindBase f vn -> SpecBase f vn
TypeAbbrSpec TypeBindBase Info VName
tdec' SpecBase Info VName
-> [SpecBase Info VName] -> [SpecBase Info VName]
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) =
  [TypeParamBase Name]
-> ([TypeParam] -> TypeM (TySet, Env, [SpecBase Info VName]))
-> TypeM (TySet, Env, [SpecBase Info VName])
forall (m :: * -> *) a.
MonadTypeChecker m =>
[TypeParamBase Name] -> ([TypeParam] -> m a) -> m a
checkTypeParams [TypeParamBase Name]
ps (([TypeParam] -> TypeM (TySet, Env, [SpecBase Info VName]))
 -> TypeM (TySet, Env, [SpecBase Info VName]))
-> ([TypeParam] -> TypeM (TySet, Env, [SpecBase Info VName]))
-> TypeM (TySet, Env, [SpecBase Info VName])
forall a b. (a -> b) -> a -> b
$ \[TypeParam]
ps' ->
    [(Namespace, Name)]
-> TypeM (TySet, Env, [SpecBase Info VName])
-> TypeM (TySet, Env, [SpecBase Info VName])
forall (m :: * -> *) a.
MonadTypeChecker m =>
[(Namespace, Name)] -> m a -> m a
bindSpaced [(Namespace
Type, Name
name)] (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
$ do
      VName
name' <- Namespace -> Name -> SrcLoc -> TypeM VName
forall (m :: * -> *).
MonadTypeChecker m =>
Namespace -> Name -> SrcLoc -> m VName
checkName Namespace
Type Name
name SrcLoc
loc
      let tenv :: Env
tenv =
            Env
forall a. Monoid a => a
mempty
              { envNameMap :: NameMap
envNameMap =
                  (Namespace, Name) -> QualName VName -> NameMap
forall k a. k -> a -> Map k a
M.singleton (Namespace
Type, Name
name) (QualName VName -> NameMap) -> QualName VName -> NameMap
forall a b. (a -> b) -> a -> b
$ VName -> QualName VName
forall v. v -> QualName v
qualName VName
name',
                envTypeTable :: Map VName TypeBinding
envTypeTable =
                  VName -> TypeBinding -> Map VName TypeBinding
forall k a. k -> a -> Map k a
M.singleton VName
name' (TypeBinding -> Map VName TypeBinding)
-> TypeBinding -> Map VName TypeBinding
forall a b. (a -> b) -> a -> b
$
                    Liftedness -> [TypeParam] -> StructType -> TypeBinding
TypeAbbr Liftedness
l [TypeParam]
ps' (StructType -> TypeBinding) -> StructType -> TypeBinding
forall a b. (a -> b) -> a -> b
$
                      ScalarTypeBase (DimDecl VName) () -> StructType
forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar (ScalarTypeBase (DimDecl VName) () -> StructType)
-> ScalarTypeBase (DimDecl VName) () -> StructType
forall a b. (a -> b) -> a -> b
$
                        ()
-> Uniqueness
-> TypeName
-> [TypeArg (DimDecl VName)]
-> ScalarTypeBase (DimDecl VName) ()
forall dim as.
as
-> Uniqueness -> TypeName -> [TypeArg dim] -> ScalarTypeBase dim as
TypeVar () Uniqueness
Nonunique (VName -> TypeName
typeName VName
name') ([TypeArg (DimDecl VName)] -> ScalarTypeBase (DimDecl VName) ())
-> [TypeArg (DimDecl VName)] -> ScalarTypeBase (DimDecl VName) ()
forall a b. (a -> b) -> a -> b
$
                          (TypeParam -> TypeArg (DimDecl VName))
-> [TypeParam] -> [TypeArg (DimDecl VName)]
forall a b. (a -> b) -> [a] -> [b]
map TypeParam -> TypeArg (DimDecl VName)
typeParamToArg [TypeParam]
ps'
              }
      (TySet
abstypes, Env
env, [SpecBase Info VName]
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
      (TySet, Env, [SpecBase Info VName])
-> TypeM (TySet, Env, [SpecBase Info VName])
forall (m :: * -> *) a. Monad m => a -> m a
return
        ( QualName VName -> Liftedness -> TySet -> TySet
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (VName -> QualName VName
forall v. v -> QualName v
qualName VName
name') Liftedness
l TySet
abstypes,
          Env
env Env -> Env -> Env
forall a. Semigroup a => a -> a -> a
<> Env
tenv,
          Liftedness
-> VName
-> [TypeParam]
-> Maybe DocComment
-> SrcLoc
-> SpecBase Info VName
forall (f :: * -> *) vn.
Liftedness
-> vn
-> [TypeParamBase vn]
-> Maybe DocComment
-> SrcLoc
-> SpecBase f vn
TypeSpec Liftedness
l VName
name' [TypeParam]
ps' Maybe DocComment
doc SrcLoc
loc SpecBase Info VName
-> [SpecBase Info VName] -> [SpecBase Info VName]
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) =
  [(Namespace, Name)]
-> TypeM (TySet, Env, [SpecBase Info VName])
-> TypeM (TySet, Env, [SpecBase Info VName])
forall (m :: * -> *) a.
MonadTypeChecker m =>
[(Namespace, Name)] -> m a -> m a
bindSpaced [(Namespace
Term, Name
name)] (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
$ do
    VName
name' <- Namespace -> Name -> SrcLoc -> TypeM VName
forall (m :: * -> *).
MonadTypeChecker m =>
Namespace -> Name -> SrcLoc -> m VName
checkName Namespace
Term Name
name SrcLoc
loc
    (MTy
mty, SigExpBase Info VName
sig') <- SigExpBase NoInfo Name -> TypeM (MTy, SigExpBase Info VName)
checkSigExp SigExpBase NoInfo Name
sig
    let senv :: Env
senv =
          Env
forall a. Monoid a => a
mempty
            { envNameMap :: NameMap
envNameMap = (Namespace, Name) -> QualName VName -> NameMap
forall k a. k -> a -> Map k a
M.singleton (Namespace
Term, Name
name) (QualName VName -> NameMap) -> QualName VName -> NameMap
forall a b. (a -> b) -> a -> b
$ VName -> QualName VName
forall v. v -> QualName v
qualName VName
name',
              envModTable :: Map VName Mod
envModTable = VName -> Mod -> Map VName Mod
forall k a. k -> a -> Map k a
M.singleton VName
name' (Mod -> Map VName Mod) -> Mod -> Map VName Mod
forall a b. (a -> b) -> a -> b
$ MTy -> Mod
mtyMod MTy
mty
            }
    (TySet
abstypes, Env
env, [SpecBase Info VName]
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
    (TySet, Env, [SpecBase Info VName])
-> TypeM (TySet, Env, [SpecBase Info VName])
forall (m :: * -> *) a. Monad m => a -> m a
return
      ( (QualName VName -> QualName VName) -> TySet -> TySet
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
M.mapKeys (VName -> QualName VName -> QualName VName
forall v. v -> QualName v -> QualName v
qualify VName
name') (MTy -> TySet
mtyAbs MTy
mty) TySet -> TySet -> TySet
forall a. Semigroup a => a -> a -> a
<> TySet
abstypes,
        Env
env Env -> Env -> Env
forall a. Semigroup a => a -> a -> a
<> Env
senv,
        VName
-> SigExpBase Info VName
-> Maybe DocComment
-> SrcLoc
-> SpecBase Info VName
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 SpecBase Info VName
-> [SpecBase Info VName] -> [SpecBase Info VName]
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, Env
e_env, SigExpBase Info VName
e') <- SigExpBase NoInfo Name -> TypeM (TySet, Env, SigExpBase Info VName)
checkSigExpToEnv SigExpBase NoInfo Name
e

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

  (TySet
abstypes, Env
env, [SpecBase Info VName]
specs') <- Env
-> TypeM (TySet, Env, [SpecBase Info VName])
-> TypeM (TySet, Env, [SpecBase Info VName])
forall a. Env -> TypeM a -> TypeM a
localEnv Env
e_env (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
  (TySet, Env, [SpecBase Info VName])
-> TypeM (TySet, Env, [SpecBase Info VName])
forall (m :: * -> *) a. Monad m => a -> m a
return
    ( TySet
abstypes TySet -> TySet -> TySet
forall a. Semigroup a => a -> a -> a
<> TySet
e_abs,
      Env
env Env -> Env -> Env
forall a. Semigroup a => a -> a -> a
<> Env
e_env,
      SigExpBase Info VName -> SrcLoc -> SpecBase Info VName
forall (f :: * -> *) vn. SigExpBase f vn -> SrcLoc -> SpecBase f vn
IncludeSpec SigExpBase Info VName
e' SrcLoc
loc SpecBase Info VName
-> [SpecBase Info VName] -> [SpecBase Info VName]
forall a. a -> [a] -> [a]
: [SpecBase Info VName]
specs'
    )
  where
    warnIfShadowing :: QualName Name -> m ()
warnIfShadowing QualName Name
qn =
      (SrcLoc
-> QualName Name
-> m (QualName VName, [TypeParam], StructType, Liftedness)
forall (m :: * -> *).
MonadTypeChecker m =>
SrcLoc
-> QualName Name
-> m (QualName VName, [TypeParam], StructType, Liftedness)
lookupType SrcLoc
loc QualName Name
qn m (QualName VName, [TypeParam], StructType, Liftedness)
-> m () -> m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> QualName Name -> m ()
forall (m :: * -> *) a. (MonadTypeChecker m, Pretty a) => a -> m ()
warnAbout QualName Name
qn)
        m () -> (e -> m ()) -> m ()
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \e
_ -> () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    warnAbout :: a -> m ()
warnAbout a
qn =
      SrcLoc -> 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
<+> Doc -> Doc
pquote (a -> Doc
forall a. Pretty a => a -> Doc
ppr a
qn) Doc -> Doc -> Doc
<+> Doc
"."

checkSigExp :: SigExpBase NoInfo Name -> TypeM (MTy, SigExpBase Info VName)
checkSigExp :: SigExpBase NoInfo Name -> TypeM (MTy, SigExpBase Info VName)
checkSigExp (SigParens SigExpBase NoInfo Name
e SrcLoc
loc) = do
  (MTy
mty, SigExpBase Info VName
e') <- SigExpBase NoInfo Name -> TypeM (MTy, SigExpBase Info VName)
checkSigExp SigExpBase NoInfo Name
e
  (MTy, SigExpBase Info VName) -> TypeM (MTy, SigExpBase Info VName)
forall (m :: * -> *) a. Monad m => a -> m a
return (MTy
mty, SigExpBase Info VName -> SrcLoc -> SigExpBase Info VName
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
  (MTy, SigExpBase Info VName) -> TypeM (MTy, SigExpBase Info VName)
forall (m :: * -> *) a. Monad m => a -> m a
return (MTy
mty', QualName VName
-> Info (Map VName VName) -> SrcLoc -> SigExpBase Info VName
forall (f :: * -> *) vn.
QualName vn -> f (Map VName VName) -> SrcLoc -> SigExpBase f vn
SigVar QualName VName
name' (Map VName VName -> Info (Map VName VName)
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
  (MTy, SigExpBase Info VName) -> TypeM (MTy, SigExpBase Info VName)
forall (m :: * -> *) a. Monad m => a -> m a
return (TySet -> Mod -> MTy
MTy TySet
abstypes (Mod -> MTy) -> Mod -> MTy
forall a b. (a -> b) -> a -> b
$ Env -> Mod
ModEnv Env
env, [SpecBase Info VName] -> SrcLoc -> SigExpBase Info VName
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 TypeDeclBase NoInfo Name
td SrcLoc
trloc) SrcLoc
loc) = do
  (TySet
s_abs, Env
s_env, SigExpBase Info VName
s') <- SigExpBase NoInfo Name -> TypeM (TySet, Env, SigExpBase Info VName)
checkSigExpToEnv SigExpBase NoInfo Name
s
  [TypeParamBase Name]
-> ([TypeParam] -> TypeM (MTy, SigExpBase Info VName))
-> TypeM (MTy, SigExpBase Info VName)
forall (m :: * -> *) a.
MonadTypeChecker m =>
[TypeParamBase Name] -> ([TypeParam] -> m a) -> m a
checkTypeParams [TypeParamBase Name]
ps (([TypeParam] -> TypeM (MTy, SigExpBase Info VName))
 -> TypeM (MTy, SigExpBase Info VName))
-> ([TypeParam] -> TypeM (MTy, SigExpBase Info VName))
-> TypeM (MTy, SigExpBase Info VName)
forall a b. (a -> b) -> a -> b
$ \[TypeParam]
ps' -> do
    (TypeDeclBase Info VName
td', Liftedness
_) <- [TypeParam]
-> TypeM (TypeDeclBase Info VName, Liftedness)
-> TypeM (TypeDeclBase Info VName, Liftedness)
forall a. [TypeParam] -> TypeM a -> TypeM a
bindingTypeParams [TypeParam]
ps' (TypeM (TypeDeclBase Info VName, Liftedness)
 -> TypeM (TypeDeclBase Info VName, Liftedness))
-> TypeM (TypeDeclBase Info VName, Liftedness)
-> TypeM (TypeDeclBase Info VName, Liftedness)
forall a b. (a -> b) -> a -> b
$ TypeDeclBase NoInfo Name
-> TypeM (TypeDeclBase Info VName, Liftedness)
forall (m :: * -> *).
MonadTypeChecker m =>
TypeDeclBase NoInfo Name -> m (TypeDeclBase Info VName, Liftedness)
checkTypeDecl TypeDeclBase NoInfo Name
td
    (QualName VName
tname', TySet
s_abs', Env
s_env') <- SrcLoc
-> TySet
-> Env
-> QualName Name
-> [TypeParam]
-> StructType
-> TypeM (QualName VName, TySet, Env)
refineEnv SrcLoc
loc TySet
s_abs Env
s_env QualName Name
tname [TypeParam]
ps' (StructType -> TypeM (QualName VName, TySet, Env))
-> StructType -> TypeM (QualName VName, TySet, Env)
forall a b. (a -> b) -> a -> b
$ Info StructType -> StructType
forall a. Info a -> a
unInfo (Info StructType -> StructType) -> Info StructType -> StructType
forall a b. (a -> b) -> a -> b
$ TypeDeclBase Info VName -> Info StructType
forall (f :: * -> *) vn. TypeDeclBase f vn -> f StructType
expandedType TypeDeclBase Info VName
td'
    (MTy, SigExpBase Info VName) -> TypeM (MTy, SigExpBase Info VName)
forall (m :: * -> *) a. Monad m => a -> m a
return (TySet -> Mod -> MTy
MTy TySet
s_abs' (Mod -> MTy) -> Mod -> MTy
forall a b. (a -> b) -> a -> b
$ Env -> Mod
ModEnv Env
s_env', SigExpBase Info VName
-> TypeRefBase Info VName -> SrcLoc -> SigExpBase Info VName
forall (f :: * -> *) vn.
SigExpBase f vn -> TypeRefBase f vn -> SrcLoc -> SigExpBase f vn
SigWith SigExpBase Info VName
s' (QualName VName
-> [TypeParam]
-> TypeDeclBase Info VName
-> SrcLoc
-> TypeRefBase Info VName
forall (f :: * -> *) vn.
QualName vn
-> [TypeParamBase vn]
-> TypeDeclBase f vn
-> SrcLoc
-> TypeRefBase f vn
TypeRef QualName VName
tname' [TypeParam]
ps' TypeDeclBase Info VName
td' SrcLoc
trloc) SrcLoc
loc)
checkSigExp (SigArrow Maybe Name
maybe_pname SigExpBase NoInfo Name
e1 SigExpBase NoInfo Name
e2 SrcLoc
loc) = do
  (MTy TySet
s_abs Mod
e1_mod, SigExpBase Info VName
e1') <- SigExpBase NoInfo Name -> TypeM (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 -> [(Namespace, Name)]
-> TypeM (Env, Maybe VName) -> TypeM (Env, Maybe VName)
forall (m :: * -> *) a.
MonadTypeChecker m =>
[(Namespace, Name)] -> m a -> m a
bindSpaced [(Namespace
Term, Name
pname)] (TypeM (Env, Maybe VName) -> TypeM (Env, Maybe VName))
-> TypeM (Env, Maybe VName) -> TypeM (Env, Maybe VName)
forall a b. (a -> b) -> a -> b
$ do
        VName
pname' <- Namespace -> Name -> SrcLoc -> TypeM VName
forall (m :: * -> *).
MonadTypeChecker m =>
Namespace -> Name -> SrcLoc -> m VName
checkName Namespace
Term Name
pname SrcLoc
loc
        (Env, Maybe VName) -> TypeM (Env, Maybe VName)
forall (m :: * -> *) a. Monad m => a -> m a
return
          ( Env
forall a. Monoid a => a
mempty
              { envNameMap :: NameMap
envNameMap = (Namespace, Name) -> QualName VName -> NameMap
forall k a. k -> a -> Map k a
M.singleton (Namespace
Term, Name
pname) (QualName VName -> NameMap) -> QualName VName -> NameMap
forall a b. (a -> b) -> a -> b
$ VName -> QualName VName
forall v. v -> QualName v
qualName VName
pname',
                envModTable :: Map VName Mod
envModTable = VName -> Mod -> Map VName Mod
forall k a. k -> a -> Map k a
M.singleton VName
pname' Mod
e1_mod
              },
            VName -> Maybe VName
forall a. a -> Maybe a
Just VName
pname'
          )
      Maybe Name
Nothing ->
        (Env, Maybe VName) -> TypeM (Env, Maybe VName)
forall (m :: * -> *) a. Monad m => a -> m a
return (Env
forall a. Monoid a => a
mempty, Maybe VName
forall a. Maybe a
Nothing)
  (MTy
e2_mod, SigExpBase Info VName
e2') <- Env
-> TypeM (MTy, SigExpBase Info VName)
-> TypeM (MTy, SigExpBase Info VName)
forall a. Env -> TypeM a -> TypeM a
localEnv Env
env_for_e2 (TypeM (MTy, SigExpBase Info VName)
 -> TypeM (MTy, SigExpBase Info VName))
-> TypeM (MTy, SigExpBase Info VName)
-> TypeM (MTy, SigExpBase Info VName)
forall a b. (a -> b) -> a -> b
$ SigExpBase NoInfo Name -> TypeM (MTy, SigExpBase Info VName)
checkSigExp SigExpBase NoInfo Name
e2
  (MTy, SigExpBase Info VName) -> TypeM (MTy, SigExpBase Info VName)
forall (m :: * -> *) a. Monad m => a -> m a
return
    ( TySet -> Mod -> MTy
MTy TySet
forall a. Monoid a => a
mempty (Mod -> MTy) -> Mod -> MTy
forall a b. (a -> b) -> a -> b
$ FunSig -> Mod
ModFun (FunSig -> Mod) -> FunSig -> Mod
forall a b. (a -> b) -> a -> b
$ TySet -> Mod -> MTy -> FunSig
FunSig TySet
s_abs Mod
e1_mod MTy
e2_mod,
      Maybe VName
-> SigExpBase Info VName
-> SigExpBase Info VName
-> SrcLoc
-> SigExpBase Info VName
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, Env, SigExpBase Info VName)
checkSigExpToEnv :: SigExpBase NoInfo Name -> TypeM (TySet, Env, SigExpBase Info VName)
checkSigExpToEnv SigExpBase NoInfo Name
e = do
  (MTy TySet
abs Mod
mod, SigExpBase Info VName
e') <- SigExpBase NoInfo Name -> TypeM (MTy, SigExpBase Info VName)
checkSigExp SigExpBase NoInfo Name
e
  case Mod
mod of
    ModEnv Env
env -> (TySet, Env, SigExpBase Info VName)
-> TypeM (TySet, Env, SigExpBase Info VName)
forall (m :: * -> *) a. Monad m => a -> m a
return (TySet
abs, Env
env, SigExpBase Info VName
e')
    ModFun {} -> SrcLoc -> TypeM (TySet, Env, SigExpBase Info VName)
forall (m :: * -> *) a. MonadTypeChecker m => SrcLoc -> m a
unappliedFunctor (SrcLoc -> TypeM (TySet, Env, SigExpBase Info VName))
-> SrcLoc -> TypeM (TySet, Env, SigExpBase Info VName)
forall a b. (a -> b) -> a -> b
$ SigExpBase NoInfo Name -> SrcLoc
forall a. Located a => a -> SrcLoc
srclocOf SigExpBase NoInfo Name
e

checkSigBind :: SigBindBase NoInfo Name -> TypeM (Env, SigBindBase Info VName)
checkSigBind :: SigBindBase NoInfo Name -> TypeM (Env, SigBindBase Info VName)
checkSigBind (SigBind Name
name SigExpBase NoInfo Name
e Maybe DocComment
doc SrcLoc
loc) = do
  (MTy
env, SigExpBase Info VName
e') <- SigExpBase NoInfo Name -> TypeM (MTy, SigExpBase Info VName)
checkSigExp SigExpBase NoInfo Name
e
  [(Namespace, Name)]
-> TypeM (Env, SigBindBase Info VName)
-> TypeM (Env, SigBindBase Info VName)
forall (m :: * -> *) a.
MonadTypeChecker m =>
[(Namespace, Name)] -> m a -> m a
bindSpaced [(Namespace
Signature, Name
name)] (TypeM (Env, SigBindBase Info VName)
 -> TypeM (Env, SigBindBase Info VName))
-> TypeM (Env, SigBindBase Info VName)
-> TypeM (Env, SigBindBase Info VName)
forall a b. (a -> b) -> a -> b
$ do
    VName
name' <- Namespace -> Name -> SrcLoc -> TypeM VName
forall (m :: * -> *).
MonadTypeChecker m =>
Namespace -> Name -> SrcLoc -> m VName
checkName Namespace
Signature Name
name SrcLoc
loc
    (Env, SigBindBase Info VName)
-> TypeM (Env, SigBindBase Info VName)
forall (m :: * -> *) a. Monad m => a -> m a
return
      ( Env
forall a. Monoid a => a
mempty
          { envSigTable :: Map VName MTy
envSigTable = VName -> MTy -> Map VName MTy
forall k a. k -> a -> Map k a
M.singleton VName
name' MTy
env,
            envNameMap :: NameMap
envNameMap = (Namespace, Name) -> QualName VName -> NameMap
forall k a. k -> a -> Map k a
M.singleton (Namespace
Signature, Name
name) (VName -> QualName VName
forall v. v -> QualName v
qualName VName
name')
          },
        VName
-> SigExpBase Info VName
-> Maybe DocComment
-> SrcLoc
-> SigBindBase Info VName
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 (MTy, ModExpBase Info VName)
checkOneModExp :: ModExpBase NoInfo Name -> TypeM (MTy, ModExpBase Info VName)
checkOneModExp (ModParens ModExpBase NoInfo Name
e SrcLoc
loc) = do
  (MTy
mty, ModExpBase Info VName
e') <- ModExpBase NoInfo Name -> TypeM (MTy, ModExpBase Info VName)
checkOneModExp ModExpBase NoInfo Name
e
  (MTy, ModExpBase Info VName) -> TypeM (MTy, ModExpBase Info VName)
forall (m :: * -> *) a. Monad m => a -> m a
return (MTy
mty, ModExpBase Info VName -> SrcLoc -> ModExpBase Info VName
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') <- [UncheckedDec] -> TypeM (TySet, Env, [Dec])
checkDecs [UncheckedDec]
decs
  (MTy, ModExpBase Info VName) -> TypeM (MTy, ModExpBase Info VName)
forall (m :: * -> *) a. Monad m => a -> m a
return
    ( TySet -> Mod -> MTy
MTy TySet
abstypes (Mod -> MTy) -> Mod -> MTy
forall a b. (a -> b) -> a -> b
$ Env -> Mod
ModEnv Env
env,
      [Dec] -> SrcLoc -> ModExpBase Info VName
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) <- SrcLoc -> QualName Name -> TypeM (QualName VName, Mod)
forall (m :: * -> *).
MonadTypeChecker m =>
SrcLoc -> QualName Name -> m (QualName VName, Mod)
lookupMod SrcLoc
loc QualName Name
v
  Bool -> TypeM () -> TypeM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when
    ( VName -> Name
baseName (QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
v') Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
nameFromString String
"intrinsics"
        Bool -> Bool -> Bool
&& VName -> Int
baseTag (QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
v') Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
maxIntrinsicTag
    )
    (TypeM () -> TypeM ()) -> TypeM () -> TypeM ()
forall a b. (a -> b) -> a -> b
$ SrcLoc -> Notes -> Doc -> TypeM ()
forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc -> m a
typeError SrcLoc
loc Notes
forall a. Monoid a => a
mempty Doc
"The 'intrinsics' module may not be used in module expressions."
  (MTy, ModExpBase Info VName) -> TypeM (MTy, ModExpBase Info VName)
forall (m :: * -> *) a. Monad m => a -> m a
return (TySet -> Mod -> MTy
MTy TySet
forall a. Monoid a => a
mempty Mod
env, QualName VName -> SrcLoc -> ModExpBase Info VName
forall (f :: * -> *) vn. QualName vn -> SrcLoc -> ModExpBase f vn
ModVar QualName VName
v' SrcLoc
loc)
checkOneModExp (ModImport String
name NoInfo String
NoInfo SrcLoc
loc) = do
  (String
name', Env
env) <- SrcLoc -> String -> TypeM (String, Env)
lookupImport SrcLoc
loc String
name
  (MTy, ModExpBase Info VName) -> TypeM (MTy, ModExpBase Info VName)
forall (m :: * -> *) a. Monad m => a -> m a
return
    ( TySet -> Mod -> MTy
MTy TySet
forall a. Monoid a => a
mempty (Mod -> MTy) -> Mod -> MTy
forall a b. (a -> b) -> a -> b
$ Env -> Mod
ModEnv Env
env,
      String -> Info String -> SrcLoc -> ModExpBase Info VName
forall (f :: * -> *) vn.
String -> f String -> SrcLoc -> ModExpBase f vn
ModImport String
name (String -> Info String
forall a. a -> Info a
Info String
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
  (MTy
f_mty, ModExpBase Info VName
f') <- ModExpBase NoInfo Name -> TypeM (MTy, ModExpBase Info VName)
checkOneModExp ModExpBase NoInfo Name
f
  case MTy -> Mod
mtyMod MTy
f_mty of
    ModFun FunSig
functor -> do
      (MTy
e_mty, ModExpBase Info VName
e') <- ModExpBase NoInfo Name -> TypeM (MTy, ModExpBase Info VName)
checkOneModExp ModExpBase NoInfo Name
e
      (MTy
mty, Map VName VName
psubsts, Map VName VName
rsubsts) <- SrcLoc
-> FunSig -> MTy -> TypeM (MTy, Map VName VName, Map VName VName)
applyFunctor SrcLoc
loc FunSig
functor MTy
e_mty
      (MTy, ModExpBase Info VName) -> TypeM (MTy, ModExpBase Info VName)
forall (m :: * -> *) a. Monad m => a -> m a
return (MTy
mty, ModExpBase Info VName
-> ModExpBase Info VName
-> Info (Map VName VName)
-> Info (Map VName VName)
-> SrcLoc
-> ModExpBase Info VName
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' (Map VName VName -> Info (Map VName VName)
forall a. a -> Info a
Info Map VName VName
psubsts) (Map VName VName -> Info (Map VName VName)
forall a. a -> Info a
Info Map VName VName
rsubsts) SrcLoc
loc)
    Mod
_ ->
      SrcLoc -> Notes -> Doc -> TypeM (MTy, ModExpBase Info VName)
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 SigExpBase NoInfo Name
se NoInfo (Map VName VName)
NoInfo SrcLoc
loc) = do
  (MTy
me_mod, ModExpBase Info VName
me') <- ModExpBase NoInfo Name -> TypeM (MTy, ModExpBase Info VName)
checkOneModExp ModExpBase NoInfo Name
me
  (MTy
se_mty, SigExpBase Info VName
se') <- SigExpBase NoInfo Name -> TypeM (MTy, SigExpBase Info VName)
checkSigExp SigExpBase NoInfo Name
se
  Map VName VName
match_subst <- Either TypeError (Map VName VName) -> TypeM (Map VName VName)
forall a. Either TypeError a -> TypeM a
badOnLeft (Either TypeError (Map VName VName) -> TypeM (Map VName VName))
-> Either TypeError (Map VName VName) -> TypeM (Map VName VName)
forall a b. (a -> b) -> a -> b
$ MTy -> MTy -> SrcLoc -> Either TypeError (Map VName VName)
matchMTys MTy
me_mod MTy
se_mty SrcLoc
loc
  (MTy, ModExpBase Info VName) -> TypeM (MTy, ModExpBase Info VName)
forall (m :: * -> *) a. Monad m => a -> m a
return (MTy
se_mty, ModExpBase Info VName
-> SigExpBase Info VName
-> Info (Map VName VName)
-> SrcLoc
-> ModExpBase Info VName
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' (Map VName VName -> Info (Map VName VName)
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) =
  ModParamBase NoInfo Name
-> (ModParamBase Info VName
    -> TySet -> Mod -> TypeM (MTy, ModExpBase Info VName))
-> TypeM (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 (MTy, ModExpBase Info VName))
 -> TypeM (MTy, ModExpBase Info VName))
-> (ModParamBase Info VName
    -> TySet -> Mod -> TypeM (MTy, ModExpBase Info VName))
-> TypeM (MTy, ModExpBase Info VName)
forall a b. (a -> b) -> a -> b
$ \ModParamBase Info VName
param' TySet
param_abs Mod
param_mod -> do
    (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
     (Maybe (SigExpBase Info VName, Info (Map VName VName)),
      ModExpBase Info VName, MTy)
checkModBody ((SigExpBase NoInfo Name, NoInfo (Map VName VName))
-> SigExpBase NoInfo Name
forall a b. (a, b) -> a
fst ((SigExpBase NoInfo Name, NoInfo (Map VName VName))
 -> SigExpBase NoInfo Name)
-> Maybe (SigExpBase NoInfo Name, NoInfo (Map VName VName))
-> Maybe (SigExpBase NoInfo Name)
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
    (MTy, ModExpBase Info VName) -> TypeM (MTy, ModExpBase Info VName)
forall (m :: * -> *) a. Monad m => a -> m a
return
      ( TySet -> Mod -> MTy
MTy TySet
forall a. Monoid a => a
mempty (Mod -> MTy) -> Mod -> MTy
forall a b. (a -> b) -> a -> b
$ FunSig -> Mod
ModFun (FunSig -> Mod) -> FunSig -> Mod
forall a b. (a -> b) -> a -> b
$ TySet -> Mod -> MTy -> FunSig
FunSig TySet
param_abs Mod
param_mod MTy
mty,
        ModParamBase Info VName
-> Maybe (SigExpBase Info VName, Info (Map VName VName))
-> ModExpBase Info VName
-> SrcLoc
-> ModExpBase Info VName
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
  (MTy TySet
abs Mod
mod, ModExpBase Info VName
e') <- ModExpBase NoInfo Name -> TypeM (MTy, ModExpBase Info VName)
checkOneModExp ModExpBase NoInfo Name
e
  case Mod
mod of
    ModEnv Env
env -> (TySet, Env, ModExpBase Info VName)
-> TypeM (TySet, Env, ModExpBase Info VName)
forall (m :: * -> *) a. Monad m => a -> m a
return (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 :: 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
  (MTy TySet
p_abs Mod
p_mod, SigExpBase Info VName
psig_e') <- SigExpBase NoInfo Name -> TypeM (MTy, SigExpBase Info VName)
checkSigExp SigExpBase NoInfo Name
psig_e
  [(Namespace, Name)] -> TypeM a -> TypeM a
forall (m :: * -> *) a.
MonadTypeChecker m =>
[(Namespace, Name)] -> m a -> m a
bindSpaced [(Namespace
Term, Name
pname)] (TypeM a -> TypeM a) -> TypeM a -> TypeM a
forall a b. (a -> b) -> a -> b
$ do
    VName
pname' <- Namespace -> Name -> SrcLoc -> TypeM VName
forall (m :: * -> *).
MonadTypeChecker m =>
Namespace -> Name -> SrcLoc -> m VName
checkName Namespace
Term Name
pname SrcLoc
loc
    let in_body_env :: Env
in_body_env = Env
forall a. Monoid a => a
mempty {envModTable :: Map VName Mod
envModTable = VName -> Mod -> Map VName Mod
forall k a. k -> a -> Map k a
M.singleton VName
pname' Mod
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
-> SigExpBase Info VName
-> Info [VName]
-> SrcLoc
-> ModParamBase Info VName
forall (f :: * -> *) vn.
vn -> SigExpBase f vn -> f [VName] -> SrcLoc -> ModParamBase f vn
ModParam VName
pname' SigExpBase 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 :: [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 (SigExpBase NoInfo Name) ->
  ModExpBase NoInfo Name ->
  SrcLoc ->
  TypeM
    ( Maybe (SigExp, Info (M.Map VName VName)),
      ModExp,
      MTy
    )
checkModBody :: Maybe (SigExpBase NoInfo Name)
-> ModExpBase NoInfo Name
-> SrcLoc
-> TypeM
     (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 = do
  (MTy
body_mty, ModExpBase Info VName
body_e') <- ModExpBase NoInfo Name -> TypeM (MTy, ModExpBase Info VName)
checkOneModExp ModExpBase NoInfo Name
body_e
  case Maybe (SigExpBase NoInfo Name)
maybe_fsig_e of
    Maybe (SigExpBase NoInfo Name)
Nothing ->
      (Maybe (SigExpBase Info VName, Info (Map VName VName)),
 ModExpBase Info VName, MTy)
-> TypeM
     (Maybe (SigExpBase Info VName, Info (Map VName VName)),
      ModExpBase Info VName, MTy)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (SigExpBase Info VName, Info (Map VName VName))
forall a. Maybe a
Nothing, ModExpBase Info VName
body_e', MTy
body_mty)
    Just SigExpBase NoInfo Name
fsig_e -> do
      (MTy
fsig_mty, SigExpBase Info VName
fsig_e') <- SigExpBase NoInfo Name -> TypeM (MTy, SigExpBase Info VName)
checkSigExp SigExpBase NoInfo Name
fsig_e
      Map VName VName
fsig_subst <- Either TypeError (Map VName VName) -> TypeM (Map VName VName)
forall a. Either TypeError a -> TypeM a
badOnLeft (Either TypeError (Map VName VName) -> TypeM (Map VName VName))
-> Either TypeError (Map VName VName) -> TypeM (Map VName VName)
forall a b. (a -> b) -> a -> b
$ MTy -> MTy -> SrcLoc -> Either TypeError (Map VName VName)
matchMTys MTy
body_mty MTy
fsig_mty SrcLoc
loc
      (Maybe (SigExpBase Info VName, Info (Map VName VName)),
 ModExpBase Info VName, MTy)
-> TypeM
     (Maybe (SigExpBase Info VName, Info (Map VName VName)),
      ModExpBase Info VName, MTy)
forall (m :: * -> *) a. Monad m => a -> m a
return ((SigExpBase Info VName, Info (Map VName VName))
-> Maybe (SigExpBase Info VName, Info (Map VName VName))
forall a. a -> Maybe a
Just (SigExpBase Info VName
fsig_e', Map VName VName -> Info (Map VName VName)
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
  (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
     (Maybe (SigExpBase Info VName, Info (Map VName VName)),
      ModExpBase Info VName, MTy)
checkModBody ((SigExpBase NoInfo Name, NoInfo (Map VName VName))
-> SigExpBase NoInfo Name
forall a b. (a, b) -> a
fst ((SigExpBase NoInfo Name, NoInfo (Map VName VName))
 -> SigExpBase NoInfo Name)
-> Maybe (SigExpBase NoInfo Name, NoInfo (Map VName VName))
-> Maybe (SigExpBase NoInfo Name)
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
  [(Namespace, Name)]
-> TypeM (TySet, Env, ModBindBase Info VName)
-> TypeM (TySet, Env, ModBindBase Info VName)
forall (m :: * -> *) a.
MonadTypeChecker m =>
[(Namespace, Name)] -> m a -> m a
bindSpaced [(Namespace
Term, Name
name)] (TypeM (TySet, Env, ModBindBase Info VName)
 -> TypeM (TySet, Env, ModBindBase Info VName))
-> TypeM (TySet, Env, ModBindBase Info VName)
-> TypeM (TySet, Env, ModBindBase Info VName)
forall a b. (a -> b) -> a -> b
$ do
    VName
name' <- Namespace -> Name -> SrcLoc -> TypeM VName
forall (m :: * -> *).
MonadTypeChecker m =>
Namespace -> Name -> SrcLoc -> m VName
checkName Namespace
Term Name
name SrcLoc
loc
    (TySet, Env, ModBindBase Info VName)
-> TypeM (TySet, Env, ModBindBase Info VName)
forall (m :: * -> *) a. Monad m => a -> m a
return
      ( MTy -> TySet
mtyAbs MTy
mty,
        Env
forall a. Monoid a => a
mempty
          { envModTable :: Map VName Mod
envModTable = VName -> Mod -> Map VName Mod
forall k a. k -> a -> Map k a
M.singleton VName
name' (Mod -> Map VName Mod) -> Mod -> Map VName Mod
forall a b. (a -> b) -> a -> b
$ MTy -> Mod
mtyMod MTy
mty,
            envNameMap :: NameMap
envNameMap = (Namespace, Name) -> QualName VName -> NameMap
forall k a. k -> a -> Map k a
M.singleton (Namespace
Term, Name
name) (QualName VName -> NameMap) -> QualName VName -> NameMap
forall a b. (a -> b) -> a -> b
$ VName -> QualName VName
forall v. v -> QualName v
qualName VName
name'
          },
        VName
-> [ModParamBase Info VName]
-> Maybe (SigExpBase Info VName, Info (Map VName VName))
-> ModExpBase Info VName
-> Maybe DocComment
-> SrcLoc
-> ModBindBase Info VName
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
  ([ModParamBase Info VName]
params', Maybe (SigExpBase Info VName, Info (Map VName VName))
maybe_fsig_e', ModExpBase Info VName
body_e', FunSig
funsig) <-
    ModParamBase NoInfo Name
-> (ModParamBase Info VName
    -> TySet
    -> Mod
    -> TypeM
         ([ModParamBase Info VName],
          Maybe (SigExpBase Info VName, Info (Map VName VName)),
          ModExpBase Info VName, FunSig))
-> TypeM
     ([ModParamBase Info VName],
      Maybe (SigExpBase Info VName, Info (Map VName VName)),
      ModExpBase Info VName, FunSig)
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
       ([ModParamBase Info VName],
        Maybe (SigExpBase Info VName, Info (Map VName VName)),
        ModExpBase Info VName, FunSig))
 -> TypeM
      ([ModParamBase Info VName],
       Maybe (SigExpBase Info VName, Info (Map VName VName)),
       ModExpBase Info VName, FunSig))
-> (ModParamBase Info VName
    -> TySet
    -> Mod
    -> TypeM
         ([ModParamBase Info VName],
          Maybe (SigExpBase Info VName, Info (Map VName VName)),
          ModExpBase Info VName, FunSig))
-> TypeM
     ([ModParamBase Info VName],
      Maybe (SigExpBase Info VName, Info (Map VName VName)),
      ModExpBase Info VName, FunSig)
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
         ([ModParamBase Info VName],
          Maybe (SigExpBase Info VName, Info (Map VName VName)),
          ModExpBase Info VName, FunSig))
-> TypeM
     ([ModParamBase Info VName],
      Maybe (SigExpBase Info VName, Info (Map VName VName)),
      ModExpBase Info VName, FunSig)
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
       ([ModParamBase Info VName],
        Maybe (SigExpBase Info VName, Info (Map VName VName)),
        ModExpBase Info VName, FunSig))
 -> TypeM
      ([ModParamBase Info VName],
       Maybe (SigExpBase Info VName, Info (Map VName VName)),
       ModExpBase Info VName, FunSig))
-> ([(ModParamBase Info VName, TySet, Mod)]
    -> TypeM
         ([ModParamBase Info VName],
          Maybe (SigExpBase Info VName, Info (Map VName VName)),
          ModExpBase Info VName, FunSig))
-> TypeM
     ([ModParamBase Info VName],
      Maybe (SigExpBase Info VName, Info (Map VName VName)),
      ModExpBase Info VName, FunSig)
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
        (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
     (Maybe (SigExpBase Info VName, Info (Map VName VName)),
      ModExpBase Info VName, MTy)
checkModBody ((SigExpBase NoInfo Name, NoInfo (Map VName VName))
-> SigExpBase NoInfo Name
forall a b. (a, b) -> a
fst ((SigExpBase NoInfo Name, NoInfo (Map VName VName))
 -> SigExpBase NoInfo Name)
-> Maybe (SigExpBase NoInfo Name, NoInfo (Map VName VName))
-> Maybe (SigExpBase NoInfo Name)
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 TySet
forall a. Monoid a => a
mempty (Mod -> MTy) -> Mod -> MTy
forall a b. (a -> b) -> a -> b
$ FunSig -> Mod
ModFun (FunSig -> Mod) -> FunSig -> Mod
forall a b. (a -> b) -> a -> b
$ TySet -> Mod -> MTy -> FunSig
FunSig TySet
x Mod
y MTy
mty'
        ([ModParamBase Info VName],
 Maybe (SigExpBase Info VName, Info (Map VName VName)),
 ModExpBase Info VName, FunSig)
-> TypeM
     ([ModParamBase Info VName],
      Maybe (SigExpBase Info VName, Info (Map VName VName)),
      ModExpBase Info VName, FunSig)
forall (m :: * -> *) a. Monad m => a -> m a
return
          ( ModParamBase Info VName
p' ModParamBase Info VName
-> [ModParamBase Info VName] -> [ModParamBase Info VName]
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 (MTy -> FunSig) -> MTy -> FunSig
forall a b. (a -> b) -> a -> b
$ ((TySet, Mod) -> MTy -> MTy) -> MTy -> [(TySet, Mod)] -> MTy
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (TySet, Mod) -> MTy -> MTy
addParam MTy
mty ([(TySet, Mod)] -> MTy) -> [(TySet, Mod)] -> MTy
forall a b. (a -> b) -> a -> b
$ [TySet] -> [Mod] -> [(TySet, Mod)]
forall a b. [a] -> [b] -> [(a, b)]
zip [TySet]
ps_abs [Mod]
ps_mod
          )
  [(Namespace, Name)]
-> TypeM (TySet, Env, ModBindBase Info VName)
-> TypeM (TySet, Env, ModBindBase Info VName)
forall (m :: * -> *) a.
MonadTypeChecker m =>
[(Namespace, Name)] -> m a -> m a
bindSpaced [(Namespace
Term, Name
name)] (TypeM (TySet, Env, ModBindBase Info VName)
 -> TypeM (TySet, Env, ModBindBase Info VName))
-> TypeM (TySet, Env, ModBindBase Info VName)
-> TypeM (TySet, Env, ModBindBase Info VName)
forall a b. (a -> b) -> a -> b
$ do
    VName
name' <- Namespace -> Name -> SrcLoc -> TypeM VName
forall (m :: * -> *).
MonadTypeChecker m =>
Namespace -> Name -> SrcLoc -> m VName
checkName Namespace
Term Name
name SrcLoc
loc
    (TySet, Env, ModBindBase Info VName)
-> TypeM (TySet, Env, ModBindBase Info VName)
forall (m :: * -> *) a. Monad m => a -> m a
return
      ( TySet
forall a. Monoid a => a
mempty,
        Env
forall a. Monoid a => a
mempty
          { envModTable :: Map VName Mod
envModTable =
              VName -> Mod -> Map VName Mod
forall k a. k -> a -> Map k a
M.singleton VName
name' (Mod -> Map VName Mod) -> Mod -> Map VName Mod
forall a b. (a -> b) -> a -> b
$ FunSig -> Mod
ModFun FunSig
funsig,
            envNameMap :: NameMap
envNameMap =
              (Namespace, Name) -> QualName VName -> NameMap
forall k a. k -> a -> Map k a
M.singleton (Namespace
Term, Name
name) (QualName VName -> NameMap) -> QualName VName -> NameMap
forall a b. (a -> b) -> a -> b
$ VName -> QualName VName
forall v. v -> QualName v
qualName VName
name'
          },
        VName
-> [ModParamBase Info VName]
-> Maybe (SigExpBase Info VName, Info (Map VName VName))
-> ModExpBase Info VName
-> Maybe DocComment
-> SrcLoc
-> ModBindBase Info VName
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 =
  (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 (m :: * -> *) a. Monad m => a -> m a
return (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]
_ TypeDeclBase 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 (TypeAbbrSpec (TypeBind Name
name Liftedness
_ [TypeParamBase Name]
_ TypeDeclBase 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
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 SigExpBase 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 (m :: * -> *) a. Monad m => a -> m a
return

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 TypeDeclBase NoInfo Name
td Maybe DocComment
doc SrcLoc
loc) =
  [TypeParamBase Name]
-> ([TypeParam] -> TypeM (Env, TypeBindBase Info VName))
-> TypeM (Env, TypeBindBase Info VName)
forall (m :: * -> *) a.
MonadTypeChecker m =>
[TypeParamBase Name] -> ([TypeParam] -> m a) -> m a
checkTypeParams [TypeParamBase Name]
tps (([TypeParam] -> TypeM (Env, TypeBindBase Info VName))
 -> TypeM (Env, TypeBindBase Info VName))
-> ([TypeParam] -> TypeM (Env, TypeBindBase Info VName))
-> TypeM (Env, TypeBindBase Info VName)
forall a b. (a -> b) -> a -> b
$ \[TypeParam]
tps' -> do
    (TypeDeclBase Info VName
td', Liftedness
l') <- [TypeParam]
-> TypeM (TypeDeclBase Info VName, Liftedness)
-> TypeM (TypeDeclBase Info VName, Liftedness)
forall a. [TypeParam] -> TypeM a -> TypeM a
bindingTypeParams [TypeParam]
tps' (TypeM (TypeDeclBase Info VName, Liftedness)
 -> TypeM (TypeDeclBase Info VName, Liftedness))
-> TypeM (TypeDeclBase Info VName, Liftedness)
-> TypeM (TypeDeclBase Info VName, Liftedness)
forall a b. (a -> b) -> a -> b
$ TypeDeclBase NoInfo Name
-> TypeM (TypeDeclBase Info VName, Liftedness)
forall (m :: * -> *).
MonadTypeChecker m =>
TypeDeclBase NoInfo Name -> m (TypeDeclBase Info VName, Liftedness)
checkTypeDecl TypeDeclBase NoInfo Name
td

    let used_dims :: Set VName
used_dims = StructType -> Set VName
forall als. TypeBase (DimDecl VName) als -> Set VName
typeDimNames (StructType -> Set VName) -> StructType -> Set VName
forall a b. (a -> b) -> a -> b
$ Info StructType -> StructType
forall a. Info a -> a
unInfo (Info StructType -> StructType) -> Info StructType -> StructType
forall a b. (a -> b) -> a -> b
$ TypeDeclBase Info VName -> Info StructType
forall (f :: * -> *) vn. TypeDeclBase f vn -> f StructType
expandedType TypeDeclBase Info VName
td'
    case (TypeParam -> Bool) -> [TypeParam] -> [TypeParam]
forall a. (a -> Bool) -> [a] -> [a]
filter ((VName -> Set VName -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.notMember` Set VName
used_dims) (VName -> Bool) -> (TypeParam -> VName) -> TypeParam -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeParam -> VName
forall vn. TypeParamBase vn -> vn
typeParamName) ([TypeParam] -> [TypeParam]) -> [TypeParam] -> [TypeParam]
forall a b. (a -> b) -> a -> b
$
      (TypeParam -> Bool) -> [TypeParam] -> [TypeParam]
forall a. (a -> Bool) -> [a] -> [a]
filter TypeParam -> Bool
forall vn. TypeParamBase vn -> Bool
isSizeParam [TypeParam]
tps' of
      [] -> () -> TypeM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      TypeParam
tp : [TypeParam]
_ ->
        SrcLoc -> Notes -> Doc -> TypeM ()
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
<+> Doc -> Doc
pquote (TypeParam -> Doc
forall a. Pretty a => a -> Doc
ppr TypeParam
tp) Doc -> Doc -> Doc
<+> Doc
"unused."

    case (Liftedness
l, Liftedness
l') of
      (Liftedness
_, Liftedness
Lifted)
        | Liftedness
l Liftedness -> Liftedness -> Bool
forall a. Ord a => a -> a -> Bool
< Liftedness
Lifted ->
          SrcLoc -> Notes -> Doc -> TypeM ()
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
</> 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 (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
</> Doc
"Hint: consider using 'type~'."
      (Liftedness
Unlifted, Liftedness
_)
        | StructType -> Bool
emptyDimParam (StructType -> Bool) -> StructType -> Bool
forall a b. (a -> b) -> a -> b
$ Info StructType -> StructType
forall a. Info a -> a
unInfo (Info StructType -> StructType) -> Info StructType -> StructType
forall a b. (a -> b) -> a -> b
$ TypeDeclBase Info VName -> Info StructType
forall (f :: * -> *) vn. TypeDeclBase f vn -> f StructType
expandedType TypeDeclBase Info VName
td' ->
          SrcLoc -> Notes -> Doc -> TypeM ()
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 anonymous sizes in their definition."
              Doc -> Doc -> Doc
</> Doc
"Hint: use 'type~' or add size parameters to"
              Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (Name -> Doc
forall v. IsName v => v -> Doc
pprName Name
name) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."
      (Liftedness, Liftedness)
_ -> () -> TypeM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

    [(Namespace, Name)]
-> TypeM (Env, TypeBindBase Info VName)
-> TypeM (Env, TypeBindBase Info VName)
forall (m :: * -> *) a.
MonadTypeChecker m =>
[(Namespace, Name)] -> m a -> m a
bindSpaced [(Namespace
Type, Name
name)] (TypeM (Env, TypeBindBase Info VName)
 -> TypeM (Env, TypeBindBase Info VName))
-> TypeM (Env, TypeBindBase Info VName)
-> TypeM (Env, TypeBindBase Info VName)
forall a b. (a -> b) -> a -> b
$ do
      VName
name' <- Namespace -> Name -> SrcLoc -> TypeM VName
forall (m :: * -> *).
MonadTypeChecker m =>
Namespace -> Name -> SrcLoc -> m VName
checkName Namespace
Type Name
name SrcLoc
loc
      (Env, TypeBindBase Info VName)
-> TypeM (Env, TypeBindBase Info VName)
forall (m :: * -> *) a. Monad m => a -> m a
return
        ( Env
forall a. Monoid a => a
mempty
            { envTypeTable :: Map VName TypeBinding
envTypeTable =
                VName -> TypeBinding -> Map VName TypeBinding
forall k a. k -> a -> Map k a
M.singleton VName
name' (TypeBinding -> Map VName TypeBinding)
-> TypeBinding -> Map VName TypeBinding
forall a b. (a -> b) -> a -> b
$ Liftedness -> [TypeParam] -> StructType -> TypeBinding
TypeAbbr Liftedness
l [TypeParam]
tps' (StructType -> TypeBinding) -> StructType -> TypeBinding
forall a b. (a -> b) -> a -> b
$ Info StructType -> StructType
forall a. Info a -> a
unInfo (Info StructType -> StructType) -> Info StructType -> StructType
forall a b. (a -> b) -> a -> b
$ TypeDeclBase Info VName -> Info StructType
forall (f :: * -> *) vn. TypeDeclBase f vn -> f StructType
expandedType TypeDeclBase Info VName
td',
              envNameMap :: NameMap
envNameMap =
                (Namespace, Name) -> QualName VName -> NameMap
forall k a. k -> a -> Map k a
M.singleton (Namespace
Type, Name
name) (QualName VName -> NameMap) -> QualName VName -> NameMap
forall a b. (a -> b) -> a -> b
$ VName -> QualName VName
forall v. v -> QualName v
qualName VName
name'
            },
          VName
-> Liftedness
-> [TypeParam]
-> TypeDeclBase Info VName
-> Maybe DocComment
-> SrcLoc
-> TypeBindBase Info VName
forall (f :: * -> *) vn.
vn
-> Liftedness
-> [TypeParamBase vn]
-> TypeDeclBase f vn
-> Maybe DocComment
-> SrcLoc
-> TypeBindBase f vn
TypeBind VName
name' Liftedness
l [TypeParam]
tps' TypeDeclBase Info VName
td' Maybe DocComment
doc SrcLoc
loc
        )

entryPoint :: [Pattern] -> Maybe (TypeExp VName) -> StructType -> EntryPoint
entryPoint :: [Pattern] -> Maybe (TypeExp VName) -> StructType -> EntryPoint
entryPoint [Pattern]
params Maybe (TypeExp VName)
orig_ret_te StructType
orig_ret =
  [EntryType] -> EntryType -> EntryPoint
EntryPoint ((Pattern -> EntryType) -> [Pattern] -> [EntryType]
forall a b. (a -> b) -> [a] -> [b]
map Pattern -> EntryType
patternEntry [Pattern]
params [EntryType] -> [EntryType] -> [EntryType]
forall a. [a] -> [a] -> [a]
++ [EntryType]
more_params) EntryType
rettype'
  where
    ([EntryType]
more_params, EntryType
rettype') =
      Maybe (TypeExp VName) -> StructType -> ([EntryType], EntryType)
onRetType Maybe (TypeExp VName)
orig_ret_te StructType
orig_ret

    patternEntry :: Pattern -> EntryType
patternEntry (PatternParens Pattern
p SrcLoc
_) =
      Pattern -> EntryType
patternEntry Pattern
p
    patternEntry (PatternAscription Pattern
_ TypeDeclBase Info VName
tdecl SrcLoc
_) =
      StructType -> Maybe (TypeExp VName) -> EntryType
EntryType (Info StructType -> StructType
forall a. Info a -> a
unInfo (TypeDeclBase Info VName -> Info StructType
forall (f :: * -> *) vn. TypeDeclBase f vn -> f StructType
expandedType TypeDeclBase Info VName
tdecl)) (TypeExp VName -> Maybe (TypeExp VName)
forall a. a -> Maybe a
Just (TypeDeclBase Info VName -> TypeExp VName
forall (f :: * -> *) vn. TypeDeclBase f vn -> TypeExp vn
declaredType TypeDeclBase Info VName
tdecl))
    patternEntry Pattern
p =
      StructType -> Maybe (TypeExp VName) -> EntryType
EntryType (Pattern -> StructType
patternStructType Pattern
p) Maybe (TypeExp VName)
forall a. Maybe a
Nothing

    onRetType :: Maybe (TypeExp VName) -> StructType -> ([EntryType], EntryType)
onRetType (Just (TEArrow Maybe VName
_ TypeExp VName
t1_te TypeExp VName
t2_te SrcLoc
_)) (Scalar (Arrow ()
_ PName
_ StructType
t1 StructType
t2)) =
      let ([EntryType]
xs, EntryType
y) = Maybe (TypeExp VName) -> StructType -> ([EntryType], EntryType)
onRetType (TypeExp VName -> Maybe (TypeExp VName)
forall a. a -> Maybe a
Just TypeExp VName
t2_te) StructType
t2
       in (StructType -> Maybe (TypeExp VName) -> EntryType
EntryType StructType
t1 (TypeExp VName -> Maybe (TypeExp VName)
forall a. a -> Maybe a
Just TypeExp VName
t1_te) EntryType -> [EntryType] -> [EntryType]
forall a. a -> [a] -> [a]
: [EntryType]
xs, EntryType
y)
    onRetType Maybe (TypeExp VName)
_ (Scalar (Arrow ()
_ PName
_ StructType
t1 StructType
t2)) =
      let ([EntryType]
xs, EntryType
y) = Maybe (TypeExp VName) -> StructType -> ([EntryType], EntryType)
onRetType Maybe (TypeExp VName)
forall a. Maybe a
Nothing StructType
t2
       in (StructType -> Maybe (TypeExp VName) -> EntryType
EntryType StructType
t1 Maybe (TypeExp VName)
forall a. Maybe a
Nothing EntryType -> [EntryType] -> [EntryType]
forall a. a -> [a] -> [a]
: [EntryType]
xs, EntryType
y)
    onRetType Maybe (TypeExp VName)
te StructType
t =
      ([], StructType -> Maybe (TypeExp VName) -> EntryType
EntryType StructType
t Maybe (TypeExp VName)
te)

entryPointNameIsAcceptable :: Name -> Bool
entryPointNameIsAcceptable :: Name -> Bool
entryPointNameIsAcceptable = String -> Bool
check (String -> Bool) -> (Name -> String) -> Name -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> String
nameToString
  where
    check :: String -> Bool
check [] = Bool
True -- academic
    check (Char
c : String
cs) = Char -> Bool
isAlpha Char
c Bool -> Bool -> Bool
&& (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
constituent String
cs
    constituent :: Char -> Bool
constituent Char
c = Char -> Bool
isAlphaNum Char
c Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'_'

checkValBind :: ValBindBase NoInfo Name -> TypeM (Env, ValBind)
checkValBind :: ValBindBase NoInfo Name -> TypeM (Env, ValBind)
checkValBind (ValBind Maybe (NoInfo EntryPoint)
entry Name
fname Maybe (TypeExp Name)
maybe_tdecl NoInfo (StructType, [VName])
NoInfo [TypeParamBase Name]
tparams [PatternBase NoInfo Name]
params UncheckedExp
body Maybe DocComment
doc [AttrInfo]
attrs SrcLoc
loc) = do
  (VName
fname', [TypeParam]
tparams', [Pattern]
params', Maybe (TypeExp VName)
maybe_tdecl', StructType
rettype, [VName]
retext, Exp
body') <-
    (Name, Maybe (TypeExp Name), [TypeParamBase Name],
 [PatternBase NoInfo Name], UncheckedExp, SrcLoc)
-> TypeM
     (VName, [TypeParam], [Pattern], Maybe (TypeExp VName), StructType,
      [VName], Exp)
checkFunDef (Name
fname, Maybe (TypeExp Name)
maybe_tdecl, [TypeParamBase Name]
tparams, [PatternBase NoInfo Name]
params, UncheckedExp
body, SrcLoc
loc)

  let ([StructType]
rettype_params, StructType
rettype') = StructType -> ([StructType], StructType)
forall dim as.
TypeBase dim as -> ([TypeBase dim as], TypeBase dim as)
unfoldFunType StructType
rettype
      entry' :: Maybe (Info EntryPoint)
entry' = EntryPoint -> Info EntryPoint
forall a. a -> Info a
Info ([Pattern] -> Maybe (TypeExp VName) -> StructType -> EntryPoint
entryPoint [Pattern]
params' Maybe (TypeExp VName)
maybe_tdecl' StructType
rettype) Info EntryPoint
-> Maybe (NoInfo EntryPoint) -> Maybe (Info EntryPoint)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Maybe (NoInfo EntryPoint)
entry

  case Maybe (Info EntryPoint)
entry' of
    Just Info EntryPoint
_
      | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Name -> Bool
entryPointNameIsAcceptable Name
fname ->
        SrcLoc -> Notes -> Doc -> TypeM ()
forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc -> m a
typeError SrcLoc
loc Notes
forall a. Monoid a => a
mempty Doc
"Entry point names must start with a letter and contain only letters, digits, and underscores."
      | (TypeParam -> Bool) -> [TypeParam] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any TypeParam -> Bool
forall vn. TypeParamBase vn -> Bool
isTypeParam [TypeParam]
tparams' ->
        SrcLoc -> Notes -> Doc -> TypeM ()
forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc -> m a
typeError SrcLoc
loc Notes
forall a. Monoid a => a
mempty Doc
"Entry point functions may not be polymorphic."
      | Bool -> Bool
not ((Pattern -> Bool) -> [Pattern] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Pattern -> Bool
forall vn. PatternBase Info vn -> Bool
patternOrderZero [Pattern]
params')
          Bool -> Bool -> Bool
|| Bool -> Bool
not ((StructType -> Bool) -> [StructType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all StructType -> Bool
forall dim as. TypeBase dim as -> Bool
orderZero [StructType]
rettype_params)
          Bool -> Bool -> Bool
|| Bool -> Bool
not (StructType -> Bool
forall dim as. TypeBase dim as -> Bool
orderZero StructType
rettype') ->
        SrcLoc -> Notes -> Doc -> TypeM ()
forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc -> m a
typeError SrcLoc
loc Notes
forall a. Monoid a => a
mempty 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 ((TypeParam -> VName) -> [TypeParam] -> [VName]
forall a b. (a -> b) -> [a] -> [b]
map TypeParam -> VName
forall vn. TypeParamBase vn -> vn
typeParamName [TypeParam]
tparams')
            Set VName -> Set VName -> Set VName
forall a. Ord a => Set a -> Set a -> Set a
`S.intersection` StructType -> Set VName
forall als. TypeBase (DimDecl VName) als -> Set VName
typeDimNames StructType
rettype'
            Set VName -> Set VName -> Set VName
forall a. Ord a => Set a -> Set a -> Set a
`S.difference` (StructType -> Set VName) -> [StructType] -> Set VName
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap StructType -> Set VName
forall als. TypeBase (DimDecl VName) als -> Set VName
typeDimNames ((Pattern -> StructType) -> [Pattern] -> [StructType]
forall a b. (a -> b) -> [a] -> [b]
map Pattern -> StructType
patternStructType [Pattern]
params' [StructType] -> [StructType] -> [StructType]
forall a. [a] -> [a] -> [a]
++ [StructType]
rettype_params),
        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 (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc -> m a
typeError SrcLoc
loc Notes
forall a. Monoid a => a
mempty Doc
"Entry point functions must not be size-polymorphic in their return type."
      | Pattern
p : [Pattern]
_ <- (Pattern -> Bool) -> [Pattern] -> [Pattern]
forall a. (a -> Bool) -> [a] -> [a]
filter Pattern -> Bool
nastyParameter [Pattern]
params' ->
        SrcLoc -> Doc -> TypeM ()
forall (m :: * -> *) loc.
(MonadTypeChecker m, Located loc) =>
loc -> Doc -> m ()
warn SrcLoc
loc (Doc -> TypeM ()) -> Doc -> TypeM ()
forall a b. (a -> b) -> a -> b
$
          Doc
"Entry point parameter\n"
            Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (Pattern -> Doc
forall a. Pretty a => a -> Doc
ppr Pattern
p)
            Doc -> Doc -> Doc
</> Doc
"\nwill have an opaque type, so the entry point will likely not be callable."
      | Maybe (TypeExp VName) -> StructType -> Bool
forall als dim.
Monoid als =>
Maybe (TypeExp VName) -> TypeBase dim als -> Bool
nastyReturnType Maybe (TypeExp VName)
maybe_tdecl' StructType
rettype ->
        SrcLoc -> Doc -> TypeM ()
forall (m :: * -> *) loc.
(MonadTypeChecker m, Located loc) =>
loc -> Doc -> m ()
warn SrcLoc
loc (Doc -> TypeM ()) -> Doc -> TypeM ()
forall a b. (a -> b) -> a -> b
$
          Doc
"Entry point return type\n"
            Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (StructType -> Doc
forall a. Pretty a => a -> Doc
ppr StructType
rettype)
            Doc -> Doc -> Doc
</> Doc
"\nwill have an opaque type, so the result will likely not be usable."
    Maybe (Info EntryPoint)
_ -> () -> TypeM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

  let vb :: ValBind
vb = Maybe (Info EntryPoint)
-> VName
-> Maybe (TypeExp VName)
-> Info (StructType, [VName])
-> [TypeParam]
-> [Pattern]
-> Exp
-> Maybe DocComment
-> [AttrInfo]
-> SrcLoc
-> ValBind
forall (f :: * -> *) vn.
Maybe (f EntryPoint)
-> vn
-> Maybe (TypeExp vn)
-> f (StructType, [VName])
-> [TypeParamBase vn]
-> [PatternBase f vn]
-> ExpBase f vn
-> Maybe DocComment
-> [AttrInfo]
-> SrcLoc
-> ValBindBase f vn
ValBind Maybe (Info EntryPoint)
entry' VName
fname' Maybe (TypeExp VName)
maybe_tdecl' ((StructType, [VName]) -> Info (StructType, [VName])
forall a. a -> Info a
Info (StructType
rettype, [VName]
retext)) [TypeParam]
tparams' [Pattern]
params' Exp
body' Maybe DocComment
doc [AttrInfo]
attrs SrcLoc
loc
  (Env, ValBind) -> TypeM (Env, ValBind)
forall (m :: * -> *) a. Monad m => a -> m a
return
    ( Env
forall a. Monoid a => a
mempty
        { envVtable :: Map VName BoundV
envVtable =
            VName -> BoundV -> Map VName BoundV
forall k a. k -> a -> Map k a
M.singleton VName
fname' (BoundV -> Map VName BoundV) -> BoundV -> Map VName BoundV
forall a b. (a -> b) -> a -> b
$ ([TypeParam] -> StructType -> BoundV)
-> ([TypeParam], StructType) -> BoundV
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [TypeParam] -> StructType -> BoundV
BoundV (([TypeParam], StructType) -> BoundV)
-> ([TypeParam], StructType) -> BoundV
forall a b. (a -> b) -> a -> b
$ ValBind -> ([TypeParam], StructType)
valBindTypeScheme ValBind
vb,
          envNameMap :: NameMap
envNameMap =
            (Namespace, Name) -> QualName VName -> NameMap
forall k a. k -> a -> Map k a
M.singleton (Namespace
Term, Name
fname) (QualName VName -> NameMap) -> QualName VName -> NameMap
forall a b. (a -> b) -> a -> b
$ VName -> QualName VName
forall v. v -> QualName v
qualName VName
fname'
        },
      ValBind
vb
    )

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

nastyParameter :: Pattern -> Bool
nastyParameter :: Pattern -> Bool
nastyParameter Pattern
p = TypeBase (DimDecl VName) Aliasing -> Bool
forall als dim. Monoid als => TypeBase dim als -> Bool
nastyType (Pattern -> TypeBase (DimDecl VName) Aliasing
patternType Pattern
p) Bool -> Bool -> Bool
&& Bool -> Bool
not (Pattern -> Bool
forall (f :: * -> *). PatternBase f VName -> Bool
ascripted Pattern
p)
  where
    ascripted :: PatternBase f VName -> Bool
ascripted (PatternAscription PatternBase f VName
_ (TypeDecl TypeExp VName
te f StructType
_) SrcLoc
_) = TypeExp VName -> Bool
niceTypeExp TypeExp VName
te
    ascripted (PatternParens PatternBase f VName
p' SrcLoc
_) = PatternBase f VName -> Bool
ascripted PatternBase f VName
p'
    ascripted PatternBase f VName
_ = Bool
False

niceTypeExp :: TypeExp VName -> Bool
niceTypeExp :: TypeExp VName -> Bool
niceTypeExp (TEVar (QualName [] VName
_) SrcLoc
_) = Bool
True
niceTypeExp (TEApply TypeExp VName
te TypeArgExpDim {} SrcLoc
_) = TypeExp VName -> Bool
niceTypeExp TypeExp VName
te
niceTypeExp (TEArray TypeExp VName
te DimExp VName
_ SrcLoc
_) = TypeExp VName -> Bool
niceTypeExp TypeExp VName
te
niceTypeExp TypeExp 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
  (TySet, Env, Dec) -> TypeM (TySet, Env, Dec)
forall (m :: * -> *) a. Monad m => a -> m a
return (TySet
abs, Env
modenv, ModBindBase Info VName -> Dec
forall (f :: * -> *) vn. ModBindBase f vn -> DecBase f vn
ModDec ModBindBase Info VName
struct')
checkOneDec (SigDec SigBindBase NoInfo Name
sig) = do
  (Env
sigenv, SigBindBase Info VName
sig') <- SigBindBase NoInfo Name -> TypeM (Env, SigBindBase Info VName)
checkSigBind SigBindBase NoInfo Name
sig
  (TySet, Env, Dec) -> TypeM (TySet, Env, Dec)
forall (m :: * -> *) a. Monad m => a -> m a
return (TySet
forall a. Monoid a => a
mempty, Env
sigenv, SigBindBase Info VName -> Dec
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
  (TySet, Env, Dec) -> TypeM (TySet, Env, Dec)
forall (m :: * -> *) a. Monad m => a -> m a
return (TySet
forall a. Monoid a => a
mempty, Env
tenv, TypeBindBase Info VName -> Dec
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
  (TySet, Env, Dec) -> TypeM (TySet, Env, Dec)
forall (m :: * -> *) a. Monad m => a -> m a
return (TySet
x_abs, Env
x_env, ModExpBase Info VName -> SrcLoc -> Dec
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
  (TySet, Env, Dec) -> TypeM (TySet, Env, Dec)
forall (m :: * -> *) a. Monad m => a -> m a
return (TySet
abstypes, Env
env, Dec -> SrcLoc -> Dec
forall (f :: * -> *) vn. DecBase f vn -> SrcLoc -> DecBase f vn
LocalDec Dec
d' SrcLoc
loc)
checkOneDec (ImportDec String
name NoInfo String
NoInfo SrcLoc
loc) = do
  (String
name', Env
env) <- SrcLoc -> String -> TypeM (String, Env)
lookupImport SrcLoc
loc String
name
  Bool -> TypeM () -> TypeM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (String
"/prelude" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
name) (TypeM () -> TypeM ()) -> TypeM () -> TypeM ()
forall a b. (a -> b) -> a -> b
$
    SrcLoc -> Notes -> Doc -> TypeM ()
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
$ String -> Doc
forall a. Pretty a => a -> Doc
ppr String
name Doc -> Doc -> Doc
<+> Doc
"may not be explicitly imported."
  (TySet, Env, Dec) -> TypeM (TySet, Env, Dec)
forall (m :: * -> *) a. Monad m => a -> m a
return (TySet
forall a. Monoid a => a
mempty, Env
env, String -> Info String -> SrcLoc -> Dec
forall (f :: * -> *) vn.
String -> f String -> SrcLoc -> DecBase f vn
ImportDec String
name (String -> Info String
forall a. a -> Info a
Info String
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
  (TySet, Env, Dec) -> TypeM (TySet, Env, Dec)
forall (m :: * -> *) a. Monad m => a -> m a
return (TySet
forall a. Monoid a => a
mempty, Env
env, ValBind -> Dec
forall (f :: * -> *) vn. ValBindBase f vn -> DecBase f vn
ValDec ValBind
vb')

checkDecs :: [DecBase NoInfo Name] -> TypeM (TySet, Env, [DecBase Info VName])
checkDecs :: [UncheckedDec] -> TypeM (TySet, Env, [Dec])
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 -> TypeM (TySet, Env, [Dec]) -> TypeM (TySet, Env, [Dec])
forall a. Env -> TypeM a -> TypeM a
localEnv Env
d_env (TypeM (TySet, Env, [Dec]) -> TypeM (TySet, Env, [Dec]))
-> TypeM (TySet, Env, [Dec]) -> TypeM (TySet, Env, [Dec])
forall a b. (a -> b) -> a -> b
$ [UncheckedDec] -> TypeM (TySet, Env, [Dec])
checkDecs [UncheckedDec]
ds
  (TySet, Env, [Dec]) -> TypeM (TySet, Env, [Dec])
forall (m :: * -> *) a. Monad m => a -> m a
return
    ( TySet
d_abstypes TySet -> TySet -> TySet
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 Env -> Env -> Env
forall a. Semigroup a => a -> a -> a
<> Env
d_env,
      Dec
d' Dec -> [Dec] -> [Dec]
forall a. a -> [a] -> [a]
: [Dec]
ds'
    )
checkDecs [] =
  (TySet, Env, [Dec]) -> TypeM (TySet, Env, [Dec])
forall (m :: * -> *) a. Monad m => a -> m a
return (TySet
forall a. Monoid a => a
mempty, Env
forall a. Monoid a => a
mempty, [])