-- | Implementation of the Futhark module system (at least most of it;
-- some is scattered elsewhere in the type checker).
module Language.Futhark.TypeChecker.Modules
  ( matchMTys,
    newNamesForMTy,
    refineEnv,
    applyFunctor,
  )
where

import Control.Monad
import Data.Either
import Data.Map.Strict qualified as M
import Data.Maybe
import Data.Ord
import Data.Set qualified as S
import Futhark.Util.Pretty
import Language.Futhark
import Language.Futhark.Semantic
import Language.Futhark.TypeChecker.Monad
import Language.Futhark.TypeChecker.Types
import Language.Futhark.TypeChecker.Unify (doUnification)
import Prelude hiding (abs, mod)

substituteTypesInMod :: TypeSubs -> Mod -> Mod
substituteTypesInMod :: TypeSubs -> Mod -> Mod
substituteTypesInMod TypeSubs
substs (ModEnv Env
e) =
  Env -> Mod
ModEnv (Env -> Mod) -> Env -> Mod
forall a b. (a -> b) -> a -> b
$ TypeSubs -> Env -> Env
substituteTypesInEnv TypeSubs
substs Env
e
substituteTypesInMod TypeSubs
substs (ModFun (FunModType TySet
abs Mod
mod MTy
mty)) =
  FunModType -> Mod
ModFun (FunModType -> Mod) -> FunModType -> Mod
forall a b. (a -> b) -> a -> b
$ TySet -> Mod -> MTy -> FunModType
FunModType TySet
abs (TypeSubs -> Mod -> Mod
substituteTypesInMod TypeSubs
substs Mod
mod) (TypeSubs -> MTy -> MTy
substituteTypesInMTy TypeSubs
substs MTy
mty)

substituteTypesInMTy :: TypeSubs -> MTy -> MTy
substituteTypesInMTy :: TypeSubs -> MTy -> MTy
substituteTypesInMTy TypeSubs
substs (MTy TySet
abs Mod
mod) = TySet -> Mod -> MTy
MTy TySet
abs (Mod -> MTy) -> Mod -> MTy
forall a b. (a -> b) -> a -> b
$ TypeSubs -> Mod -> Mod
substituteTypesInMod TypeSubs
substs Mod
mod

substituteTypesInEnv :: TypeSubs -> Env -> Env
substituteTypesInEnv :: TypeSubs -> Env -> Env
substituteTypesInEnv TypeSubs
substs Env
env =
  Env
env
    { envVtable = M.map (snd . substituteTypesInBoundV substs) $ envVtable env,
      envTypeTable = M.mapWithKey subT $ envTypeTable env,
      envModTable = M.map (substituteTypesInMod substs) $ envModTable env
    }
  where
    subT :: VName -> TypeBinding -> TypeBinding
subT VName
name (TypeAbbr Liftedness
l [TypeParam]
_ StructRetType
_)
      | Just (Subst [TypeParam]
ps StructRetType
rt) <- TypeSubs
substs VName
name = Liftedness -> [TypeParam] -> StructRetType -> TypeBinding
TypeAbbr Liftedness
l [TypeParam]
ps StructRetType
rt
    subT VName
_ (TypeAbbr Liftedness
l [TypeParam]
ps (RetType [VName]
dims TypeBase Size NoUniqueness
t)) =
      Liftedness -> [TypeParam] -> StructRetType -> TypeBinding
TypeAbbr Liftedness
l [TypeParam]
ps (StructRetType -> TypeBinding) -> StructRetType -> TypeBinding
forall a b. (a -> b) -> a -> b
$ TypeSubs -> StructRetType -> StructRetType
forall a. Substitutable a => TypeSubs -> a -> a
applySubst TypeSubs
substs (StructRetType -> StructRetType) -> StructRetType -> StructRetType
forall a b. (a -> b) -> a -> b
$ [VName] -> TypeBase Size NoUniqueness -> StructRetType
forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
dims TypeBase Size NoUniqueness
t

-- Also returns names of new sizes arising from substituting a
-- size-lifted type at the outermost part of the type. This is a
-- somewhat rare case (see #2120). The right solution is to generally
-- fresh (or at least unique) names.
substituteTypesInBoundV :: TypeSubs -> BoundV -> ([VName], BoundV)
substituteTypesInBoundV :: TypeSubs -> BoundV -> ([VName], BoundV)
substituteTypesInBoundV TypeSubs
substs (BoundV [TypeParam]
tps TypeBase Size NoUniqueness
t) =
  let RetType [VName]
dims TypeBase Size NoUniqueness
t' = TypeSubs -> StructRetType -> StructRetType
forall a. Substitutable a => TypeSubs -> a -> a
applySubst TypeSubs
substs (StructRetType -> StructRetType) -> StructRetType -> StructRetType
forall a b. (a -> b) -> a -> b
$ [VName] -> TypeBase Size NoUniqueness -> StructRetType
forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [] TypeBase Size NoUniqueness
t
   in ([VName]
dims, [TypeParam] -> TypeBase Size NoUniqueness -> BoundV
BoundV ([TypeParam]
tps [TypeParam] -> [TypeParam] -> [TypeParam]
forall a. Semigroup a => a -> a -> a
<> (VName -> TypeParam) -> [VName] -> [TypeParam]
forall a b. (a -> b) -> [a] -> [b]
map (VName -> SrcLoc -> TypeParam
forall vn. vn -> SrcLoc -> TypeParamBase vn
`TypeParamDim` SrcLoc
forall a. Monoid a => a
mempty) [VName]
dims) TypeBase Size NoUniqueness
t')

-- | All names defined anywhere in the 'Env'.
allNamesInEnv :: Env -> S.Set VName
allNamesInEnv :: Env -> Set VName
allNamesInEnv (Env Map VName BoundV
vtable Map VName TypeBinding
ttable Map VName MTy
stable Map VName Mod
modtable NameMap
_names) =
  [VName] -> Set VName
forall a. Ord a => [a] -> Set a
S.fromList
    ( Map VName BoundV -> [VName]
forall k a. Map k a -> [k]
M.keys Map VName BoundV
vtable
        [VName] -> [VName] -> [VName]
forall a. [a] -> [a] -> [a]
++ Map VName TypeBinding -> [VName]
forall k a. Map k a -> [k]
M.keys Map VName TypeBinding
ttable
        [VName] -> [VName] -> [VName]
forall a. [a] -> [a] -> [a]
++ Map VName MTy -> [VName]
forall k a. Map k a -> [k]
M.keys Map VName MTy
stable
        [VName] -> [VName] -> [VName]
forall a. [a] -> [a] -> [a]
++ Map VName Mod -> [VName]
forall k a. Map k a -> [k]
M.keys Map VName Mod
modtable
    )
    Set VName -> Set VName -> Set VName
forall a. Semigroup a => a -> a -> a
<> [Set VName] -> Set VName
forall a. Monoid a => [a] -> a
mconcat
      ( (MTy -> Set VName) -> [MTy] -> [Set VName]
forall a b. (a -> b) -> [a] -> [b]
map MTy -> Set VName
allNamesInMTy (Map VName MTy -> [MTy]
forall k a. Map k a -> [a]
M.elems Map VName MTy
stable)
          [Set VName] -> [Set VName] -> [Set VName]
forall a. [a] -> [a] -> [a]
++ (Mod -> Set VName) -> [Mod] -> [Set VName]
forall a b. (a -> b) -> [a] -> [b]
map Mod -> Set VName
allNamesInMod (Map VName Mod -> [Mod]
forall k a. Map k a -> [a]
M.elems Map VName Mod
modtable)
          [Set VName] -> [Set VName] -> [Set VName]
forall a. [a] -> [a] -> [a]
++ (TypeBinding -> Set VName) -> [TypeBinding] -> [Set VName]
forall a b. (a -> b) -> [a] -> [b]
map TypeBinding -> Set VName
allNamesInType (Map VName TypeBinding -> [TypeBinding]
forall k a. Map k a -> [a]
M.elems Map VName TypeBinding
ttable)
      )
  where
    allNamesInType :: TypeBinding -> Set VName
allNamesInType (TypeAbbr Liftedness
_ [TypeParam]
ps StructRetType
_) = [VName] -> Set VName
forall a. Ord a => [a] -> Set a
S.fromList ([VName] -> Set VName) -> [VName] -> Set VName
forall a b. (a -> b) -> a -> b
$ (TypeParam -> VName) -> [TypeParam] -> [VName]
forall a b. (a -> b) -> [a] -> [b]
map TypeParam -> VName
forall vn. TypeParamBase vn -> vn
typeParamName [TypeParam]
ps

allNamesInMod :: Mod -> S.Set VName
allNamesInMod :: Mod -> Set VName
allNamesInMod (ModEnv Env
env) = Env -> Set VName
allNamesInEnv Env
env
allNamesInMod ModFun {} = Set VName
forall a. Monoid a => a
mempty

allNamesInMTy :: MTy -> S.Set VName
allNamesInMTy :: MTy -> Set VName
allNamesInMTy (MTy TySet
abs Mod
mod) =
  [VName] -> Set VName
forall a. Ord a => [a] -> Set a
S.fromList ((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
abs) Set VName -> Set VName -> Set VName
forall a. Semigroup a => a -> a -> a
<> Mod -> Set VName
allNamesInMod Mod
mod

-- | Create unique renames for the module type.  This is used for
-- e.g. generative functor application.
newNamesForMTy :: MTy -> TypeM (MTy, M.Map VName VName)
newNamesForMTy :: MTy -> TypeM (MTy, Map VName VName)
newNamesForMTy MTy
orig_mty = do
  [(VName, VName)]
pairs <- [VName]
-> (VName -> TypeM (VName, VName)) -> TypeM [(VName, VName)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Set VName -> [VName]
forall a. Set a -> [a]
S.toList (Set VName -> [VName]) -> Set VName -> [VName]
forall a b. (a -> b) -> a -> b
$ MTy -> Set VName
allNamesInMTy MTy
orig_mty) ((VName -> TypeM (VName, VName)) -> TypeM [(VName, VName)])
-> (VName -> TypeM (VName, VName)) -> TypeM [(VName, VName)]
forall a b. (a -> b) -> a -> b
$ \VName
v -> do
    VName
v' <- VName -> TypeM VName
forall (m :: * -> *). MonadTypeChecker m => VName -> m VName
newName VName
v
    (VName, VName) -> TypeM (VName, VName)
forall a. a -> TypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VName
v, VName
v')
  let substs :: Map VName VName
substs = [(VName, VName)] -> Map VName VName
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(VName, VName)]
pairs
      rev_substs :: Map VName VName
rev_substs = [(VName, VName)] -> Map VName VName
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(VName, VName)] -> Map VName VName)
-> [(VName, VName)] -> Map VName VName
forall a b. (a -> b) -> a -> b
$ ((VName, VName) -> (VName, VName))
-> [(VName, VName)] -> [(VName, VName)]
forall a b. (a -> b) -> [a] -> [b]
map ((VName -> VName -> (VName, VName))
-> (VName, VName) -> (VName, VName)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((VName -> VName -> (VName, VName))
 -> (VName, VName) -> (VName, VName))
-> (VName -> VName -> (VName, VName))
-> (VName, VName)
-> (VName, VName)
forall a b. (a -> b) -> a -> b
$ (VName -> VName -> (VName, VName))
-> VName -> VName -> (VName, VName)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (,)) [(VName, VName)]
pairs

  (MTy, Map VName VName) -> TypeM (MTy, Map VName VName)
forall a. a -> TypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map VName VName -> MTy -> MTy
substituteInMTy Map VName VName
substs MTy
orig_mty, Map VName VName
rev_substs)
  where
    substituteInMTy :: M.Map VName VName -> MTy -> MTy
    substituteInMTy :: Map VName VName -> MTy -> MTy
substituteInMTy Map VName VName
substs (MTy TySet
mty_abs Mod
mty_mod) =
      TySet -> Mod -> MTy
MTy ((QualName VName -> QualName VName) -> TySet -> TySet
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
M.mapKeys ((VName -> VName) -> QualName VName -> QualName VName
forall a b. (a -> b) -> QualName a -> QualName b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap VName -> VName
substitute) TySet
mty_abs) (Mod -> Mod
substituteInMod Mod
mty_mod)
      where
        substituteInEnv :: Env -> Env
substituteInEnv (Env Map VName BoundV
vtable Map VName TypeBinding
ttable Map VName MTy
_stable Map VName Mod
modtable NameMap
names) =
          let vtable' :: Map VName BoundV
vtable' = (BoundV -> BoundV) -> Map VName BoundV -> Map VName BoundV
forall {a} {a}. (a -> a) -> Map VName a -> Map VName a
substituteInMap BoundV -> BoundV
substituteInBinding Map VName BoundV
vtable
              ttable' :: Map VName TypeBinding
ttable' = (TypeBinding -> TypeBinding)
-> Map VName TypeBinding -> Map VName TypeBinding
forall {a} {a}. (a -> a) -> Map VName a -> Map VName a
substituteInMap TypeBinding -> TypeBinding
substituteInTypeBinding Map VName TypeBinding
ttable
              mtable' :: Map VName Mod
