-- | 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.Except
import Control.Monad.Writer hiding (Sum)
import Data.Either
import Data.List (intersect)
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 forall a b. (a -> b) -> a -> b
$ TypeSubs -> Env -> Env
substituteTypesInEnv TypeSubs
substs Env
e
substituteTypesInMod TypeSubs
substs (ModFun (FunSig TySet
abs Mod
mod MTy
mty)) =
  FunSig -> Mod
ModFun forall a b. (a -> b) -> a -> b
$ TySet -> Mod -> MTy -> FunSig
FunSig 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 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 :: Map VName BoundV
envVtable = forall a b k. (a -> b) -> Map k a -> Map k b
M.map (TypeSubs -> BoundV -> BoundV
substituteTypesInBoundV TypeSubs
substs) forall a b. (a -> b) -> a -> b
$ Env -> Map VName BoundV
envVtable Env
env,
      envTypeTable :: Map VName TypeBinding
envTypeTable = forall k a b. (k -> a -> b) -> Map k a -> Map k b
M.mapWithKey VName -> TypeBinding -> TypeBinding
subT forall a b. (a -> b) -> a -> b
$ Env -> Map VName TypeBinding
envTypeTable Env
env,
      envModTable :: Map VName Mod
envModTable = forall a b k. (a -> b) -> Map k a -> Map k b
M.map (TypeSubs -> Mod -> Mod
substituteTypesInMod TypeSubs
substs) forall a b. (a -> b) -> a -> b
$ Env -> Map VName Mod
envModTable Env
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 ()
t)) =
      Liftedness -> [TypeParam] -> StructRetType -> TypeBinding
TypeAbbr Liftedness
l [TypeParam]
ps forall a b. (a -> b) -> a -> b
$ forall a. Substitutable a => TypeSubs -> a -> a
applySubst TypeSubs
substs forall a b. (a -> b) -> a -> b
$ forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
dims TypeBase Size ()
t

substituteTypesInBoundV :: TypeSubs -> BoundV -> BoundV
substituteTypesInBoundV :: TypeSubs -> BoundV -> BoundV
substituteTypesInBoundV TypeSubs
substs (BoundV [TypeParam]
tps TypeBase Size ()
t) =
  let RetType [VName]
dims TypeBase Size ()
t' = forall a. Substitutable a => TypeSubs -> a -> a
applySubst TypeSubs
substs forall a b. (a -> b) -> a -> b
$ forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [] TypeBase Size ()
t
   in [TypeParam] -> TypeBase Size () -> BoundV
BoundV ([TypeParam]
tps forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (forall vn. vn -> SrcLoc -> TypeParamBase vn
`TypeParamDim` forall a. Monoid a => a
mempty) [VName]
dims) TypeBase Size ()
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) =
  forall a. Ord a => [a] -> Set a
S.fromList
    ( forall k a. Map k a -> [k]
M.keys Map VName BoundV
vtable
        forall a. [a] -> [a] -> [a]
++ forall k a. Map k a -> [k]
M.keys Map VName TypeBinding
ttable
        forall a. [a] -> [a] -> [a]
++ forall k a. Map k a -> [k]
M.keys Map VName MTy
stable
        forall a. [a] -> [a] -> [a]
++ forall k a. Map k a -> [k]
M.keys Map VName Mod
modtable
    )
    forall a. Semigroup a => a -> a -> a
<> forall a. Monoid a => [a] -> a
mconcat
      ( forall a b. (a -> b) -> [a] -> [b]
map MTy -> Set VName
allNamesInMTy (forall k a. Map k a -> [a]
M.elems Map VName MTy
stable)
          forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map Mod -> Set VName
allNamesInMod (forall k a. Map k a -> [a]
M.elems Map VName Mod
modtable)
          forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map TypeBinding -> Set VName
allNamesInType (forall k a. Map k a -> [a]
M.elems Map VName TypeBinding
ttable)
      )
  where
    allNamesInType :: TypeBinding -> Set VName
allNamesInType (TypeAbbr Liftedness
_ [TypeParam]
ps StructRetType
_) = forall a. Ord a => [a] -> Set a
S.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map 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 {} = forall a. Monoid a => a
mempty

