{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TupleSections #-}

-- | 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 qualified Data.Map.Strict as M
import Data.Maybe
import Data.Ord
import qualified Data.Set 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 (FunSig TySet
abs Mod
mod MTy
mty)) =
  FunSig -> Mod
ModFun (FunSig -> Mod) -> FunSig -> Mod
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 (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 :: Map VName BoundV
envVtable = (BoundV -> BoundV) -> Map VName BoundV -> Map VName BoundV
forall a b k. (a -> b) -> Map k a -> Map k b
M.map (TypeSubs -> BoundV -> BoundV
substituteTypesInBoundV TypeSubs
substs) (Map VName BoundV -> Map VName BoundV)
-> Map VName BoundV -> Map VName BoundV
forall a b. (a -> b) -> a -> b
$ Env -> Map VName BoundV
envVtable Env
env,
      envTypeTable :: Map VName TypeBinding
envTypeTable = (VName -> TypeBinding -> TypeBinding)
-> Map VName TypeBinding -> Map VName TypeBinding
forall k a b. (k -> a -> b) -> Map k a -> Map k b
M.mapWithKey VName -> TypeBinding -> TypeBinding
subT (Map VName TypeBinding -> Map VName TypeBinding)
-> Map VName TypeBinding -> Map VName TypeBinding
forall a b. (a -> b) -> a -> b
$ Env -> Map VName TypeBinding
envTypeTable Env
env,
      envModTable :: Map VName Mod
envModTable = (Mod -> Mod) -> Map VName Mod -> Map VName Mod
forall a b k. (a -> b) -> Map k a -> Map k b
M.map (TypeSubs -> Mod -> Mod
substituteTypesInMod TypeSubs
substs) (Map VName Mod -> Map VName Mod) -> Map VName Mod -> Map VName Mod
forall a b. (a -> b) -> a -> b
$ Env -> Map VName Mod
envModTable Env
env
    }
  where
    subT :: VName -> TypeBinding -> TypeBinding
subT VName
name TypeBinding
_
      | Just (TypeSub (TypeAbbr Liftedness
l [TypeParam]
ps StructType
t)) <- VName -> TypeSubs -> Maybe TypeSub
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
name TypeSubs
substs = Liftedness -> [TypeParam] -> StructType -> TypeBinding
TypeAbbr Liftedness
l [TypeParam]
ps StructType
t
    subT VName
_ (TypeAbbr Liftedness
l [TypeParam]
ps StructType
t) = Liftedness -> [TypeParam] -> StructType -> TypeBinding
TypeAbbr Liftedness
l [TypeParam]
ps (StructType -> TypeBinding) -> StructType -> TypeBinding
forall a b. (a -> b) -> a -> b
$ TypeSubs -> StructType -> StructType
forall als.
Monoid als =>
TypeSubs
-> TypeBase (DimDecl VName) als -> TypeBase (DimDecl VName) als
substituteTypes TypeSubs
substs StructType
t

substituteTypesInBoundV :: TypeSubs -> BoundV -> BoundV
substituteTypesInBoundV :: TypeSubs -> BoundV -> BoundV
substituteTypesInBoundV TypeSubs
substs (BoundV [TypeParam]
tps StructType
t) =
  [TypeParam] -> StructType -> BoundV