mtable' = (Mod -> Mod) -> Map VName Mod -> Map VName Mod
forall {a} {a}. (a -> a) -> Map VName a -> Map VName a
substituteInMap Mod -> Mod
substituteInMod Map VName Mod
modtable
           in Env
                { envVtable :: Map VName BoundV
envVtable = Map VName BoundV
vtable',
                  envTypeTable :: Map VName TypeBinding
envTypeTable = Map VName TypeBinding
ttable',
                  envModTypeTable :: Map VName MTy
envModTypeTable = Map VName MTy
forall a. Monoid a => a
mempty,
                  envModTable :: Map VName Mod
envModTable = Map VName Mod
mtable',
                  envNameMap :: NameMap
envNameMap = (QualName VName -> QualName VName) -> NameMap -> NameMap
forall a b k. (a -> b) -> Map k a -> Map k b
M.map ((VName -> VName) -> QualName VName -> QualName VName
forall a b. (a -> b) -> QualName a -> QualName b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap VName -> VName
substitute) NameMap
names
                }

        substitute :: VName -> VName
substitute VName
v =
          VName -> Maybe VName -> VName
forall a. a -> Maybe a -> a
fromMaybe VName
v (Maybe VName -> VName) -> Maybe VName -> VName
forall a b. (a -> b) -> a -> b
$ VName -> Map VName VName -> Maybe VName
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
v Map VName VName
substs

        -- For applySubst and friends.
        subst :: VName -> Maybe (Subst t)
subst VName
v =
          Size -> Subst t
forall t. Size -> Subst t
ExpSubst (Size -> Subst t) -> (VName -> Size) -> VName -> Subst t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (QualName VName -> SrcLoc -> Size)
-> SrcLoc -> QualName VName -> Size
forall a b c. (a -> b -> c) -> b -> a -> c
flip QualName VName -> SrcLoc -> Size
sizeFromName SrcLoc
forall a. Monoid a => a
mempty (QualName VName -> Size)
-> (VName -> QualName VName) -> VName -> Size
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VName -> QualName VName
forall v. v -> QualName v
qualName (VName -> Subst t) -> Maybe VName -> Maybe (Subst t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VName -> Map VName VName -> Maybe VName
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
v Map VName VName
substs

        substituteInMap :: (a -> a) -> Map VName a -> Map VName a
substituteInMap a -> a
f Map VName a
m =
          let ([VName]
ks, [a]
vs) = [(VName, a)] -> ([VName], [a])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(VName, a)] -> ([VName], [a])) -> [(VName, a)] -> ([VName], [a])
forall a b. (a -> b) -> a -> b
$ Map VName a -> [(VName, a)]
forall k a. Map k a -> [(k, a)]
M.toList Map VName a
m
           in [(VName, a)] -> Map VName a
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(VName, a)] -> Map VName a) -> [(VName, a)] -> Map VName a
forall a b. (a -> b) -> a -> b
$
                [VName] -> [a] -> [(VName, a)]
forall a b. [a] -> [b] -> [(a, b)]
zip
                  ((VName -> VName) -> [VName] -> [VName]
forall a b. (a -> b) -> [a] -> [b]
map (\VName
k -> VName -> Maybe VName -> VName
forall a. a -> Maybe a -> a
fromMaybe VName
k (Maybe VName -> VName) -> Maybe VName -> VName
forall a b. (a -> b) -> a -> b
$ VName -> Map VName VName -> Maybe VName
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
k Map VName VName
substs) [VName]
ks)
                  ((a -> a) -> [a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map a -> a
f [a]
vs)

        substituteInBinding :: BoundV -> BoundV
substituteInBinding (BoundV [TypeParam]
ps TypeBase Size NoUniqueness
t) =
          [TypeParam] -> TypeBase Size NoUniqueness -> BoundV
BoundV ((TypeParam -> TypeParam) -> [TypeParam] -> [TypeParam]
forall a b. (a -> b) -> [a] -> [b]
map TypeParam -> TypeParam
substituteInTypeParam [TypeParam]
ps) (TypeBase Size NoUniqueness -> TypeBase Size NoUniqueness
forall u. TypeBase Size u -> TypeBase Size u
substituteInType TypeBase Size NoUniqueness
t)

        substituteInMod :: Mod -> Mod
substituteInMod (ModEnv Env
env) =
          Env -> Mod
ModEnv (Env -> Mod) -> Env -> Mod
forall a b. (a -> b) -> a -> b
$ Env -> Env
substituteInEnv Env
env
        substituteInMod (ModFun FunModType
funsig) =
          FunModType -> Mod
ModFun (FunModType -> Mod) -> FunModType -> Mod
forall a b. (a -> b) -> a -> b
$ FunModType -> FunModType
substituteInFunModType FunModType
funsig

        substituteInFunModType :: FunModType -> FunModType
substituteInFunModType (FunModType TySet
abs Mod
mod MTy
mty) =
          TySet -> Mod -> MTy -> FunModType
FunModType
            ((QualName VName -> QualName VName) -> TySet -> TySet
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
M.mapKeys ((VName -> VName) -> QualName VName -> QualName VName
forall a b. (a -> b) -> QualName a -> QualName b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap VName -> VName
substitute) TySet
abs)
            (Mod -> Mod
substituteInMod Mod
mod)
            (Map VName VName -> MTy -> MTy
substituteInMTy Map VName VName
substs MTy
mty)

        substituteInTypeBinding :: TypeBinding -> TypeBinding
substituteInTypeBinding (TypeAbbr Liftedness
l [TypeParam]
ps (RetType [VName]
dims TypeBase Size NoUniqueness
t)) =
          Liftedness -> [TypeParam] -> StructRetType -> TypeBinding
TypeAbbr Liftedness
l ((TypeParam -> TypeParam) -> [TypeParam] -> [TypeParam]
forall a b. (a -> b) -> [a] -> [b]
map TypeParam -> TypeParam
substituteInTypeParam [TypeParam]
ps) (StructRetType -> TypeBinding) -> StructRetType -> TypeBinding
forall a b. (a -> b) -> a -> b
$ [VName] -> TypeBase Size NoUniqueness -> StructRetType
forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
dims (TypeBase Size NoUniqueness -> StructRetType)
-> TypeBase Size NoUniqueness -> StructRetType
forall a b. (a -> b) -> a -> b
$ TypeBase Size NoUniqueness -> TypeBase Size NoUniqueness
forall u. TypeBase Size u -> TypeBase Size u
substituteInType TypeBase Size NoUniqueness
t

        substituteInTypeParam :: TypeParam -> TypeParam
substituteInTypeParam (TypeParamDim VName
p SrcLoc
loc) =
          VName -> SrcLoc -> TypeParam
forall vn. vn -> SrcLoc -> TypeParamBase vn
TypeParamDim (VName -> VName
substitute VName
p) SrcLoc
loc
        substituteInTypeParam (TypeParamType Liftedness
l VName
p SrcLoc
loc) =
          Liftedness -> VName -> SrcLoc -> TypeParam
forall vn. Liftedness -> vn -> SrcLoc -> TypeParamBase vn
TypeParamType Liftedness
l (VName -> VName
substitute VName
p) SrcLoc
loc

        substituteInScalarType :: ScalarTypeBase Size u -> ScalarTypeBase Size u
        substituteInScalarType :: forall u. ScalarTypeBase Size u -> ScalarTypeBase Size u
substituteInScalarType (TypeVar u
u (QualName [VName]
qs VName
v) [TypeArg Size]
targs) =
          u -> QualName VName -> [TypeArg Size] -> ScalarTypeBase Size u
forall dim u.
u -> QualName VName -> [TypeArg dim] -> ScalarTypeBase dim u
TypeVar u
u ([VName] -> VName -> QualName VName
forall vn. [vn] -> vn -> QualName vn
QualName ((VName -> VName) -> [VName] -> [VName]
forall a b. (a -> b) -> [a] -> [b]
map VName -> VName
substitute [VName]
qs) (VName -> QualName VName) -> VName -> QualName VName
forall a b. (a -> b) -> a -> b
$ VName -> VName
substitute VName
v) ([TypeArg Size] -> ScalarTypeBase Size u)
-> [TypeArg Size] -> ScalarTypeBase Size u
forall a b. (a -> b) -> a -> b
$
            (TypeArg Size -> TypeArg Size) -> [TypeArg Size] -> [TypeArg Size]
forall a b. (a -> b) -> [a] -> [b]
map TypeArg Size -> TypeArg Size
substituteInTypeArg [TypeArg Size]
targs
        substituteInScalarType (Prim PrimType
t) =
          PrimType -> ScalarTypeBase Size u
forall dim u. PrimType -> ScalarTypeBase dim u
Prim PrimType
t
        substituteInScalarType (Record Map Name (TypeBase Size u)
ts) =
          Map Name (TypeBase Size u) -> ScalarTypeBase Size u
forall dim u. Map Name (TypeBase dim u) -> ScalarTypeBase dim u
Record (Map Name (TypeBase Size u) -> ScalarTypeBase Size u)
-> Map Name (TypeBase Size u) -> ScalarTypeBase Size u
forall a b. (a -> b) -> a -> b
$ (TypeBase Size u -> TypeBase Size u)
-> Map Name (TypeBase Size u) -> Map Name (TypeBase Size u)
forall a b. (a -> b) -> Map Name a -> Map Name b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TypeBase Size u -> TypeBase Size u
forall u. TypeBase Size u -> TypeBase Size u
substituteInType Map Name (TypeBase Size u)
ts
        substituteInScalarType (Sum Map Name [TypeBase Size u]
ts) =
          Map Name [TypeBase Size u] -> ScalarTypeBase Size u
forall dim u. Map Name [TypeBase dim u] -> ScalarTypeBase dim u
Sum (Map Name [TypeBase Size u] -> ScalarTypeBase Size u)
-> Map Name [TypeBase Size u] -> ScalarTypeBase Size u
forall a b. (a -> b) -> a -> b
$ (([TypeBase Size u] -> [TypeBase Size u])
-> Map Name [TypeBase Size u] -> Map Name [TypeBase Size u]
forall a b. (a -> b) -> Map Name a -> Map Name b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([TypeBase Size u] -> [TypeBase Size u])
 -> Map Name [TypeBase Size u] -> Map Name [TypeBase Size u])
-> ((TypeBase Size u -> TypeBase Size u)
    -> [TypeBase Size u] -> [TypeBase Size u])
-> (TypeBase Size u -> TypeBase Size u)
-> Map Name [TypeBase Size u]
-> Map Name [TypeBase Size u]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TypeBase Size u -> TypeBase Size u)
-> [TypeBase Size u] -> [TypeBase Size u]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) TypeBase Size u -> TypeBase Size u
forall u. TypeBase Size u -> TypeBase Size u
substituteInType Map Name [TypeBase Size u]
ts
        substituteInScalarType (Arrow u
als PName
v Diet
d1 TypeBase Size NoUniqueness
t1 (RetType [VName]
dims TypeBase Size Uniqueness
t2)) =
          u
-> PName
-> Diet
-> TypeBase Size NoUniqueness
-> RetTypeBase Size Uniqueness
-> ScalarTypeBase Size u
forall dim u.
u
-> PName
-> Diet
-> TypeBase dim NoUniqueness
-> RetTypeBase dim Uniqueness
-> ScalarTypeBase dim u
Arrow u
als PName
v Diet
d1 (TypeBase Size NoUniqueness -> TypeBase Size NoUniqueness
forall u. TypeBase Size u -> TypeBase Size u
substituteInType TypeBase Size NoUniqueness
t1) (RetTypeBase Size Uniqueness -> ScalarTypeBase Size u)
-> RetTypeBase Size Uniqueness -> ScalarTypeBase Size u
forall a b. (a -> b) -> a -> b
$ [VName] -> TypeBase Size Uniqueness -> RetTypeBase Size Uniqueness
forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
dims (TypeBase Size Uniqueness -> RetTypeBase Size Uniqueness)
-> TypeBase Size Uniqueness -> RetTypeBase Size Uniqueness
forall a b. (a -> b) -> a -> b
$ TypeBase Size Uniqueness -> TypeBase Size Uniqueness
forall u. TypeBase Size u -> TypeBase Size u
substituteInType TypeBase Size Uniqueness
t2

        substituteInType :: TypeBase Size u -> TypeBase Size u
        substituteInType :: forall u. TypeBase Size u -> TypeBase Size u
substituteInType (Scalar ScalarTypeBase Size u
t) = ScalarTypeBase Size u -> TypeBase Size u
forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar (ScalarTypeBase Size u -> TypeBase Size u)
-> ScalarTypeBase Size u -> TypeBase Size u
forall a b. (a -> b) -> a -> b
$ ScalarTypeBase Size u -> ScalarTypeBase Size u
forall u. ScalarTypeBase Size u -> ScalarTypeBase Size u
substituteInScalarType ScalarTypeBase Size u
t
        substituteInType (Array u
u Shape Size
shape ScalarTypeBase Size NoUniqueness
t) =
          u