allNamesInMTy :: MTy -> S.Set VName
allNamesInMTy :: MTy -> Set VName
allNamesInMTy (MTy TySet
abs Mod
mod) =
  forall a. Ord a => [a] -> Set a
S.fromList (forall a b. (a -> b) -> [a] -> [b]
map forall vn. QualName vn -> vn
qualLeaf forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [k]
M.keys TySet
abs) 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 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall a. Set a -> [a]
S.toList forall a b. (a -> b) -> a -> b
$ MTy -> Set VName
allNamesInMTy MTy
orig_mty) forall a b. (a -> b) -> a -> b
$ \VName
v -> do
    VName
v' <- forall (m :: * -> *). MonadTypeChecker m => VName -> m VName
newName VName
v
    forall (f :: * -> *) a. Applicative f => a -> f a
pure (VName
v, VName
v')
  let substs :: Map VName VName
substs = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(VName, VName)]
pairs
      rev_substs :: Map VName VName
rev_substs = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> b -> a -> c
flip (,)) [(VName, VName)]
pairs

  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 (forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
M.mapKeys (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' = forall {a} {a}. (a -> a) -> Map VName a -> Map VName a
substituteInMap BoundV -> BoundV
substituteInBinding Map VName BoundV
vtable
              ttable' :: Map VName TypeBinding
ttable' = forall {a} {a}. (a -> a) -> Map VName a -> Map VName a
substituteInMap TypeBinding -> TypeBinding
substituteInTypeBinding Map VName TypeBinding
ttable
              mtable' :: Map VName Mod
mtable' = 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',
                  envSigTable :: Map VName MTy
envSigTable = forall a. Monoid a => a
mempty,
                  envModTable :: Map VName Mod
envModTable = Map VName Mod
mtable',
                  envNameMap :: NameMap
envNameMap = forall a b k. (a -> b) -> Map k a -> Map k b
M.map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap VName -> VName
substitute) NameMap
names
                }

        substitute :: VName -> VName
substitute VName
v =
          forall a. a -> Maybe a -> a
fromMaybe VName
v forall a b. (a -> b) -> a -> b
$ 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) = forall a b. [(a, b)] -> ([a], [b])
unzip forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
M.toList Map VName a
m
           in forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall a b. (a -> b) -> a -> b
$
                forall a b. [a] -> [b] -> [(a, b)]
zip
                  (forall a b. (a -> b) -> [a] -> [b]
map (\VName
k -> forall a. a -> Maybe a -> a
fromMaybe VName
k forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
k Map VName VName
substs) [VName]
ks)
                  (forall a b. (a -> b) -> [a] -> [b]
map a -> a
f [a]
vs)

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

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

        substituteInFunSig :: FunSig -> FunSig
substituteInFunSig (FunSig TySet
abs Mod
mod MTy
mty) =
          TySet -> Mod -> MTy -> FunSig
FunSig
            (forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
M.mapKeys (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 ()
t)) =
          Liftedness -> [TypeParam] -> StructRetType -> TypeBinding
TypeAbbr Liftedness
l (forall a b. (a -> b) -> [a] -> [b]
map TypeParam -> TypeParam
substituteInTypeParam [TypeParam]
ps) forall a b. (a -> b) -> a -> b
$ forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
dims forall a b. (a -> b) -> a -> b
$ TypeBase Size () -> TypeBase Size ()
substituteInType TypeBase Size ()
t

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

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

        substituteInShape :: Shape Size -> Shape Size
substituteInShape (Shape [Size]
ds) =
          forall dim. [dim] -> Shape dim
Shape forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Size -> Size
substituteInDim [Size]
ds
        substituteInDim :: Size -> Size
substituteInDim (NamedSize (QualName [VName]
qs VName
v)) =
          QualName VName -> Size
NamedSize forall a b. (a -> b) -> a -> b
$ forall vn. [vn] -> vn -> QualName vn
QualName (forall a b. (a -> b) -> [a] -> [b]
map VName -> VName
substitute [VName]
qs) forall a b. (a -> b) -> a -> b
$ VName -> VName
substitute VName
v
        substituteInDim Size
d = Size
d

        substituteInTypeArg :: TypeArg Size -> TypeArg Size