BoundV [TypeParam]
tps (TypeSubs -> StructType -> StructType
forall als.
Monoid als =>
TypeSubs
-> TypeBase (DimDecl VName) als -> TypeBase (DimDecl VName) als
substituteTypes TypeSubs
substs StructType
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 StructType
_) = [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 (m :: * -> *) a. Monad m => a -> m a
return (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 (m :: * -> *) a. Monad m => a -> m a
return (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 (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 :: Map VName BoundV
-> Map VName TypeBinding
-> Map VName MTy
-> Map VName Mod
-> NameMap
-> Env
Env
                { envVtable :: Map VName BoundV
envVtable = Map VName BoundV
vtable',
                  envTypeTable :: Map VName TypeBinding
envTypeTable = Map VName TypeBinding
ttable',
                  envSigTable :: Map VName MTy
envSigTable = 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 (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

        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 StructType
t) =
          [TypeParam] -> StructType -> BoundV
BoundV ((TypeParam -> TypeParam) -> [TypeParam] -> [TypeParam]
forall a b. (a -> b) -> [a] -> [b]
map TypeParam -> TypeParam
substituteInTypeParam [TypeParam]
ps) (StructType -> StructType
substituteInType StructType
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 FunSig
funsig) =
          FunSig -> Mod
ModFun (FunSig -> Mod) -> FunSig -> Mod
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
            ((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 (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 StructType
t) =
          Liftedness -> [TypeParam] -> StructType -> TypeBinding
TypeAbbr Liftedness
l ((TypeParam -> TypeParam) -> [TypeParam] -> [TypeParam]
forall a b. (a -> b) -> [a] -> [b]
map TypeParam -> TypeParam
substituteInTypeParam [TypeParam]
ps) (StructType -> TypeBinding) -> StructType -> TypeBinding
forall a b. (a -> b) -> a -> b
$ StructType -> StructType
substituteInType StructType
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

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

        substituteInShape :: ShapeDecl (DimDecl VName) -> ShapeDecl (DimDecl VName)
substituteInShape (ShapeDecl [DimDecl VName]
ds) =
          [DimDecl VName] -> ShapeDecl (DimDecl VName)
forall dim. [dim] -> ShapeDecl dim
ShapeDecl ([DimDecl VName] -> ShapeDecl (DimDecl VName))
-> [DimDecl VName] -> ShapeDecl (DimDecl VName)
forall a b. (a -> b) -> a -> b
$ (DimDecl VName -> DimDecl VName)
-> [DimDecl VName] -> [DimDecl VName]
forall a b. (a -> b) -> [a] -> [b]
map DimDecl VName -> DimDecl VName
substituteInDim [DimDecl VName]
ds
        substituteInDim :: DimDecl VName -> DimDecl VName
substituteInDim (NamedDim (QualName [VName]
qs VName
v)) =
          QualName VName -> DimDecl VName
forall vn. QualName vn -> DimDecl vn
NamedDim (QualName VName -> DimDecl VName)
-> QualName VName -> DimDecl VName
forall a b. (a -> b) -> a -> b
$ [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
        substituteInDim DimDecl VName
d = DimDecl VName
d

        substituteInTypeArg :: TypeArg (DimDecl VName) -> TypeArg (DimDecl VName)
substituteInTypeArg (TypeArgDim (NamedDim (QualName [VName]
qs VName
v)) SrcLoc
loc) =
          DimDecl VName -> SrcLoc -> TypeArg (DimDecl VName)
forall dim. dim -> SrcLoc -> TypeArg dim
TypeArgDim (QualName VName -> DimDecl VName
forall vn. QualName vn -> DimDecl vn
NamedDim (QualName VName -> DimDecl VName)
-> QualName VName -> DimDecl VName
forall a b. (a -> b) -> a -> b
$ [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) SrcLoc
loc
        substituteInTypeArg (TypeArgDim (ConstDim Int
x) SrcLoc
loc) =
          DimDecl VName -> SrcLoc -> TypeArg (DimDecl VName)
forall dim. dim -> SrcLoc -> TypeArg dim
TypeArgDim (Int -> DimDecl VName
forall vn. Int -> DimDecl vn
ConstDim Int
x) SrcLoc
loc
        substituteInTypeArg (TypeArgDim DimDecl VName
AnyDim SrcLoc
loc) =
          DimDecl VName -> SrcLoc -> TypeArg (DimDecl VName)
forall dim. dim -> SrcLoc -> TypeArg dim
TypeArgDim DimDecl VName
forall vn. DimDecl vn
AnyDim SrcLoc
loc
        substituteInTypeArg (TypeArgType StructType
t SrcLoc
loc) =
          StructType -> SrcLoc -> TypeArg (DimDecl VName)
forall dim. TypeBase dim () -> SrcLoc -> TypeArg dim
TypeArgType (StructType -> StructType
substituteInType StructType
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 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]
-> StructType
-> TypeM (QualName VName, TySet, Env)
refineEnv SrcLoc
loc TySet
tset Env
env QualName Name
tname [TypeParam]
ps StructType
t
  | Just (QualName VName
tname', TypeAbbr Liftedness
l [TypeParam]
cur_ps (Scalar (TypeVar () Uniqueness
_ (TypeName [VName]
qs VName
v) [TypeArg (DimDecl VName)]
_))) <-
      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 (m :: * -> *) a. Monad m => a -> m a
return
          ( 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, TypeSub)] -> TypeSubs
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
                  [ ( QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
tname',
                      TypeBinding -> TypeSub
TypeSub (TypeBinding -> TypeSub) -> TypeBinding -> TypeSub
forall a b. (a -> b) -> a -> b
$ Liftedness -> [TypeParam] -> StructType -> TypeBinding
TypeAbbr Liftedness
l [TypeParam]
cur_ps StructType
t
                    ),
                    (VName
v, TypeBinding -> TypeSub
TypeSub (TypeBinding -> TypeSub) -> TypeBinding -> TypeSub
forall a b. (a -> b) -> a -> b
$ Liftedness -> [TypeParam] -> StructType -> TypeBinding
TypeAbbr Liftedness
l [TypeParam]
ps StructType
t)
                  ]
              )
              Env
env
          )
      else
        SrcLoc -> Notes -> Doc -> TypeM (QualName VName, TySet, Env)
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
<+> [TypeParam] -> Doc
forall a. Pretty a => [a] -> Doc
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. Pretty a => [a] -> Doc
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 (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
$ QualName Name -> Doc
forall a. Pretty a => a -> Doc
ppr QualName Name
tname Doc -> Doc -> Doc
<+> Doc
"is not an abstract type in the module type."
  where
    tpMsg :: [a] -> Doc
tpMsg [] = Doc
"no type parameters"
    tpMsg [a]
xs = Doc
"type parameters" Doc -> Doc -> Doc
<+> [Doc] -> Doc
spread ((a -> Doc) -> [a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map a -> Doc
forall a. Pretty a => a -> Doc
ppr [a]
xs)

paramsMatch :: [TypeParam] -> [TypeParam] -> Bool
paramsMatch :: [TypeParam] -> [TypeParam] -> Bool
paramsMatch [TypeParam]
ps1 [TypeParam]
ps2 = [TypeParam] -> 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 (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 :: (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 (m :: * -> *) a. Monad m => a -> m a
return (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 (m :: * -> *) a. Monad m => a -> m a
return ([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 ->
  SrcLoc ->
  Either TypeError (M.Map VName (QualName VName, TypeBinding))
resolveAbsTypes :: TySet
-> Mod
-> TySet
-> SrcLoc
-> Either TypeError (Map VName (QualName VName, TypeBinding))
resolveAbsTypes TySet
mod_abs Mod
mod TySet
sig_abs SrcLoc
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 (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 (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)))
-> Either TypeError [(VName, (QualName VName, TypeBinding))]
-> Either TypeError (Map VName (QualName VName, TypeBinding))
forall a b. (a -> b) -> a -> b
$
    [(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 [(VName, (QualName VName, TypeBinding))])
-> ((QualName VName, Liftedness)
    -> Either TypeError (VName, (QualName VName, TypeBinding)))
-> Either TypeError [(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 (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 StructType
t)
          | Liftedness
mod_l Liftedness -> Liftedness -> Bool
forall a. Ord a => a -> a -> Bool
> Liftedness
name_l ->
            Liftedness
-> [VName]
-> VName
-> (Liftedness, [TypeParam], StructType)
-> Either TypeError (VName, (QualName VName, TypeBinding))
forall b.
Liftedness
-> [VName]
-> VName
-> (Liftedness, [TypeParam], StructType)
-> 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 -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
name)
              (Liftedness
mod_l, [TypeParam]
ps, StructType
t)
          | Liftedness
name_l Liftedness -> Liftedness -> Bool
forall a. Ord a => a -> a -> Bool
< Liftedness
SizeLifted,
            StructType -> Bool
emptyDims StructType
t ->
            [VName]
-> VName
-> (Liftedness, [TypeParam], StructType)
-> Either TypeError (VName, (QualName VName, TypeBinding))
forall b.
[VName]
-> VName
-> (Liftedness, [TypeParam], StructType)
-> 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 -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
name)
              (Liftedness
mod_l, [TypeParam]
ps, StructType
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 (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 (m :: * -> *) a. Monad m => a -> m a
return (QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
name, (QualName VName
abs_name, Liftedness -> [TypeParam] -> StructType -> TypeBinding
TypeAbbr Liftedness
name_l [TypeParam]
ps StructType
t))
          | Bool
otherwise ->
            (VName, (QualName VName, TypeBinding))
-> Either TypeError (VName, (QualName VName, TypeBinding))
forall (m :: * -> *) a. Monad m => a -> m a
return (QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
name, (QualName VName
name', Liftedness -> [TypeParam] -> StructType -> TypeBinding
TypeAbbr Liftedness
name_l [TypeParam]
ps StructType
t))
        Maybe (QualName VName, TypeBinding)
_ ->
          SrcLoc
-> QualName Name
-> Either TypeError (VName, (QualName VName, TypeBinding))
forall a b. Pretty a => SrcLoc -> a -> Either TypeError b
missingType SrcLoc
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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap VName -> Name
baseName QualName VName
name
  where
    mismatchedLiftedness :: Liftedness
-> [VName]
-> VName
-> (Liftedness, [TypeParam], StructType)
-> Either TypeError b
mismatchedLiftedness Liftedness
name_l [VName]
abs VName
name (Liftedness, [TypeParam], StructType)
mod_t =
      TypeError -> Either TypeError b
forall a b. a -> Either a b
Left (TypeError -> Either TypeError b)
-> TypeError -> Either TypeError b
forall a b. (a -> b) -> a -> b
$
        SrcLoc -> Notes -> Doc -> TypeError
TypeError SrcLoc
loc Notes
forall a. Monoid a => a
mempty (Doc -> TypeError) -> Doc -> TypeError
forall a b. (a -> b) -> a -> b
$
          Doc
"Module defines"
            Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 ([VName] -> VName -> (Liftedness, [TypeParam], StructType) -> Doc
ppTypeAbbr [VName]
abs VName
name (Liftedness, [TypeParam], StructType)
mod_t)
            Doc -> Doc -> Doc
</> Doc
"but module type requires" Doc -> Doc -> Doc
<+> String -> Doc
text String
what Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."
      where
        what :: String
what = case Liftedness
name_l of
          Liftedness
Unlifted -> String
"a non-lifted type"
          Liftedness
SizeLifted -> String
"a size-lifted type"
          Liftedness
Lifted -> String
"a lifted type"

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

    emptyDims :: StructType -> Bool
    emptyDims :: StructType -> Bool
emptyDims = Maybe StructType -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe StructType -> Bool)
-> (StructType -> Maybe StructType) -> StructType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set VName -> DimPos -> DimDecl VName -> Maybe (DimDecl VName))
-> StructType -> Maybe StructType
forall (f :: * -> *) fdim tdim als.
Applicative f =>
(Set VName -> DimPos -> fdim -> f tdim)
-> TypeBase fdim als -> f (TypeBase tdim als)
traverseDims Set VName -> DimPos -> DimDecl VName -> Maybe (DimDecl VName)
forall p vn. p -> DimPos -> DimDecl vn -> Maybe (DimDecl vn)
onDim
      where
        onDim :: p -> DimPos -> DimDecl vn -> Maybe (DimDecl vn)
onDim p
_ DimPos
PosImmediate DimDecl vn
AnyDim = Maybe (DimDecl vn)
forall a. Maybe a
Nothing
        onDim p
_ DimPos
_ DimDecl vn
d = DimDecl vn -> Maybe (DimDecl vn)
forall a. a -> Maybe a
Just DimDecl vn
d

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)
        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' (FunSig -> MTy
funSigMty FunSig
mod_fun) (FunSig -> MTy
funSigMty FunSig
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 p.
Namespace -> Env -> Map VName p -> 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 p.
Namespace -> Env -> Map VName p -> 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 p.
Namespace -> Env -> Map VName p -> 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 p.
Namespace -> Env -> Map VName p -> 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 p -> Map VName (QualName VName)
resolve Namespace
namespace Env
mod_env = (VName -> p -> Maybe (QualName VName))
-> Map VName p -> Map VName (QualName VName)
forall k a b. (k -> a -> Maybe b) -> Map k a -> Map k b
M.mapMaybeWithKey VName -> p -> 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 => SrcLoc -> a -> Either TypeError b
missingType :: SrcLoc -> a -> Either TypeError b
missingType SrcLoc
loc a
name =
  TypeError -> Either TypeError b
forall a b. a -> Either a b
Left (TypeError -> Either TypeError b)
-> TypeError -> Either TypeError b
forall a b. (a -> b) -> a -> b
$
    SrcLoc -> Notes -> Doc -> TypeError
TypeError SrcLoc
loc Notes
forall a. Monoid a => a
mempty (Doc -> TypeError) -> Doc -> TypeError
forall a b. (a -> b) -> a -> b
$
      Doc
"Module does not define a type named" Doc -> Doc -> Doc
<+> a -> Doc
forall a. Pretty a => a -> Doc
ppr a
name Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."

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

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

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

ppTypeAbbr :: [VName] -> VName -> (Liftedness, [TypeParam], StructType) -> Doc
ppTypeAbbr :: [VName] -> VName -> (Liftedness, [TypeParam], StructType) -> Doc
ppTypeAbbr [VName]
abs VName
name (Liftedness
l, [TypeParam]
ps, Scalar (TypeVar () Uniqueness
_ TypeName
tn [TypeArg (DimDecl VName)]
args))
  | TypeName -> VName
typeLeaf TypeName
tn VName -> [VName] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [VName]
abs,
    (TypeParam -> TypeArg (DimDecl VName))
-> [TypeParam] -> [TypeArg (DimDecl VName)]
forall a b. (a -> b) -> [a] -> [b]
map TypeParam -> TypeArg (DimDecl VName)
typeParamToArg [TypeParam]
ps [TypeArg (DimDecl VName)] -> [TypeArg (DimDecl VName)] -> Bool
forall a. Eq a => a -> a -> Bool
== [TypeArg (DimDecl VName)]
args =
    Doc
"type" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Liftedness -> Doc
forall a. Pretty a => a -> Doc
ppr Liftedness
l Doc -> Doc -> Doc
<+> VName -> Doc
forall v. IsName v => v -> Doc
pprName VName
name
      Doc -> Doc -> Doc
<+> [Doc] -> Doc
spread ((TypeParam -> Doc) -> [TypeParam] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map TypeParam -> Doc
forall a. Pretty a => a -> Doc
ppr [TypeParam]
ps)
ppTypeAbbr [VName]
_ VName
name (Liftedness
l, [TypeParam]
ps, StructType
t) =
  Doc
"type" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Liftedness -> Doc
forall a. Pretty a => a -> Doc
ppr Liftedness
l Doc -> Doc -> Doc
<+> VName -> Doc
forall v. IsName v => v -> Doc
pprName VName
name
    Doc -> Doc -> Doc
<+> [Doc] -> Doc
spread ((TypeParam -> Doc) -> [TypeParam] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map TypeParam -> Doc
forall a. Pretty a => a -> Doc
ppr [TypeParam]
ps)
    Doc -> Doc -> Doc
<+> Doc
equals
    Doc -> Doc -> Doc
<+/> Int -> Doc -> Doc
nest Int
2 (Doc -> Doc
align (StructType -> Doc
forall a. Pretty a => a -> Doc
ppr StructType
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 ->
  SrcLoc ->
  Either TypeError (M.Map VName VName)
matchMTys :: MTy -> MTy -> SrcLoc -> Either TypeError (Map VName VName)
matchMTys MTy
orig_mty MTy
orig_mty_sig =
  TypeSubs
-> MTy -> MTy -> SrcLoc -> Either TypeError (Map VName VName)
matchMTys'
    ( (QualName VName -> TypeSub)
-> Map VName (QualName VName) -> TypeSubs
forall a b k. (a -> b) -> Map k a -> Map k b
M.map (DimDecl VName -> TypeSub
DimSub (DimDecl VName -> TypeSub)
-> (QualName VName -> DimDecl VName) -> QualName VName -> TypeSub
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QualName VName -> DimDecl VName
forall vn. QualName vn -> DimDecl vn
NamedDim) (Map VName (QualName VName) -> TypeSubs)
-> Map VName (QualName VName) -> TypeSubs
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' ::
      TypeSubs ->
      MTy ->
      MTy ->
      SrcLoc ->
      Either TypeError (M.Map VName VName)

    matchMTys' :: TypeSubs
-> MTy -> MTy -> SrcLoc -> Either TypeError (Map VName VName)
matchMTys' TypeSubs
_ (MTy TySet
_ ModFun {}) (MTy TySet
_ ModEnv {}) SrcLoc
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
$
        SrcLoc -> Notes -> Doc -> TypeError
TypeError
          SrcLoc
loc
          Notes
forall a. Monoid a => a
mempty
          Doc
"Cannot match parametric module with non-parametric module type."
    matchMTys' TypeSubs
_ (MTy TySet
_ ModEnv {}) (MTy TySet
_ ModFun {}) SrcLoc
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
$
        SrcLoc -> Notes -> Doc -> TypeError
TypeError
          SrcLoc
loc
          Notes
forall a. Monoid a => a
mempty
          Doc
"Cannot match non-parametric module with paramatric module type."
    matchMTys' TypeSubs
old_abs_subst_to_type (MTy TySet
mod_abs Mod
mod) (MTy TySet
sig_abs Mod
sig) SrcLoc
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
-> SrcLoc
-> Either TypeError (Map VName (QualName VName, TypeBinding))
resolveAbsTypes TySet
mod_abs Mod
mod TySet
sig_abs SrcLoc
loc

      let abs_subst_to_type :: TypeSubs
abs_subst_to_type =
            TypeSubs
old_abs_subst_to_type
              TypeSubs -> TypeSubs -> TypeSubs
forall a. Semigroup a => a -> a -> a
<> ((QualName VName, TypeBinding) -> TypeSub)
-> Map VName (QualName VName, TypeBinding) -> TypeSubs
forall a b k. (a -> b) -> Map k a -> Map k b
M.map (TypeBinding -> TypeSub
TypeSub (TypeBinding -> TypeSub)
-> ((QualName VName, TypeBinding) -> TypeBinding)
-> (QualName VName, TypeBinding)
-> TypeSub
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 <- TypeSubs
-> Mod -> Mod -> SrcLoc -> Either TypeError (Map VName VName)
matchMods TypeSubs
abs_subst_to_type Mod
mod Mod
sig SrcLoc
loc
      Map VName VName -> Either TypeError (Map VName VName)
forall (m :: * -> *) a. Monad m => a -> m a
return (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 ::
      TypeSubs ->
      Mod ->
      Mod ->
      SrcLoc ->
      Either TypeError (M.Map VName VName)
    matchMods :: TypeSubs
-> Mod -> Mod -> SrcLoc -> Either TypeError (Map VName VName)
matchMods TypeSubs
_ ModEnv {} ModFun {} SrcLoc
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
$
        SrcLoc -> Notes -> Doc -> TypeError
TypeError
          SrcLoc
loc
          Notes
forall a. Monoid a => a
mempty
          Doc
"Cannot match non-parametric module with parametric module type."
    matchMods TypeSubs
_ ModFun {} ModEnv {} SrcLoc
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
$
        SrcLoc -> Notes -> Doc -> TypeError
TypeError
          SrcLoc
loc
          Notes
forall a. Monoid a => a
mempty
          Doc
"Cannot match parametric module with non-parametric module type."
    matchMods TypeSubs
abs_subst_to_type (ModEnv Env
mod) (ModEnv Env
sig) SrcLoc
loc =
      TypeSubs
-> Env -> Env -> SrcLoc -> Either TypeError (Map VName VName)
matchEnvs TypeSubs
abs_subst_to_type Env
mod Env
sig SrcLoc
loc
    matchMods
      TypeSubs
old_abs_subst_to_type
      (ModFun (FunSig TySet
mod_abs Mod
mod_pmod MTy
mod_mod))
      (ModFun (FunSig TySet
sig_abs Mod
sig_pmod MTy
sig_mod))
      SrcLoc
loc = do
        Map VName (QualName VName, TypeBinding)
abs_substs <- TySet
-> Mod
-> TySet
-> SrcLoc
-> Either TypeError (Map VName (QualName VName, TypeBinding))
resolveAbsTypes TySet
mod_abs Mod
mod_pmod TySet
sig_abs SrcLoc
loc
        let abs_subst_to_type :: TypeSubs
abs_subst_to_type =
              TypeSubs
old_abs_subst_to_type
                TypeSubs -> TypeSubs -> TypeSubs
forall a. Semigroup a => a -> a -> a
<> ((QualName VName, TypeBinding) -> TypeSub)
-> Map VName (QualName VName, TypeBinding) -> TypeSubs
forall a b k. (a -> b) -> Map k a -> Map k b
M.map (TypeBinding -> TypeSub
TypeSub (TypeBinding -> TypeSub)
-> ((QualName VName, TypeBinding) -> TypeBinding)
-> (QualName VName, TypeBinding)
-> TypeSub
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
pmod_substs <- TypeSubs
-> Mod -> Mod -> SrcLoc -> Either TypeError (Map VName VName)
matchMods TypeSubs
abs_subst_to_type Mod
mod_pmod Mod
sig_pmod SrcLoc
loc
        Map VName VName
mod_substs <- TypeSubs
-> MTy -> MTy -> SrcLoc -> Either TypeError (Map VName VName)
matchMTys' TypeSubs
abs_subst_to_type MTy
mod_mod MTy
sig_mod SrcLoc
loc
        Map VName VName -> Either TypeError (Map VName VName)
forall (m :: * -> *) a. Monad m => a -> m a
return (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 ::
      TypeSubs ->
      Env ->
      Env ->
      SrcLoc ->
      Either TypeError (M.Map VName VName)
    matchEnvs :: TypeSubs
-> Env -> Env -> SrcLoc -> Either TypeError (Map VName VName)
matchEnvs TypeSubs
abs_subst_to_type Env
env Env
sig SrcLoc
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 (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 StructType
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 StructType
t) ->
                SrcLoc
-> TypeSubs
-> VName
-> Liftedness
-> [TypeParam]
-> StructType
-> VName
-> Liftedness
-> [TypeParam]
-> StructType
-> Either TypeError (VName, VName)
matchTypeAbbr SrcLoc
loc TypeSubs
abs_subst_to_type VName
name Liftedness
spec_l [TypeParam]
spec_ps StructType
spec_t VName
name' Liftedness
l [TypeParam]
ps StructType
t
              Maybe (VName, TypeBinding)
Nothing -> SrcLoc -> Name -> Either TypeError (VName, VName)
forall a b. Pretty a => SrcLoc -> a -> Either TypeError b
missingType SrcLoc
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 (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 spec_bv' :: BoundV
spec_bv' = TypeSubs -> BoundV -> BoundV
substituteTypesInBoundV TypeSubs
abs_subst_to_type BoundV
spec_bv
          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) -> SrcLoc
-> VName
-> BoundV
-> VName
-> BoundV
-> Either TypeError (VName, VName)
matchVal SrcLoc
loc VName
name BoundV
spec_bv' VName
name' BoundV
bv
            Maybe (VName, BoundV)
_ -> SrcLoc -> Name -> Either TypeError (VName, VName)
forall a b. Pretty a => SrcLoc -> a -> Either TypeError b
missingVal SrcLoc
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 (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
<$> TypeSubs
-> Mod -> Mod -> SrcLoc -> Either TypeError (Map VName VName)
matchMods TypeSubs
abs_subst_to_type Mod
mod Mod
modspec SrcLoc
loc
            Maybe (VName, Mod)
Nothing ->
              SrcLoc -> Name -> Either TypeError (Map VName VName)
forall a b. Pretty a => SrcLoc -> a -> Either TypeError b
missingMod SrcLoc
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 (m :: * -> *) a. Monad m => a -> m a
return (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 ::
      SrcLoc ->
      TypeSubs ->
      VName ->
      Liftedness ->
      [TypeParam] ->
      StructType ->
      VName ->
      Liftedness ->
      [TypeParam] ->
      StructType ->
      Either TypeError (VName, VName)
    matchTypeAbbr :: SrcLoc
-> TypeSubs
-> VName
-> Liftedness
-> [TypeParam]
-> StructType
-> VName
-> Liftedness
-> [TypeParam]
-> StructType
-> Either TypeError (VName, VName)
matchTypeAbbr SrcLoc
loc TypeSubs
abs_subst_to_type VName
spec_name Liftedness
spec_l [TypeParam]
spec_ps StructType
spec_t VName
name Liftedness
l [TypeParam]
ps StructType
t = do
      -- We have to create substitutions for the type parameters, too.
      Bool -> Either TypeError () -> Either TypeError ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([TypeParam] -> 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 (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
$ StructType -> Either TypeError ()
forall b. StructType -> Either TypeError b
nomatch StructType
spec_t
      TypeSubs
param_substs <- [TypeSubs] -> TypeSubs
forall a. Monoid a => [a] -> a
mconcat ([TypeSubs] -> TypeSubs)
-> Either TypeError [TypeSubs] -> Either TypeError TypeSubs
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TypeParam -> TypeParam -> Either TypeError TypeSubs)
-> [TypeParam] -> [TypeParam] -> Either TypeError [TypeSubs]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM TypeParam -> TypeParam -> Either TypeError TypeSubs
forall k.
TypeParamBase k -> TypeParam -> Either TypeError (Map k TypeSub)
matchTypeParam [TypeParam]
spec_ps [TypeParam]
ps

      -- 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 -> TypeSubs -> Bool
forall k a. Ord k => k -> Map k a -> Bool
M.member VName
spec_name TypeSubs
abs_subst_to_type) (Either TypeError () -> Either TypeError ())
-> Either TypeError () -> Either TypeError ()
forall a b. (a -> b) -> a -> b
$
        case Set VName -> [VName]
forall a. Set a -> [a]
S.toList (StructType -> Set VName
mustBeExplicitInType StructType
t) [VName] -> [VName] -> [VName]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` (TypeParam -> VName) -> [TypeParam] -> [VName]
forall a b. (a -> b) -> [a] -> [b]
map TypeParam -> VName
forall vn. TypeParamBase vn -> vn
typeParamName [TypeParam]
ps of
          [] -> () -> Either TypeError ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
          VName
d : [VName]
_ ->
            TypeError -> Either TypeError ()
forall a b. a -> Either a b
Left (TypeError -> Either TypeError ())
-> TypeError -> Either TypeError ()
forall a b. (a -> b) -> a -> b
$
              SrcLoc -> Notes -> Doc -> TypeError
TypeError SrcLoc
loc Notes
forall a. Monoid a => a
mempty (Doc -> TypeError) -> Doc -> TypeError
forall a b. (a -> b) -> a -> b
$
                Doc
"Type"
                  Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 ([VName] -> VName -> (Liftedness, [TypeParam], StructType) -> Doc
ppTypeAbbr [] VName
name (Liftedness
l, [TypeParam]
ps, StructType
t))
                  Doc -> Doc -> Doc
</> String -> Doc
textwrap String
"cannot be made abstract because size parameter"
                  Doc -> Doc -> Doc
<+/> Doc -> Doc
pquote (VName -> Doc
forall v. IsName v => v -> Doc
pprName VName
d)
                  Doc -> Doc -> Doc
<+/> String -> Doc
textwrap String
"is not used as an array size in the definition."

      let spec_t' :: StructType
spec_t' = TypeSubs -> StructType -> StructType
forall als.
Monoid als =>
TypeSubs
-> TypeBase (DimDecl VName) als -> TypeBase (DimDecl VName) als
substituteTypes (TypeSubs
param_substs TypeSubs -> TypeSubs -> TypeSubs
forall a. Semigroup a => a -> a -> a
<> TypeSubs
abs_subst_to_type) StructType
spec_t
      if StructType
spec_t' StructType -> StructType -> Bool
forall a. Eq a => a -> a -> Bool
== StructType
t
        then (VName, VName) -> Either TypeError (VName, VName)
forall (m :: * -> *) a. Monad m => a -> m a
return (VName
spec_name, VName
name)
        else StructType -> Either TypeError (VName, VName)
forall b. StructType -> Either TypeError b
nomatch StructType
spec_t'
      where
        nomatch :: StructType -> Either TypeError b
nomatch StructType
spec_t' =
          SrcLoc
-> [VName]
-> VName
-> (Liftedness, [TypeParam], StructType)
-> (Liftedness, [TypeParam], StructType)
-> Either TypeError b
forall b.
SrcLoc
-> [VName]
-> VName
-> (Liftedness, [TypeParam], StructType)
-> (Liftedness, [TypeParam], StructType)
-> Either TypeError b
mismatchedType
            SrcLoc
loc
            (TypeSubs -> [VName]
forall k a. Map k a -> [k]
M.keys TypeSubs
abs_subst_to_type)
            VName
spec_name
            (Liftedness
spec_l, [TypeParam]
spec_ps, StructType
spec_t')
            (Liftedness
l, [TypeParam]
ps, StructType
t)

        matchTypeParam :: TypeParamBase k -> TypeParam -> Either TypeError (Map k TypeSub)
matchTypeParam (TypeParamDim k
x SrcLoc
_) (TypeParamDim VName
y SrcLoc
_) =
          Map k TypeSub -> Either TypeError (Map k TypeSub)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map k TypeSub -> Either TypeError (Map k TypeSub))
-> Map k TypeSub -> Either TypeError (Map k TypeSub)
forall a b. (a -> b) -> a -> b
$ k -> TypeSub -> Map k TypeSub
forall k a. k -> a -> Map k a
M.singleton k
x (TypeSub -> Map k TypeSub) -> TypeSub -> Map k TypeSub
forall a b. (a -> b) -> a -> b
$ DimDecl VName -> TypeSub
DimSub (DimDecl VName -> TypeSub) -> DimDecl VName -> TypeSub
forall a b. (a -> b) -> a -> b
$ QualName VName -> DimDecl VName
forall vn. QualName vn -> DimDecl vn
NamedDim (QualName VName -> DimDecl VName)
-> QualName VName -> DimDecl VName
forall a b. (a -> b) -> a -> b
$ VName -> QualName VName
forall v. v -> QualName v
qualName VName
y
        matchTypeParam (TypeParamType Liftedness
Unlifted k
x SrcLoc
_) (TypeParamType Liftedness
Unlifted VName
y SrcLoc
_) =
          Map k TypeSub -> Either TypeError (Map k TypeSub)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map k TypeSub -> Either TypeError (Map k TypeSub))
-> Map k TypeSub -> Either TypeError (Map k TypeSub)
forall a b. (a -> b) -> a -> b
$
            k -> TypeSub -> Map k TypeSub
forall k a. k -> a -> Map k a
M.singleton k
x (TypeSub -> Map k TypeSub) -> TypeSub -> Map k TypeSub
forall a b. (a -> b) -> a -> b
$
              TypeBinding -> TypeSub
TypeSub (TypeBinding -> TypeSub) -> TypeBinding -> TypeSub
forall a b. (a -> b) -> a -> b
$
                Liftedness -> [TypeParam] -> StructType -> TypeBinding
TypeAbbr Liftedness
Unlifted [] (StructType -> TypeBinding) -> StructType -> TypeBinding
forall a b. (a -> b) -> a -> b
$
                  ScalarTypeBase (DimDecl VName) () -> StructType
forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar (ScalarTypeBase (DimDecl VName) () -> StructType)
-> ScalarTypeBase (DimDecl VName) () -> StructType
forall a b. (a -> b) -> a -> b
$ ()
-> Uniqueness
-> TypeName
-> [TypeArg (DimDecl VName)]
-> ScalarTypeBase (DimDecl VName) ()
forall dim as.
as
-> Uniqueness -> TypeName -> [TypeArg dim] -> ScalarTypeBase dim as
TypeVar () Uniqueness
Nonunique (VName -> TypeName
typeName VName
y) []
        matchTypeParam (TypeParamType Liftedness
_ k
x SrcLoc
_) (TypeParamType Liftedness
Lifted VName
y SrcLoc
_) =
          Map k TypeSub -> Either TypeError (Map k TypeSub)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map k TypeSub -> Either TypeError (Map k TypeSub))
-> Map k TypeSub -> Either TypeError (Map k TypeSub)
forall a b. (a -> b) -> a -> b
$
            k -> TypeSub -> Map k TypeSub
forall k a. k -> a -> Map k a
M.singleton k
x (TypeSub -> Map k TypeSub) -> TypeSub -> Map k TypeSub
forall a b. (a -> b) -> a -> b
$
              TypeBinding -> TypeSub
TypeSub (TypeBinding -> TypeSub) -> TypeBinding -> TypeSub
forall a b. (a -> b) -> a -> b
$
                Liftedness -> [TypeParam] -> StructType -> TypeBinding
TypeAbbr Liftedness
Lifted [] (StructType -> TypeBinding) -> StructType -> TypeBinding
forall a b. (a -> b) -> a -> b
$
                  ScalarTypeBase (DimDecl VName) () -> StructType
forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar (ScalarTypeBase (DimDecl VName) () -> StructType)
-> ScalarTypeBase (DimDecl VName) () -> StructType
forall a b. (a -> b) -> a -> b
$ ()
-> Uniqueness
-> TypeName
-> [TypeArg (DimDecl VName)]
-> ScalarTypeBase (DimDecl VName) ()
forall dim as.
as
-> Uniqueness -> TypeName -> [TypeArg dim] -> ScalarTypeBase dim as
TypeVar () Uniqueness
Nonunique (VName -> TypeName
typeName VName
y) []
        matchTypeParam TypeParamBase k
_ TypeParam
_ =
          StructType -> Either TypeError (Map k TypeSub)
forall b. StructType -> Either TypeError b
nomatch StructType
spec_t

    matchVal ::
      SrcLoc ->
      VName ->
      BoundV ->
      VName ->
      BoundV ->
      Either TypeError (VName, VName)
    matchVal :: SrcLoc
-> VName
-> BoundV
-> VName
-> BoundV
-> Either TypeError (VName, VName)
matchVal SrcLoc
loc VName
spec_name BoundV
spec_v VName
name BoundV
v =
      case SrcLoc -> BoundV -> BoundV -> Maybe (Maybe Doc)
matchValBinding SrcLoc
loc BoundV
spec_v BoundV
v of
        Maybe (Maybe Doc)
Nothing -> (VName, VName) -> Either TypeError (VName, VName)
forall (m :: * -> *) a. Monad m => a -> m a
return (VName
spec_name, VName
name)
        Just Maybe 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
$
            SrcLoc -> Notes -> Doc -> TypeError
TypeError SrcLoc
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
</> Int -> Doc -> Doc
indent Int
2 (VName -> BoundV -> Doc
forall v. IsName v => v -> BoundV -> Doc
ppValBind VName
spec_name BoundV
spec_v)
                Doc -> Doc -> Doc
</> Doc
"but module provides"
                Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (VName -> BoundV -> Doc
forall v. IsName v => v -> BoundV -> Doc
ppValBind VName
spec_name BoundV
v)
                Doc -> Doc -> Doc
</> Doc -> Maybe Doc -> Doc
forall a. a -> Maybe a -> a
fromMaybe Doc
forall a. Monoid a => a
mempty Maybe Doc
problem

    matchValBinding :: SrcLoc -> BoundV -> BoundV -> Maybe (Maybe Doc)
    matchValBinding :: SrcLoc -> BoundV -> BoundV -> Maybe (Maybe Doc)
matchValBinding SrcLoc
loc (BoundV [TypeParam]
_ StructType
orig_spec_t) (BoundV [TypeParam]
tps StructType
orig_t) =
      case SrcLoc
-> [TypeParam]
-> StructType
-> StructType
-> Either TypeError StructType
doUnification SrcLoc
loc [TypeParam]
tps (StructType -> StructType
forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct StructType
orig_spec_t) (StructType -> StructType
forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct StructType
orig_t) of
        Left (TypeError SrcLoc
_ Notes
notes Doc
msg) ->
          Maybe Doc -> Maybe (Maybe Doc)
forall a. a -> Maybe a
Just (Maybe Doc -> Maybe (Maybe Doc)) -> Maybe Doc -> Maybe (Maybe Doc)
forall a b. (a -> b) -> a -> b
$ 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. Pretty a => a -> Doc
ppr Notes
notes
        -- Even if they unify, we still have to verify the uniqueness
        -- properties.
        Right StructType
t
          | StructType -> TypeBase () ()
forall vn as. TypeBase (DimDecl vn) as -> TypeBase () as
noSizes StructType
t
              TypeBase () () -> TypeBase () () -> Bool
forall dim as1 as2.
ArrayDim dim =>
TypeBase dim as1 -> TypeBase dim as2 -> Bool
`subtypeOf` StructType -> TypeBase () ()
forall vn as. TypeBase (DimDecl vn) as -> TypeBase () as
noSizes StructType
orig_spec_t ->
            Maybe (Maybe Doc)
forall a. Maybe a
Nothing
          | Bool
otherwise -> Maybe Doc -> Maybe (Maybe Doc)
forall a. a -> Maybe a
Just Maybe Doc
forall a. Maybe a
Nothing

    ppValBind :: v -> BoundV -> Doc
ppValBind v
v (BoundV [TypeParam]
tps StructType
t) =
      Doc
"val" Doc -> Doc -> Doc
<+> v -> Doc
forall v. IsName v => v -> Doc
pprName v
v Doc -> Doc -> Doc
<+> [Doc] -> Doc
spread ((TypeParam -> Doc) -> [TypeParam] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map TypeParam -> Doc
forall a. Pretty a => a -> Doc
ppr [TypeParam]
tps) Doc -> Doc -> Doc
<+> Doc
colon
        Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (Doc -> Doc
align (StructType -> Doc
forall a. Pretty a => a -> Doc
ppr StructType
t))

-- | Apply a parametric module to an argument.
applyFunctor ::
  SrcLoc ->
  FunSig ->
  MTy ->
  TypeM
    ( MTy,
      M.Map VName VName,
      M.Map VName VName
    )
applyFunctor :: SrcLoc
-> FunSig -> MTy -> TypeM (MTy, Map VName VName, Map VName VName)
applyFunctor SrcLoc
applyloc (FunSig 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 -> SrcLoc -> Either TypeError (Map VName VName)
matchMTys MTy
a_mty (TySet -> Mod -> MTy
MTy TySet
p_abs Mod
p_mod) SrcLoc
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 :: VName -> Maybe TypeSub
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 -> TypeSub -> Maybe TypeSub
forall a. a -> Maybe a
Just (TypeSub -> Maybe TypeSub) -> TypeSub -> Maybe TypeSub
forall a b. (a -> b) -> a -> b
$ TypeBinding -> TypeSub
TypeSub TypeBinding
abbr
        Maybe TypeBinding
_ -> TypeSub -> Maybe TypeSub
forall a. a -> Maybe a
Just (TypeSub -> Maybe TypeSub) -> TypeSub -> Maybe TypeSub
forall a b. (a -> b) -> a -> b
$ DimDecl VName -> TypeSub
DimSub (DimDecl VName -> TypeSub) -> DimDecl VName -> TypeSub
forall a b. (a -> b) -> a -> b
$ QualName VName -> DimDecl VName
forall vn. QualName vn -> DimDecl vn
NamedDim (QualName VName -> DimDecl VName)
-> QualName VName -> DimDecl VName
forall a b. (a -> b) -> a -> b
$ VName -> QualName VName
forall v. v -> QualName v
qualName VName
v
      type_subst :: TypeSubs
type_subst = (VName -> Maybe TypeSub) -> Map VName VName -> TypeSubs
forall a b k. (a -> Maybe b) -> Map k a -> Map k b
M.mapMaybe VName -> Maybe TypeSub
isSub Map VName VName
p_subst
      body_mty' :: MTy
body_mty' = TypeSubs -> MTy -> MTy
substituteTypesInMTy TypeSubs
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 (m :: * -> *) a. Monad m => a -> m a
return (MTy
body_mty'', Map VName VName
p_subst, Map VName VName
body_subst)