-> Shape Size
-> ScalarTypeBase Size NoUniqueness
-> TypeBase Size u
forall dim u.
u -> Shape dim -> ScalarTypeBase dim NoUniqueness -> TypeBase dim u
Array u
u (Shape Size -> Shape Size
forall {dim}. Substitutable dim => Shape dim -> Shape dim
substituteInShape Shape Size
shape) (ScalarTypeBase Size NoUniqueness -> TypeBase Size u)
-> ScalarTypeBase Size NoUniqueness -> TypeBase Size u
forall a b. (a -> b) -> a -> b
$ ScalarTypeBase Size NoUniqueness
-> ScalarTypeBase Size NoUniqueness
forall u. ScalarTypeBase Size u -> ScalarTypeBase Size u
substituteInScalarType ScalarTypeBase Size NoUniqueness
t

        substituteInShape :: Shape dim -> Shape dim
substituteInShape (Shape [dim]
ds) = [dim] -> Shape dim
forall dim. [dim] -> Shape dim
Shape ([dim] -> Shape dim) -> [dim] -> Shape dim
forall a b. (a -> b) -> a -> b
$ (dim -> dim) -> [dim] -> [dim]
forall a b. (a -> b) -> [a] -> [b]
map (TypeSubs -> dim -> dim
forall a. Substitutable a => TypeSubs -> a -> a
applySubst TypeSubs
forall {t}. VName -> Maybe (Subst t)
subst) [dim]
ds

        substituteInTypeArg :: TypeArg Size -> TypeArg Size
substituteInTypeArg (TypeArgDim Size
e) =
          Size -> TypeArg Size
forall dim. dim -> TypeArg dim
TypeArgDim (Size -> TypeArg Size) -> Size -> TypeArg Size
forall a b. (a -> b) -> a -> b
$ TypeSubs -> Size -> Size
forall a. Substitutable a => TypeSubs -> a -> a
applySubst TypeSubs
forall {t}. VName -> Maybe (Subst t)
subst Size
e
        substituteInTypeArg (TypeArgType TypeBase Size NoUniqueness
t) =
          TypeBase Size NoUniqueness -> TypeArg Size
forall dim. TypeBase dim NoUniqueness -> TypeArg dim
TypeArgType (TypeBase Size NoUniqueness -> TypeArg Size)
-> TypeBase Size NoUniqueness -> TypeArg Size
forall a b. (a -> b) -> a -> b
$ TypeBase Size NoUniqueness -> TypeBase Size NoUniqueness
forall u. TypeBase Size u -> TypeBase Size u
substituteInType TypeBase Size NoUniqueness
t

mtyTypeAbbrs :: MTy -> M.Map VName TypeBinding
mtyTypeAbbrs :: MTy -> Map VName TypeBinding
mtyTypeAbbrs (MTy TySet
_ Mod
mod) = Mod -> Map VName TypeBinding
modTypeAbbrs Mod
mod

modTypeAbbrs :: Mod -> M.Map VName TypeBinding
modTypeAbbrs :: Mod -> Map VName TypeBinding
modTypeAbbrs (ModEnv Env
env) =
  Env -> Map VName TypeBinding
envTypeAbbrs Env
env
modTypeAbbrs (ModFun (FunModType TySet
_ Mod
mod MTy
mty)) =
  Mod -> Map VName TypeBinding
modTypeAbbrs Mod
mod Map VName TypeBinding
-> Map VName TypeBinding -> Map VName TypeBinding
forall a. Semigroup a => a -> a -> a
<> MTy -> Map VName TypeBinding
mtyTypeAbbrs MTy
mty

envTypeAbbrs :: Env -> M.Map VName TypeBinding
envTypeAbbrs :: Env -> Map VName TypeBinding
envTypeAbbrs Env
env =
  Env -> Map VName TypeBinding
envTypeTable Env
env
    Map VName TypeBinding
-> Map VName TypeBinding -> Map VName TypeBinding
forall a. Semigroup a => a -> a -> a
<> ([Map VName TypeBinding] -> Map VName TypeBinding
forall a. Monoid a => [a] -> a
mconcat ([Map VName TypeBinding] -> Map VName TypeBinding)
-> (Env -> [Map VName TypeBinding]) -> Env -> Map VName TypeBinding
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Mod -> Map VName TypeBinding) -> [Mod] -> [Map VName TypeBinding]
forall a b. (a -> b) -> [a] -> [b]
map Mod -> Map VName TypeBinding
modTypeAbbrs ([Mod] -> [Map VName TypeBinding])
-> (Env -> [Mod]) -> Env -> [Map VName TypeBinding]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map VName Mod -> [Mod]
forall k a. Map k a -> [a]
M.elems (Map VName Mod -> [Mod]) -> (Env -> Map VName Mod) -> Env -> [Mod]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> Map VName Mod
envModTable) Env
env

-- | Refine the given type name in the given env.
refineEnv ::
  SrcLoc ->
  TySet ->
  Env ->
  QualName Name ->
  [TypeParam] ->
  StructType ->
  TypeM (QualName VName, TySet, Env)
refineEnv :: SrcLoc
-> TySet
-> Env
-> QualName Name
-> [TypeParam]
-> TypeBase Size NoUniqueness
-> TypeM (QualName VName, TySet, Env)
refineEnv SrcLoc
loc TySet
tset Env
env QualName Name
tname [TypeParam]
ps TypeBase Size NoUniqueness
t
  | Just (QualName VName
tname', TypeAbbr Liftedness
_ [TypeParam]
cur_ps (RetType [VName]
_ (Scalar (TypeVar NoUniqueness
_ (QualName [VName]
qs VName
v) [TypeArg Size]
_)))) <-
      QualName Name -> Mod -> Maybe (QualName VName, TypeBinding)
findTypeDef QualName Name
tname (Env -> Mod
ModEnv Env
env),
    [VName] -> VName -> QualName VName
forall vn. [vn] -> vn -> QualName vn
QualName (QualName VName -> [VName]
forall vn. QualName vn -> [vn]
qualQuals QualName VName
tname') VName
v QualName VName -> TySet -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`M.member` TySet
tset =
      if [TypeParam] -> [TypeParam] -> Bool
paramsMatch [TypeParam]
cur_ps [TypeParam]
ps
        then
          (QualName VName, TySet, Env) -> TypeM (QualName VName, TySet, Env)
forall a. a -> TypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
            ( QualName VName
tname',
              [VName] -> VName -> QualName VName
forall vn. [vn] -> vn -> QualName vn
QualName [VName]
qs VName
v QualName VName -> TySet -> TySet
forall k a. Ord k => k -> Map k a -> Map k a
`M.delete` TySet
tset,
              TypeSubs -> Env -> Env
substituteTypesInEnv
                ( (VName
 -> Map VName (Subst StructRetType) -> Maybe (Subst StructRetType))
-> Map VName (Subst StructRetType) -> TypeSubs
forall a b c. (a -> b -> c) -> b -> a -> c
flip VName
-> Map VName (Subst StructRetType) -> Maybe (Subst StructRetType)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Map VName (Subst StructRetType) -> TypeSubs)
-> Map VName (Subst StructRetType) -> TypeSubs
forall a b. (a -> b) -> a -> b
$
                    [(VName, Subst StructRetType)] -> Map VName (Subst StructRetType)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
                      [ (QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
tname', [TypeParam] -> StructRetType -> Subst StructRetType
forall t. [TypeParam] -> t -> Subst t
Subst [TypeParam]
cur_ps (StructRetType -> Subst StructRetType)
-> StructRetType -> Subst StructRetType
forall a b. (a -> b) -> a -> b
$ [VName] -> TypeBase Size NoUniqueness -> StructRetType
forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [] TypeBase Size NoUniqueness
t),
                        (VName
v, [TypeParam] -> StructRetType -> Subst StructRetType
forall t. [TypeParam] -> t -> Subst t
Subst [TypeParam]
ps (StructRetType -> Subst StructRetType)
-> StructRetType -> Subst StructRetType
forall a b. (a -> b) -> a -> b
$ [VName] -> TypeBase Size NoUniqueness -> StructRetType
forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [] TypeBase Size NoUniqueness
t)
                      ]
                )
                Env
env
            )
        else
          SrcLoc -> Notes -> Doc () -> TypeM (QualName VName, TySet, Env)
forall loc a. Located loc => loc -> Notes -> Doc () -> TypeM a
forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc Notes
forall a. Monoid a => a
mempty (Doc () -> TypeM (QualName VName, TySet, Env))
-> Doc () -> TypeM (QualName VName, TySet, Env)
forall a b. (a -> b) -> a -> b
$
            Doc ()
"Cannot refine a type having"
              Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [TypeParam] -> Doc ()
forall {a} {ann}. Pretty a => [a] -> Doc ann
tpMsg [TypeParam]
ps
              Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
" with a type having "
              Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> [TypeParam] -> Doc ()
forall {a} {ann}. Pretty a => [a] -> Doc ann
tpMsg [TypeParam]
cur_ps
              Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
  | Bool
otherwise =
      SrcLoc -> Notes -> Doc () -> TypeM (QualName VName, TySet, Env)
forall loc a. Located loc => loc -> Notes -> Doc () -> TypeM a
forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc Notes
forall a. Monoid a => a
mempty (Doc () -> TypeM (QualName VName, TySet, Env))
-> Doc () -> TypeM (QualName VName, TySet, Env)
forall a b. (a -> b) -> a -> b
$ Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (QualName Name -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. QualName Name -> Doc ann
pretty QualName Name
tname) Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"is not an abstract type in the module type."
  where
    tpMsg :: [a] -> Doc ann
tpMsg [] = Doc ann
"no type parameters"
    tpMsg [a]
xs = Doc ann
"type parameters" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep ((a -> Doc ann) -> [a] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map a -> Doc ann
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty [a]
xs)

paramsMatch :: [TypeParam] -> [TypeParam] -> Bool
paramsMatch :: [TypeParam] -> [TypeParam] -> Bool
paramsMatch [TypeParam]
ps1 [TypeParam]
ps2 = [TypeParam] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeParam]
ps1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [TypeParam] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeParam]
ps2 Bool -> Bool -> Bool
&& ((TypeParam, TypeParam) -> Bool)
-> [(TypeParam, TypeParam)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (TypeParam, TypeParam) -> Bool
forall {vn} {vn}. (TypeParamBase vn, TypeParamBase vn) -> Bool
match ([TypeParam] -> [TypeParam] -> [(TypeParam, TypeParam)]
forall a b. [a] -> [b] -> [(a, b)]
zip [TypeParam]
ps1 [TypeParam]
ps2)
  where
    match :: (TypeParamBase vn, TypeParamBase vn) -> Bool
match (TypeParamType Liftedness
l1 vn
_ SrcLoc
_, TypeParamType Liftedness
l2 vn
_ SrcLoc
_) = Liftedness
l1 Liftedness -> Liftedness -> Bool
forall a. Ord a => a -> a -> Bool
<= Liftedness
l2
    match (TypeParamDim vn
_ SrcLoc
_, TypeParamDim vn
_ SrcLoc
_) = Bool
True
    match (TypeParamBase vn, TypeParamBase vn)
_ = Bool
False

findBinding ::
  (Env -> M.Map VName v) ->
  Namespace ->
  Name ->
  Env ->
  Maybe (VName, v)
findBinding :: forall v.
(Env -> Map VName v)
-> Namespace -> Name -> Env -> Maybe (VName, v)
findBinding Env -> Map VName v
table Namespace
namespace Name
name Env
the_env = do
  QualName [VName]
_ VName
name' <- (Namespace, Name) -> NameMap -> Maybe (QualName VName)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Namespace
namespace, Name
name) (NameMap -> Maybe (QualName VName))
-> NameMap -> Maybe (QualName VName)
forall a b. (a -> b) -> a -> b
$ Env -> NameMap
envNameMap Env
the_env
  (VName
name',) (v -> (VName, v)) -> Maybe v -> Maybe (VName, v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VName -> Map VName v -> Maybe v
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
name' (Env -> Map VName v
table Env
the_env)

findTypeDef :: QualName Name -> Mod -> Maybe (QualName VName, TypeBinding)
findTypeDef :: QualName Name -> Mod -> Maybe (QualName VName, TypeBinding)
findTypeDef QualName Name
_ ModFun {} = Maybe (QualName VName, TypeBinding)
forall a. Maybe a
Nothing
findTypeDef (QualName [] Name
name) (ModEnv Env
the_env) = do
  (VName
name', TypeBinding
tb) <- (Env -> Map VName TypeBinding)
-> Namespace -> Name -> Env -> Maybe (VName, TypeBinding)
forall v.
(Env -> Map VName v)
-> Namespace -> Name -> Env -> Maybe (VName, v)
findBinding Env -> Map VName TypeBinding
envTypeTable Namespace
Type Name
name Env
the_env
  (QualName VName, TypeBinding)