substituteInTypeArg (TypeArgDim (NamedSize (QualName [VName]
qs VName
v)) SrcLoc
loc) =
          forall dim. dim -> SrcLoc -> TypeArg dim
TypeArgDim (QualName VName -> Size
NamedSize forall a b. (a -> b) -> a -> b
$ forall vn. [vn] -> vn -> QualName vn
QualName (forall a b. (a -> b) -> [a] -> [b]
map VName -> VName
substitute [VName]
qs) forall a b. (a -> b) -> a -> b
$ VName -> VName
substitute VName
v) SrcLoc
loc
        substituteInTypeArg (TypeArgDim (ConstSize Int
x) SrcLoc
loc) =
          forall dim. dim -> SrcLoc -> TypeArg dim
TypeArgDim (Int -> Size
ConstSize Int
x) SrcLoc
loc
        substituteInTypeArg (TypeArgDim (AnySize Maybe VName
v) SrcLoc
loc) =
          forall dim. dim -> SrcLoc -> TypeArg dim
TypeArgDim (Maybe VName -> Size
AnySize Maybe VName
v) SrcLoc
loc
        substituteInTypeArg (TypeArgType TypeBase Size ()
t SrcLoc
loc) =
          forall dim. TypeBase dim () -> SrcLoc -> TypeArg dim
TypeArgType (TypeBase Size () -> TypeBase Size ()
substituteInType TypeBase Size ()
t) SrcLoc
loc

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 (FunSig TySet
_ Mod
mod MTy
mty)) =
  Mod -> Map VName TypeBinding
modTypeAbbrs Mod
mod 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
    forall a. Semigroup a => a -> a -> a
