{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Safe #-}
-- | 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.List (isPrefixOf)
import Data.Maybe
import Data.Either
import Data.Ord
import qualified Data.Map.Strict as M
import qualified Data.Set as S

import Prelude hiding (abs, mod)

import Language.Futhark
import Language.Futhark.Semantic
import Futhark.FreshNames hiding (newName)
import Language.Futhark.TypeChecker.Monad
import Language.Futhark.TypeChecker.Modules
import Language.Futhark.TypeChecker.Terms
import Language.Futhark.TypeChecker.Types
import Futhark.Util.Pretty hiding (space)

--- 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 checker results.  The 'FilePath' is used to resolve
-- relative @import@s.
checkProg :: Imports
          -> VNameSource
          -> ImportName
          -> UncheckedProg
          -> Either TypeError (FileModule, Warnings, VNameSource)
checkProg :: Imports
-> VNameSource
-> ImportName
-> UncheckedProg
-> Either TypeError (FileModule, Warnings, VNameSource)
checkProg Imports
files VNameSource
src ImportName
name UncheckedProg
prog =
  Env
-> ImportTable
-> ImportName
-> VNameSource
-> TypeM FileModule
-> Either TypeError (FileModule, Warnings, VNameSource)
forall a.
Env
-> ImportTable
-> ImportName
-> VNameSource
-> TypeM a
-> Either TypeError (a, Warnings, VNameSource)
runTypeM Env
initialEnv ImportTable
files' ImportName
name VNameSource
src (TypeM FileModule
 -> Either TypeError (FileModule, Warnings, VNameSource))
-> TypeM FileModule
-> Either TypeError (FileModule, Warnings, 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
         -> Either TypeError ([TypeParam], Exp)
checkExp :: Imports
-> VNameSource
-> Env
-> UncheckedExp
-> Either TypeError ([TypeParam], Exp)
checkExp Imports
files VNameSource
src Env
env UncheckedExp
e = do
  (([TypeParam], Exp)
e', Warnings
_, VNameSource
_) <- Env
-> ImportTable
-> ImportName
-> VNameSource
-> TypeM ([TypeParam], Exp)
-> Either TypeError (([TypeParam], Exp), Warnings, VNameSource)
forall a.
Env
-> ImportTable
-> ImportName
-> VNameSource
-> TypeM a
-> Either TypeError (a, Warnings, VNameSource)
runTypeM Env
env ImportTable
files' (String -> ImportName
mkInitialImport String
"") VNameSource
src (TypeM ([TypeParam], Exp)
 -> Either TypeError (([TypeParam], Exp), Warnings, VNameSource))
-> TypeM ([TypeParam], Exp)
-> Either TypeError (([TypeParam], Exp), Warnings, VNameSource)
forall a b. (a -> b) -> a -> b
$ UncheckedExp -> TypeM ([TypeParam], Exp)
checkOneExp UncheckedExp
e
  ([TypeParam], Exp) -> Either TypeError ([TypeParam], Exp)
forall (m :: * -> *) a. Monad m => a -> m a
return ([TypeParam], Exp)
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
         -> Either TypeError (Env, Dec, VNameSource)
checkDec :: Imports
-> VNameSource
-> Env
-> ImportName
-> UncheckedDec
-> Either TypeError (Env, Dec, VNameSource)
checkDec Imports
files VNameSource
src Env
env ImportName
name UncheckedDec
d = do
  ((Env
env', Dec
d'), Warnings
_, VNameSource
src') <- Env
-> ImportTable
-> ImportName
-> VNameSource
-> TypeM (Env, Dec)
-> Either TypeError ((Env, Dec), Warnings, VNameSource)
forall a.
Env
-> ImportTable
-> ImportName
-> VNameSource
-> TypeM a
-> Either TypeError (a, Warnings, VNameSource)
runTypeM Env
env ImportTable
files' ImportName
name VNameSource
src (TypeM (Env, Dec)
 -> Either TypeError ((Env, Dec), Warnings, VNameSource))
-> TypeM (Env, Dec)
-> Either TypeError ((Env, Dec), Warnings, 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')
  (Env, Dec, VNameSource) -> Either TypeError (Env, Dec, VNameSource)
forall (m :: * -> *) a. Monad m => a -> m a
return (Env
env', Dec
d', VNameSource
src')
  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 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
            -> Either TypeError (MTy, ModExpBase Info VName)
checkModExp :: Imports
-> VNameSource
-> Env
-> ModExpBase NoInfo Name
-> Either TypeError (MTy, ModExpBase Info VName)
checkModExp Imports
files VNameSource
src Env
env ModExpBase NoInfo Name
me = do
  ((MTy, ModExpBase Info VName)
x, Warnings
_, VNameSource
_) <- Env
-> ImportTable
-> ImportName
-> VNameSource
-> TypeM (MTy, ModExpBase Info VName)
-> Either
     TypeError ((MTy, ModExpBase Info VName), Warnings, VNameSource)
forall a.
Env
-> ImportTable
-> ImportName
-> VNameSource
-> TypeM a
-> Either TypeError (a, Warnings, VNameSource)
runTypeM Env
env ImportTable
files' (String -> ImportName
mkInitialImport String
"") VNameSource
src (TypeM (MTy, ModExpBase Info VName)
 -> Either
      TypeError ((MTy, ModExpBase Info VName), Warnings, VNameSource))
-> TypeM (MTy, ModExpBase Info VName)
-> Either
     TypeError ((MTy, ModExpBase Info VName), Warnings, VNameSource)
forall a b. (a -> b) -> a -> b
$ ModExpBase NoInfo Name -> TypeM (MTy, ModExpBase Info VName)
checkOneModExp ModExpBase NoInfo Name
me
  (MTy, ModExpBase Info VName)
-> Either TypeError (MTy, ModExpBase Info VName)
forall (m :: * -> *) a. Monad m => a -> m a
return (MTy, ModExpBase Info VName)
x
  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
Int32) }
        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 -> String -> m ()
forall (m :: * -> *) loc.
(MonadTypeChecker m, Located loc) =>
loc -> String -> m ()
warn SrcLoc
loc (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"Inclusion shadows type " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
quote (a -> String
forall a. Pretty a => a -> String
pretty a
qn) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"."

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)

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
_
      | (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 -> String -> TypeM ()
forall (m :: * -> *) loc.
(MonadTypeChecker m, Located loc) =>
loc -> String -> m ()
warn SrcLoc
loc (String -> TypeM ()) -> String -> TypeM ()
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Pretty a => a -> String
pretty (Doc -> String) -> Doc -> String
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 -> String -> TypeM ()
forall (m :: * -> *) loc.
(MonadTypeChecker m, Located loc) =>
loc -> String -> m ()
warn SrcLoc
loc (String -> TypeM ()) -> String -> TypeM ()
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Pretty a => a -> String
pretty (Doc -> String) -> Doc -> String
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 arrow :: (PName, TypeBase dim ()) -> TypeBase dim () -> TypeBase dim ()
arrow (PName
xp, TypeBase dim ()
xt) TypeBase dim ()
yt = ScalarTypeBase dim () -> TypeBase dim ()
forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar (ScalarTypeBase dim () -> TypeBase dim ())
-> ScalarTypeBase dim () -> TypeBase dim ()
forall a b. (a -> b) -> a -> b
$ ()
-> PName
-> TypeBase dim ()
-> TypeBase dim ()
-> ScalarTypeBase dim ()
forall dim as.
as
-> PName
-> TypeBase dim as
-> TypeBase dim as
-> ScalarTypeBase dim as
Arrow () PName
xp TypeBase dim ()
xt TypeBase dim ()
yt
  (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
BoundV [TypeParam]
tparams' (StructType -> BoundV) -> StructType -> BoundV
forall a b. (a -> b) -> a -> b
$ (Pattern -> StructType -> StructType)
-> StructType -> [Pattern] -> StructType
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((PName, StructType) -> StructType -> StructType
forall dim.
(PName, TypeBase dim ()) -> TypeBase dim () -> TypeBase dim ()
arrow ((PName, StructType) -> StructType -> StructType)
-> (Pattern -> (PName, StructType))
-> Pattern
-> StructType
-> StructType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pattern -> (PName, StructType)
patternParam) StructType
rettype [Pattern]
params'
                 , 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'
                 },
           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)

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 (LocalDec UncheckedDec
d SrcLoc
loc:[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,
          Env
ds_env,
          Dec -> SrcLoc -> Dec
forall (f :: * -> *) vn. DecBase f vn -> SrcLoc -> DecBase f vn
LocalDec Dec
d' SrcLoc
loc Dec -> [Dec] -> [Dec]
forall a. a -> [a] -> [a]
: [Dec]
ds')

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,
          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, [])