-> Maybe (QualName VName, TypeBinding)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VName -> QualName VName
forall v. v -> QualName v
qualName VName
name', TypeBinding
tb)
findTypeDef (QualName (Name
q : [Name]
qs) Name
name) (ModEnv Env
the_env) = do
  (VName
q', Mod
q_mod) <- (Env -> Map VName Mod)
-> Namespace -> Name -> Env -> Maybe (VName, Mod)
forall v.
(Env -> Map VName v)
-> Namespace -> Name -> Env -> Maybe (VName, v)
findBinding Env -> Map VName Mod
envModTable Namespace
Term Name
q Env
the_env
  (QualName [VName]
qs' VName
name', TypeBinding
tb) <- QualName Name -> Mod -> Maybe (QualName VName, TypeBinding)
findTypeDef ([Name] -> Name -> QualName Name
forall vn. [vn] -> vn -> QualName vn
QualName [Name]
qs Name
name) Mod
q_mod
  (QualName VName, TypeBinding)
-> Maybe (QualName VName, TypeBinding)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([VName] -> VName -> QualName VName
forall vn. [vn] -> vn -> QualName vn
QualName (VName
q' VName -> [VName] -> [VName]
forall a. a -> [a] -> [a]
: [VName]
qs') VName
name', TypeBinding
tb)

resolveAbsTypes ::
  TySet ->
  Mod ->
  TySet ->
  Loc ->
  Either TypeError (M.Map VName (QualName VName, TypeBinding))
resolveAbsTypes :: TySet
-> Mod
-> TySet
-> Loc
-> Either TypeError (Map VName (QualName VName, TypeBinding))
resolveAbsTypes TySet
mod_abs Mod
mod TySet
sig_abs Loc
loc = do
  let abs_mapping :: Map (QualName Name) (QualName VName, Liftedness)
abs_mapping =
        [(QualName Name, (QualName VName, Liftedness))]
-> Map (QualName Name) (QualName VName, Liftedness)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(QualName Name, (QualName VName, Liftedness))]
 -> Map (QualName Name) (QualName VName, Liftedness))
-> [(QualName Name, (QualName VName, Liftedness))]
-> Map (QualName Name) (QualName VName, Liftedness)
forall a b. (a -> b) -> a -> b
$
          [QualName Name]
-> [(QualName VName, Liftedness)]
-> [(QualName Name, (QualName VName, Liftedness))]
forall a b. [a] -> [b] -> [(a, b)]
zip
            (((QualName VName, Liftedness) -> QualName Name)
-> [(QualName VName, Liftedness)] -> [QualName Name]
forall a b. (a -> b) -> [a] -> [b]
map ((VName -> Name) -> QualName VName -> QualName Name
forall a b. (a -> b) -> QualName a -> QualName b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap VName -> Name
baseName (QualName VName -> QualName Name)
-> ((QualName VName, Liftedness) -> QualName VName)
-> (QualName VName, Liftedness)
-> QualName Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (QualName VName, Liftedness) -> QualName VName
forall a b. (a, b) -> a
fst) ([(QualName VName, Liftedness)] -> [QualName Name])
-> [(QualName VName, Liftedness)] -> [QualName Name]
forall a b. (a -> b) -> a -> b
$ TySet -> [(QualName VName, Liftedness)]
forall k a. Map k a -> [(k, a)]
M.toList TySet
mod_abs)
            (TySet -> [(QualName VName, Liftedness)]
forall k a. Map k a -> [(k, a)]
M.toList TySet
mod_abs)
  ([(VName, (QualName VName, TypeBinding))]
 -> Map VName (QualName VName, TypeBinding))
-> Either TypeError [(VName, (QualName VName, TypeBinding))]
-> Either TypeError (Map VName (QualName VName, TypeBinding))
forall a b. (a -> b) -> Either TypeError a -> Either TypeError b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(VName, (QualName VName, TypeBinding))]
-> Map VName (QualName VName, TypeBinding)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (Either TypeError [(VName, (QualName VName, TypeBinding))]
 -> Either TypeError (Map VName (QualName VName, TypeBinding)))
-> (((QualName VName, Liftedness)
     -> Either TypeError (VName, (QualName VName, TypeBinding)))
    -> Either TypeError [(VName, (QualName VName, TypeBinding))])
-> ((QualName VName, Liftedness)
    -> Either TypeError (VName, (QualName VName, TypeBinding)))
-> Either TypeError (Map VName (QualName VName, TypeBinding))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(QualName VName, Liftedness)]
-> ((QualName VName, Liftedness)
    -> Either TypeError (VName, (QualName VName, TypeBinding)))
-> Either TypeError [(VName, (QualName VName, TypeBinding))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (TySet -> [(QualName VName, Liftedness)]
forall k a. Map k a -> [(k, a)]
M.toList TySet
sig_abs) (((QualName VName, Liftedness)
  -> Either TypeError (VName, (QualName VName, TypeBinding)))
 -> Either TypeError (Map VName (QualName VName, TypeBinding)))
-> ((QualName VName, Liftedness)
    -> Either TypeError (VName, (QualName VName, TypeBinding)))
-> Either TypeError (Map VName (QualName VName, TypeBinding))
forall a b. (a -> b) -> a -> b
$ \(QualName VName
name, Liftedness
name_l) ->
    case QualName Name -> Mod -> Maybe (QualName VName, TypeBinding)
findTypeDef ((VName -> Name) -> QualName VName -> QualName Name
forall a b. (a -> b) -> QualName a -> QualName b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap VName -> Name
baseName QualName VName
name) Mod
mod of
      Just (QualName VName
name', TypeAbbr Liftedness
mod_l [TypeParam]
ps StructRetType
t)
        | Liftedness
mod_l Liftedness -> Liftedness -> Bool
forall a. Ord a => a -> a -> Bool
> Liftedness
name_l ->
            Liftedness
-> [VName]
-> QualName VName
-> (Liftedness, [TypeParam], StructRetType)
-> Either TypeError (VName, (QualName VName, TypeBinding))
forall {b}.
Liftedness
-> [VName]
-> QualName VName
-> (Liftedness, [TypeParam], StructRetType)
-> Either TypeError b
mismatchedLiftedness
              Liftedness
name_l
              ((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
mod_abs)
              QualName VName
name
              (Liftedness
mod_l, [TypeParam]
ps, StructRetType
t)
        | Liftedness
name_l Liftedness -> Liftedness -> Bool
forall a. Ord a => a -> a -> Bool
< Liftedness
SizeLifted,
          Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [VName] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([VName] -> Bool) -> [VName] -> Bool
forall a b. (a -> b) -> a -> b
$ StructRetType -> [VName]
forall dim as. RetTypeBase dim as -> [VName]
retDims StructRetType
t ->
            [VName]
-> QualName VName
-> (Liftedness, [TypeParam], StructRetType)
-> Either TypeError (VName, (QualName VName, TypeBinding))
forall {b}.
[VName]
-> QualName VName
-> (Liftedness, [TypeParam], StructRetType)
-> Either TypeError b
anonymousSizes
              ((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
mod_abs)
              QualName VName
name
              (Liftedness
mod_l, [TypeParam]
ps, StructRetType
t)
        | Just (QualName VName
abs_name, Liftedness
_) <- QualName Name
-> Map (QualName Name) (QualName VName, Liftedness)
-> Maybe (QualName VName, Liftedness)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup ((VName -> Name) -> QualName VName -> QualName Name
forall a b. (a -> b) -> QualName a -> QualName b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap VName -> Name
baseName QualName VName
name) Map (QualName Name) (QualName VName, Liftedness)
abs_mapping ->
            (VName, (QualName VName, TypeBinding))
-> Either TypeError (VName, (QualName VName, TypeBinding))
forall a. a -> Either TypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
name, (QualName VName
abs_name, Liftedness -> [TypeParam] -> StructRetType -> TypeBinding
TypeAbbr Liftedness
name_l [TypeParam]
ps StructRetType
t))
        | Bool
otherwise ->
            (VName, (QualName VName, TypeBinding))
-> Either TypeError (VName, (QualName VName, TypeBinding))
forall a. a -> Either TypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
name, (QualName VName
name', Liftedness -> [TypeParam] -> StructRetType -> TypeBinding
TypeAbbr Liftedness
name_l [TypeParam]
ps StructRetType
t))
      Maybe (QualName VName, TypeBinding)
_ ->
        Loc
-> QualName Name
-> Either TypeError (VName, (QualName VName, TypeBinding))
forall a b. Pretty a => Loc -> a -> Either TypeError b
missingType Loc
loc (QualName Name
 -> Either TypeError (VName, (QualName VName, TypeBinding)))
-> QualName Name
-> Either TypeError (VName, (QualName VName, TypeBinding))
forall a b. (a -> b) -> a -> b
$ (VName -> Name) -> QualName VName -> QualName Name
forall a b. (a -> b) -> QualName a -> QualName b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap VName -> Name
baseName QualName VName
name
  where
    mismatchedLiftedness :: Liftedness
-> [VName]
-> QualName VName
-> (Liftedness, [TypeParam], StructRetType)
-> Either TypeError b
mismatchedLiftedness Liftedness
name_l [VName]
abs QualName VName
name (Liftedness, [TypeParam], StructRetType)
mod_t =
      TypeError -> Either TypeError b
forall a b. a -> Either a b
Left (TypeError -> Either TypeError b)
-> (Doc () -> TypeError) -> Doc () -> Either TypeError b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Loc -> Notes -> Doc () -> TypeError
TypeError (Loc -> Loc
forall a. Located a => a -> Loc
locOf Loc
loc) Notes
forall a. Monoid a => a
mempty (Doc () -> Either TypeError b) -> Doc () -> Either TypeError b
forall a b. (a -> b) -> a -> b
$
        Doc ()
"Module defines"
          Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Int -> Doc () -> Doc ()
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 ([VName]
-> QualName VName
-> (Liftedness, [TypeParam], StructRetType)
-> Doc ()
forall a.
[VName]
-> QualName VName
-> (Liftedness, [TypeParam], StructRetType)
-> Doc a
ppTypeAbbr [VName]
abs QualName VName
name (Liftedness, [TypeParam], StructRetType)
mod_t)
          Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"but module type requires"
          Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
what
          Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
      where
        what :: Doc ()
what = case Liftedness
name_l of
          Liftedness
Unlifted -> Doc ()
"a non-lifted type"
          Liftedness
SizeLifted -> Doc ()
"a size-lifted type"
          Liftedness
Lifted -> Doc ()
"a lifted type"

    anonymousSizes :: [VName]
-> QualName VName
-> (Liftedness, [TypeParam], StructRetType)
-> Either TypeError b
anonymousSizes [VName]
abs QualName VName
name (Liftedness, [TypeParam], StructRetType)
mod_t =
      TypeError -> Either TypeError b
forall a b. a -> Either a b
Left (TypeError -> Either TypeError b)
-> (Doc () -> TypeError) -> Doc () -> Either TypeError b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Loc -> Notes -> Doc () -> TypeError
TypeError (Loc -> Loc
forall a. Located a => a -> Loc
locOf Loc
loc) Notes
forall a. Monoid a => a
mempty (Doc () -> Either TypeError b) -> Doc () -> Either TypeError b
forall a b. (a -> b) -> a -> b
$
        Doc ()
"Module defines"
          Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Int -> Doc () -> Doc ()
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 ([VName]
-> QualName VName
-> (Liftedness, [TypeParam], StructRetType)
-> Doc ()
forall a.
[VName]
-> QualName VName
-> (Liftedness, [TypeParam], StructRetType)
-> Doc a
ppTypeAbbr [VName]
abs QualName VName
name (Liftedness, [TypeParam], StructRetType)
mod_t)
          Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"which contains anonymous sizes, but module type requires non-lifted type."

resolveMTyNames ::
  MTy ->
  MTy ->
  M.Map VName (QualName VName)
resolveMTyNames :: MTy -> MTy -> Map VName (QualName VName)
resolveMTyNames = MTy -> MTy -> Map VName (QualName VName)
resolveMTyNames'
  where
    resolveMTyNames' :: MTy -> MTy -> Map VName (QualName VName)
resolveMTyNames' (MTy TySet
_mod_abs Mod
mod) (MTy TySet
_sig_abs Mod
sig) =
      Mod -> Mod -> Map VName (QualName VName)
resolveModNames Mod
mod Mod
sig

    resolveModNames :: Mod -> Mod -> Map VName (QualName VName)
resolveModNames (ModEnv Env
mod_env) (ModEnv Env
sig_env) =
      Env -> Env -> Map VName (QualName VName)
resolveEnvNames Env
mod_env Env
sig_env
    resolveModNames (ModFun FunModType
mod_fun) (ModFun FunModType
sig_fun) =
      Mod -> Mod -> Map VName (QualName VName)
resolveModNames (FunModType -> Mod
funModTypeMod FunModType
mod_fun) (FunModType -> Mod
funModTypeMod FunModType
sig_fun)
        Map VName (QualName VName)
-> Map VName (QualName VName) -> Map VName (QualName VName)
forall a. Semigroup a => a -> a -> a
<> MTy -> MTy -> Map VName (QualName VName)
resolveMTyNames' (FunModType -> MTy
funModTypeMty FunModType
mod_fun) (FunModType -> MTy
funModTypeMty FunModType
sig_fun)
    resolveModNames Mod