<> (forall a. Monoid a => [a] -> a
mconcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map Mod -> Map VName TypeBinding
modTypeAbbrs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [a]
M.elems 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 ()
-> TypeM (QualName VName, TySet, Env)
refineEnv SrcLoc
loc TySet
tset Env
env QualName Name
tname [TypeParam]
ps TypeBase Size ()
t
  | Just (QualName VName
tname', TypeAbbr Liftedness
_ [TypeParam]
cur_ps (RetType [VName]
_ (Scalar (TypeVar () Uniqueness
_ (QualName [VName]
qs VName
v) [TypeArg Size]
_)))) <-
      QualName Name -> Mod -> Maybe (QualName VName, TypeBinding)
findTypeDef QualName Name
tname (Env -> Mod
ModEnv Env
env),
    forall vn. [vn] -> vn -> QualName vn
QualName (forall vn. QualName vn -> [vn]
qualQuals QualName VName
tname') VName
v 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
          forall (f :: * -> *) a. Applicative f => a -> f a
pure
            ( QualName VName
tname',
              forall vn. [vn] -> vn -> QualName vn
QualName [VName]
qs VName
v forall k a. Ord k => k -> Map k a -> Map k a
`M.delete` TySet
tset,
              TypeSubs -> Env -> Env
substituteTypesInEnv
                ( forall a b c. (a -> b -> c) -> b -> a -> c
flip forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup forall a b. (a -> b) -> a -> b
$
                    forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
                      [ (forall vn. QualName vn -> vn
qualLeaf QualName VName
tname', forall t. [TypeParam] -> t -> Subst t
Subst [TypeParam]
cur_ps forall a b. (a -> b) -> a -> b
$ forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [] TypeBase Size ()
t),
                        (VName
v, forall t. [TypeParam] -> t -> Subst t
Subst [TypeParam]
ps forall a b. (a -> b) -> a -> b
$ forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [] TypeBase Size ()
t)
                      ]
                )
                Env
env
            )
        else
          forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
            Doc ()
"Cannot refine a type having"
              forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall {a} {ann}. Pretty a => [a] -> Doc ann
tpMsg [TypeParam]
ps forall a. Semigroup a => a -> a -> a
<> Doc ()
" with a type having " forall a. Semigroup a => a -> a -> a
<> forall {a} {ann}. Pretty a => [a] -> Doc ann
tpMsg [TypeParam]
cur_ps forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
  | Bool
otherwise =
      forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$ forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty QualName Name
tname) 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" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. [Doc ann] -> Doc ann
hsep (forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [a]
xs)

paramsMatch :: [TypeParam] -> [TypeParam] -> Bool
paramsMatch :: [TypeParam] -> [TypeParam] -> Bool
paramsMatch [TypeParam]
ps1 [TypeParam]
ps2 = forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeParam]
ps1 forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeParam]
ps2 Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall {vn} {vn}. (TypeParamBase vn, TypeParamBase vn) -> Bool
match (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 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' <- forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Namespace
namespace, Name
name) forall a b. (a -> b) -> a -> b
$ Env -> NameMap
envNameMap Env
the_env
  (VName
name',) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 {} = forall a. Maybe a
Nothing
findTypeDef (QualName [] Name
name) (ModEnv Env
the_env) = do
  (VName
name', TypeBinding
tb) <- 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
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (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) <- 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 (forall vn. [vn] -> vn -> QualName vn
QualName [Name]
qs Name
name) Mod
q_mod
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall vn. [vn] -> vn -> QualName vn
QualName (VName
q' 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 =
        forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall a b. (a -> b) -> a -> b
$
          forall a b. [a] -> [b] -> [(a, b)]
zip
            (forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap VName -> Name
baseName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
M.toList TySet
mod_abs)
            (forall k a. Map k a -> [(k, a)]
M.toList TySet
mod_abs)
  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall k a. Map k a -> [(k, a)]
M.toList TySet
sig_abs) forall a b. (a -> b) -> a -> b
$ \(QualName VName
name, Liftedness
name_l) ->
    case QualName Name -> Mod -> Maybe (QualName VName, TypeBinding)
findTypeDef (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 forall a. Ord a => a -> a -> Bool
> Liftedness
name_l ->
            forall {b}.
Liftedness
-> [VName]
-> QualName VName
-> (Liftedness, [TypeParam], StructRetType)
-> Either TypeError b
mismatchedLiftedness
              Liftedness
name_l
              (forall a b. (a -> b) -> [a] -> [b]
map forall vn. QualName vn -> vn
qualLeaf forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [k]
M.keys TySet
mod_abs)
              QualName VName
name
              (Liftedness
mod_l, [TypeParam]
ps, StructRetType
t)
        | Liftedness
name_l forall a. Ord a => a -> a -> Bool
< Liftedness
SizeLifted,
          Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Bool
null forall a b. (a -> b) -> a -> b
$ forall dim as. RetTypeBase dim as -> [VName]
retDims StructRetType
t ->
            forall {b}.
[VName]
-> QualName VName
-> (Liftedness, [TypeParam], StructRetType)
-> Either TypeError b
anonymousSizes
              (forall a b. (a -> b) -> [a] -> [b]
map forall vn. QualName vn -> vn
qualLeaf forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [k]
M.keys TySet
mod_abs)
              QualName VName
name
              (Liftedness
mod_l, [TypeParam]
ps, StructRetType
t)
        | Just (QualName VName
abs_name, Liftedness
_) <- forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (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 ->
            forall (f :: * -> *) a. Applicative f => a -> f a
pure (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 ->
            forall (f :: * -> *) a. Applicative f => a -> f a
pure (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)
_ ->
        forall a b. Pretty a => Loc -> a -> Either TypeError b
missingType Loc
loc forall a b. (a -> b) -> a -> 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 =
      forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. Loc -> Notes -> Doc () -> TypeError
TypeError (forall a. Located a => a -> Loc
locOf Loc
loc) forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
        Doc ()
"Module defines"
          forall ann. Doc ann -> Doc ann -> Doc ann
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a.
[VName]
-> QualName VName
-> (Liftedness, [TypeParam], StructRetType)
-> Doc a
ppTypeAbbr [VName]
abs QualName VName
name (Liftedness, [TypeParam], StructRetType)
mod_t)
          forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"but module type requires"
          forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
what 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 =
      forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. Loc -> Notes -> Doc () -> TypeError
TypeError (forall a. Located a => a -> Loc
locOf Loc
loc) forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
        Doc ()
"Module defines"
          forall ann. Doc ann -> Doc ann -> Doc ann
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a.
[VName]
-> QualName VName
-> (Liftedness, [TypeParam], StructRetType)
-> Doc a
ppTypeAbbr [VName]
abs QualName VName
name (Liftedness, [TypeParam], StructRetType)
mod_t)
          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 FunSig
mod_fun) (ModFun FunSig
sig_fun) =
      Mod -> Mod -> Map VName (QualName VName)
resolveModNames (FunSig -> Mod
funSigMod FunSig
mod_fun) (FunSig -> Mod
funSigMod FunSig
sig_fun)
        forall a. Semigroup a => a -> a -> a
<> MTy -> MTy -> Map VName (QualName VName)
resolveMTyNames' (FunSig -> MTy
funSigMty FunSig
mod_fun) (FunSig -> MTy
funSigMty FunSig
sig_fun)
    resolveModNames Mod