_ Mod
_ =
      Map VName (QualName VName)
forall a. Monoid a => a
mempty

    resolveEnvNames :: Env -> Env -> Map VName (QualName VName)
resolveEnvNames Env
mod_env Env
sig_env =
      let mod_substs :: Map VName (QualName VName)
mod_substs = Namespace -> Env -> Map VName Mod -> Map VName (QualName VName)
forall {a}.
Namespace -> Env -> Map VName a -> Map VName (QualName VName)
resolve Namespace
Term Env
mod_env (Map VName Mod -> Map VName (QualName VName))
-> Map VName Mod -> Map VName (QualName VName)
forall a b. (a -> b) -> a -> b
$ Env -> Map VName Mod
envModTable Env
sig_env
          onMod :: (VName, Mod) -> Map VName (QualName VName)
onMod (VName
modname, Mod
mod_env_mod) =
            case VName -> Map VName (QualName VName) -> Maybe (QualName VName)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
modname Map VName (QualName VName)
mod_substs of
              Just (QualName [VName]
_ VName
modname')
                | Just Mod
sig_env_mod <-
                    VName -> Map VName Mod -> Maybe Mod
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
modname' (Map VName Mod -> Maybe Mod) -> Map VName Mod -> Maybe Mod
forall a b. (a -> b) -> a -> b
$ Env -> Map VName Mod
envModTable Env
mod_env ->
                    Mod -> Mod -> Map VName (QualName VName)
resolveModNames Mod
sig_env_mod Mod
mod_env_mod
              Maybe (QualName VName)
_ -> Map VName (QualName VName)
forall a. Monoid a => a
mempty
       in [Map VName (QualName VName)] -> Map VName (QualName VName)
forall a. Monoid a => [a] -> a
mconcat
            [ Namespace -> Env -> Map VName BoundV -> Map VName (QualName VName)
forall {a}.
Namespace -> Env -> Map VName a -> Map VName (QualName VName)
resolve Namespace
Term Env
mod_env (Map VName BoundV -> Map VName (QualName VName))
-> Map VName BoundV -> Map VName (QualName VName)
forall a b. (a -> b) -> a -> b
$ Env -> Map VName BoundV
envVtable Env
sig_env,
              Namespace -> Env -> Map VName BoundV -> Map VName (QualName VName)
forall {a}.
Namespace -> Env -> Map VName a -> Map VName (QualName VName)
resolve Namespace
Type Env
mod_env (Map VName BoundV -> Map VName (QualName VName))
-> Map VName BoundV -> Map VName (QualName VName)
forall a b. (a -> b) -> a -> b
$ Env -> Map VName BoundV
envVtable Env
sig_env,
              Namespace -> Env -> Map VName BoundV -> Map VName (QualName VName)
forall {a}.
Namespace -> Env -> Map VName a -> Map VName (QualName VName)
resolve Namespace
Signature Env
mod_env (Map VName BoundV -> Map VName (QualName VName))
-> Map VName BoundV -> Map VName (QualName VName)
forall a b. (a -> b) -> a -> b
$ Env -> Map VName BoundV
envVtable Env
sig_env,
              Map VName (QualName VName)
mod_substs,
              [Map VName (QualName VName)] -> Map VName (QualName VName)
forall a. Monoid a => [a] -> a
mconcat ([Map VName (QualName VName)] -> Map VName (QualName VName))
-> [Map VName (QualName VName)] -> Map VName (QualName VName)
forall a b. (a -> b) -> a -> b
$ ((VName, Mod) -> Map VName (QualName VName))
-> [(VName, Mod)] -> [Map VName (QualName VName)]
forall a b. (a -> b) -> [a] -> [b]
map (VName, Mod) -> Map VName (QualName VName)
onMod ([(VName, Mod)] -> [Map VName (QualName VName)])
-> [(VName, Mod)] -> [Map VName (QualName VName)]
forall a b. (a -> b) -> a -> b
$ Map VName Mod -> [(VName, Mod)]
forall k a. Map k a -> [(k, a)]
M.toList (Map VName Mod -> [(VName, Mod)])
-> Map VName Mod -> [(VName, Mod)]
forall a b. (a -> b) -> a -> b
$ Env -> Map VName Mod
envModTable Env
sig_env
            ]

    resolve :: Namespace -> Env -> Map VName a -> Map VName (QualName VName)
resolve Namespace
namespace Env
mod_env = (VName -> a -> Maybe (QualName VName))
-> Map VName a -> Map VName (QualName VName)
forall k a b. (k -> a -> Maybe b) -> Map k a -> Map k b
M.mapMaybeWithKey VName -> a -> Maybe (QualName VName)
forall {p}. VName -> p -> Maybe (QualName VName)
resolve'
      where
        resolve' :: VName -> p -> Maybe (QualName VName)
resolve' VName
name p
_ =
          (Namespace, Name) -> NameMap -> Maybe (QualName VName)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Namespace
namespace, VName -> Name
baseName VName
name) (NameMap -> Maybe (QualName VName))
-> NameMap -> Maybe (QualName VName)
forall a b. (a -> b) -> a -> b
$ Env -> NameMap
envNameMap Env
mod_env

missingType :: (Pretty a) => Loc -> a -> Either TypeError b
missingType :: forall a b. Pretty a => Loc -> a -> Either TypeError b
missingType Loc
loc a
name =
  TypeError -> Either TypeError b
forall a b. a -> Either a b
Left (TypeError -> Either TypeError b)
-> (Doc () -> TypeError) -> Doc () -> Either TypeError b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Loc -> Notes -> Doc () -> TypeError
TypeError Loc
loc Notes
forall a. Monoid a => a
mempty (Doc () -> Either TypeError b) -> Doc () -> Either TypeError b
forall a b. (a -> b) -> a -> b
$
    Doc ()
"Module does not define a type named" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> a -> Doc ()
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
name Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."

missingVal :: (Pretty a) => Loc -> a -> Either TypeError b
missingVal :: forall a b. Pretty a => Loc -> a -> Either TypeError b
missingVal Loc
loc a
name =
  TypeError -> Either TypeError b
forall a b. a -> Either a b
Left (TypeError -> Either TypeError b)
-> (Doc () -> TypeError) -> Doc () -> Either TypeError b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Loc -> Notes -> Doc () -> TypeError
TypeError Loc
loc Notes
forall a. Monoid a => a
mempty (Doc () -> Either TypeError b) -> Doc () -> Either TypeError b
forall a b. (a -> b) -> a -> b
$
    Doc ()
"Module does not define a value named" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> a -> Doc ()
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
name Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."

topLevelSize :: Loc -> VName -> Either TypeError b
topLevelSize :: forall b. Loc -> VName -> Either TypeError b
topLevelSize Loc
loc VName
name =
  TypeError -> Either TypeError b
forall a b. a -> Either a b
Left (TypeError -> Either TypeError b)
-> (Doc () -> TypeError) -> Doc () -> Either TypeError b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Loc -> Notes -> Doc () -> TypeError
TypeError Loc
loc Notes
forall a. Monoid a => a
mempty (Doc () -> Either TypeError b) -> Doc () -> Either TypeError b
forall a b. (a -> b) -> a -> b
$
    Doc ()
"Type substitution in" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (VName -> Doc ()
forall a. VName -> Doc a
forall v a. IsName v => v -> Doc a
prettyName VName
name) Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"results in a top-level size."

missingMod :: (Pretty a) => Loc -> a -> Either TypeError b
missingMod :: forall a b. Pretty a => Loc -> a -> Either TypeError b
missingMod Loc
loc a
name =
  TypeError -> Either TypeError b
forall a b. a -> Either a b
Left (TypeError -> Either TypeError b)
-> (Doc () -> TypeError) -> Doc () -> Either TypeError b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Loc -> Notes -> Doc () -> TypeError
TypeError Loc
loc Notes
forall a. Monoid a => a
mempty (Doc () -> Either TypeError b) -> Doc () -> Either TypeError b
forall a b. (a -> b) -> a -> b
$
    Doc ()
"Module does not define a module named" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> a -> Doc ()
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
name Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."

mismatchedType ::
  Loc ->
  [VName] ->
  [VName] ->
  VName ->
  (Liftedness, [TypeParam], StructRetType) ->
  (Liftedness, [TypeParam], StructRetType) ->
  Either TypeError b
mismatchedType :: forall b.
Loc
-> [VName]
-> [VName]
-> VName
-> (Liftedness, [TypeParam], StructRetType)
-> (Liftedness, [TypeParam], StructRetType)
-> Either TypeError b
mismatchedType Loc
loc [VName]
abs [VName]
quals VName
name (Liftedness, [TypeParam], StructRetType)
spec_t (Liftedness, [TypeParam], StructRetType)
env_t =
  TypeError -> Either TypeError b
forall a b. a -> Either a b
Left (TypeError -> Either TypeError b)
-> (Doc () -> TypeError) -> Doc () -> Either TypeError b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Loc -> Notes -> Doc () -> TypeError
TypeError Loc
loc Notes
forall a. Monoid a => a
mempty (Doc () -> Either TypeError b) -> Doc () -> Either TypeError b
forall a b. (a -> b) -> a -> b
$
    Doc ()
"Module defines"
      Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Int -> Doc () -> Doc ()
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 ([VName]
-> QualName VName
-> (Liftedness, [TypeParam], StructRetType)
-> Doc ()
forall a.
[VName]
-> QualName VName
-> (Liftedness, [TypeParam], StructRetType)
-> Doc a
ppTypeAbbr [VName]
abs ([VName] -> VName -> QualName VName
forall vn. [vn] -> vn -> QualName vn
QualName [VName]
quals VName
name) (Liftedness, [TypeParam], StructRetType)
env_t)
      Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"but module type requires"
      Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Int -> Doc () -> Doc ()
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 ([VName]
-> QualName VName
-> (Liftedness, [TypeParam], StructRetType)
-> Doc ()
forall a.
[VName]
-> QualName VName
-> (Liftedness, [TypeParam], StructRetType)
-> Doc a
ppTypeAbbr [VName]
abs ([VName] -> VName -> QualName VName
forall vn. [vn] -> vn -> QualName vn
QualName [VName]
quals VName
name) (Liftedness, [TypeParam], StructRetType)
spec_t)

ppTypeAbbr :: [VName] -> QualName VName -> (Liftedness, [TypeParam], StructRetType) -> Doc a
ppTypeAbbr :: forall a.
[VName]
-> QualName VName
-> (Liftedness, [TypeParam], StructRetType)
-> Doc a
ppTypeAbbr [VName]
abs QualName VName
name (Liftedness
l, [TypeParam]
ps, RetType [] (Scalar (TypeVar NoUniqueness
_ QualName VName
tn [TypeArg Size]
args)))
  | QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
tn VName -> [VName] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [VName]
abs,
    (TypeParam -> TypeArg Size) -> [TypeParam] -> [TypeArg Size]
forall a b. (a -> b) -> [a] -> [b]
map TypeParam -> TypeArg Size
typeParamToArg [TypeParam]
ps [TypeArg Size] -> [TypeArg Size] -> Bool
forall a. Eq a => a -> a -> Bool
== [TypeArg Size]
args =
      Doc a
"type"
        Doc a -> Doc a -> Doc a
forall a. Semigroup a => a -> a -> a
<> Liftedness -> Doc a
forall a ann. Pretty a => a -> Doc ann
forall ann. Liftedness -> Doc ann
pretty Liftedness
l
          Doc a -> Doc a -> Doc a
forall ann. Doc ann -> Doc ann -> Doc ann
<+> QualName VName -> Doc a
forall a ann. Pretty a => a -> Doc ann
forall ann. QualName VName -> Doc ann
pretty QualName VName
name
          Doc a -> Doc a -> Doc a
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Doc a] -> Doc a
forall ann. [Doc ann] -> Doc ann
hsep ((TypeParam -> Doc a) -> [TypeParam] -> [Doc a]
forall a b. (a -> b) -> [a] -> [b]
map TypeParam -> Doc a
forall a ann. Pretty a => a -> Doc ann
forall ann. TypeParam -> Doc ann
pretty [TypeParam]
ps)
ppTypeAbbr [VName]
_ QualName VName
name (Liftedness
l, [TypeParam]
ps, StructRetType
t) =
  Doc a
"type"
    Doc a -> Doc a -> Doc a
forall a. Semigroup a => a -> a -> a
<> Liftedness -> Doc a
forall a ann. Pretty a => a -> Doc ann
forall ann. Liftedness -> Doc ann
pretty Liftedness
l
      Doc a -> Doc a -> Doc a
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Doc a] -> Doc a
forall ann. [Doc ann] -> Doc ann
hsep (QualName VName -> Doc a
forall a ann. Pretty a => a -> Doc ann
forall ann. QualName VName -> Doc ann
pretty QualName VName
name Doc a -> [Doc a] -> [Doc a]
forall a. a -> [a] -> [a]
: (TypeParam -> Doc a) -> [TypeParam] -> [Doc a]
forall a b. (a -> b) -> [a] -> [b]
map TypeParam -> Doc a
forall a ann. Pretty a => a -> Doc ann
forall ann. TypeParam -> Doc ann
pretty [TypeParam]
ps)
      Doc a -> Doc a -> Doc a
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc a
forall ann. Doc ann
equals
      Doc a -> Doc a -> Doc a
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Int -> Doc a -> Doc a
forall ann. Int -> Doc ann -> Doc ann
nest Int
2 (Doc a -> Doc a
forall ann. Doc ann -> Doc ann
align (StructRetType -> Doc a
forall a ann. Pretty a => a -> Doc ann
forall ann. StructRetType -> Doc ann
pretty StructRetType
t))

-- | Return new renamed/abstracted env, as well as a mapping from
-- names in the signature to names in the new env.  This is used for
-- functor application.  The first env is the module env, and the
-- second the env it must match.
matchMTys ::
  MTy ->
  MTy ->
  Loc ->
  Either TypeError (M.Map VName VName)
matchMTys :: MTy -> MTy -> Loc -> Either TypeError (Map VName VName)
matchMTys MTy
orig_mty MTy
orig_mty_sig =
  Map VName (Subst StructRetType)
-> [VName]
-> MTy
-> MTy
-> Loc
-> Either TypeError (Map VName VName)
matchMTys'
    ((QualName VName -> Subst StructRetType)
-> Map VName (QualName VName) -> Map VName (Subst StructRetType)
forall a b k. (a -> b) -> Map k a -> Map k b
M.map (Size -> Subst StructRetType
forall t. Size -> Subst t
ExpSubst (Size -> Subst StructRetType)
-> (QualName VName -> Size)
-> QualName VName
-> Subst StructRetType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (QualName VName -> SrcLoc -> Size)
-> SrcLoc -> QualName VName -> Size
forall a b c. (a -> b -> c) -> b -> a -> c
flip QualName VName -> SrcLoc -> Size
sizeFromName SrcLoc
forall a. Monoid a => a
mempty) (Map VName (QualName VName) -> Map VName (Subst StructRetType))
-> Map VName (QualName VName) -> Map VName (Subst StructRetType)
forall a b. (a -> b) -> a -> b
$ MTy -> MTy -> Map VName (QualName VName)
resolveMTyNames MTy
orig_mty MTy
orig_mty_sig)
    []
    MTy
orig_mty
    MTy
orig_mty_sig
  where
    matchMTys' ::
      M.Map VName (Subst StructRetType) ->
      [VName] ->
      MTy ->
      MTy ->
      Loc ->
      Either TypeError (M.Map VName VName)

    matchMTys' :: Map VName (Subst StructRetType)
-> [VName]
-> MTy
-> MTy
-> Loc
-> Either TypeError (Map VName VName)
matchMTys' Map VName (Subst StructRetType)
_ [VName]
_ (MTy TySet
_ ModFun {}) (MTy TySet
_ ModEnv {}) Loc
loc =
      TypeError -> Either TypeError (Map VName VName)
forall a b. a -> Either a b
Left (TypeError -> Either TypeError (Map VName VName))
-> TypeError -> Either TypeError (Map VName VName)
forall a b. (a -> b) -> a -> b
$
        Loc -> Notes -> Doc () -> TypeError
TypeError
          Loc
loc
          Notes
forall a. Monoid a => a
mempty
          Doc ()
"Cannot match parametric module with non-parametric module type."
    matchMTys' Map VName (Subst StructRetType)
_ [VName]
_ (MTy TySet
_ ModEnv {}) (MTy TySet
_ ModFun {}) Loc
loc =
      TypeError -> Either TypeError (Map VName VName)
forall a b. a -> Either a b
Left (TypeError -> Either TypeError (Map VName VName))
-> TypeError -> Either TypeError (Map VName VName)
forall a b. (a -> b) -> a -> b
$
        Loc -> Notes -> Doc () -> TypeError
TypeError
          Loc
loc
          Notes
forall a. Monoid a => a
mempty
          Doc ()
"Cannot match non-parametric module with paramatric module type."
    matchMTys' Map VName (Subst StructRetType)
old_abs_subst_to_type [VName]
quals (MTy TySet
mod_abs Mod
mod) (MTy TySet
sig_abs Mod
sig) Loc
loc = do
      -- Check that abstract types in 'sig' have an implementation in
      -- 'mod'.  This also gives us a substitution that we use to check
      -- the types of values.
      Map VName (QualName VName, TypeBinding)
abs_substs <- TySet
-> Mod
-> TySet
-> Loc
-> Either TypeError (Map VName (QualName VName, TypeBinding))
resolveAbsTypes TySet
mod_abs Mod
mod TySet
sig_abs Loc
loc

      let abs_subst_to_type :: Map VName (Subst StructRetType)
abs_subst_to_type =
            Map VName (Subst StructRetType)
old_abs_subst_to_type Map VName (Subst StructRetType)
-> Map VName (Subst StructRetType)
-> Map VName (Subst StructRetType)
forall a. Semigroup a => a -> a -> a
<> ((QualName VName, TypeBinding) -> Subst StructRetType)
-> Map VName (QualName VName, TypeBinding)
-> Map VName (Subst StructRetType)
forall a b k. (a -> b) -> Map k a -> Map k b
M.map (TypeBinding -> Subst StructRetType
substFromAbbr (TypeBinding -> Subst StructRetType)
-> ((QualName VName, TypeBinding) -> TypeBinding)
-> (QualName VName, TypeBinding)
-> Subst StructRetType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (QualName VName, TypeBinding) -> TypeBinding
forall a b. (a, b) -> b
snd) Map VName (QualName VName, TypeBinding)
abs_substs
          abs_name_substs :: Map VName VName
abs_name_substs = ((QualName VName, TypeBinding) -> VName)
-> Map VName (QualName VName, TypeBinding) -> Map VName VName
forall a b k. (a -> b) -> Map k a -> Map k b
M.map (QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf (QualName VName -> VName)
-> ((QualName VName, TypeBinding) -> QualName VName)
-> (QualName VName, TypeBinding)
-> VName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (QualName VName, TypeBinding) -> QualName VName
forall a b. (a, b) -> a
fst) Map VName (QualName VName, TypeBinding)
abs_substs
      Map VName VName
substs <- Map VName (Subst StructRetType)
-> [VName]
-> Mod
-> Mod
-> Loc
-> Either TypeError (Map VName VName)
matchMods Map VName (Subst StructRetType)
abs_subst_to_type [VName]
quals Mod
mod Mod
sig Loc
loc
      Map VName VName -> Either TypeError (Map VName VName)
forall a. a -> Either TypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map VName VName
substs Map VName VName -> Map VName VName -> Map VName VName
forall a. Semigroup a => a -> a -> a
<> Map VName VName
abs_name_substs)

    matchMods ::
      M.Map VName (Subst StructRetType) ->
      [VName] ->
      Mod ->
      Mod ->
      Loc ->
      Either TypeError (M.Map VName VName)
    matchMods :: Map VName (Subst StructRetType)
-> [VName]
-> Mod
-> Mod
-> Loc
-> Either TypeError (Map VName VName)
matchMods Map VName (Subst StructRetType)
_ [VName]
_ ModEnv {} ModFun {} Loc
loc =
      TypeError -> Either TypeError (Map VName VName)
forall a b. a -> Either a b
Left (TypeError -> Either TypeError (Map VName VName))
-> TypeError -> Either TypeError (Map VName VName)
forall a b. (a -> b) -> a -> b
$
        Loc -> Notes -> Doc () -> TypeError
TypeError
          Loc
loc
          Notes
forall a. Monoid a => a
mempty
          Doc ()
"Cannot match non-parametric module with parametric module type."
    matchMods Map VName (Subst StructRetType)
_ [VName]
_ ModFun {} ModEnv {} Loc
loc =
      TypeError -> Either TypeError (Map VName VName)
forall a b. a -> Either a b
Left (TypeError -> Either TypeError (Map VName VName))
-> TypeError -> Either TypeError (Map VName VName)
forall a b. (a -> b) -> a -> b
$
        Loc -> Notes -> Doc () -> TypeError
TypeError
          Loc
loc
          Notes
forall a. Monoid a => a
mempty
          Doc ()
"Cannot match parametric module with non-parametric module type."
    matchMods Map VName (Subst StructRetType)
abs_subst_to_type [VName]
quals (ModEnv Env
mod) (ModEnv Env
sig) Loc
loc =
      Map VName (Subst StructRetType)
-> [VName]
-> Env
-> Env
-> Loc
-> Either TypeError (Map VName VName)
matchEnvs Map VName (Subst StructRetType)
abs_subst_to_type [VName]
quals Env
mod Env
sig Loc
loc
    matchMods
      Map VName (Subst StructRetType)
old_abs_subst_to_type
      [VName]
quals
      (ModFun (FunModType TySet
mod_abs Mod
mod_pmod MTy
mod_mod))
      (ModFun (FunModType TySet
sig_abs Mod
sig_pmod MTy
sig_mod))
      Loc
loc = do
        -- We need to use different substitutions when matching
        -- parameter and body signatures - this is because the
        -- concrete parameter must be *at least as* general as the
        -- ascripted parameter, while the concrete body must be *at
        -- most as* general as the ascripted body.
        Map VName (QualName VName, TypeBinding)
abs_substs <- TySet
-> Mod
-> TySet
-> Loc
-> Either TypeError (Map VName (QualName VName, TypeBinding))
resolveAbsTypes TySet
mod_abs Mod
mod_pmod TySet
sig_abs Loc
loc
        Map VName (QualName VName, TypeBinding)
p_abs_substs <- TySet
-> Mod
-> TySet
-> Loc
-> Either TypeError (Map VName (QualName VName, TypeBinding))
resolveAbsTypes TySet
sig_abs Mod
sig_pmod TySet
mod_abs Loc
loc
        let abs_subst_to_type :: Map VName (Subst StructRetType)
abs_subst_to_type =
              Map VName (Subst StructRetType)
old_abs_subst_to_type Map VName (Subst StructRetType)
-> Map VName (Subst StructRetType)
-> Map VName (Subst StructRetType)
forall a. Semigroup a => a -> a -> a
<> ((QualName VName, TypeBinding) -> Subst StructRetType)
-> Map VName (QualName VName, TypeBinding)
-> Map VName (Subst StructRetType)
forall a b k. (a -> b) -> Map k a -> Map k b
M.map (TypeBinding -> Subst StructRetType
substFromAbbr (TypeBinding -> Subst StructRetType)
-> ((QualName VName, TypeBinding) -> TypeBinding)
-> (QualName VName, TypeBinding)
-> Subst StructRetType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (QualName VName, TypeBinding) -> TypeBinding
forall a b. (a, b) -> b
snd) Map VName (QualName VName, TypeBinding)
abs_substs
            p_abs_subst_to_type :: Map VName (Subst StructRetType)
p_abs_subst_to_type =
              Map VName (Subst StructRetType)
old_abs_subst_to_type Map VName (Subst StructRetType)
-> Map VName (Subst StructRetType)
-> Map VName (Subst StructRetType)
forall a. Semigroup a => a -> a -> a
<> ((QualName VName, TypeBinding) -> Subst StructRetType)
-> Map VName (QualName VName, TypeBinding)
-> Map VName (Subst StructRetType)
forall a b k. (a -> b) -> Map k a -> Map k b
M.map (TypeBinding -> Subst StructRetType
substFromAbbr (TypeBinding -> Subst StructRetType)
-> ((QualName VName, TypeBinding) -> TypeBinding)
-> (QualName VName, TypeBinding)
-> Subst StructRetType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (QualName VName, TypeBinding) -> TypeBinding
forall a b. (a, b) -> b
snd) Map VName (QualName VName, TypeBinding)
p_abs_substs
            abs_name_substs :: Map VName VName
abs_name_substs = ((QualName VName, TypeBinding) -> VName)
-> Map VName (QualName VName, TypeBinding) -> Map VName VName
forall a b k. (a -> b) -> Map k a -> Map k b
M.map (QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf (QualName VName -> VName)
-> ((QualName VName, TypeBinding) -> QualName VName)
-> (QualName VName, TypeBinding)
-> VName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (QualName VName, TypeBinding) -> QualName VName
forall a b. (a, b) -> a
fst) Map VName (QualName VName, TypeBinding)
abs_substs
        Map VName VName
pmod_substs <- Map VName (Subst StructRetType)
-> [VName]
-> Mod
-> Mod
-> Loc
-> Either TypeError (Map VName VName)
matchMods Map VName (Subst StructRetType)
p_abs_subst_to_type [VName]
quals Mod
sig_pmod Mod
mod_pmod Loc
loc
        Map VName VName
mod_substs <- Map VName (Subst StructRetType)
-> [VName]
-> MTy
-> MTy
-> Loc
-> Either TypeError (Map VName VName)
matchMTys' Map VName (Subst StructRetType)
abs_subst_to_type [VName]
quals MTy
mod_mod MTy
sig_mod Loc
loc
        Map VName VName -> Either TypeError (Map VName VName)