_ Mod
_ =
      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 = forall {a}.
Namespace -> Env -> Map VName a -> Map VName (QualName VName)
resolve Namespace
Term Env
mod_env 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 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 <-
                    forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
modname' 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)
_ -> forall a. Monoid a => a
mempty
       in forall a. Monoid a => [a] -> a
mconcat
            [ forall {a}.
Namespace -> Env -> Map VName a -> Map VName (QualName VName)
resolve Namespace
Term Env
mod_env forall a b. (a -> b) -> a -> b
$ Env -> Map VName BoundV
envVtable Env
sig_env,
              forall {a}.
Namespace -> Env -> Map VName a -> Map VName (QualName VName)
resolve Namespace
Type Env
mod_env forall a b. (a -> b) -> a -> b
$ Env -> Map VName BoundV
envVtable Env
sig_env,
              forall {a}.
Namespace -> Env -> Map VName a -> Map VName (QualName VName)
resolve Namespace
Signature Env
mod_env forall a b. (a -> b) -> a -> b
$ Env -> Map VName BoundV
envVtable Env
sig_env,
              Map VName (QualName VName)
mod_substs,
              forall a. Monoid a => [a] -> a
mconcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (VName, Mod) -> Map VName (QualName VName)
onMod forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
M.toList 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 = forall k a b. (k -> a -> Maybe b) -> Map k a -> Map k b
M.mapMaybeWithKey forall {p}. VName -> p -> Maybe (QualName VName)
resolve'
      where
        resolve' :: VName -> p -> Maybe (QualName VName)
resolve' VName
name p
_ =
          forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Namespace
namespace, VName -> Name
baseName VName
name) 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 =
  forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. Loc -> Notes -> Doc () -> TypeError
TypeError Loc
loc forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
    Doc ()
"Module does not define a type named" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty a
name 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 =
  forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. Loc -> Notes -> Doc () -> TypeError
TypeError Loc
loc forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
    Doc ()
"Module does not define a value named" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty a
name forall a. Semigroup a => a -> a -> a
<> Doc ()
"."

missingMod :: Pretty a => Loc -> a -> Either TypeError b
missingMod :: forall a b. Pretty a => Loc -> a -> Either TypeError b
missingMod Loc
loc a
name =
  forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. Loc -> Notes -> Doc () -> TypeError
TypeError Loc
loc forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
    Doc ()
"Module does not define a module named" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty a
name 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 =
  forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. Loc -> Notes -> Doc () -> TypeError
TypeError Loc
loc forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
    Doc ()
"Module defines"
      forall ann. Doc ann -> Doc ann -> Doc ann
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a.
[VName]
-> QualName VName
-> (Liftedness, [TypeParam], StructRetType)
-> Doc a
ppTypeAbbr [VName]
abs (forall vn. [vn] -> vn -> QualName vn
QualName [VName]
quals VName
name) (Liftedness, [TypeParam], StructRetType)
env_t)
      forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"but module type requires"
      forall ann. Doc ann -> Doc ann -> Doc ann
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a.
[VName]
-> QualName VName
-> (Liftedness, [TypeParam], StructRetType)
-> Doc a
ppTypeAbbr [VName]
abs (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 () Uniqueness
_ QualName VName
tn [TypeArg Size]
args)))
  | forall vn. QualName vn -> vn
qualLeaf QualName VName
tn forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [VName]
abs,
    forall a b. (a -> b) -> [a] -> [b]
map TypeParam -> TypeArg Size
typeParamToArg [TypeParam]
ps forall a. Eq a => a -> a -> Bool
== [TypeArg Size]
args =
      Doc a
"type" forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty Liftedness
l
        forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty QualName VName