forall a. a -> Either TypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map VName VName
pmod_substs Map VName VName -> Map VName VName -> Map VName VName
forall a. Semigroup a => a -> a -> a
<> Map VName VName
mod_substs Map VName VName -> Map VName VName -> Map VName VName
forall a. Semigroup a => a -> a -> a
<> Map VName VName
abs_name_substs)

    matchEnvs ::
      M.Map VName (Subst StructRetType) ->
      [VName] ->
      Env ->
      Env ->
      Loc ->
      Either TypeError (M.Map VName VName)
    matchEnvs :: Map VName (Subst StructRetType)
-> [VName]
-> Env
-> Env
-> Loc
-> Either TypeError (Map VName VName)
matchEnvs Map VName (Subst StructRetType)
abs_subst_to_type [VName]
quals Env
env Env
sig Loc
loc = do
      -- XXX: we only want to create substitutions for visible names.
      -- This must be wrong in some cases.  Probably we need to
      -- rethink how we do shadowing for module types.
      let visible :: Set VName
visible = [VName] -> Set VName
forall a. Ord a => [a] -> Set a
S.fromList ([VName] -> Set VName) -> [VName] -> Set 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
$ NameMap -> [QualName VName]
forall k a. Map k a -> [a]
M.elems (NameMap -> [QualName VName]) -> NameMap -> [QualName VName]
forall a b. (a -> b) -> a -> b
$ Env -> NameMap
envNameMap Env
sig
          isVisible :: VName -> Bool
isVisible VName
name = VName
name VName -> Set VName -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set VName
visible

      -- Check that all type abbreviations are correctly defined.
      Map VName VName
abbr_name_substs <- ([(VName, VName)] -> Map VName VName)
-> Either TypeError [(VName, VName)]
-> Either TypeError (Map VName VName)
forall a b. (a -> b) -> Either TypeError a -> Either TypeError b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(VName, VName)] -> Map VName VName
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (Either TypeError [(VName, VName)]
 -> Either TypeError (Map VName VName))
-> Either TypeError [(VName, VName)]
-> Either TypeError (Map VName VName)
forall a b. (a -> b) -> a -> b
$
        [(VName, TypeBinding)]
-> ((VName, TypeBinding) -> Either TypeError (VName, VName))
-> Either TypeError [(VName, VName)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (((VName, TypeBinding) -> Bool)
-> [(VName, TypeBinding)] -> [(VName, TypeBinding)]
forall a. (a -> Bool) -> [a] -> [a]
filter (VName -> Bool
isVisible (VName -> Bool)
-> ((VName, TypeBinding) -> VName) -> (VName, TypeBinding) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VName, TypeBinding) -> VName
forall a b. (a, b) -> a
fst) ([(VName, TypeBinding)] -> [(VName, TypeBinding)])
-> [(VName, TypeBinding)] -> [(VName, TypeBinding)]
forall a b. (a -> b) -> a -> b
$ Map VName TypeBinding -> [(VName, TypeBinding)]
forall k a. Map k a -> [(k, a)]
M.toList (Map VName TypeBinding -> [(VName, TypeBinding)])
-> Map VName TypeBinding -> [(VName, TypeBinding)]
forall a b. (a -> b) -> a -> b
$ Env -> Map VName TypeBinding
envTypeTable Env
sig) (((VName, TypeBinding) -> Either TypeError (VName, VName))
 -> Either TypeError [(VName, VName)])
-> ((VName, TypeBinding) -> Either TypeError (VName, VName))
-> Either TypeError [(VName, VName)]
forall a b. (a -> b) -> a -> b
$
          \(VName
name, TypeAbbr Liftedness
spec_l [TypeParam]
spec_ps StructRetType
spec_t) ->
            case (Env -> Map VName TypeBinding)
-> Namespace -> Name -> Env -> Maybe (VName, TypeBinding)
forall v.
(Env -> Map VName v)
-> Namespace -> Name -> Env -> Maybe (VName, v)
findBinding Env -> Map VName TypeBinding
envTypeTable Namespace
Type (VName -> Name
baseName VName
name) Env
env of
              Just (VName
name', TypeAbbr Liftedness
l [TypeParam]
ps StructRetType
t) ->
                Loc
-> Map VName (Subst StructRetType)
-> [VName]
-> VName
-> Liftedness
-> [TypeParam]
-> StructRetType
-> VName
-> Liftedness
-> [TypeParam]
-> StructRetType
-> Either TypeError (VName, VName)
matchTypeAbbr Loc
loc Map VName (Subst StructRetType)
abs_subst_to_type [VName]
quals VName
name Liftedness
spec_l [TypeParam]
spec_ps StructRetType
spec_t VName
name' Liftedness
l [TypeParam]
ps StructRetType
t
              Maybe (VName, TypeBinding)
Nothing -> Loc -> Name -> Either TypeError (VName, VName)
forall a b. Pretty a => Loc -> a -> Either TypeError b
missingType Loc
loc (Name -> Either TypeError (VName, VName))
-> Name -> Either TypeError (VName, VName)
forall a b. (a -> b) -> a -> b
$ VName -> Name
baseName VName
name

      -- Check that all values are defined correctly, substituting the
      -- abstract types first.
      Map VName VName
val_substs <- ([(VName, VName)] -> Map VName VName)
-> Either TypeError [(VName, VName)]
-> Either TypeError (Map VName VName)
forall a b. (a -> b) -> Either TypeError a -> Either TypeError b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(VName, VName)] -> Map VName VName
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (Either TypeError [(VName, VName)]
 -> Either TypeError (Map VName VName))
-> Either TypeError [(VName, VName)]
-> Either TypeError (Map VName VName)
forall a b. (a -> b) -> a -> b
$
        [(VName, BoundV)]
-> ((VName, BoundV) -> Either TypeError (VName, VName))
-> Either TypeError [(VName, VName)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Map VName BoundV -> [(VName, BoundV)]
forall k a. Map k a -> [(k, a)]
M.toList (Map VName BoundV -> [(VName, BoundV)])
-> Map VName BoundV -> [(VName, BoundV)]
forall a b. (a -> b) -> a -> b
$ Env -> Map VName BoundV
envVtable Env
sig) (((VName, BoundV) -> Either TypeError (VName, VName))
 -> Either TypeError [(VName, VName)])
-> ((VName, BoundV) -> Either TypeError (VName, VName))
-> Either TypeError [(VName, VName)]
forall a b. (a -> b) -> a -> b
$ \(VName
name, BoundV
spec_bv) -> do
          let ([VName]
spec_dims, BoundV
spec_bv') =
                TypeSubs -> BoundV -> ([VName], BoundV)
substituteTypesInBoundV (VName
-> Map VName (Subst StructRetType) -> Maybe (Subst StructRetType)
forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` Map VName (Subst StructRetType)
abs_subst_to_type) BoundV
spec_bv
              (Set VName
spec_witnesses, Set VName
_) = TypeBase Size NoUniqueness -> (Set VName, Set VName)
determineSizeWitnesses (TypeBase Size NoUniqueness -> (Set VName, Set VName))
-> TypeBase Size NoUniqueness -> (Set VName, Set VName)
forall a b. (a -> b) -> a -> b
$ BoundV -> TypeBase Size NoUniqueness
boundValType BoundV
spec_bv'
          -- The hacky check for #2120.
          Bool -> Either TypeError () -> Either TypeError ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ((VName -> Bool) -> [VName] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (VName -> Set VName -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set VName
spec_witnesses) [VName]
spec_dims) (Either TypeError () -> Either TypeError ())
-> Either TypeError () -> Either TypeError ()
forall a b. (a -> b) -> a -> b
$ Loc -> VName -> Either TypeError ()
forall b. Loc -> VName -> Either TypeError b
topLevelSize Loc
loc VName
name
          case (Env -> Map VName BoundV)
-> Namespace -> Name -> Env -> Maybe (VName, BoundV)
forall v.
(Env -> Map VName v)
-> Namespace -> Name -> Env -> Maybe (VName, v)
findBinding Env -> Map VName BoundV
envVtable Namespace
Term (VName -> Name
baseName VName
name) Env
env of
            Just (VName
name', BoundV
bv) -> Loc
-> [VName]
-> VName
-> BoundV
-> VName
-> BoundV
-> Either TypeError (VName, VName)
matchVal Loc
loc [VName]
quals VName
name BoundV
spec_bv' VName
name' BoundV
bv
            Maybe (VName, BoundV)
_ -> Loc -> Name -> Either TypeError (VName, VName)
forall a b. Pretty a => Loc -> a -> Either TypeError b
missingVal Loc
loc (VName -> Name
baseName VName
name)

      -- Check for correct modules.
      Map VName VName
mod_substs <- ([Map VName VName] -> Map VName VName)
-> Either TypeError [Map VName VName]
-> Either TypeError (Map VName VName)
forall a b. (a -> b) -> Either TypeError a -> Either TypeError b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Map VName VName] -> Map VName VName
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
M.unions (Either TypeError [Map VName VName]
 -> Either TypeError (Map VName VName))
-> Either TypeError [Map VName VName]
-> Either TypeError (Map VName VName)
forall a b. (a -> b) -> a -> b
$
        [(VName, Mod)]
-> ((VName, Mod) -> Either TypeError (Map VName VName))
-> Either TypeError [Map VName VName]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Map VName Mod -> [(VName, Mod)]
forall k a. Map k a -> [(k, a)]
M.toList (Map VName Mod -> [(VName, Mod)])
-> Map VName Mod -> [(VName, Mod)]
forall a b. (a -> b) -> a -> b
$ Env -> Map VName Mod
envModTable Env
sig) (((VName, Mod) -> Either TypeError (Map VName VName))
 -> Either TypeError [Map VName VName])
-> ((VName, Mod) -> Either TypeError (Map VName VName))
-> Either TypeError [Map VName VName]
forall a b. (a -> b) -> a -> b
$ \(VName
name, Mod
modspec) ->
          case (Env -> Map VName Mod)
-> Namespace -> Name -> Env -> Maybe (VName, Mod)
forall v.
(Env -> Map VName v)
-> Namespace -> Name -> Env -> Maybe (VName, v)
findBinding Env -> Map VName Mod
envModTable Namespace
Term (VName -> Name
baseName VName
name) Env
env of
            Just (VName
name', Mod
mod) ->
              VName -> VName -> Map VName VName -> Map VName VName
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
name VName
name'
                (Map VName VName -> Map VName VName)
-> Either TypeError (Map VName VName)
-> Either TypeError (Map VName VName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map VName (Subst StructRetType)
-> [VName]
-> Mod
-> Mod
-> Loc
-> Either TypeError (Map VName VName)
matchMods Map VName (Subst StructRetType)
abs_subst_to_type ([VName]
quals [VName] -> [VName] -> [VName]
forall a. [a] -> [a] -> [a]
++ [VName
name]) Mod
mod Mod
modspec Loc
loc
            Maybe (VName, Mod)
Nothing ->
              Loc -> Name -> Either TypeError (Map VName VName)
forall a b. Pretty a => Loc -> a -> Either TypeError b
missingMod Loc
loc (Name -> Either TypeError (Map VName VName))
-> Name -> Either TypeError (Map VName VName)
forall a b. (a -> b) -> a -> b
$ VName -> Name
baseName VName
name

      Map VName VName -> Either TypeError (Map VName VName)
forall a. a -> Either TypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map VName VName -> Either TypeError (Map VName VName))
-> Map VName VName -> Either TypeError (Map VName VName)
forall a b. (a -> b) -> a -> b
$ Map VName VName
val_substs Map VName VName -> Map VName VName -> Map VName VName
forall a. Semigroup a => a -> a -> a
<> Map VName VName
mod_substs Map VName VName -> Map VName VName -> Map VName VName
forall a. Semigroup a => a -> a -> a
<> Map VName VName
abbr_name_substs

    matchTypeAbbr ::
      Loc ->
      M.Map VName (Subst StructRetType) ->
      [VName] ->
      VName ->
      Liftedness ->
      [TypeParam] ->
      StructRetType ->
      VName ->
      Liftedness ->
      [TypeParam] ->
      StructRetType ->
      Either TypeError (VName, VName)
    matchTypeAbbr :: Loc
-> Map VName (Subst StructRetType)
-> [VName]
-> VName
-> Liftedness
-> [TypeParam]
-> StructRetType
-> VName
-> Liftedness
-> [TypeParam]
-> StructRetType
-> Either TypeError (VName, VName)
matchTypeAbbr Loc
loc Map VName (Subst StructRetType)
abs_subst_to_type [VName]
quals VName
spec_name Liftedness
spec_l [TypeParam]
spec_ps StructRetType
spec_t VName
name Liftedness
l [TypeParam]
ps StructRetType
t = do
      -- Number of type parameters must match.
      Bool -> Either TypeError () -> Either TypeError ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([TypeParam] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeParam]
spec_ps Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [TypeParam] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeParam]
ps) (Either TypeError () -> Either TypeError ())
-> Either TypeError () -> Either TypeError ()
forall a b. (a -> b) -> a -> b
$ StructRetType -> Either TypeError ()
forall {b}. StructRetType -> Either TypeError b
nomatch StructRetType
spec_t

      -- Abstract types have a particular restriction to ensure that
      -- if we have a value of an abstract type 't [n]', then there is
      -- an array of size 'n' somewhere inside.
      Bool -> Either TypeError () -> Either TypeError ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (VName -> Map VName (Subst StructRetType) -> Bool
forall k a. Ord k => k -> Map k a -> Bool
M.member VName
spec_name Map VName (Subst StructRetType)
abs_subst_to_type) (Either TypeError () -> Either TypeError ())
-> Either TypeError () -> Either TypeError ()
forall a b. (a -> b) -> a -> b
$
        case (VName -> Bool) -> [VName] -> [VName]
forall a. (a -> Bool) -> [a] -> [a]
filter
          (VName -> Set VName -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.notMember` (Set VName, Set VName) -> Set VName
forall a b. (a, b) -> a
fst (TypeBase Size NoUniqueness -> (Set VName, Set VName)
determineSizeWitnesses (StructRetType -> TypeBase Size NoUniqueness
forall dim as. RetTypeBase dim as -> TypeBase dim as
retType StructRetType
t)))
          ((TypeParam -> VName) -> [TypeParam] -> [VName]
forall a b. (a -> b) -> [a] -> [b]
map TypeParam -> VName
forall vn. TypeParamBase vn -> vn
typeParamName ([TypeParam] -> [VName]) -> [TypeParam] -> [VName]
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]
ps) of
          [] -> () -> Either TypeError ()
forall a. a -> Either TypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
          VName
d : [VName]
_ ->
            TypeError -> Either TypeError ()
forall a b. a -> Either a b
Left (TypeError -> Either TypeError ())
-> (Doc () -> TypeError) -> Doc () -> Either TypeError ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Loc -> Notes -> Doc () -> TypeError
TypeError Loc
loc Notes
forall a. Monoid a => a
mempty (Doc () -> Either TypeError ()) -> Doc () -> Either TypeError ()
forall a b. (a -> b) -> a -> b
$
              Doc ()
"Type"
                Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Int -> Doc () -> Doc ()
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 ([VName]
-> QualName VName
-> (Liftedness, [TypeParam], StructRetType)
-> Doc ()
forall a.
[VName]
-> QualName VName
-> (Liftedness, [TypeParam], StructRetType)
-> Doc a
ppTypeAbbr [] ([VName] -> VName -> QualName VName
forall vn. [vn] -> vn -> QualName vn
QualName [VName]
quals VName
name) (Liftedness
l, [TypeParam]
ps, StructRetType
t))
                Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Text -> Doc ()
forall a. Text -> Doc a
textwrap Text
"cannot be made abstract because size parameter"
                Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Int -> Doc () -> Doc ()
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (VName -> Doc ()
forall a. VName -> Doc a
forall v a. IsName v => v -> Doc a
prettyName VName
d)
                Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Text -> Doc ()
forall a. Text -> Doc a
textwrap Text
"is not used constructively as an array size in the definition."

      let spec_t' :: StructRetType
spec_t' = TypeSubs -> StructRetType -> StructRetType
forall a. Substitutable a => TypeSubs -> a -> a
applySubst (VName
-> Map VName (Subst StructRetType) -> Maybe (Subst StructRetType)
forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` Map VName (Subst StructRetType)
abs_subst_to_type) StructRetType
spec_t
          nonrigid :: [TypeParam]
nonrigid = [TypeParam]
ps [TypeParam] -> [TypeParam] -> [TypeParam]
forall a. Semigroup a => a -> a -> a
<> (VName -> TypeParam) -> [VName] -> [TypeParam]
forall a b. (a -> b) -> [a] -> [b]
map (VName -> SrcLoc -> TypeParam
forall vn. vn -> SrcLoc -> TypeParamBase vn
`TypeParamDim` SrcLoc
forall a. Monoid a => a
mempty) (StructRetType -> [VName]
forall dim as. RetTypeBase dim as -> [VName]
retDims StructRetType
t)
      case Loc
-> [TypeParam]
-> [TypeParam]
-> TypeBase Size NoUniqueness
-> TypeBase Size NoUniqueness
-> Either TypeError (TypeBase Size NoUniqueness)
doUnification Loc
loc [TypeParam]
spec_ps [TypeParam]
nonrigid (StructRetType -> TypeBase Size NoUniqueness
forall dim as. RetTypeBase dim as -> TypeBase dim as
retType StructRetType
spec_t') (StructRetType -> TypeBase Size NoUniqueness
forall dim as. RetTypeBase dim as -> TypeBase dim as
retType StructRetType
t) of
        Right TypeBase Size NoUniqueness
_ -> (VName, VName) -> Either TypeError (VName, VName)
forall a. a -> Either TypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VName
spec_name, VName
name)
        Either TypeError (TypeBase Size NoUniqueness)
_ -> StructRetType -> Either TypeError (VName, VName)
forall {b}. StructRetType -> Either TypeError b
nomatch StructRetType
spec_t'
      where
        nomatch :: StructRetType -> Either TypeError b
nomatch StructRetType
spec_t' =
          Loc
-> [VName]
-> [VName]
-> VName
-> (Liftedness, [TypeParam], StructRetType)
-> (Liftedness, [TypeParam], StructRetType)
-> Either TypeError b
forall b.
Loc
-> [VName]
-> [VName]
-> VName
-> (Liftedness, [TypeParam], StructRetType)
-> (Liftedness, [TypeParam], StructRetType)
-> Either TypeError b
mismatchedType
            Loc
loc
            (Map VName (Subst StructRetType) -> [VName]
forall k a. Map k a -> [k]
M.keys Map VName (Subst StructRetType)
abs_subst_to_type)
            [VName]
quals
            VName
spec_name
            (Liftedness
spec_l, [TypeParam]
spec_ps, StructRetType
spec_t')
            (Liftedness
l, [TypeParam]
ps, StructRetType
t)

    matchVal ::
      Loc ->
      [VName] ->
      VName ->
      BoundV ->
      VName ->
      BoundV ->
      Either TypeError (VName, VName)
    matchVal :: Loc
-> [VName]
-> VName
-> BoundV
-> VName
-> BoundV
-> Either TypeError (VName, VName)
matchVal Loc
loc [VName]
quals VName
spec_name BoundV
spec_v VName
name BoundV
v =
      case Loc -> BoundV -> BoundV -> Maybe (Doc ())
matchValBinding Loc
loc BoundV
spec_v BoundV
v of
        Maybe (Doc ())
Nothing -> (VName, VName) -> Either TypeError (VName, VName)
forall a. a -> Either TypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VName
spec_name, VName
name)
        Just Doc ()
problem ->
          TypeError -> Either TypeError (VName, VName)
forall a b. a -> Either a b
Left (TypeError -> Either TypeError (VName, VName))
-> TypeError -> Either TypeError (VName, VName)
forall a b. (a -> b) -> a -> b
$
            Loc -> Notes -> Doc () -> TypeError
TypeError Loc
loc Notes
forall a. Monoid a => a
mempty (Doc () -> TypeError) -> Doc () -> TypeError
forall a b. (a -> b) -> a -> b
$
              Doc ()
"Module type specifies"
                Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Int -> Doc () -> Doc ()
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (QualName VName -> BoundV -> Doc ()
forall {a} {ann}. Pretty a => a -> BoundV -> Doc ann
ppValBind ([VName] -> VName -> QualName VName
forall vn. [vn] -> vn -> QualName vn
QualName [VName]
quals VName
spec_name) BoundV
spec_v)
                Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"but module provides"
                Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Int -> Doc () -> Doc ()
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (QualName VName -> BoundV -> Doc ()
forall {a} {ann}. Pretty a => a -> BoundV -> Doc ann
ppValBind ([VName] -> VName -> QualName VName
forall vn. [vn] -> vn -> QualName vn
QualName [VName]
quals VName
spec_name) BoundV
v)
                Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
problem

    matchValBinding :: Loc -> BoundV -> BoundV -> Maybe (Doc ())
    matchValBinding :: Loc -> BoundV -> BoundV -> Maybe (Doc ())
matchValBinding Loc
loc (BoundV [TypeParam]
spec_tps TypeBase Size NoUniqueness
orig_spec_t) (BoundV [TypeParam]
tps TypeBase Size NoUniqueness
orig_t) = do
      case Loc
-> [TypeParam]
-> [TypeParam]
-> TypeBase Size NoUniqueness
-> TypeBase Size NoUniqueness
-> Either TypeError (TypeBase Size NoUniqueness)
doUnification Loc
loc [TypeParam]
spec_tps [TypeParam]
tps (TypeBase Size NoUniqueness -> TypeBase Size NoUniqueness
forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct TypeBase Size NoUniqueness
orig_spec_t) (TypeBase Size NoUniqueness -> TypeBase Size NoUniqueness
forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct TypeBase Size NoUniqueness
orig_t) of
        Left (TypeError Loc
_ Notes
notes Doc ()
msg) ->
          Doc () -> Maybe (Doc ())
forall a. a -> Maybe a
Just (Doc () -> Maybe (Doc ())) -> Doc () -> Maybe (Doc ())
forall a b. (a -> b) -> a -> b
$ Doc ()
msg Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Notes -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. Notes -> Doc ann
pretty Notes
notes
        Right TypeBase Size NoUniqueness
_ ->
          Maybe (Doc ())
forall a. Maybe a
Nothing

    ppValBind :: a -> BoundV -> Doc ann
ppValBind a
v (BoundV [TypeParam]
tps TypeBase Size NoUniqueness
t) =
      Doc ann
"val"
        Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> a -> Doc ann
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
v
        Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep ((TypeParam -> Doc ann) -> [TypeParam] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map TypeParam -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. TypeParam -> Doc ann
pretty [TypeParam]
tps)
        Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
forall ann. Doc ann
colon
        Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
</> Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
align (TypeBase Size NoUniqueness -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. TypeBase Size NoUniqueness -> Doc ann
pretty TypeBase Size NoUniqueness
t))

-- | Apply a parametric module to an argument.
applyFunctor ::
  Loc ->
  FunModType ->
  MTy ->
  TypeM
    ( MTy,
      M.Map VName VName,
      M.Map VName VName
    )
applyFunctor :: Loc
-> FunModType
-> MTy
-> TypeM (MTy, Map VName VName, Map VName VName)
applyFunctor Loc
applyloc (FunModType TySet
p_abs Mod
p_mod MTy
body_mty) MTy
a_mty = do
  Map VName VName
p_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 -> Loc -> Either TypeError (Map VName VName)
matchMTys MTy
a_mty (TySet -> Mod -> MTy
MTy TySet
p_abs Mod
p_mod) Loc
applyloc

  -- Apply type abbreviations from a_mty to body_mty.
  let a_abbrs :: Map VName TypeBinding
a_abbrs = MTy -> Map VName TypeBinding
mtyTypeAbbrs MTy
a_mty
      isSub :: TypeSubs
isSub VName
v = case VName -> Map VName TypeBinding -> Maybe TypeBinding
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
v Map VName TypeBinding
a_abbrs of
        Just TypeBinding
abbr -> Subst StructRetType -> Maybe (Subst StructRetType)
forall a. a -> Maybe a
Just (Subst StructRetType -> Maybe (Subst StructRetType))
-> Subst StructRetType -> Maybe (Subst StructRetType)
forall a b. (a -> b) -> a -> b
$ TypeBinding -> Subst StructRetType
substFromAbbr TypeBinding
abbr
        Maybe TypeBinding
_ -> Subst StructRetType -> Maybe (Subst StructRetType)
forall a. a -> Maybe a
Just (Subst StructRetType -> Maybe (Subst StructRetType))
-> Subst StructRetType -> Maybe (Subst StructRetType)
forall a b. (a -> b) -> a -> b
$ Size -> Subst StructRetType
forall t. Size -> Subst t
ExpSubst (Size -> Subst StructRetType) -> Size -> Subst StructRetType
forall a b. (a -> b) -> a -> b
$ QualName VName -> SrcLoc -> Size
sizeFromName (VName -> QualName VName
forall v. v -> QualName v
qualName VName
v) SrcLoc
forall a. Monoid a => a
mempty
      type_subst :: Map VName (Subst StructRetType)
type_subst = TypeSubs -> Map VName VName -> Map VName (Subst StructRetType)
forall a b k. (a -> Maybe b) -> Map k a -> Map k b
M.mapMaybe TypeSubs
isSub Map VName VName
p_subst
      body_mty' :: MTy
body_mty' = TypeSubs -> MTy -> MTy
substituteTypesInMTy (VName
-> Map VName (Subst StructRetType) -> Maybe (Subst StructRetType)
forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` Map VName (Subst StructRetType)
type_subst) MTy
body_mty
  (MTy
body_mty'', Map VName VName
body_subst) <- MTy -> TypeM (MTy, Map VName VName)
newNamesForMTy MTy
body_mty'
  (MTy, Map VName VName, Map VName VName)
-> TypeM (MTy, Map VName VName, Map VName VName)
forall a. a -> TypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (MTy
body_mty'', Map VName VName
p_subst, Map VName VName
body_subst)