name
        forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. [Doc ann] -> Doc ann
hsep (forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [TypeParam]
ps)
ppTypeAbbr [VName]
_ QualName VName
name (Liftedness
l, [TypeParam]
ps, StructRetType
t) =
  Doc a
"type" forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty Liftedness
l
    forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. [Doc ann] -> Doc ann
hsep (forall a ann. Pretty a => a -> Doc ann
pretty QualName VName
name forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [TypeParam]
ps)
    forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann
equals
    forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Int -> Doc ann -> Doc ann
nest Int
2 (forall ann. Doc ann -> Doc ann
align (forall a ann. Pretty a => a -> 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'
    (forall a b k. (a -> b) -> Map k a -> Map k b
M.map (forall t. Size -> Subst t
SizeSubst forall b c a. (b -> c) -> (a -> b) -> a -> c
. QualName VName -> Size
NamedSize) 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 =
      forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$
        Loc -> Notes -> Doc () -> TypeError
TypeError
          Loc
loc
          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 =
      forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$
        Loc -> Notes -> Doc () -> TypeError
TypeError
          Loc
loc
          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 forall a. Semigroup a => a -> a -> a
<> forall a b k. (a -> b) -> Map k a -> Map k b
M.map (TypeBinding -> Subst StructRetType
substFromAbbr forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) Map VName (QualName VName, TypeBinding)
abs_substs
          abs_name_substs :: Map VName VName
abs_name_substs = forall a b k. (a -> b) -> Map k a -> Map k b
M.map (forall vn. QualName vn -> vn
qualLeaf forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map VName VName
substs 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 =
      forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$
        Loc -> Notes -> Doc () -> TypeError
TypeError
          Loc
loc
          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 =
      forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$
        Loc -> Notes -> Doc () -> TypeError
TypeError
          Loc
loc
          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 (FunSig TySet
mod_abs Mod
mod_pmod MTy
mod_mod))
      (ModFun (FunSig 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 forall a. Semigroup a => a -> a -> a
<> forall a b k. (a -> b) -> Map k a -> Map k b
M.map (TypeBinding -> Subst StructRetType
substFromAbbr forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall a. Semigroup a => a -> a -> a
<> forall a b k. (a -> b) -> Map k a -> Map k b
M.map (TypeBinding -> Subst StructRetType
substFromAbbr forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) Map VName (QualName VName, TypeBinding)
p_abs_substs
            abs_name_substs :: Map VName VName
abs_name_substs = forall a b k. (a -> b) -> Map k a -> Map k b
M.map (forall vn. QualName vn -> vn
qualLeaf forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map VName VName
pmod_substs forall a. Semigroup a => a -> a -> a
<> Map VName VName
mod_substs 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 = forall a. Ord a => [a] -> Set a
S.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall vn. QualName vn -> vn
qualLeaf forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [a]
M.elems forall a b. (a -> b) -> a -> b
$ Env -> NameMap
envNameMap Env
sig
          isVisible :: VName -> Bool
isVisible VName
name = VName
name 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 <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall a b. (a -> b) -> a -> b
$
        forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall a. (a -> Bool) -> [a] -> [a]
filter (VName -> Bool
isVisible forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
M.toList forall a b. (a -> b) -> a -> b
$ Env -> Map VName TypeBinding
envTypeTable Env
sig) forall a b. (a -> b) -> a -> b
$
          \(VName
name, TypeAbbr Liftedness
spec_l [TypeParam]
spec_ps StructRetType
spec_t) ->
            case 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 -> forall a b. Pretty a => Loc -> a -> Either TypeError b
missingType Loc
loc 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 <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall a b. (a -> b) -> a -> b
$
        forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall k a. Map k a -> [(k, a)]
M.toList forall a b. (a -> b) -> a -> b
$ Env -> Map VName BoundV
envVtable Env
sig) forall a b. (a -> b) -> a -> b
$ \(VName
name, BoundV
spec_bv) -> do
          let spec_bv' :: BoundV
spec_bv' = TypeSubs -> BoundV -> BoundV
substituteTypesInBoundV (forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` Map VName (Subst StructRetType)
abs_subst_to_type) BoundV
spec_bv
          case 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)
_ -> 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 <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
M.unions forall a b. (a -> b) -> a -> b
$
        forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall k a. Map k a -> [(k, a)]
M.toList forall a b. (a -> b) -> a -> b
$ Env -> Map VName Mod
envModTable Env
sig) forall a b. (a -> b) -> a -> b
$ \(VName
name, Mod
modspec) ->
          case 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) ->
              forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
name VName
name'
                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 forall a. [a] -> [a] -> [a]
++ [VName
name]) Mod
mod Mod
modspec Loc
loc
            Maybe (VName, Mod)
Nothing ->
              forall a b. Pretty a => Loc -> a -> Either TypeError b
missingMod Loc
loc forall a b. (a -> b) -> a -> b
$ VName -> Name
baseName VName
name

      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Map VName VName
val_substs forall a. Semigroup a => a -> a -> a
<> Map VName VName
mod_substs 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.
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeParam]
spec_ps forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeParam]
ps) forall a b. (a -> b) -> a -> b
$ 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.
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall k a. Ord k => k -> Map k a -> Bool
M.member VName
spec_name Map VName (Subst StructRetType)
abs_subst_to_type) forall a b. (a -> b) -> a -> b
$
        case forall a. Set a -> [a]
S.toList (TypeBase Size () -> Set VName
mustBeExplicitInType (forall dim as. RetTypeBase dim as -> TypeBase dim as
retType StructRetType
t)) forall a. Eq a => [a] -> [a] -> [a]
`intersect` forall a b. (a -> b) -> [a] -> [b]
map forall vn. TypeParamBase vn -> vn
typeParamName [TypeParam]
ps of
          [] -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
          VName
d : [VName]
_ ->
            forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. Loc -> Notes -> Doc () -> TypeError
TypeError Loc
loc forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
              Doc ()
"Type"
                forall ann. Doc ann -> Doc ann -> Doc ann
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a.
[VName]
-> QualName VName
-> (Liftedness, [TypeParam], StructRetType)
-> Doc a
ppTypeAbbr [] (forall vn. [vn] -> vn -> QualName vn
QualName [VName]
quals VName
name) (Liftedness
l, [TypeParam]
ps, StructRetType
t))
                forall ann. Doc ann -> Doc ann -> Doc ann
</> forall a. Text -> Doc a
textwrap Text
"cannot be made abstract because size parameter"
                forall ann. Doc ann -> Doc ann -> Doc ann
</> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName VName
d)
                forall ann. Doc ann -> Doc ann -> Doc ann
</> forall a. Text -> Doc a
textwrap Text
"is not used as an array size in the definition."

      let spec_t' :: StructRetType
spec_t' = forall a. Substitutable a => TypeSubs -> a -> a
applySubst (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 forall a. Semigroup a => a -> a -> a
<> forall a b. (a -> b) -> [a] -> [b]
map (forall vn. vn -> SrcLoc -> TypeParamBase vn
`TypeParamDim` forall a. Monoid a => a
mempty) (forall dim as. RetTypeBase dim as -> [VName]
retDims StructRetType
t)
      case Loc
-> [TypeParam]
-> [TypeParam]
-> TypeBase Size ()
-> TypeBase Size ()
-> Either TypeError (TypeBase Size ())
doUnification Loc
loc [TypeParam]
spec_ps [TypeParam]
nonrigid (forall dim as. RetTypeBase dim as -> TypeBase dim as
retType StructRetType
spec_t') (forall dim as. RetTypeBase dim as -> TypeBase dim as
retType StructRetType
t) of
        Right TypeBase Size ()
t'
          | forall as. TypeBase Size as -> TypeBase () as
noSizes TypeBase Size ()
t' TypeBase () () -> TypeBase () () -> Bool
`subtypeOf` forall as. TypeBase Size as -> TypeBase () as
noSizes (forall dim as. RetTypeBase dim as -> TypeBase dim as
retType StructRetType
spec_t') -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (VName
spec_name, VName
name)
        Either TypeError (TypeBase Size ())
_ -> forall {b}. StructRetType -> Either TypeError b
nomatch StructRetType
spec_t'
      where
        nomatch :: StructRetType -> Either TypeError b
nomatch StructRetType
spec_t' =
          forall b.
Loc
-> [VName]
-> [VName]
-> VName
-> (Liftedness, [TypeParam], StructRetType)
-> (Liftedness, [TypeParam], StructRetType)
-> Either TypeError b
mismatchedType
            Loc
loc
            (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 (Maybe (Doc ()))
matchValBinding Loc
loc BoundV
spec_v BoundV
v of
        Maybe (Maybe (Doc ()))
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (VName
spec_name, VName
name)
        Just Maybe (Doc ())
problem ->
          forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$
            Loc -> Notes -> Doc () -> TypeError
TypeError Loc
loc forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
              Doc ()
"Module type specifies"
                forall ann. Doc ann -> Doc ann -> Doc ann
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall {a} {ann}. Pretty a => a -> BoundV -> Doc ann
ppValBind (forall vn. [vn] -> vn -> QualName vn
QualName [VName]
quals VName
spec_name) BoundV
spec_v)
                forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"but module provides"
                forall ann. Doc ann -> Doc ann -> Doc ann
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall {a} {ann}. Pretty a => a -> BoundV -> Doc ann
ppValBind (forall vn. [vn] -> vn -> QualName vn
QualName [VName]
quals VName
spec_name) BoundV
v)
                forall ann. Doc ann -> Doc ann -> Doc ann
</> forall a. a -> Maybe a -> a
fromMaybe forall a. Monoid a => a
mempty Maybe (Doc ())
problem

    matchValBinding :: Loc -> BoundV -> BoundV -> Maybe (Maybe (Doc ()))
    matchValBinding :: Loc -> BoundV -> BoundV -> Maybe (Maybe (Doc ()))
matchValBinding Loc
loc (BoundV [TypeParam]
spec_tps TypeBase Size ()
orig_spec_t) (BoundV [TypeParam]
tps TypeBase Size ()
orig_t) = do
      case Loc
-> [TypeParam]
-> [TypeParam]
-> TypeBase Size ()
-> TypeBase Size ()
-> Either TypeError (TypeBase Size ())
doUnification Loc
loc [TypeParam]
spec_tps [TypeParam]
tps (forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct TypeBase Size ()
orig_spec_t) (forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct TypeBase Size ()
orig_t) of
        Left (TypeError Loc
_ Notes
notes Doc ()
msg) ->
          forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Doc ()
msg forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty Notes
notes
        -- Even if they unify, we still have to verify the uniqueness
        -- properties.
        Right TypeBase Size ()
t
          | forall as. TypeBase Size as -> TypeBase () as
noSizes TypeBase Size ()
t TypeBase () () -> TypeBase () () -> Bool
`subtypeOf` forall as. TypeBase Size as -> TypeBase () as
noSizes TypeBase Size ()
orig_spec_t -> forall a. Maybe a
Nothing
          | Bool
otherwise -> forall a. a -> Maybe a
Just forall a. Maybe a
Nothing

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

-- | Apply a parametric module to an argument.
applyFunctor ::
  Loc ->
  FunSig ->
  MTy ->
  TypeM
    ( MTy,
      M.Map VName VName,
      M.Map VName VName
    )
applyFunctor :: Loc
-> FunSig -> MTy -> TypeM (MTy, Map VName VName, Map VName VName)
applyFunctor Loc
applyloc (FunSig TySet
p_abs Mod
p_mod MTy
body_mty) MTy
a_mty = do
  Map VName VName
p_subst <- forall a. Either TypeError a -> TypeM a
badOnLeft forall a b. (a -> b) -> a -> b
$ MTy -> MTy -> Loc -> Either TypeError (Map VName VName)
matchMTys MTy
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 forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
v Map VName TypeBinding
a_abbrs of
        Just TypeBinding
abbr -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ TypeBinding -> Subst StructRetType
substFromAbbr TypeBinding
abbr
        Maybe TypeBinding
_ -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t. Size -> Subst t
SizeSubst forall a b. (a -> b) -> a -> b
$ QualName VName -> Size
NamedSize forall a b. (a -> b) -> a -> b
$ forall v. v -> QualName v
qualName VName
v
      type_subst :: Map VName (Subst StructRetType)
type_subst = 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 (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'
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (MTy
body_mty'', Map VName VName
p_subst, Map VName VName
body_subst)