-- | Type checker building blocks that do not involve unification.
module Language.Futhark.TypeChecker.Types
  ( checkTypeExp,
    renameRetType,
    typeParamToArg,
    Subst (..),
    substFromAbbr,
    TypeSubs,
    Substitutable (..),
    substTypesAny,

    -- * Witnesses
    mustBeExplicitInType,
    mustBeExplicitInBinding,
    determineSizeWitnesses,
  )
where

import Control.Monad
import Control.Monad.Identity
import Control.Monad.State
import Data.Bifunctor
import Data.List qualified as L
import Data.Map.Strict qualified as M
import Data.Set qualified as S
import Futhark.Util (nubOrd)
import Futhark.Util.Pretty
import Language.Futhark
import Language.Futhark.Traversals
import Language.Futhark.TypeChecker.Monad

mustBeExplicitAux :: StructType -> M.Map VName Bool
mustBeExplicitAux :: StructType -> Map VName Bool
mustBeExplicitAux StructType
t =
  State (Map VName Bool) (TypeBase () NoUniqueness)
-> Map VName Bool -> Map VName Bool
forall s a. State s a -> s -> s
execState ((Set VName
 -> DimPos
 -> ExpBase Info VName
 -> StateT (Map VName Bool) Identity ())
-> StructType -> State (Map VName Bool) (TypeBase () NoUniqueness)
forall (f :: * -> *) fdim tdim als.
Applicative f =>
(Set VName -> DimPos -> fdim -> f tdim)
-> TypeBase fdim als -> f (TypeBase tdim als)
traverseDims Set VName
-> DimPos
-> ExpBase Info VName
-> StateT (Map VName Bool) Identity ()
forall {m :: * -> *}.
MonadState (Map VName Bool) m =>
Set VName -> DimPos -> ExpBase Info VName -> m ()
onDim StructType
t) Map VName Bool
forall a. Monoid a => a
mempty
  where
    onDim :: Set VName -> DimPos -> ExpBase Info VName -> m ()
onDim Set VName
bound DimPos
_ (Var QualName VName
d Info StructType
_ SrcLoc
_)
      | QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
d VName -> Set VName -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set VName
bound =
          (Map VName Bool -> Map VName Bool) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Map VName Bool -> Map VName Bool) -> m ())
-> (Map VName Bool -> Map VName Bool) -> m ()
forall a b. (a -> b) -> a -> b
$ \Map VName Bool
s -> (Bool -> Bool -> Bool)
-> VName -> Bool -> Map VName Bool -> Map VName Bool
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
M.insertWith Bool -> Bool -> Bool
(&&) (QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
d) Bool
False Map VName Bool
s
    onDim Set VName
_ DimPos
PosImmediate (Var QualName VName
d Info StructType
_ SrcLoc
_) =
      (Map VName Bool -> Map VName Bool) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Map VName Bool -> Map VName Bool) -> m ())
-> (Map VName Bool -> Map VName Bool) -> m ()
forall a b. (a -> b) -> a -> b
$ \Map VName Bool
s -> (Bool -> Bool -> Bool)
-> VName -> Bool -> Map VName Bool -> Map VName Bool
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
M.insertWith Bool -> Bool -> Bool
(&&) (QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
d) Bool
False Map VName Bool
s
    onDim Set VName
_ DimPos
_ ExpBase Info VName
e =
      (Map VName Bool -> Map VName Bool) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Map VName Bool -> Map VName Bool) -> m ())
-> (Map VName Bool -> Map VName Bool) -> m ()
forall a b. (a -> b) -> a -> b
$ (Map VName Bool -> Set VName -> Map VName Bool)
-> Set VName -> Map VName Bool -> Map VName Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((VName -> Map VName Bool -> Map VName Bool)
-> Map VName Bool -> Set VName -> Map VName Bool
forall a b. (a -> b -> b) -> b -> Set a -> b
S.foldr (\VName
v -> (Bool -> Bool -> Bool)
-> VName -> Bool -> Map VName Bool -> Map VName Bool
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
M.insertWith Bool -> Bool -> Bool
(&&) VName
v Bool
True)) (Set VName -> Map VName Bool -> Map VName Bool)
-> Set VName -> Map VName Bool -> Map VName Bool
forall a b. (a -> b) -> a -> b
$ FV -> Set VName
fvVars (FV -> Set VName) -> FV -> Set VName
forall a b. (a -> b) -> a -> b
$ ExpBase Info VName -> FV
freeInExp ExpBase Info VName
e

-- | Determine which of the sizes in a type are used as sizes outside
-- of functions in the type, and which are not.  The former are said
-- to be "witnessed" by this type, while the latter are not.  In
-- practice, the latter means that the actual sizes must come from
-- somewhere else.
determineSizeWitnesses :: StructType -> (S.Set VName, S.Set VName)
determineSizeWitnesses :: StructType -> (Set VName, Set VName)
determineSizeWitnesses StructType
t =
  (Map VName Bool -> Set VName)
-> (Map VName Bool -> Set VName)
-> (Map VName Bool, Map VName Bool)
-> (Set VName, Set VName)
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap ([VName] -> Set VName
forall a. Ord a => [a] -> Set a
S.fromList ([VName] -> Set VName)
-> (Map VName Bool -> [VName]) -> Map VName Bool -> Set VName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map VName Bool -> [VName]
forall k a. Map k a -> [k]
M.keys) ([VName] -> Set VName
forall a. Ord a => [a] -> Set a
S.fromList ([VName] -> Set VName)
-> (Map VName Bool -> [VName]) -> Map VName Bool -> Set VName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map VName Bool -> [VName]
forall k a. Map k a -> [k]
M.keys) ((Map VName Bool, Map VName Bool) -> (Set VName, Set VName))
-> (Map VName Bool, Map VName Bool) -> (Set VName, Set VName)
forall a b. (a -> b) -> a -> b
$
    (Bool -> Bool)
-> Map VName Bool -> (Map VName Bool, Map VName Bool)
forall a k. (a -> Bool) -> Map k a -> (Map k a, Map k a)
M.partition Bool -> Bool
not (Map VName Bool -> (Map VName Bool, Map VName Bool))
-> Map VName Bool -> (Map VName Bool, Map VName Bool)
forall a b. (a -> b) -> a -> b
$
      StructType -> Map VName Bool
mustBeExplicitAux StructType
t

-- | Figure out which of the sizes in a binding type must be passed
-- explicitly, because their first use is as something else than just
-- an array dimension.
mustBeExplicitInBinding :: StructType -> S.Set VName
mustBeExplicitInBinding :: StructType -> Set VName
mustBeExplicitInBinding StructType
bind_t =
  let ([TypeBase (ExpBase Info VName) Diet]
ts, StructType
ret) = StructType -> ([TypeBase (ExpBase Info VName) Diet], StructType)
forall dim as.
TypeBase dim as -> ([TypeBase dim Diet], TypeBase dim NoUniqueness)
unfoldFunType StructType
bind_t
      alsoRet :: Map VName Bool -> Map VName Bool
alsoRet = (Bool -> Bool -> Bool)
-> Map VName Bool -> Map VName Bool -> Map VName Bool
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith Bool -> Bool -> Bool
(&&) (Map VName Bool -> Map VName Bool -> Map VName Bool)
-> Map VName Bool -> Map VName Bool -> Map VName Bool
forall a b. (a -> b) -> a -> b
$ [(VName, Bool)] -> Map VName Bool
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(VName, Bool)] -> Map VName Bool)
-> [(VName, Bool)] -> Map VName Bool
forall a b. (a -> b) -> a -> b
$ (VName -> (VName, Bool)) -> [VName] -> [(VName, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map (,Bool
True) (Set VName -> [VName]
forall a. Set a -> [a]
S.toList (FV -> Set VName
fvVars (StructType -> FV
forall u. TypeBase (ExpBase Info VName) u -> FV
freeInType StructType
ret)))
   in [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
$ Map VName Bool -> [VName]
forall k a. Map k a -> [k]
M.keys (Map VName Bool -> [VName]) -> Map VName Bool -> [VName]
forall a b. (a -> b) -> a -> b
$ (Bool -> Bool) -> Map VName Bool -> Map VName Bool
forall a k. (a -> Bool) -> Map k a -> Map k a
M.filter Bool -> Bool
forall a. a -> a
id (Map VName Bool -> Map VName Bool)
-> Map VName Bool -> Map VName Bool
forall a b. (a -> b) -> a -> b
$ Map VName Bool -> Map VName Bool
alsoRet (Map VName Bool -> Map VName Bool)
-> Map VName Bool -> Map VName Bool
forall a b. (a -> b) -> a -> b
$ (Map VName Bool -> StructType -> Map VName Bool)
-> Map VName Bool -> [StructType] -> Map VName Bool
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' Map VName Bool -> StructType -> Map VName Bool
onType Map VName Bool
forall a. Monoid a => a
mempty ([StructType] -> Map VName Bool) -> [StructType] -> Map VName Bool
forall a b. (a -> b) -> a -> b
$ (TypeBase (ExpBase Info VName) Diet -> StructType)
-> [TypeBase (ExpBase Info VName) Diet] -> [StructType]
forall a b. (a -> b) -> [a] -> [b]
map TypeBase (ExpBase Info VName) Diet -> StructType
forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct [TypeBase (ExpBase Info VName) Diet]
ts
  where
    onType :: Map VName Bool -> StructType -> Map VName Bool
onType Map VName Bool
uses StructType
t = Map VName Bool
uses Map VName Bool -> Map VName Bool -> Map VName Bool
forall a. Semigroup a => a -> a -> a
<> StructType -> Map VName Bool
mustBeExplicitAux StructType
t -- Left-biased union.

-- | Figure out which of the sizes in a parameter type must be passed
-- explicitly, because their first use is as something else than just
-- an array dimension.
mustBeExplicitInType :: StructType -> S.Set VName
mustBeExplicitInType :: StructType -> Set VName
mustBeExplicitInType = (Set VName, Set VName) -> Set VName
forall a b. (a, b) -> b
snd ((Set VName, Set VName) -> Set VName)
-> (StructType -> (Set VName, Set VName))
-> StructType
-> Set VName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StructType -> (Set VName, Set VName)
determineSizeWitnesses

-- | Ensure that the dimensions of the RetType are unique by
-- generating new names for them.  This is to avoid name capture.
renameRetType :: (MonadTypeChecker m) => ResRetType -> m ResRetType
renameRetType :: forall (m :: * -> *).
MonadTypeChecker m =>
ResRetType -> m ResRetType
renameRetType (RetType [VName]
dims TypeBase (ExpBase Info VName) Uniqueness
st)
  | [VName]
dims [VName] -> [VName] -> Bool
forall a. Eq a => a -> a -> Bool
/= [VName]
forall a. Monoid a => a
mempty = do
      [VName]
dims' <- (VName -> m VName) -> [VName] -> m [VName]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM VName -> m VName
forall (m :: * -> *). MonadTypeChecker m => VName -> m VName
newName [VName]
dims
      let mkSubst :: VName -> Subst t
mkSubst = ExpBase Info VName -> Subst t
forall t. ExpBase Info VName -> Subst t
ExpSubst (ExpBase Info VName -> Subst t)
-> (VName -> ExpBase Info VName) -> VName -> Subst t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (QualName VName -> SrcLoc -> ExpBase Info VName)
-> SrcLoc -> QualName VName -> ExpBase Info VName
forall a b c. (a -> b -> c) -> b -> a -> c
flip QualName VName -> SrcLoc -> ExpBase Info VName
sizeFromName SrcLoc
forall a. Monoid a => a
mempty (QualName VName -> ExpBase Info VName)
-> (VName -> QualName VName) -> VName -> ExpBase Info VName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VName -> QualName VName
forall v. v -> QualName v
qualName
          m :: Map VName (Subst t)
m = [(VName, Subst t)] -> Map VName (Subst t)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(VName, Subst t)] -> Map VName (Subst t))
-> ([Subst t] -> [(VName, Subst t)])
-> [Subst t]
-> Map VName (Subst t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [VName] -> [Subst t] -> [(VName, Subst t)]
forall a b. [a] -> [b] -> [(a, b)]
zip [VName]
dims ([Subst t] -> Map VName (Subst t))
-> [Subst t] -> Map VName (Subst t)
forall a b. (a -> b) -> a -> b
$ (VName -> Subst t) -> [VName] -> [Subst t]
forall a b. (a -> b) -> [a] -> [b]
map VName -> Subst t
forall {t}. VName -> Subst t
mkSubst [VName]
dims'
          st' :: TypeBase (ExpBase Info VName) Uniqueness
st' = TypeSubs
-> TypeBase (ExpBase Info VName) Uniqueness
-> TypeBase (ExpBase Info VName) Uniqueness
forall a. Substitutable a => TypeSubs -> a -> a
applySubst (VName
-> Map VName (Subst StructRetType) -> Maybe (Subst StructRetType)
forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` Map VName (Subst StructRetType)
forall {t}. Map VName (Subst t)
m) TypeBase (ExpBase Info VName) Uniqueness
st
      ResRetType -> m ResRetType
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ResRetType -> m ResRetType) -> ResRetType -> m ResRetType
forall a b. (a -> b) -> a -> b
$ [VName] -> TypeBase (ExpBase Info VName) Uniqueness -> ResRetType
forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
dims' TypeBase (ExpBase Info VName) Uniqueness
st'
  | Bool
otherwise =
      ResRetType -> m ResRetType
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ResRetType -> m ResRetType) -> ResRetType -> m ResRetType
forall a b. (a -> b) -> a -> b
$ [VName] -> TypeBase (ExpBase Info VName) Uniqueness -> ResRetType
forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
dims TypeBase (ExpBase Info VName) Uniqueness
st

evalTypeExp ::
  (MonadTypeChecker m, Pretty df) =>
  (df -> m Exp) ->
  TypeExp df VName ->
  m (TypeExp Exp VName, [VName], ResRetType, Liftedness)
evalTypeExp :: forall (m :: * -> *) df.
(MonadTypeChecker m, Pretty df) =>
(df -> m (ExpBase Info VName))
-> TypeExp df VName
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
evalTypeExp df -> m (ExpBase Info VName)
_ (TEVar QualName VName
name SrcLoc
loc) = do
  ([TypeParam]
ps, StructRetType
t, Liftedness
l) <- QualName VName -> m ([TypeParam], StructRetType, Liftedness)
forall (m :: * -> *).
MonadTypeChecker m =>
QualName VName -> m ([TypeParam], StructRetType, Liftedness)
lookupType QualName VName
name
  ResRetType
t' <- ResRetType -> m ResRetType
forall (m :: * -> *).
MonadTypeChecker m =>
ResRetType -> m ResRetType
renameRetType (ResRetType -> m ResRetType) -> ResRetType -> m ResRetType
forall a b. (a -> b) -> a -> b
$ Uniqueness -> StructRetType -> ResRetType
forall u.
Uniqueness -> RetTypeBase (ExpBase Info VName) u -> ResRetType
toResRet Uniqueness
Nonunique StructRetType
t
  case [TypeParam]
ps of
    [] -> (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
 Liftedness)
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (QualName VName -> SrcLoc -> TypeExp (ExpBase Info VName) VName
forall d vn. QualName vn -> SrcLoc -> TypeExp d vn
TEVar QualName VName
name SrcLoc
loc, [], ResRetType
t', Liftedness
l)
    [TypeParam]
_ ->
      SrcLoc
-> Notes
-> Doc ()
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
forall loc a. Located loc => loc -> Notes -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc Notes
forall a. Monoid a => a
mempty (Doc ()
 -> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
       Liftedness))
-> Doc ()
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
forall a b. (a -> b) -> a -> b
$
        Doc ()
"Type constructor"
          Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes ([Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
hsep (QualName VName -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. QualName VName -> Doc ann
pretty QualName VName
name Doc () -> [Doc ()] -> [Doc ()]
forall a. a -> [a] -> [a]
: (TypeParam -> Doc ()) -> [TypeParam] -> [Doc ()]
forall a b. (a -> b) -> [a] -> [b]
map TypeParam -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. TypeParam -> Doc ann
pretty [TypeParam]
ps))
          Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"used without any arguments."
--
evalTypeExp df -> m (ExpBase Info VName)
df (TEParens TypeExp df VName
te SrcLoc
loc) = do
  (TypeExp (ExpBase Info VName) VName
te', [VName]
svars, ResRetType
ts, Liftedness
ls) <- (df -> m (ExpBase Info VName))
-> TypeExp df VName
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
forall (m :: * -> *) df.
(MonadTypeChecker m, Pretty df) =>
(df -> m (ExpBase Info VName))
-> TypeExp df VName
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
evalTypeExp df -> m (ExpBase Info VName)
df TypeExp df VName
te
  (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
 Liftedness)
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeExp (ExpBase Info VName) VName
-> SrcLoc -> TypeExp (ExpBase Info VName) VName
forall d vn. TypeExp d vn -> SrcLoc -> TypeExp d vn
TEParens TypeExp (ExpBase Info VName) VName
te' SrcLoc
loc, [VName]
svars, ResRetType
ts, Liftedness
ls)
--
evalTypeExp df -> m (ExpBase Info VName)
df (TETuple [TypeExp df VName]
ts SrcLoc
loc) = do
  ([TypeExp (ExpBase Info VName) VName]
ts', [[VName]]
svars, [ResRetType]
ts_s, [Liftedness]
ls) <- [(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
  Liftedness)]
-> ([TypeExp (ExpBase Info VName) VName], [[VName]], [ResRetType],
    [Liftedness])
forall a b c d. [(a, b, c, d)] -> ([a], [b], [c], [d])
L.unzip4 ([(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
   Liftedness)]
 -> ([TypeExp (ExpBase Info VName) VName], [[VName]], [ResRetType],
     [Liftedness]))
-> m [(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
       Liftedness)]
-> m ([TypeExp (ExpBase Info VName) VName], [[VName]],
      [ResRetType], [Liftedness])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TypeExp df VName
 -> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
       Liftedness))
-> [TypeExp df VName]
-> m [(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
       Liftedness)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((df -> m (ExpBase Info VName))
-> TypeExp df VName
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
forall (m :: * -> *) df.
(MonadTypeChecker m, Pretty df) =>
(df -> m (ExpBase Info VName))
-> TypeExp df VName
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
evalTypeExp df -> m (ExpBase Info VName)
df) [TypeExp df VName]
ts
  (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
 Liftedness)
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    ( [TypeExp (ExpBase Info VName) VName]
-> SrcLoc -> TypeExp (ExpBase Info VName) VName
forall d vn. [TypeExp d vn] -> SrcLoc -> TypeExp d vn
TETuple [TypeExp (ExpBase Info VName) VName]
ts' SrcLoc
loc,
      [[VName]] -> [VName]
forall a. Monoid a => [a] -> a
mconcat [[VName]]
svars,
      [VName] -> TypeBase (ExpBase Info VName) Uniqueness -> ResRetType
forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType ((ResRetType -> [VName]) -> [ResRetType] -> [VName]
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ResRetType -> [VName]
forall dim as. RetTypeBase dim as -> [VName]
retDims [ResRetType]
ts_s) (TypeBase (ExpBase Info VName) Uniqueness -> ResRetType)
-> TypeBase (ExpBase Info VName) Uniqueness -> ResRetType
forall a b. (a -> b) -> a -> b
$ ScalarTypeBase (ExpBase Info VName) Uniqueness
-> TypeBase (ExpBase Info VName) Uniqueness
forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar (ScalarTypeBase (ExpBase Info VName) Uniqueness
 -> TypeBase (ExpBase Info VName) Uniqueness)
-> ScalarTypeBase (ExpBase Info VName) Uniqueness
-> TypeBase (ExpBase Info VName) Uniqueness
forall a b. (a -> b) -> a -> b
$ [TypeBase (ExpBase Info VName) Uniqueness]
-> ScalarTypeBase (ExpBase Info VName) Uniqueness
forall dim as. [TypeBase dim as] -> ScalarTypeBase dim as
tupleRecord ([TypeBase (ExpBase Info VName) Uniqueness]
 -> ScalarTypeBase (ExpBase Info VName) Uniqueness)
-> [TypeBase (ExpBase Info VName) Uniqueness]
-> ScalarTypeBase (ExpBase Info VName) Uniqueness
forall a b. (a -> b) -> a -> b
$ (ResRetType -> TypeBase (ExpBase Info VName) Uniqueness)
-> [ResRetType] -> [TypeBase (ExpBase Info VName) Uniqueness]
forall a b. (a -> b) -> [a] -> [b]
map ResRetType -> TypeBase (ExpBase Info VName) Uniqueness
forall dim as. RetTypeBase dim as -> TypeBase dim as
retType [ResRetType]
ts_s,
      (Liftedness -> Liftedness -> Liftedness)
-> Liftedness -> [Liftedness] -> Liftedness
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' Liftedness -> Liftedness -> Liftedness
forall a. Ord a => a -> a -> a
max Liftedness
Unlifted [Liftedness]
ls
    )
--
evalTypeExp df -> m (ExpBase Info VName)
df t :: TypeExp df VName
t@(TERecord [(Name, TypeExp df VName)]
fs SrcLoc
loc) = do
  -- Check for duplicate field names.
  let field_names :: [Name]
field_names = ((Name, TypeExp df VName) -> Name)
-> [(Name, TypeExp df VName)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, TypeExp df VName) -> Name
forall a b. (a, b) -> a
fst [(Name, TypeExp df VName)]
fs
  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Name] -> [Name]
forall a. Ord a => [a] -> [a]
L.sort [Name]
field_names [Name] -> [Name] -> Bool
forall a. Eq a => a -> a -> Bool
== [Name] -> [Name]
forall a. Ord a => [a] -> [a]
L.sort ([Name] -> [Name]
forall a. Ord a => [a] -> [a]
nubOrd [Name]
field_names)) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
    SrcLoc -> Notes -> Doc () -> m ()
forall loc a. Located loc => loc -> Notes -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc Notes
forall a. Monoid a => a
mempty (Doc () -> m ()) -> Doc () -> m ()
forall a b. (a -> b) -> a -> b
$
      Doc ()
"Duplicate record fields in" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> TypeExp df VName -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. TypeExp df VName -> Doc ann
pretty TypeExp df VName
t Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."

  Map
  Name
  (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
   Liftedness)
checked <- (TypeExp df VName
 -> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
       Liftedness))
-> Map Name (TypeExp df VName)
-> m (Map
        Name
        (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
         Liftedness))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Map Name a -> f (Map Name b)
traverse ((df -> m (ExpBase Info VName))
-> TypeExp df VName
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
forall (m :: * -> *) df.
(MonadTypeChecker m, Pretty df) =>
(df -> m (ExpBase Info VName))
-> TypeExp df VName
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
evalTypeExp df -> m (ExpBase Info VName)
df) (Map Name (TypeExp df VName)
 -> m (Map
         Name
         (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
          Liftedness)))
-> Map Name (TypeExp df VName)
-> m (Map
        Name
        (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
         Liftedness))
forall a b. (a -> b) -> a -> b
$ [(Name, TypeExp df VName)] -> Map Name (TypeExp df VName)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Name, TypeExp df VName)]
fs
  let fs' :: Map Name (TypeExp (ExpBase Info VName) VName)
fs' = ((TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
  Liftedness)
 -> TypeExp (ExpBase Info VName) VName)
-> Map
     Name
     (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
-> Map Name (TypeExp (ExpBase Info VName) VName)
forall a b. (a -> b) -> Map Name a -> Map Name b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(TypeExp (ExpBase Info VName) VName
x, [VName]
_, ResRetType
_, Liftedness
_) -> TypeExp (ExpBase Info VName) VName
x) Map
  Name
  (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
   Liftedness)
checked
      fs_svars :: [VName]
fs_svars = ((TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
  Liftedness)
 -> [VName])
-> Map
     Name
     (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
-> [VName]
forall m a. Monoid m => (a -> m) -> Map Name a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (\(TypeExp (ExpBase Info VName) VName
_, [VName]
y, ResRetType
_, Liftedness
_) -> [VName]
y) Map
  Name
  (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
   Liftedness)
checked
      ts_s :: Map Name ResRetType
ts_s = ((TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
  Liftedness)
 -> ResRetType)
-> Map
     Name
     (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
-> Map Name ResRetType
forall a b. (a -> b) -> Map Name a -> Map Name b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(TypeExp (ExpBase Info VName) VName
_, [VName]
_, ResRetType
z, Liftedness
_) -> ResRetType
z) Map
  Name
  (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
   Liftedness)
checked
      ls :: Map Name Liftedness
ls = ((TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
  Liftedness)
 -> Liftedness)
-> Map
     Name
     (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
-> Map Name Liftedness
forall a b. (a -> b) -> Map Name a -> Map Name b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(TypeExp (ExpBase Info VName) VName
_, [VName]
_, ResRetType
_, Liftedness
v) -> Liftedness
v) Map
  Name
  (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
   Liftedness)
checked
  (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
 Liftedness)
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    ( [(Name, TypeExp (ExpBase Info VName) VName)]
-> SrcLoc -> TypeExp (ExpBase Info VName) VName
forall d vn. [(Name, TypeExp d vn)] -> SrcLoc -> TypeExp d vn
TERecord (Map Name (TypeExp (ExpBase Info VName) VName)
-> [(Name, TypeExp (ExpBase Info VName) VName)]
forall k a. Map k a -> [(k, a)]
M.toList Map Name (TypeExp (ExpBase Info VName) VName)
fs') SrcLoc
loc,
      [VName]
fs_svars,
      [VName] -> TypeBase (ExpBase Info VName) Uniqueness -> ResRetType
forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType ((ResRetType -> [VName]) -> Map Name ResRetType -> [VName]
forall m a. Monoid m => (a -> m) -> Map Name a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ResRetType -> [VName]
forall dim as. RetTypeBase dim as -> [VName]
retDims Map Name ResRetType
ts_s) (TypeBase (ExpBase Info VName) Uniqueness -> ResRetType)
-> TypeBase (ExpBase Info VName) Uniqueness -> ResRetType
forall a b. (a -> b) -> a -> b
$ ScalarTypeBase (ExpBase Info VName) Uniqueness
-> TypeBase (ExpBase Info VName) Uniqueness
forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar (ScalarTypeBase (ExpBase Info VName) Uniqueness
 -> TypeBase (ExpBase Info VName) Uniqueness)
-> ScalarTypeBase (ExpBase Info VName) Uniqueness
-> TypeBase (ExpBase Info VName) Uniqueness
forall a b. (a -> b) -> a -> b
$ Map Name (TypeBase (ExpBase Info VName) Uniqueness)
-> ScalarTypeBase (ExpBase Info VName) Uniqueness
forall dim u. Map Name (TypeBase dim u) -> ScalarTypeBase dim u
Record (Map Name (TypeBase (ExpBase Info VName) Uniqueness)
 -> ScalarTypeBase (ExpBase Info VName) Uniqueness)
-> Map Name (TypeBase (ExpBase Info VName) Uniqueness)
-> ScalarTypeBase (ExpBase Info VName) Uniqueness
forall a b. (a -> b) -> a -> b
$ (ResRetType -> TypeBase (ExpBase Info VName) Uniqueness)
-> Map Name ResRetType
-> Map Name (TypeBase (ExpBase Info VName) Uniqueness)
forall a b k. (a -> b) -> Map k a -> Map k b
M.map ResRetType -> TypeBase (ExpBase Info VName) Uniqueness
forall dim as. RetTypeBase dim as -> TypeBase dim as
retType Map Name ResRetType
ts_s,
      (Liftedness -> Liftedness -> Liftedness)
-> Liftedness -> Map Name Liftedness -> Liftedness
forall b a. (b -> a -> b) -> b -> Map Name a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' Liftedness -> Liftedness -> Liftedness
forall a. Ord a => a -> a -> a
max Liftedness
Unlifted Map Name Liftedness
ls
    )
--
evalTypeExp df -> m (ExpBase Info VName)
df (TEArray SizeExp df
d TypeExp df VName
t SrcLoc
loc) = do
  ([VName]
d_svars, SizeExp (ExpBase Info VName)
d', ExpBase Info VName
d'') <- SizeExp df
-> m ([VName], SizeExp (ExpBase Info VName), ExpBase Info VName)
checkSizeExp SizeExp df
d
  (TypeExp (ExpBase Info VName) VName
t', [VName]
svars, RetType [VName]
dims TypeBase (ExpBase Info VName) Uniqueness
st, Liftedness
l) <- (df -> m (ExpBase Info VName))
-> TypeExp df VName
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
forall (m :: * -> *) df.
(MonadTypeChecker m, Pretty df) =>
(df -> m (ExpBase Info VName))
-> TypeExp df VName
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
evalTypeExp df -> m (ExpBase Info VName)
df TypeExp df VName
t
  case (Liftedness
l, Uniqueness
-> Shape (ExpBase Info VName)
-> TypeBase (ExpBase Info VName) Uniqueness
-> TypeBase (ExpBase Info VName) Uniqueness
forall u dim u'.
u -> Shape dim -> TypeBase dim u' -> TypeBase dim u
arrayOfWithAliases Uniqueness
Nonunique ([ExpBase Info VName] -> Shape (ExpBase Info VName)
forall dim. [dim] -> Shape dim
Shape [ExpBase Info VName
d'']) TypeBase (ExpBase Info VName) Uniqueness
st) of
    (Liftedness
Unlifted, TypeBase (ExpBase Info VName) Uniqueness
st') ->
      (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
 Liftedness)
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( SizeExp (ExpBase Info VName)
-> TypeExp (ExpBase Info VName) VName
-> SrcLoc
-> TypeExp (ExpBase Info VName) VName
forall d vn. SizeExp d -> TypeExp d vn -> SrcLoc -> TypeExp d vn
TEArray SizeExp (ExpBase Info VName)
d' TypeExp (ExpBase Info VName) VName
t' SrcLoc
loc,
          [VName]
svars,
          [VName] -> TypeBase (ExpBase Info VName) Uniqueness -> ResRetType
forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType ([VName]
d_svars [VName] -> [VName] -> [VName]
forall a. [a] -> [a] -> [a]
++ [VName]
dims) TypeBase (ExpBase Info VName) Uniqueness
st',
          Liftedness
Unlifted
        )
    (Liftedness
SizeLifted, TypeBase (ExpBase Info VName) Uniqueness
_) ->
      SrcLoc
-> Notes
-> Doc ()
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
forall loc a. Located loc => loc -> Notes -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc Notes
forall a. Monoid a => a
mempty (Doc ()
 -> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
       Liftedness))
-> Doc ()
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
forall a b. (a -> b) -> a -> b
$
        Doc ()
"Cannot create array with elements of size-lifted type"
          Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (TypeExp df VName -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. TypeExp df VName -> Doc ann
pretty TypeExp df VName
t)
          Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"(might cause irregular array)."
    (Liftedness
Lifted, TypeBase (ExpBase Info VName) Uniqueness
_) ->
      SrcLoc
-> Notes
-> Doc ()
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
forall loc a. Located loc => loc -> Notes -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc Notes
forall a. Monoid a => a
mempty (Doc ()
 -> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
       Liftedness))
-> Doc ()
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
forall a b. (a -> b) -> a -> b
$
        Doc ()
"Cannot create array with elements of lifted type"
          Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (TypeExp df VName -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. TypeExp df VName -> Doc ann
pretty TypeExp df VName
t)
          Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"(might contain function)."
  where
    checkSizeExp :: SizeExp df
-> m ([VName], SizeExp (ExpBase Info VName), ExpBase Info VName)
checkSizeExp (SizeExpAny SrcLoc
dloc) = do
      VName
dv <- Name -> m VName
forall (m :: * -> *). MonadTypeChecker m => Name -> m VName
newTypeName Name
"d"
      ([VName], SizeExp (ExpBase Info VName), ExpBase Info VName)
-> m ([VName], SizeExp (ExpBase Info VName), ExpBase Info VName)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([VName
dv], SrcLoc -> SizeExp (ExpBase Info VName)
forall d. SrcLoc -> SizeExp d
SizeExpAny SrcLoc
dloc, QualName VName -> SrcLoc -> ExpBase Info VName
sizeFromName (VName -> QualName VName
forall v. v -> QualName v
qualName VName
dv) SrcLoc
dloc)
    checkSizeExp (SizeExp df
e SrcLoc
dloc) = do
      ExpBase Info VName
e' <- df -> m (ExpBase Info VName)
df df
e
      ([VName], SizeExp (ExpBase Info VName), ExpBase Info VName)
-> m ([VName], SizeExp (ExpBase Info VName), ExpBase Info VName)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([], ExpBase Info VName -> SrcLoc -> SizeExp (ExpBase Info VName)
forall d. d -> SrcLoc -> SizeExp d
SizeExp ExpBase Info VName
e' SrcLoc
dloc, ExpBase Info VName
e')
--
evalTypeExp df -> m (ExpBase Info VName)
df (TEUnique TypeExp df VName
t SrcLoc
loc) = do
  (TypeExp (ExpBase Info VName) VName
t', [VName]
svars, RetType [VName]
dims TypeBase (ExpBase Info VName) Uniqueness
st, Liftedness
l) <- (df -> m (ExpBase Info VName))
-> TypeExp df VName
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
forall (m :: * -> *) df.
(MonadTypeChecker m, Pretty df) =>
(df -> m (ExpBase Info VName))
-> TypeExp df VName
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
evalTypeExp df -> m (ExpBase Info VName)
df TypeExp df VName
t
  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (TypeBase (ExpBase Info VName) Uniqueness -> Bool
forall {dim} {u}. TypeBase dim u -> Bool
mayContainArray TypeBase (ExpBase Info VName) Uniqueness
st) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
    SrcLoc -> Doc () -> m ()
forall loc. Located loc => loc -> Doc () -> m ()
forall (m :: * -> *) loc.
(MonadTypeChecker m, Located loc) =>
loc -> Doc () -> m ()
warn SrcLoc
loc (Doc () -> m ()) -> Doc () -> m ()
forall a b. (a -> b) -> a -> b
$
      Doc ()
"Declaring" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (TypeBase (ExpBase Info VName) Uniqueness -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. TypeBase (ExpBase Info VName) Uniqueness -> Doc ann
pretty TypeBase (ExpBase Info VName) Uniqueness
st) Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"as unique has no effect."
  (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
 Liftedness)
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeExp (ExpBase Info VName) VName
-> SrcLoc -> TypeExp (ExpBase Info VName) VName
forall d vn. TypeExp d vn -> SrcLoc -> TypeExp d vn
TEUnique TypeExp (ExpBase Info VName) VName
t' SrcLoc
loc, [VName]
svars, [VName] -> TypeBase (ExpBase Info VName) Uniqueness -> ResRetType
forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
dims (TypeBase (ExpBase Info VName) Uniqueness -> ResRetType)
-> TypeBase (ExpBase Info VName) Uniqueness -> ResRetType
forall a b. (a -> b) -> a -> b
$ TypeBase (ExpBase Info VName) Uniqueness
st TypeBase (ExpBase Info VName) Uniqueness
-> Uniqueness -> TypeBase (ExpBase Info VName) Uniqueness
forall dim u1 u2. TypeBase dim u1 -> u2 -> TypeBase dim u2
`setUniqueness` Uniqueness
Unique, Liftedness
l)
  where
    mayContainArray :: TypeBase dim u -> Bool
mayContainArray (Scalar Prim {}) = Bool
False
    mayContainArray Array {} = Bool
True
    mayContainArray (Scalar (Record Map Name (TypeBase dim u)
fs)) = (TypeBase dim u -> Bool) -> Map Name (TypeBase dim u) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any TypeBase dim u -> Bool
mayContainArray Map Name (TypeBase dim u)
fs
    mayContainArray (Scalar TypeVar {}) = Bool
True
    mayContainArray (Scalar Arrow {}) = Bool
False
    mayContainArray (Scalar (Sum Map Name [TypeBase dim u]
cs)) = (([TypeBase dim u] -> Bool) -> Map Name [TypeBase dim u] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (([TypeBase dim u] -> Bool) -> Map Name [TypeBase dim u] -> Bool)
-> ((TypeBase dim u -> Bool) -> [TypeBase dim u] -> Bool)
-> (TypeBase dim u -> Bool)
-> Map Name [TypeBase dim u]
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TypeBase dim u -> Bool) -> [TypeBase dim u] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any) TypeBase dim u -> Bool
mayContainArray Map Name [TypeBase dim u]
cs
--
evalTypeExp df -> m (ExpBase Info VName)
df (TEArrow (Just VName
v) TypeExp df VName
t1 TypeExp df VName
t2 SrcLoc
loc) = do
  (TypeExp (ExpBase Info VName) VName
t1', [VName]
svars1, RetType [VName]
dims1 TypeBase (ExpBase Info VName) Uniqueness
st1, Liftedness
_) <- (df -> m (ExpBase Info VName))
-> TypeExp df VName
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
forall (m :: * -> *) df.
(MonadTypeChecker m, Pretty df) =>
(df -> m (ExpBase Info VName))
-> TypeExp df VName
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
evalTypeExp df -> m (ExpBase Info VName)
df TypeExp df VName
t1
  VName
-> BoundV
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
forall a. VName -> BoundV -> m a -> m a
forall (m :: * -> *) a.
MonadTypeChecker m =>
VName -> BoundV -> m a -> m a
bindVal VName
v ([TypeParam] -> StructType -> BoundV
BoundV [] (StructType -> BoundV) -> StructType -> BoundV
forall a b. (a -> b) -> a -> b
$ TypeBase (ExpBase Info VName) Uniqueness -> StructType
forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct TypeBase (ExpBase Info VName) Uniqueness
st1) (m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
    Liftedness)
 -> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
       Liftedness))
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
forall a b. (a -> b) -> a -> b
$ do
    (TypeExp (ExpBase Info VName) VName
t2', [VName]
svars2, RetType [VName]
dims2 TypeBase (ExpBase Info VName) Uniqueness
st2, Liftedness
_) <- (df -> m (ExpBase Info VName))
-> TypeExp df VName
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
forall (m :: * -> *) df.
(MonadTypeChecker m, Pretty df) =>
(df -> m (ExpBase Info VName))
-> TypeExp df VName
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
evalTypeExp df -> m (ExpBase Info VName)
df TypeExp df VName
t2
    (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
 Liftedness)
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
      ( Maybe VName
-> TypeExp (ExpBase Info VName) VName
-> TypeExp (ExpBase Info VName) VName
-> SrcLoc
-> TypeExp (ExpBase Info VName) VName
forall d vn.
Maybe vn -> TypeExp d vn -> TypeExp d vn -> SrcLoc -> TypeExp d vn
TEArrow (VName -> Maybe VName
forall a. a -> Maybe a
Just VName
v) TypeExp (ExpBase Info VName) VName
t1' TypeExp (ExpBase Info VName) VName
t2' SrcLoc
loc,
        [VName]
svars1 [VName] -> [VName] -> [VName]
forall a. [a] -> [a] -> [a]
++ [VName]
dims1 [VName] -> [VName] -> [VName]
forall a. [a] -> [a] -> [a]
++ [VName]
svars2,
        [VName] -> TypeBase (ExpBase Info VName) Uniqueness -> ResRetType
forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [] (TypeBase (ExpBase Info VName) Uniqueness -> ResRetType)
-> TypeBase (ExpBase Info VName) Uniqueness -> ResRetType
forall a b. (a -> b) -> a -> b
$ ScalarTypeBase (ExpBase Info VName) Uniqueness
-> TypeBase (ExpBase Info VName) Uniqueness
forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar (ScalarTypeBase (ExpBase Info VName) Uniqueness
 -> TypeBase (ExpBase Info VName) Uniqueness)
-> ScalarTypeBase (ExpBase Info VName) Uniqueness
-> TypeBase (ExpBase Info VName) Uniqueness
forall a b. (a -> b) -> a -> b
$ Uniqueness
-> PName
-> Diet
-> StructType
-> ResRetType
-> ScalarTypeBase (ExpBase Info VName) Uniqueness
forall dim u.
u
-> PName
-> Diet
-> TypeBase dim NoUniqueness
-> RetTypeBase dim Uniqueness
-> ScalarTypeBase dim u
Arrow Uniqueness
Nonunique (VName -> PName
Named VName
v) (TypeBase (ExpBase Info VName) Diet -> Diet
forall shape. TypeBase shape Diet -> Diet
diet (TypeBase (ExpBase Info VName) Diet -> Diet)
-> TypeBase (ExpBase Info VName) Diet -> Diet
forall a b. (a -> b) -> a -> b
$ TypeBase (ExpBase Info VName) Uniqueness
-> TypeBase (ExpBase Info VName) Diet
resToParam TypeBase (ExpBase Info VName) Uniqueness
st1) (TypeBase (ExpBase Info VName) Uniqueness -> StructType
forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct TypeBase (ExpBase Info VName) Uniqueness
st1) ([VName] -> TypeBase (ExpBase Info VName) Uniqueness -> ResRetType
forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
dims2 TypeBase (ExpBase Info VName) Uniqueness
st2),
        Liftedness
Lifted
      )
--
evalTypeExp df -> m (ExpBase Info VName)
df (TEArrow Maybe VName
Nothing TypeExp df VName
t1 TypeExp df VName
t2 SrcLoc
loc) = do
  (TypeExp (ExpBase Info VName) VName
t1', [VName]
svars1, RetType [VName]
dims1 TypeBase (ExpBase Info VName) Uniqueness
st1, Liftedness
_) <- (df -> m (ExpBase Info VName))
-> TypeExp df VName
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
forall (m :: * -> *) df.
(MonadTypeChecker m, Pretty df) =>
(df -> m (ExpBase Info VName))
-> TypeExp df VName
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
evalTypeExp df -> m (ExpBase Info VName)
df TypeExp df VName
t1
  (TypeExp (ExpBase Info VName) VName
t2', [VName]
svars2, RetType [VName]
dims2 TypeBase (ExpBase Info VName) Uniqueness
st2, Liftedness
_) <- (df -> m (ExpBase Info VName))
-> TypeExp df VName
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
forall (m :: * -> *) df.
(MonadTypeChecker m, Pretty df) =>
(df -> m (ExpBase Info VName))
-> TypeExp df VName
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
evalTypeExp df -> m (ExpBase Info VName)
df TypeExp df VName
t2
  (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
 Liftedness)
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    ( Maybe VName
-> TypeExp (ExpBase Info VName) VName
-> TypeExp (ExpBase Info VName) VName
-> SrcLoc
-> TypeExp (ExpBase Info VName) VName
forall d vn.
Maybe vn -> TypeExp d vn -> TypeExp d vn -> SrcLoc -> TypeExp d vn
TEArrow Maybe VName
forall a. Maybe a
Nothing TypeExp (ExpBase Info VName) VName
t1' TypeExp (ExpBase Info VName) VName
t2' SrcLoc
loc,
      [VName]
svars1 [VName] -> [VName] -> [VName]
forall a. [a] -> [a] -> [a]
++ [VName]
dims1 [VName] -> [VName] -> [VName]
forall a. [a] -> [a] -> [a]
++ [VName]
svars2,
      [VName] -> TypeBase (ExpBase Info VName) Uniqueness -> ResRetType
forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [] (TypeBase (ExpBase Info VName) Uniqueness -> ResRetType)
-> (ScalarTypeBase (ExpBase Info VName) Uniqueness
    -> TypeBase (ExpBase Info VName) Uniqueness)
-> ScalarTypeBase (ExpBase Info VName) Uniqueness
-> ResRetType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScalarTypeBase (ExpBase Info VName) Uniqueness
-> TypeBase (ExpBase Info VName) Uniqueness
forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar (ScalarTypeBase (ExpBase Info VName) Uniqueness -> ResRetType)
-> ScalarTypeBase (ExpBase Info VName) Uniqueness -> ResRetType
forall a b. (a -> b) -> a -> b
$
        Uniqueness
-> PName
-> Diet
-> StructType
-> ResRetType
-> ScalarTypeBase (ExpBase Info VName) Uniqueness
forall dim u.
u
-> PName
-> Diet
-> TypeBase dim NoUniqueness
-> RetTypeBase dim Uniqueness
-> ScalarTypeBase dim u
Arrow Uniqueness
Nonunique PName
Unnamed (TypeBase (ExpBase Info VName) Diet -> Diet
forall shape. TypeBase shape Diet -> Diet
diet (TypeBase (ExpBase Info VName) Diet -> Diet)
-> TypeBase (ExpBase Info VName) Diet -> Diet
forall a b. (a -> b) -> a -> b
$ TypeBase (ExpBase Info VName) Uniqueness
-> TypeBase (ExpBase Info VName) Diet
resToParam TypeBase (ExpBase Info VName) Uniqueness
st1) (TypeBase (ExpBase Info VName) Uniqueness -> StructType
forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct TypeBase (ExpBase Info VName) Uniqueness
st1) (ResRetType -> ScalarTypeBase (ExpBase Info VName) Uniqueness)
-> ResRetType -> ScalarTypeBase (ExpBase Info VName) Uniqueness
forall a b. (a -> b) -> a -> b
$
          [VName] -> TypeBase (ExpBase Info VName) Uniqueness -> ResRetType
forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
dims2 TypeBase (ExpBase Info VName) Uniqueness
st2,
      Liftedness
Lifted
    )
--
evalTypeExp df -> m (ExpBase Info VName)
df (TEDim [VName]
dims TypeExp df VName
t SrcLoc
loc) = do
  [VName]
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
forall {m :: * -> *} {a}.
MonadTypeChecker m =>
[VName] -> m a -> m a
bindDims [VName]
dims (m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
    Liftedness)
 -> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
       Liftedness))
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
forall a b. (a -> b) -> a -> b
$ do
    (TypeExp (ExpBase Info VName) VName
t', [VName]
svars, RetType [VName]
t_dims TypeBase (ExpBase Info VName) Uniqueness
st, Liftedness
l) <- (df -> m (ExpBase Info VName))
-> TypeExp df VName
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
forall (m :: * -> *) df.
(MonadTypeChecker m, Pretty df) =>
(df -> m (ExpBase Info VName))
-> TypeExp df VName
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
evalTypeExp df -> m (ExpBase Info VName)
df TypeExp df VName
t
    let (Set VName
witnessed, Set VName
_) = StructType -> (Set VName, Set VName)
determineSizeWitnesses (StructType -> (Set VName, Set VName))
-> StructType -> (Set VName, Set VName)
forall a b. (a -> b) -> a -> b
$ TypeBase (ExpBase Info VName) Uniqueness -> StructType
forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct TypeBase (ExpBase Info VName) Uniqueness
st
    case (VName -> Bool) -> [VName] -> Maybe VName
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
L.find (VName -> Set VName -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.notMember` Set VName
witnessed) [VName]
dims of
      Just VName
d ->
        SrcLoc
-> Notes
-> Doc ()
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
forall loc a. Located loc => loc -> Notes -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc Notes
forall a. Monoid a => a
mempty (Doc ()
 -> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
       Liftedness))
-> (Doc () -> Doc ())
-> Doc ()
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
withIndexLink Doc ()
"unused-existential" (Doc ()
 -> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
       Liftedness))
-> Doc ()
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
forall a b. (a -> b) -> a -> b
$
          Doc ()
"Existential size "
            Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (VName -> Doc ()
forall a. VName -> Doc a
forall v a. IsName v => v -> Doc a
prettyName VName
d)
            Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
" not used as array size."
      Maybe VName
Nothing ->
        (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
 Liftedness)
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
          ( [VName]
-> TypeExp (ExpBase Info VName) VName
-> SrcLoc
-> TypeExp (ExpBase Info VName) VName
forall d vn. [vn] -> TypeExp d vn -> SrcLoc -> TypeExp d vn
TEDim [VName]
dims TypeExp (ExpBase Info VName) VName
t' SrcLoc
loc,
            [VName]
svars,
            [VName] -> TypeBase (ExpBase Info VName) Uniqueness -> ResRetType
forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType ([VName]
dims [VName] -> [VName] -> [VName]
forall a. [a] -> [a] -> [a]
++ [VName]
t_dims) TypeBase (ExpBase Info VName) Uniqueness
st,
            Liftedness -> Liftedness -> Liftedness
forall a. Ord a => a -> a -> a
max Liftedness
l Liftedness
SizeLifted
          )
  where
    bindDims :: [VName] -> m a -> m a
bindDims [] m a
m = m a
m
    bindDims (VName
d : [VName]
ds) m a
m =
      VName -> BoundV -> m a -> m a
forall a. VName -> BoundV -> m a -> m a
forall (m :: * -> *) a.
MonadTypeChecker m =>
VName -> BoundV -> m a -> m a
bindVal VName
d ([TypeParam] -> StructType -> BoundV
BoundV [] (StructType -> BoundV) -> StructType -> BoundV
forall a b. (a -> b) -> a -> b
$ ScalarTypeBase (ExpBase Info VName) NoUniqueness -> StructType
forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar (ScalarTypeBase (ExpBase Info VName) NoUniqueness -> StructType)
-> ScalarTypeBase (ExpBase Info VName) NoUniqueness -> StructType
forall a b. (a -> b) -> a -> b
$ PrimType -> ScalarTypeBase (ExpBase Info VName) NoUniqueness
forall dim u. PrimType -> ScalarTypeBase dim u
Prim (PrimType -> ScalarTypeBase (ExpBase Info VName) NoUniqueness)
-> PrimType -> ScalarTypeBase (ExpBase Info VName) NoUniqueness
forall a b. (a -> b) -> a -> b
$ IntType -> PrimType
Signed IntType
Int64) (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ [VName] -> m a -> m a
bindDims [VName]
ds m a
m
--
evalTypeExp df -> m (ExpBase Info VName)
df t :: TypeExp df VName
t@(TESum [(Name, [TypeExp df VName])]
cs SrcLoc
loc) = do
  let constructors :: [Name]
constructors = ((Name, [TypeExp df VName]) -> Name)
-> [(Name, [TypeExp df VName])] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, [TypeExp df VName]) -> Name
forall a b. (a, b) -> a
fst [(Name, [TypeExp df VName])]
cs
  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Name] -> [Name]
forall a. Ord a => [a] -> [a]
L.sort [Name]
constructors [Name] -> [Name] -> Bool
forall a. Eq a => a -> a -> Bool
== [Name] -> [Name]
forall a. Ord a => [a] -> [a]
L.sort ([Name] -> [Name]
forall a. Ord a => [a] -> [a]
nubOrd [Name]
constructors)) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
    SrcLoc -> Notes -> Doc () -> m ()
forall loc a. Located loc => loc -> Notes -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc Notes
forall a. Monoid a => a
mempty (Doc () -> m ()) -> Doc () -> m ()
forall a b. (a -> b) -> a -> b
$
      Doc ()
"Duplicate constructors in" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> TypeExp df VName -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. TypeExp df VName -> Doc ann
pretty TypeExp df VName
t

  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
constructors Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
256) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
    SrcLoc -> Notes -> Doc () -> m ()
forall loc a. Located loc => loc -> Notes -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc Notes
forall a. Monoid a => a
mempty Doc ()
"Sum types must have less than 256 constructors."

  Map
  Name
  [(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
    Liftedness)]
checked <- (([TypeExp df VName]
 -> m [(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
        Liftedness)])
-> Map Name [TypeExp df VName]
-> m (Map
        Name
        [(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
          Liftedness)])
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Map Name a -> f (Map Name b)
traverse (([TypeExp df VName]
  -> m [(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
         Liftedness)])
 -> Map Name [TypeExp df VName]
 -> m (Map
         Name
         [(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
           Liftedness)]))
-> ((TypeExp df VName
     -> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
           Liftedness))
    -> [TypeExp df VName]
    -> m [(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
           Liftedness)])
-> (TypeExp df VName
    -> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
          Liftedness))
-> Map Name [TypeExp df VName]
-> m (Map
        Name
        [(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
          Liftedness)])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TypeExp df VName
 -> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
       Liftedness))
-> [TypeExp df VName]
-> m [(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
       Liftedness)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse) ((df -> m (ExpBase Info VName))
-> TypeExp df VName
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
forall (m :: * -> *) df.
(MonadTypeChecker m, Pretty df) =>
(df -> m (ExpBase Info VName))
-> TypeExp df VName
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
evalTypeExp df -> m (ExpBase Info VName)
df) (Map Name [TypeExp df VName]
 -> m (Map
         Name
         [(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
           Liftedness)]))
-> Map Name [TypeExp df VName]
-> m (Map
        Name
        [(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
          Liftedness)])
forall a b. (a -> b) -> a -> b
$ [(Name, [TypeExp df VName])] -> Map Name [TypeExp df VName]
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Name, [TypeExp df VName])]
cs
  let cs' :: Map Name [TypeExp (ExpBase Info VName) VName]
cs' = (([(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
   Liftedness)]
 -> [TypeExp (ExpBase Info VName) VName])
-> Map
     Name
     [(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
       Liftedness)]
-> Map Name [TypeExp (ExpBase Info VName) VName]
forall a b. (a -> b) -> Map Name a -> Map Name b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
    Liftedness)]
  -> [TypeExp (ExpBase Info VName) VName])
 -> Map
      Name
      [(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
        Liftedness)]
 -> Map Name [TypeExp (ExpBase Info VName) VName])
-> (((TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
     -> TypeExp (ExpBase Info VName) VName)
    -> [(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
         Liftedness)]
    -> [TypeExp (ExpBase Info VName) VName])
-> ((TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
     Liftedness)
    -> TypeExp (ExpBase Info VName) VName)
-> Map
     Name
     [(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
       Liftedness)]
-> Map Name [TypeExp (ExpBase Info VName) VName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
  Liftedness)
 -> TypeExp (ExpBase Info VName) VName)
-> [(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
     Liftedness)]
-> [TypeExp (ExpBase Info VName) VName]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) (\(TypeExp (ExpBase Info VName) VName
x, [VName]
_, ResRetType
_, Liftedness
_) -> TypeExp (ExpBase Info VName) VName
x) Map
  Name
  [(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
    Liftedness)]
checked
      cs_svars :: [VName]
cs_svars = (([(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
   Liftedness)]
 -> [VName])
-> Map
     Name
     [(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
       Liftedness)]
-> [VName]
forall m a. Monoid m => (a -> m) -> Map Name a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (([(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
    Liftedness)]
  -> [VName])
 -> Map
      Name
      [(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
        Liftedness)]
 -> [VName])
-> (((TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
     -> [VName])
    -> [(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
         Liftedness)]
    -> [VName])
-> ((TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
     Liftedness)
    -> [VName])
-> Map
     Name
     [(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
       Liftedness)]
-> [VName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
  Liftedness)
 -> [VName])
-> [(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
     Liftedness)]
-> [VName]
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap) (\(TypeExp (ExpBase Info VName) VName
_, [VName]
y, ResRetType
_, Liftedness
_) -> [VName]
y) Map
  Name
  [(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
    Liftedness)]
checked
      ts_s :: Map Name [ResRetType]
ts_s = (([(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
   Liftedness)]
 -> [ResRetType])
-> Map
     Name
     [(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
       Liftedness)]
-> Map Name [ResRetType]
forall a b. (a -> b) -> Map Name a -> Map Name b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
    Liftedness)]
  -> [ResRetType])
 -> Map
      Name
      [(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
        Liftedness)]
 -> Map Name [ResRetType])
-> (((TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
     -> ResRetType)
    -> [(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
         Liftedness)]
    -> [ResRetType])
-> ((TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
     Liftedness)
    -> ResRetType)
-> Map
     Name
     [(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
       Liftedness)]
-> Map Name [ResRetType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
  Liftedness)
 -> ResRetType)
-> [(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
     Liftedness)]
-> [ResRetType]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) (\(TypeExp (ExpBase Info VName) VName
_, [VName]
_, ResRetType
z, Liftedness
_) -> ResRetType
z) Map
  Name
  [(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
    Liftedness)]
checked
      ls :: [Liftedness]
ls = (([(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
   Liftedness)]
 -> [Liftedness])
-> Map
     Name
     [(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
       Liftedness)]
-> [Liftedness]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (([(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
    Liftedness)]
  -> [Liftedness])
 -> Map
      Name
      [(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
        Liftedness)]
 -> [Liftedness])
-> (((TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
     -> Liftedness)
    -> [(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
         Liftedness)]
    -> [Liftedness])
-> ((TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
     Liftedness)
    -> Liftedness)
-> Map
     Name
     [(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
       Liftedness)]
-> [Liftedness]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
  Liftedness)
 -> Liftedness)
-> [(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
     Liftedness)]
-> [Liftedness]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) (\(TypeExp (ExpBase Info VName) VName
_, [VName]
_, ResRetType
_, Liftedness
v) -> Liftedness
v) Map
  Name
  [(TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
    Liftedness)]
checked
  (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
 Liftedness)
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    ( [(Name, [TypeExp (ExpBase Info VName) VName])]
-> SrcLoc -> TypeExp (ExpBase Info VName) VName
forall d vn. [(Name, [TypeExp d vn])] -> SrcLoc -> TypeExp d vn
TESum (Map Name [TypeExp (ExpBase Info VName) VName]
-> [(Name, [TypeExp (ExpBase Info VName) VName])]
forall k a. Map k a -> [(k, a)]
M.toList Map Name [TypeExp (ExpBase Info VName) VName]
cs') SrcLoc
loc,
      [VName]
cs_svars,
      [VName] -> TypeBase (ExpBase Info VName) Uniqueness -> ResRetType
forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType (([ResRetType] -> [VName]) -> Map Name [ResRetType] -> [VName]
forall m a. Monoid m => (a -> m) -> Map Name a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((ResRetType -> [VName]) -> [ResRetType] -> [VName]
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ResRetType -> [VName]
forall dim as. RetTypeBase dim as -> [VName]
retDims) Map Name [ResRetType]
ts_s) (TypeBase (ExpBase Info VName) Uniqueness -> ResRetType)
-> TypeBase (ExpBase Info VName) Uniqueness -> ResRetType
forall a b. (a -> b) -> a -> b
$
        ScalarTypeBase (ExpBase Info VName) Uniqueness
-> TypeBase (ExpBase Info VName) Uniqueness
forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar (ScalarTypeBase (ExpBase Info VName) Uniqueness
 -> TypeBase (ExpBase Info VName) Uniqueness)
-> ScalarTypeBase (ExpBase Info VName) Uniqueness
-> TypeBase (ExpBase Info VName) Uniqueness
forall a b. (a -> b) -> a -> b
$
          Map Name [TypeBase (ExpBase Info VName) Uniqueness]
-> ScalarTypeBase (ExpBase Info VName) Uniqueness
forall dim u. Map Name [TypeBase dim u] -> ScalarTypeBase dim u
Sum (Map Name [TypeBase (ExpBase Info VName) Uniqueness]
 -> ScalarTypeBase (ExpBase Info VName) Uniqueness)
-> Map Name [TypeBase (ExpBase Info VName) Uniqueness]
-> ScalarTypeBase (ExpBase Info VName) Uniqueness
forall a b. (a -> b) -> a -> b
$
            ([ResRetType] -> [TypeBase (ExpBase Info VName) Uniqueness])
-> Map Name [ResRetType]
-> Map Name [TypeBase (ExpBase Info VName) Uniqueness]
forall a b k. (a -> b) -> Map k a -> Map k b
M.map ((ResRetType -> TypeBase (ExpBase Info VName) Uniqueness)
-> [ResRetType] -> [TypeBase (ExpBase Info VName) Uniqueness]
forall a b. (a -> b) -> [a] -> [b]
map ResRetType -> TypeBase (ExpBase Info VName) Uniqueness
forall dim as. RetTypeBase dim as -> TypeBase dim as
retType) Map Name [ResRetType]
ts_s,
      (Liftedness -> Liftedness -> Liftedness)
-> Liftedness -> [Liftedness] -> Liftedness
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' Liftedness -> Liftedness -> Liftedness
forall a. Ord a => a -> a -> a
max Liftedness
Unlifted [Liftedness]
ls
    )
evalTypeExp df -> m (ExpBase Info VName)
df ote :: TypeExp df VName
ote@TEApply {} = do
  (QualName VName
tname, SrcLoc
tname_loc, [TypeArgExp df VName]
targs) <- TypeExp df VName
-> m (QualName VName, SrcLoc, [TypeArgExp df VName])
forall {f :: * -> *} {vn} {d}.
(MonadTypeChecker f, IsName vn, Pretty d) =>
TypeExp d vn -> f (QualName vn, SrcLoc, [TypeArgExp d vn])
rootAndArgs TypeExp df VName
ote
  ([TypeParam]
ps, StructRetType
tname_t, Liftedness
l) <- QualName VName -> m ([TypeParam], StructRetType, Liftedness)
forall (m :: * -> *).
MonadTypeChecker m =>
QualName VName -> m ([TypeParam], StructRetType, Liftedness)
lookupType QualName VName
tname
  RetType [VName]
t_dims TypeBase (ExpBase Info VName) Uniqueness
t <- ResRetType -> m ResRetType
forall (m :: * -> *).
MonadTypeChecker m =>
ResRetType -> m ResRetType
renameRetType (ResRetType -> m ResRetType) -> ResRetType -> m ResRetType
forall a b. (a -> b) -> a -> b
$ Uniqueness -> StructRetType -> ResRetType
forall u.
Uniqueness -> RetTypeBase (ExpBase Info VName) u -> ResRetType
toResRet Uniqueness
Nonunique StructRetType
tname_t
  if [TypeParam] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeParam]
ps Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [TypeArgExp df VName] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeArgExp df VName]
targs
    then
      SrcLoc
-> Notes
-> Doc ()
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
forall loc a. Located loc => loc -> Notes -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
tloc Notes
forall a. Monoid a => a
mempty (Doc ()
 -> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
       Liftedness))
-> Doc ()
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
forall a b. (a -> b) -> a -> b
$
        Doc ()
"Type constructor"
          Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (QualName VName -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. QualName VName -> Doc ann
pretty QualName VName
tname)
          Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"requires"
          Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Int -> Doc ()
forall ann. Int -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty ([TypeParam] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeParam]
ps)
          Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"arguments, but provided"
          Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Int -> Doc ()
forall ann. Int -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty ([TypeArgExp df VName] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeArgExp df VName]
targs)
          Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
    else do
      ([TypeArgExp (ExpBase Info VName) VName]
targs', [[VName]]
dims, [Map VName (Subst StructRetType)]
substs) <- [(TypeArgExp (ExpBase Info VName) VName, [VName],
  Map VName (Subst StructRetType))]
-> ([TypeArgExp (ExpBase Info VName) VName], [[VName]],
    [Map VName (Subst StructRetType)])
forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 ([(TypeArgExp (ExpBase Info VName) VName, [VName],
   Map VName (Subst StructRetType))]
 -> ([TypeArgExp (ExpBase Info VName) VName], [[VName]],
     [Map VName (Subst StructRetType)]))
-> m [(TypeArgExp (ExpBase Info VName) VName, [VName],
       Map VName (Subst StructRetType))]
-> m ([TypeArgExp (ExpBase Info VName) VName], [[VName]],
      [Map VName (Subst StructRetType)])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TypeParam
 -> TypeArgExp df VName
 -> m (TypeArgExp (ExpBase Info VName) VName, [VName],
       Map VName (Subst StructRetType)))
-> [TypeParam]
-> [TypeArgExp df VName]
-> m [(TypeArgExp (ExpBase Info VName) VName, [VName],
       Map VName (Subst StructRetType))]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM TypeParam
-> TypeArgExp df VName
-> m (TypeArgExp (ExpBase Info VName) VName, [VName],
      Map VName (Subst StructRetType))
forall {k}.
(Eq k, IsName k) =>
TypeParamBase k
-> TypeArgExp df VName
-> m (TypeArgExp (ExpBase Info VName) VName, [VName],
      Map k (Subst StructRetType))
checkArgApply [TypeParam]
ps [TypeArgExp df VName]
targs
      (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
 Liftedness)
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( (TypeExp (ExpBase Info VName) VName
 -> TypeArgExp (ExpBase Info VName) VName
 -> TypeExp (ExpBase Info VName) VName)
-> TypeExp (ExpBase Info VName) VName
-> [TypeArgExp (ExpBase Info VName) VName]
-> TypeExp (ExpBase Info VName) VName
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\TypeExp (ExpBase Info VName) VName
x TypeArgExp (ExpBase Info VName) VName
y -> TypeExp (ExpBase Info VName) VName
-> TypeArgExp (ExpBase Info VName) VName
-> SrcLoc
-> TypeExp (ExpBase Info VName) VName
forall d vn.
TypeExp d vn -> TypeArgExp d vn -> SrcLoc -> TypeExp d vn
TEApply TypeExp (ExpBase Info VName) VName
x TypeArgExp (ExpBase Info VName) VName
y SrcLoc
tloc) (QualName VName -> SrcLoc -> TypeExp (ExpBase Info VName) VName
forall d vn. QualName vn -> SrcLoc -> TypeExp d vn
TEVar QualName VName
tname SrcLoc
tname_loc) [TypeArgExp (ExpBase Info VName) VName]
targs',
          [],
          [VName] -> TypeBase (ExpBase Info VName) Uniqueness -> ResRetType
forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType ([VName]
t_dims [VName] -> [VName] -> [VName]
forall a. [a] -> [a] -> [a]
++ [[VName]] -> [VName]
forall a. Monoid a => [a] -> a
mconcat [[VName]]
dims) (TypeBase (ExpBase Info VName) Uniqueness -> ResRetType)
-> TypeBase (ExpBase Info VName) Uniqueness -> ResRetType
forall a b. (a -> b) -> a -> b
$
            TypeSubs
-> TypeBase (ExpBase Info VName) Uniqueness
-> TypeBase (ExpBase Info VName) Uniqueness
forall a. Substitutable a => TypeSubs -> a -> a
applySubst (VName
-> Map VName (Subst StructRetType) -> Maybe (Subst StructRetType)
forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` [Map VName (Subst StructRetType)]
-> Map VName (Subst StructRetType)
forall a. Monoid a => [a] -> a
mconcat [Map VName (Subst StructRetType)]
substs) TypeBase (ExpBase Info VName) Uniqueness
t,
          Liftedness
l
        )
  where
    tloc :: SrcLoc
tloc = TypeExp df VName -> SrcLoc
forall a. Located a => a -> SrcLoc
srclocOf TypeExp df VName
ote

    rootAndArgs :: TypeExp d vn -> f (QualName vn, SrcLoc, [TypeArgExp d vn])
rootAndArgs (TEVar QualName vn
qn SrcLoc
loc) = (QualName vn, SrcLoc, [TypeArgExp d vn])
-> f (QualName vn, SrcLoc, [TypeArgExp d vn])
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (QualName vn
qn, SrcLoc
loc, [])
    rootAndArgs (TEApply TypeExp d vn
op TypeArgExp d vn
arg SrcLoc
_) = do
      (QualName vn
op', SrcLoc
loc, [TypeArgExp d vn]
args) <- TypeExp d vn -> f (QualName vn, SrcLoc, [TypeArgExp d vn])
rootAndArgs TypeExp d vn
op
      (QualName vn, SrcLoc, [TypeArgExp d vn])
-> f (QualName vn, SrcLoc, [TypeArgExp d vn])
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (QualName vn
op', SrcLoc
loc, [TypeArgExp d vn]
args [TypeArgExp d vn] -> [TypeArgExp d vn] -> [TypeArgExp d vn]
forall a. [a] -> [a] -> [a]
++ [TypeArgExp d vn
arg])
    rootAndArgs TypeExp d vn
te' =
      SrcLoc
-> Notes -> Doc () -> f (QualName vn, SrcLoc, [TypeArgExp d vn])
forall loc a. Located loc => loc -> Notes -> Doc () -> f a
forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError (TypeExp d vn -> SrcLoc
forall a. Located a => a -> SrcLoc
srclocOf TypeExp d vn
te') Notes
forall a. Monoid a => a
mempty (Doc () -> f (QualName vn, SrcLoc, [TypeArgExp d vn]))
-> Doc () -> f (QualName vn, SrcLoc, [TypeArgExp d vn])
forall a b. (a -> b) -> a -> b
$
        Doc ()
"Type" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (TypeExp d vn -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. TypeExp d vn -> Doc ann
pretty TypeExp d vn
te') Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"is not a type constructor."

    checkSizeExp :: SizeExp df
-> m (TypeArgExp (ExpBase Info VName) vn, [VName], Subst t)
checkSizeExp (SizeExp df
e SrcLoc
dloc) = do
      ExpBase Info VName
e' <- df -> m (ExpBase Info VName)
df df
e
      (TypeArgExp (ExpBase Info VName) vn, [VName], Subst t)
-> m (TypeArgExp (ExpBase Info VName) vn, [VName], Subst t)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( SizeExp (ExpBase Info VName) -> TypeArgExp (ExpBase Info VName) vn
forall d vn. SizeExp d -> TypeArgExp d vn
TypeArgExpSize (ExpBase Info VName -> SrcLoc -> SizeExp (ExpBase Info VName)
forall d. d -> SrcLoc -> SizeExp d
SizeExp ExpBase Info VName
e' SrcLoc
dloc),
          [],
          ExpBase Info VName -> Subst t
forall t. ExpBase Info VName -> Subst t
ExpSubst ExpBase Info VName
e'
        )
    checkSizeExp (SizeExpAny SrcLoc
loc) = do
      VName
d <- Name -> m VName
forall (m :: * -> *). MonadTypeChecker m => Name -> m VName
newTypeName Name
"d"
      (TypeArgExp (ExpBase Info VName) vn, [VName], Subst t)
-> m (TypeArgExp (ExpBase Info VName) vn, [VName], Subst t)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( SizeExp (ExpBase Info VName) -> TypeArgExp (ExpBase Info VName) vn
forall d vn. SizeExp d -> TypeArgExp d vn
TypeArgExpSize (SrcLoc -> SizeExp (ExpBase Info VName)
forall d. SrcLoc -> SizeExp d
SizeExpAny SrcLoc
loc),
          [VName
d],
          ExpBase Info VName -> Subst t
forall t. ExpBase Info VName -> Subst t
ExpSubst (ExpBase Info VName -> Subst t) -> ExpBase Info VName -> Subst t
forall a b. (a -> b) -> a -> b
$ QualName VName -> SrcLoc -> ExpBase Info VName
sizeFromName (VName -> QualName VName
forall v. v -> QualName v
qualName VName
d) SrcLoc
loc
        )

    checkArgApply :: TypeParamBase k
-> TypeArgExp df VName
-> m (TypeArgExp (ExpBase Info VName) VName, [VName],
      Map k (Subst StructRetType))
checkArgApply (TypeParamDim k
pv SrcLoc
_) (TypeArgExpSize SizeExp df
d) = do
      (TypeArgExp (ExpBase Info VName) VName
d', [VName]
svars, Subst StructRetType
subst) <- SizeExp df
-> m (TypeArgExp (ExpBase Info VName) VName, [VName],
      Subst StructRetType)
forall {vn} {t}.
SizeExp df
-> m (TypeArgExp (ExpBase Info VName) vn, [VName], Subst t)
checkSizeExp SizeExp df
d
      (TypeArgExp (ExpBase Info VName) VName, [VName],
 Map k (Subst StructRetType))
-> m (TypeArgExp (ExpBase Info VName) VName, [VName],
      Map k (Subst StructRetType))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeArgExp (ExpBase Info VName) VName
d', [VName]
svars, k -> Subst StructRetType -> Map k (Subst StructRetType)
forall k a. k -> a -> Map k a
M.singleton k
pv Subst StructRetType
subst)
    checkArgApply (TypeParamType Liftedness
_ k
pv SrcLoc
_) (TypeArgExpType TypeExp df VName
te) = do
      (TypeExp (ExpBase Info VName) VName
te', [VName]
svars, RetType [VName]
dims TypeBase (ExpBase Info VName) Uniqueness
st, Liftedness
_) <- (df -> m (ExpBase Info VName))
-> TypeExp df VName
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
forall (m :: * -> *) df.
(MonadTypeChecker m, Pretty df) =>
(df -> m (ExpBase Info VName))
-> TypeExp df VName
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
evalTypeExp df -> m (ExpBase Info VName)
df TypeExp df VName
te
      (TypeArgExp (ExpBase Info VName) VName, [VName],
 Map k (Subst StructRetType))
-> m (TypeArgExp (ExpBase Info VName) VName, [VName],
      Map k (Subst StructRetType))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( TypeExp (ExpBase Info VName) VName
-> TypeArgExp (ExpBase Info VName) VName
forall d vn. TypeExp d vn -> TypeArgExp d vn
TypeArgExpType TypeExp (ExpBase Info VName) VName
te',
          [VName]
svars [VName] -> [VName] -> [VName]
forall a. [a] -> [a] -> [a]
++ [VName]
dims,
          k -> Subst StructRetType -> Map k (Subst StructRetType)
forall k a. k -> a -> Map k a
M.singleton k
pv (Subst StructRetType -> Map k (Subst StructRetType))
-> Subst StructRetType -> Map k (Subst StructRetType)
forall a b. (a -> b) -> a -> b
$ [TypeParam] -> StructRetType -> Subst StructRetType
forall t. [TypeParam] -> t -> Subst t
Subst [] (StructRetType -> Subst StructRetType)
-> StructRetType -> Subst StructRetType
forall a b. (a -> b) -> a -> b
$ [VName] -> StructType -> StructRetType
forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [] (StructType -> StructRetType) -> StructType -> StructRetType
forall a b. (a -> b) -> a -> b
$ TypeBase (ExpBase Info VName) Uniqueness -> StructType
forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct TypeBase (ExpBase Info VName) Uniqueness
st
        )
    checkArgApply TypeParamBase k
p TypeArgExp df VName
a =
      SrcLoc
-> Notes
-> Doc ()
-> m (TypeArgExp (ExpBase Info VName) VName, [VName],
      Map k (Subst StructRetType))
forall loc a. Located loc => loc -> Notes -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
tloc Notes
forall a. Monoid a => a
mempty (Doc ()
 -> m (TypeArgExp (ExpBase Info VName) VName, [VName],
       Map k (Subst StructRetType)))
-> Doc ()
-> m (TypeArgExp (ExpBase Info VName) VName, [VName],
      Map k (Subst StructRetType))
forall a b. (a -> b) -> a -> b
$
        Doc ()
"Type argument"
          Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> TypeArgExp df VName -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. TypeArgExp df VName -> Doc ann
pretty TypeArgExp df VName
a
          Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"not valid for a type parameter"
          Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> TypeParamBase k -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. TypeParamBase k -> Doc ann
pretty TypeParamBase k
p
          Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."

-- | Check a type expression, producing:
--
-- * The checked expression.
-- * Size variables for any anonymous sizes in the expression.
-- * The elaborated type.
-- * The liftedness of the type.
checkTypeExp ::
  (MonadTypeChecker m, Pretty df) =>
  (df -> m Exp) ->
  TypeExp df VName ->
  m (TypeExp Exp VName, [VName], ResRetType, Liftedness)
checkTypeExp :: forall (m :: * -> *) df.
(MonadTypeChecker m, Pretty df) =>
(df -> m (ExpBase Info VName))
-> TypeExp df VName
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
checkTypeExp = (df -> m (ExpBase Info VName))
-> TypeExp df VName
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
forall (m :: * -> *) df.
(MonadTypeChecker m, Pretty df) =>
(df -> m (ExpBase Info VName))
-> TypeExp df VName
-> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
evalTypeExp

-- | Construct a type argument corresponding to a type parameter.
typeParamToArg :: TypeParam -> StructTypeArg
typeParamToArg :: TypeParam -> StructTypeArg
typeParamToArg (TypeParamDim VName
v SrcLoc
ploc) =
  ExpBase Info VName -> StructTypeArg
forall dim. dim -> TypeArg dim
TypeArgDim (ExpBase Info VName -> StructTypeArg)
-> ExpBase Info VName -> StructTypeArg
forall a b. (a -> b) -> a -> b
$ QualName VName -> SrcLoc -> ExpBase Info VName
sizeFromName (VName -> QualName VName
forall v. v -> QualName v
qualName VName
v) SrcLoc
ploc
typeParamToArg (TypeParamType Liftedness
_ VName
v SrcLoc
_) =
  StructType -> StructTypeArg
forall dim. TypeBase dim NoUniqueness -> TypeArg dim
TypeArgType (StructType -> StructTypeArg) -> StructType -> StructTypeArg
forall a b. (a -> b) -> a -> b
$ ScalarTypeBase (ExpBase Info VName) NoUniqueness -> StructType
forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar (ScalarTypeBase (ExpBase Info VName) NoUniqueness -> StructType)
-> ScalarTypeBase (ExpBase Info VName) NoUniqueness -> StructType
forall a b. (a -> b) -> a -> b
$ NoUniqueness
-> QualName VName
-> [StructTypeArg]
-> ScalarTypeBase (ExpBase Info VName) NoUniqueness
forall dim u.
u -> QualName VName -> [TypeArg dim] -> ScalarTypeBase dim u
TypeVar NoUniqueness
forall a. Monoid a => a
mempty (VName -> QualName VName
forall v. v -> QualName v
qualName VName
v) []

-- | A type substitution may be a substitution or a yet-unknown
-- substitution (but which is certainly an overloaded primitive
-- type!).
data Subst t = Subst [TypeParam] t | ExpSubst Exp
  deriving (Int -> Subst t -> ShowS
[Subst t] -> ShowS
Subst t -> String
(Int -> Subst t -> ShowS)
-> (Subst t -> String) -> ([Subst t] -> ShowS) -> Show (Subst t)
forall t. Show t => Int -> Subst t -> ShowS
forall t. Show t => [Subst t] -> ShowS
forall t. Show t => Subst t -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall t. Show t => Int -> Subst t -> ShowS
showsPrec :: Int -> Subst t -> ShowS
$cshow :: forall t. Show t => Subst t -> String
show :: Subst t -> String
$cshowList :: forall t. Show t => [Subst t] -> ShowS
showList :: [Subst t] -> ShowS
Show)

instance (Pretty t) => Pretty (Subst t) where
  pretty :: forall ann. Subst t -> Doc ann
pretty (Subst [] t
t) = t -> Doc ann
forall ann. t -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty t
t
  pretty (Subst [TypeParam]
tps t
t) = [Doc ann] -> Doc ann
forall a. Monoid a => [a] -> a
mconcat ((TypeParam -> Doc ann) -> [TypeParam] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map TypeParam -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. TypeParam -> Doc ann
pretty [TypeParam]
tps) Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
colon Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> t -> Doc ann
forall ann. t -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty t
t
  pretty (ExpSubst ExpBase Info VName
e) = ExpBase Info VName -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. ExpBase Info VName -> Doc ann
pretty ExpBase Info VName
e

instance Functor Subst where
  fmap :: forall a b. (a -> b) -> Subst a -> Subst b
fmap a -> b
f (Subst [TypeParam]
ps a
t) = [TypeParam] -> b -> Subst b
forall t. [TypeParam] -> t -> Subst t
Subst [TypeParam]
ps (b -> Subst b) -> b -> Subst b
forall a b. (a -> b) -> a -> b
$ a -> b
f a
t
  fmap a -> b
_ (ExpSubst ExpBase Info VName
e) = ExpBase Info VName -> Subst b
forall t. ExpBase Info VName -> Subst t
ExpSubst ExpBase Info VName
e

-- | Create a type substitution corresponding to a type binding.
substFromAbbr :: TypeBinding -> Subst StructRetType
substFromAbbr :: TypeBinding -> Subst StructRetType
substFromAbbr (TypeAbbr Liftedness
_ [TypeParam]
ps StructRetType
rt) = [TypeParam] -> StructRetType -> Subst StructRetType
forall t. [TypeParam] -> t -> Subst t
Subst [TypeParam]
ps StructRetType
rt

-- | Substitutions to apply in a type.
type TypeSubs = VName -> Maybe (Subst StructRetType)

-- | Class of types which allow for substitution of types with no
-- annotations for type variable names.
class Substitutable a where
  applySubst :: TypeSubs -> a -> a

instance Substitutable (RetTypeBase Size Uniqueness) where
  applySubst :: TypeSubs -> ResRetType -> ResRetType
applySubst TypeSubs
f (RetType [VName]
dims TypeBase (ExpBase Info VName) Uniqueness
t) =
    let RetType [VName]
more_dims TypeBase (ExpBase Info VName) Uniqueness
t' = (VName -> Maybe (Subst ResRetType))
-> TypeBase (ExpBase Info VName) Uniqueness -> ResRetType
forall u.
Monoid u =>
(VName -> Maybe (Subst (RetTypeBase (ExpBase Info VName) u)))
-> TypeBase (ExpBase Info VName) u
-> RetTypeBase (ExpBase Info VName) u
substTypesRet VName -> Maybe (Subst ResRetType)
f' TypeBase (ExpBase Info VName) Uniqueness
t
     in [VName] -> TypeBase (ExpBase Info VName) Uniqueness -> ResRetType
forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType ([VName]
dims [VName] -> [VName] -> [VName]
forall a. [a] -> [a] -> [a]
++ [VName]
more_dims) TypeBase (ExpBase Info VName) Uniqueness
t'
    where
      f' :: VName -> Maybe (Subst ResRetType)
f' = (Subst StructRetType -> Subst ResRetType)
-> Maybe (Subst StructRetType) -> Maybe (Subst ResRetType)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((StructRetType -> ResRetType)
-> Subst StructRetType -> Subst ResRetType
forall a b. (a -> b) -> Subst a -> Subst b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((NoUniqueness -> Uniqueness) -> StructRetType -> ResRetType
forall b c a. (b -> c) -> RetTypeBase a b -> RetTypeBase a c
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (Uniqueness -> NoUniqueness -> Uniqueness
forall a b. a -> b -> a
const Uniqueness
forall a. Monoid a => a
mempty))) (Maybe (Subst StructRetType) -> Maybe (Subst ResRetType))
-> TypeSubs -> VName -> Maybe (Subst ResRetType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeSubs
f

instance Substitutable (RetTypeBase Size NoUniqueness) where
  applySubst :: TypeSubs -> StructRetType -> StructRetType
applySubst TypeSubs
f (RetType [VName]
dims StructType
t) =
    let RetType [VName]
more_dims StructType
t' = TypeSubs -> StructType -> StructRetType
forall u.
Monoid u =>
(VName -> Maybe (Subst (RetTypeBase (ExpBase Info VName) u)))
-> TypeBase (ExpBase Info VName) u
-> RetTypeBase (ExpBase Info VName) u
substTypesRet TypeSubs
f StructType
t
     in [VName] -> StructType -> StructRetType
forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType ([VName]
dims [VName] -> [VName] -> [VName]
forall a. [a] -> [a] -> [a]
++ [VName]
more_dims) StructType
t'

instance Substitutable StructType where
  applySubst :: TypeSubs -> StructType -> StructType
applySubst = TypeSubs -> StructType -> StructType
forall u.
Monoid u =>
(VName -> Maybe (Subst (RetTypeBase (ExpBase Info VName) u)))
-> TypeBase (ExpBase Info VName) u
-> TypeBase (ExpBase Info VName) u
substTypesAny

instance Substitutable ParamType where
  applySubst :: TypeSubs
-> TypeBase (ExpBase Info VName) Diet
-> TypeBase (ExpBase Info VName) Diet
applySubst TypeSubs
f = (VName -> Maybe (Subst (RetTypeBase (ExpBase Info VName) Diet)))
-> TypeBase (ExpBase Info VName) Diet
-> TypeBase (ExpBase Info VName) Diet
forall u.
Monoid u =>
(VName -> Maybe (Subst (RetTypeBase (ExpBase Info VName) u)))
-> TypeBase (ExpBase Info VName) u
-> TypeBase (ExpBase Info VName) u
substTypesAny ((VName -> Maybe (Subst (RetTypeBase (ExpBase Info VName) Diet)))
 -> TypeBase (ExpBase Info VName) Diet
 -> TypeBase (ExpBase Info VName) Diet)
-> (VName -> Maybe (Subst (RetTypeBase (ExpBase Info VName) Diet)))
-> TypeBase (ExpBase Info VName) Diet
-> TypeBase (ExpBase Info VName) Diet
forall a b. (a -> b) -> a -> b
$ (Subst StructRetType
 -> Subst (RetTypeBase (ExpBase Info VName) Diet))
-> Maybe (Subst StructRetType)
-> Maybe (Subst (RetTypeBase (ExpBase Info VName) Diet))
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((StructRetType -> RetTypeBase (ExpBase Info VName) Diet)
-> Subst StructRetType
-> Subst (RetTypeBase (ExpBase Info VName) Diet)
forall a b. (a -> b) -> Subst a -> Subst b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((StructRetType -> RetTypeBase (ExpBase Info VName) Diet)
 -> Subst StructRetType
 -> Subst (RetTypeBase (ExpBase Info VName) Diet))
-> (StructRetType -> RetTypeBase (ExpBase Info VName) Diet)
-> Subst StructRetType
-> Subst (RetTypeBase (ExpBase Info VName) Diet)
forall a b. (a -> b) -> a -> b
$ (NoUniqueness -> Diet)
-> StructRetType -> RetTypeBase (ExpBase Info VName) Diet
forall b c a. (b -> c) -> RetTypeBase a b -> RetTypeBase a c
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ((NoUniqueness -> Diet)
 -> StructRetType -> RetTypeBase (ExpBase Info VName) Diet)
-> (NoUniqueness -> Diet)
-> StructRetType
-> RetTypeBase (ExpBase Info VName) Diet
forall a b. (a -> b) -> a -> b
$ Diet -> NoUniqueness -> Diet
forall a b. a -> b -> a
const Diet
Observe) (Maybe (Subst StructRetType)
 -> Maybe (Subst (RetTypeBase (ExpBase Info VName) Diet)))
-> TypeSubs
-> VName
-> Maybe (Subst (RetTypeBase (ExpBase Info VName) Diet))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeSubs
f

instance Substitutable (TypeBase Size Uniqueness) where
  applySubst :: TypeSubs
-> TypeBase (ExpBase Info VName) Uniqueness
-> TypeBase (ExpBase Info VName) Uniqueness
applySubst TypeSubs
f = (VName -> Maybe (Subst ResRetType))
-> TypeBase (ExpBase Info VName) Uniqueness
-> TypeBase (ExpBase Info VName) Uniqueness
forall u.
Monoid u =>
(VName -> Maybe (Subst (RetTypeBase (ExpBase Info VName) u)))
-> TypeBase (ExpBase Info VName) u
-> TypeBase (ExpBase Info VName) u
substTypesAny ((VName -> Maybe (Subst ResRetType))
 -> TypeBase (ExpBase Info VName) Uniqueness
 -> TypeBase (ExpBase Info VName) Uniqueness)
-> (VName -> Maybe (Subst ResRetType))
-> TypeBase (ExpBase Info VName) Uniqueness
-> TypeBase (ExpBase Info VName) Uniqueness
forall a b. (a -> b) -> a -> b
$ (Subst StructRetType -> Subst ResRetType)
-> Maybe (Subst StructRetType) -> Maybe (Subst ResRetType)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((StructRetType -> ResRetType)
-> Subst StructRetType -> Subst ResRetType
forall a b. (a -> b) -> Subst a -> Subst b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((StructRetType -> ResRetType)
 -> Subst StructRetType -> Subst ResRetType)
-> (StructRetType -> ResRetType)
-> Subst StructRetType
-> Subst ResRetType
forall a b. (a -> b) -> a -> b
$ (NoUniqueness -> Uniqueness) -> StructRetType -> ResRetType
forall b c a. (b -> c) -> RetTypeBase a b -> RetTypeBase a c
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ((NoUniqueness -> Uniqueness) -> StructRetType -> ResRetType)
-> (NoUniqueness -> Uniqueness) -> StructRetType -> ResRetType
forall a b. (a -> b) -> a -> b
$ Uniqueness -> NoUniqueness -> Uniqueness
forall a b. a -> b -> a
const Uniqueness
Nonunique) (Maybe (Subst StructRetType) -> Maybe (Subst ResRetType))
-> TypeSubs -> VName -> Maybe (Subst ResRetType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeSubs
f

instance Substitutable Exp where
  applySubst :: TypeSubs -> ExpBase Info VName -> ExpBase Info VName
applySubst TypeSubs
f = Identity (ExpBase Info VName) -> ExpBase Info VName
forall a. Identity a -> a
runIdentity (Identity (ExpBase Info VName) -> ExpBase Info VName)
-> (ExpBase Info VName -> Identity (ExpBase Info VName))
-> ExpBase Info VName
-> ExpBase Info VName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExpBase Info VName -> Identity (ExpBase Info VName)
mapOnExp
    where
      mapOnExp :: ExpBase Info VName -> Identity (ExpBase Info VName)
mapOnExp (Var (QualName [VName]
_ VName
v) Info StructType
_ SrcLoc
_)
        | Just (ExpSubst ExpBase Info VName
e') <- TypeSubs
f VName
v = ExpBase Info VName -> Identity (ExpBase Info VName)
forall a. a -> Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ExpBase Info VName
e'
      mapOnExp ExpBase Info VName
e' = ASTMapper Identity
-> ExpBase Info VName -> Identity (ExpBase Info VName)
forall x (m :: * -> *).
(ASTMappable x, Monad m) =>
ASTMapper m -> x -> m x
forall (m :: * -> *).
Monad m =>
ASTMapper m -> ExpBase Info VName -> m (ExpBase Info VName)
astMap ASTMapper Identity
mapper ExpBase Info VName
e'

      mapper :: ASTMapper Identity
mapper =
        ASTMapper
          { ExpBase Info VName -> Identity (ExpBase Info VName)
mapOnExp :: ExpBase Info VName -> Identity (ExpBase Info VName)
mapOnExp :: ExpBase Info VName -> Identity (ExpBase Info VName)
mapOnExp,
            mapOnName :: QualName VName -> Identity (QualName VName)
mapOnName = QualName VName -> Identity (QualName VName)
forall a. a -> Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure,
            mapOnStructType :: StructType -> Identity StructType
mapOnStructType = StructType -> Identity StructType
forall a. a -> Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StructType -> Identity StructType)
-> (StructType -> StructType) -> StructType -> Identity StructType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeSubs -> StructType -> StructType
forall a. Substitutable a => TypeSubs -> a -> a
applySubst TypeSubs
f,
            mapOnParamType :: TypeBase (ExpBase Info VName) Diet
-> Identity (TypeBase (ExpBase Info VName) Diet)
mapOnParamType = TypeBase (ExpBase Info VName) Diet
-> Identity (TypeBase (ExpBase Info VName) Diet)
forall a. a -> Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeBase (ExpBase Info VName) Diet
 -> Identity (TypeBase (ExpBase Info VName) Diet))
-> (TypeBase (ExpBase Info VName) Diet
    -> TypeBase (ExpBase Info VName) Diet)
-> TypeBase (ExpBase Info VName) Diet
-> Identity (TypeBase (ExpBase Info VName) Diet)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeSubs
-> TypeBase (ExpBase Info VName) Diet
-> TypeBase (ExpBase Info VName) Diet
forall a. Substitutable a => TypeSubs -> a -> a
applySubst TypeSubs
f,
            mapOnResRetType :: ResRetType -> Identity ResRetType
mapOnResRetType = ResRetType -> Identity ResRetType
forall a. a -> Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ResRetType -> Identity ResRetType)
-> (ResRetType -> ResRetType) -> ResRetType -> Identity ResRetType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeSubs -> ResRetType -> ResRetType
forall a. Substitutable a => TypeSubs -> a -> a
applySubst TypeSubs
f
          }

instance (Substitutable d) => Substitutable (Shape d) where
  applySubst :: TypeSubs -> Shape d -> Shape d
applySubst TypeSubs
f = (d -> d) -> Shape d -> Shape d
forall a b. (a -> b) -> Shape a -> Shape b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((d -> d) -> Shape d -> Shape d) -> (d -> d) -> Shape d -> Shape d
forall a b. (a -> b) -> a -> b
$ TypeSubs -> d -> d
forall a. Substitutable a => TypeSubs -> a -> a
applySubst TypeSubs
f

instance Substitutable (Pat StructType) where
  applySubst :: TypeSubs -> Pat StructType -> Pat StructType
applySubst TypeSubs
f = Identity (Pat StructType) -> Pat StructType
forall a. Identity a -> a
runIdentity (Identity (Pat StructType) -> Pat StructType)
-> (Pat StructType -> Identity (Pat StructType))
-> Pat StructType
-> Pat StructType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ASTMapper Identity -> Pat StructType -> Identity (Pat StructType)
forall x (m :: * -> *).
(ASTMappable x, Monad m) =>
ASTMapper m -> x -> m x
forall (m :: * -> *).
Monad m =>
ASTMapper m -> Pat StructType -> m (Pat StructType)
astMap ASTMapper Identity
mapper
    where
      mapper :: ASTMapper Identity
mapper =
        ASTMapper
          { mapOnExp :: ExpBase Info VName -> Identity (ExpBase Info VName)
mapOnExp = ExpBase Info VName -> Identity (ExpBase Info VName)
forall a. a -> Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ExpBase Info VName -> Identity (ExpBase Info VName))
-> (ExpBase Info VName -> ExpBase Info VName)
-> ExpBase Info VName
-> Identity (ExpBase Info VName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeSubs -> ExpBase Info VName -> ExpBase Info VName
forall a. Substitutable a => TypeSubs -> a -> a
applySubst TypeSubs
f,
            mapOnName :: QualName VName -> Identity (QualName VName)
mapOnName = QualName VName -> Identity (QualName VName)
forall a. a -> Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure,
            mapOnStructType :: StructType -> Identity StructType
mapOnStructType = StructType -> Identity StructType
forall a. a -> Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StructType -> Identity StructType)
-> (StructType -> StructType) -> StructType -> Identity StructType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeSubs -> StructType -> StructType
forall a. Substitutable a => TypeSubs -> a -> a
applySubst TypeSubs
f,
            mapOnParamType :: TypeBase (ExpBase Info VName) Diet
-> Identity (TypeBase (ExpBase Info VName) Diet)
mapOnParamType = TypeBase (ExpBase Info VName) Diet
-> Identity (TypeBase (ExpBase Info VName) Diet)
forall a. a -> Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeBase (ExpBase Info VName) Diet
 -> Identity (TypeBase (ExpBase Info VName) Diet))
-> (TypeBase (ExpBase Info VName) Diet
    -> TypeBase (ExpBase Info VName) Diet)
-> TypeBase (ExpBase Info VName) Diet
-> Identity (TypeBase (ExpBase Info VName) Diet)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeSubs
-> TypeBase (ExpBase Info VName) Diet
-> TypeBase (ExpBase Info VName) Diet
forall a. Substitutable a => TypeSubs -> a -> a
applySubst TypeSubs
f,
            mapOnResRetType :: ResRetType -> Identity ResRetType
mapOnResRetType = ResRetType -> Identity ResRetType
forall a. a -> Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ResRetType -> Identity ResRetType)
-> (ResRetType -> ResRetType) -> ResRetType -> Identity ResRetType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeSubs -> ResRetType -> ResRetType
forall a. Substitutable a => TypeSubs -> a -> a
applySubst TypeSubs
f
          }

instance Substitutable (Pat ParamType) where
  applySubst :: TypeSubs
-> Pat (TypeBase (ExpBase Info VName) Diet)
-> Pat (TypeBase (ExpBase Info VName) Diet)
applySubst TypeSubs
f = Identity (Pat (TypeBase (ExpBase Info VName) Diet))
-> Pat (TypeBase (ExpBase Info VName) Diet)
forall a. Identity a -> a
runIdentity (Identity (Pat (TypeBase (ExpBase Info VName) Diet))
 -> Pat (TypeBase (ExpBase Info VName) Diet))
-> (Pat (TypeBase (ExpBase Info VName) Diet)
    -> Identity (Pat (TypeBase (ExpBase Info VName) Diet)))
-> Pat (TypeBase (ExpBase Info VName) Diet)
-> Pat (TypeBase (ExpBase Info VName) Diet)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ASTMapper Identity
-> Pat (TypeBase (ExpBase Info VName) Diet)
-> Identity (Pat (TypeBase (ExpBase Info VName) Diet))
forall x (m :: * -> *).
(ASTMappable x, Monad m) =>
ASTMapper m -> x -> m x
forall (m :: * -> *).
Monad m =>
ASTMapper m
-> Pat (TypeBase (ExpBase Info VName) Diet)
-> m (Pat (TypeBase (ExpBase Info VName) Diet))
astMap ASTMapper Identity
mapper
    where
      mapper :: ASTMapper Identity
mapper =
        ASTMapper
          { mapOnExp :: ExpBase Info VName -> Identity (ExpBase Info VName)
mapOnExp = ExpBase Info VName -> Identity (ExpBase Info VName)
forall a. a -> Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ExpBase Info VName -> Identity (ExpBase Info VName))
-> (ExpBase Info VName -> ExpBase Info VName)
-> ExpBase Info VName
-> Identity (ExpBase Info VName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeSubs -> ExpBase Info VName -> ExpBase Info VName
forall a. Substitutable a => TypeSubs -> a -> a
applySubst TypeSubs
f,
            mapOnName :: QualName VName -> Identity (QualName VName)
mapOnName = QualName VName -> Identity (QualName VName)
forall a. a -> Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure,
            mapOnStructType :: StructType -> Identity StructType
mapOnStructType = StructType -> Identity StructType
forall a. a -> Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StructType -> Identity StructType)
-> (StructType -> StructType) -> StructType -> Identity StructType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeSubs -> StructType -> StructType
forall a. Substitutable a => TypeSubs -> a -> a
applySubst TypeSubs
f,
            mapOnParamType :: TypeBase (ExpBase Info VName) Diet
-> Identity (TypeBase (ExpBase Info VName) Diet)
mapOnParamType = TypeBase (ExpBase Info VName) Diet
-> Identity (TypeBase (ExpBase Info VName) Diet)
forall a. a -> Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeBase (ExpBase Info VName) Diet
 -> Identity (TypeBase (ExpBase Info VName) Diet))
-> (TypeBase (ExpBase Info VName) Diet
    -> TypeBase (ExpBase Info VName) Diet)
-> TypeBase (ExpBase Info VName) Diet
-> Identity (TypeBase (ExpBase Info VName) Diet)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeSubs
-> TypeBase (ExpBase Info VName) Diet
-> TypeBase (ExpBase Info VName) Diet
forall a. Substitutable a => TypeSubs -> a -> a
applySubst TypeSubs
f,
            mapOnResRetType :: ResRetType -> Identity ResRetType
mapOnResRetType = ResRetType -> Identity ResRetType
forall a. a -> Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ResRetType -> Identity ResRetType)
-> (ResRetType -> ResRetType) -> ResRetType -> Identity ResRetType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeSubs -> ResRetType -> ResRetType
forall a. Substitutable a => TypeSubs -> a -> a
applySubst TypeSubs
f
          }

applyType ::
  (Monoid u) =>
  [TypeParam] ->
  TypeBase Size u ->
  [StructTypeArg] ->
  TypeBase Size u
applyType :: forall u.
Monoid u =>
[TypeParam]
-> TypeBase (ExpBase Info VName) u
-> [StructTypeArg]
-> TypeBase (ExpBase Info VName) u
applyType [TypeParam]
ps TypeBase (ExpBase Info VName) u
t [StructTypeArg]
args = (VName -> Maybe (Subst (RetTypeBase (ExpBase Info VName) u)))
-> TypeBase (ExpBase Info VName) u
-> TypeBase (ExpBase Info VName) u
forall u.
Monoid u =>
(VName -> Maybe (Subst (RetTypeBase (ExpBase Info VName) u)))
-> TypeBase (ExpBase Info VName) u
-> TypeBase (ExpBase Info VName) u
substTypesAny (VName
-> Map VName (Subst (RetTypeBase (ExpBase Info VName) u))
-> Maybe (Subst (RetTypeBase (ExpBase Info VName) u))
forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` Map VName (Subst (RetTypeBase (ExpBase Info VName) u))
substs) TypeBase (ExpBase Info VName) u
t
  where
    substs :: Map VName (Subst (RetTypeBase (ExpBase Info VName) u))
substs = [(VName, Subst (RetTypeBase (ExpBase Info VName) u))]
-> Map VName (Subst (RetTypeBase (ExpBase Info VName) u))
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(VName, Subst (RetTypeBase (ExpBase Info VName) u))]
 -> Map VName (Subst (RetTypeBase (ExpBase Info VName) u)))
-> [(VName, Subst (RetTypeBase (ExpBase Info VName) u))]
-> Map VName (Subst (RetTypeBase (ExpBase Info VName) u))
forall a b. (a -> b) -> a -> b
$ (TypeParam
 -> StructTypeArg
 -> (VName, Subst (RetTypeBase (ExpBase Info VName) u)))
-> [TypeParam]
-> [StructTypeArg]
-> [(VName, Subst (RetTypeBase (ExpBase Info VName) u))]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith TypeParam
-> StructTypeArg
-> (VName, Subst (RetTypeBase (ExpBase Info VName) u))
forall {as} {a}.
(Monoid as, Eq a, IsName a) =>
TypeParamBase a
-> StructTypeArg
-> (a, Subst (RetTypeBase (ExpBase Info VName) as))
mkSubst [TypeParam]
ps [StructTypeArg]
args
    -- We are assuming everything has already been type-checked for correctness.
    mkSubst :: TypeParamBase a
-> StructTypeArg
-> (a, Subst (RetTypeBase (ExpBase Info VName) as))
mkSubst (TypeParamDim a
pv SrcLoc
_) (TypeArgDim ExpBase Info VName
e) =
      (a
pv, ExpBase Info VName -> Subst (RetTypeBase (ExpBase Info VName) as)
forall t. ExpBase Info VName -> Subst t
ExpSubst ExpBase Info VName
e)
    mkSubst (TypeParamType Liftedness
_ a
pv SrcLoc
_) (TypeArgType StructType
at) =
      (a
pv, [TypeParam]
-> RetTypeBase (ExpBase Info VName) as
-> Subst (RetTypeBase (ExpBase Info VName) as)
forall t. [TypeParam] -> t -> Subst t
Subst [] (RetTypeBase (ExpBase Info VName) as
 -> Subst (RetTypeBase (ExpBase Info VName) as))
-> RetTypeBase (ExpBase Info VName) as
-> Subst (RetTypeBase (ExpBase Info VName) as)
forall a b. (a -> b) -> a -> b
$ [VName]
-> TypeBase (ExpBase Info VName) as
-> RetTypeBase (ExpBase Info VName) as
forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [] (TypeBase (ExpBase Info VName) as
 -> RetTypeBase (ExpBase Info VName) as)
-> TypeBase (ExpBase Info VName) as
-> RetTypeBase (ExpBase Info VName) as
forall a b. (a -> b) -> a -> b
$ (NoUniqueness -> as)
-> StructType -> TypeBase (ExpBase Info VName) as
forall b c a. (b -> c) -> TypeBase a b -> TypeBase a c
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second NoUniqueness -> as
forall a. Monoid a => a
mempty StructType
at)
    mkSubst TypeParamBase a
p StructTypeArg
a =
      String -> (a, Subst (RetTypeBase (ExpBase Info VName) as))
forall a. HasCallStack => String -> a
error (String -> (a, Subst (RetTypeBase (ExpBase Info VName) as)))
-> String -> (a, Subst (RetTypeBase (ExpBase Info VName) as))
forall a b. (a -> b) -> a -> b
$ String
"applyType mkSubst: cannot substitute " String -> ShowS
forall a. [a] -> [a] -> [a]
++ StructTypeArg -> String
forall a. Pretty a => a -> String
prettyString StructTypeArg
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" for " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeParamBase a -> String
forall a. Pretty a => a -> String
prettyString TypeParamBase a
p

substTypesRet ::
  (Monoid u) =>
  (VName -> Maybe (Subst (RetTypeBase Size u))) ->
  TypeBase Size u ->
  RetTypeBase Size u
substTypesRet :: forall u.
Monoid u =>
(VName -> Maybe (Subst (RetTypeBase (ExpBase Info VName) u)))
-> TypeBase (ExpBase Info VName) u
-> RetTypeBase (ExpBase Info VName) u
substTypesRet VName -> Maybe (Subst (RetTypeBase (ExpBase Info VName) u))
lookupSubst TypeBase (ExpBase Info VName) u
ot =
  (TypeBase (ExpBase Info VName) u
 -> [VName] -> RetTypeBase (ExpBase Info VName) u)
-> (TypeBase (ExpBase Info VName) u, [VName])
-> RetTypeBase (ExpBase Info VName) u
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (([VName]
 -> TypeBase (ExpBase Info VName) u
 -> RetTypeBase (ExpBase Info VName) u)
-> TypeBase (ExpBase Info VName) u
-> [VName]
-> RetTypeBase (ExpBase Info VName) u
forall a b c. (a -> b -> c) -> b -> a -> c
flip [VName]
-> TypeBase (ExpBase Info VName) u
-> RetTypeBase (ExpBase Info VName) u
forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType) ((TypeBase (ExpBase Info VName) u, [VName])
 -> RetTypeBase (ExpBase Info VName) u)
-> (TypeBase (ExpBase Info VName) u, [VName])
-> RetTypeBase (ExpBase Info VName) u
forall a b. (a -> b) -> a -> b
$ State [VName] (TypeBase (ExpBase Info VName) u)
-> [VName] -> (TypeBase (ExpBase Info VName) u, [VName])
forall s a. State s a -> s -> (a, s)
runState (TypeBase (ExpBase Info VName) u
-> State [VName] (TypeBase (ExpBase Info VName) u)
forall as.
Monoid as =>
TypeBase (ExpBase Info VName) as
-> State [VName] (TypeBase (ExpBase Info VName) as)
onType TypeBase (ExpBase Info VName) u
ot) []
  where
    -- In case we are substituting the same RetType in multiple
    -- places, we must ensure each instance is given distinct
    -- dimensions.  E.g. substituting 'a ↦ ?[n].[n]bool' into '(a,a)'
    -- should give '?[n][m].([n]bool,[m]bool)'.
    --
    -- XXX: the size names we invent here not globally unique.  This
    -- is _probably_ not a problem, since substituting types with
    -- outermost non-null existential sizes is done only when type
    -- checking modules and monomorphising.
    freshDims :: RetTypeBase (ExpBase Info VName) as
-> f (RetTypeBase (ExpBase Info VName) as)
freshDims (RetType [] TypeBase (ExpBase Info VName) as
t) = RetTypeBase (ExpBase Info VName) as
-> f (RetTypeBase (ExpBase Info VName) as)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RetTypeBase (ExpBase Info VName) as
 -> f (RetTypeBase (ExpBase Info VName) as))
-> RetTypeBase (ExpBase Info VName) as
-> f (RetTypeBase (ExpBase Info VName) as)
forall a b. (a -> b) -> a -> b
$ [VName]
-> TypeBase (ExpBase Info VName) as
-> RetTypeBase (ExpBase Info VName) as
forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [] TypeBase (ExpBase Info VName) as
t
    freshDims (RetType [VName]
ext TypeBase (ExpBase Info VName) as
t) = do
      [VName]
seen_ext <- f [VName]
forall s (m :: * -> *). MonadState s m => m s
get
      if Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (VName -> Bool) -> [VName] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (VName -> [VName] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [VName]
seen_ext) [VName]
ext
        then RetTypeBase (ExpBase Info VName) as
-> f (RetTypeBase (ExpBase Info VName) as)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RetTypeBase (ExpBase Info VName) as
 -> f (RetTypeBase (ExpBase Info VName) as))
-> RetTypeBase (ExpBase Info VName) as
-> f (RetTypeBase (ExpBase Info VName) as)
forall a b. (a -> b) -> a -> b
$ [VName]
-> TypeBase (ExpBase Info VName) as
-> RetTypeBase (ExpBase Info VName) as
forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
ext TypeBase (ExpBase Info VName) as
t
        else do
          let start :: Int
start = [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ (VName -> Int) -> [VName] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map VName -> Int
baseTag [VName]
seen_ext
              ext' :: [VName]
ext' = (Name -> Int -> VName) -> [Name] -> [Int] -> [VName]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Name -> Int -> VName
VName ((VName -> Name) -> [VName] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map VName -> Name
baseName [VName]
ext) [Int
start Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1 ..]
              mkSubst :: VName -> Subst t
mkSubst = ExpBase Info VName -> Subst t
forall t. ExpBase Info VName -> Subst t
ExpSubst (ExpBase Info VName -> Subst t)
-> (VName -> ExpBase Info VName) -> VName -> Subst t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (QualName VName -> SrcLoc -> ExpBase Info VName)
-> SrcLoc -> QualName VName -> ExpBase Info VName
forall a b c. (a -> b -> c) -> b -> a -> c
flip QualName VName -> SrcLoc -> ExpBase Info VName
sizeFromName SrcLoc
forall a. Monoid a => a
mempty (QualName VName -> ExpBase Info VName)
-> (VName -> QualName VName) -> VName -> ExpBase Info VName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VName -> QualName VName
forall v. v -> QualName v
qualName
              extsubsts :: Map VName (Subst t)
extsubsts = [(VName, Subst t)] -> Map VName (Subst t)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(VName, Subst t)] -> Map VName (Subst t))
-> [(VName, Subst t)] -> Map VName (Subst t)
forall a b. (a -> b) -> a -> b
$ [VName] -> [Subst t] -> [(VName, Subst t)]
forall a b. [a] -> [b] -> [(a, b)]
zip [VName]
ext ([Subst t] -> [(VName, Subst t)])
-> [Subst t] -> [(VName, Subst t)]
forall a b. (a -> b) -> a -> b
$ (VName -> Subst t) -> [VName] -> [Subst t]
forall a b. (a -> b) -> [a] -> [b]
map VName -> Subst t
forall {t}. VName -> Subst t
mkSubst [VName]
ext'
              RetType [] TypeBase (ExpBase Info VName) as
t' = (VName -> Maybe (Subst (RetTypeBase (ExpBase Info VName) as)))
-> TypeBase (ExpBase Info VName) as
-> RetTypeBase (ExpBase Info VName) as
forall u.
Monoid u =>
(VName -> Maybe (Subst (RetTypeBase (ExpBase Info VName) u)))
-> TypeBase (ExpBase Info VName) u
-> RetTypeBase (ExpBase Info VName) u
substTypesRet (VName
-> Map VName (Subst (RetTypeBase (ExpBase Info VName) as))
-> Maybe (Subst (RetTypeBase (ExpBase Info VName) as))
forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` Map VName (Subst (RetTypeBase (ExpBase Info VName) as))
forall {t}. Map VName (Subst t)
extsubsts) TypeBase (ExpBase Info VName) as
t
          RetTypeBase (ExpBase Info VName) as
-> f (RetTypeBase (ExpBase Info VName) as)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RetTypeBase (ExpBase Info VName) as
 -> f (RetTypeBase (ExpBase Info VName) as))
-> RetTypeBase (ExpBase Info VName) as
-> f (RetTypeBase (ExpBase Info VName) as)
forall a b. (a -> b) -> a -> b
$ [VName]
-> TypeBase (ExpBase Info VName) as
-> RetTypeBase (ExpBase Info VName) as
forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
ext' TypeBase (ExpBase Info VName) as
t'

    onType ::
      forall as.
      (Monoid as) =>
      TypeBase Size as ->
      State [VName] (TypeBase Size as)

    onType :: forall as.
Monoid as =>
TypeBase (ExpBase Info VName) as
-> State [VName] (TypeBase (ExpBase Info VName) as)
onType (Array as
u Shape (ExpBase Info VName)
shape ScalarTypeBase (ExpBase Info VName) NoUniqueness
et) =
      as
-> Shape (ExpBase Info VName)
-> StructType
-> TypeBase (ExpBase Info VName) as
forall u dim u'.
u -> Shape dim -> TypeBase dim u' -> TypeBase dim u
arrayOfWithAliases as
u (TypeSubs
-> Shape (ExpBase Info VName) -> Shape (ExpBase Info VName)
forall a. Substitutable a => TypeSubs -> a -> a
applySubst TypeSubs
lookupSubst' Shape (ExpBase Info VName)
shape)
        (StructType -> TypeBase (ExpBase Info VName) as)
-> StateT [VName] Identity StructType
-> StateT [VName] Identity (TypeBase (ExpBase Info VName) as)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StructType -> StateT [VName] Identity StructType
forall as.
Monoid as =>
TypeBase (ExpBase Info VName) as
-> State [VName] (TypeBase (ExpBase Info VName) as)
onType (ScalarTypeBase (ExpBase Info VName) NoUniqueness -> StructType
forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar ScalarTypeBase (ExpBase Info VName) NoUniqueness
et)
    onType (Scalar (Prim PrimType
t)) = TypeBase (ExpBase Info VName) as
-> StateT [VName] Identity (TypeBase (ExpBase Info VName) as)
forall a. a -> StateT [VName] Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeBase (ExpBase Info VName) as
 -> StateT [VName] Identity (TypeBase (ExpBase Info VName) as))
-> TypeBase (ExpBase Info VName) as
-> StateT [VName] Identity (TypeBase (ExpBase Info VName) as)
forall a b. (a -> b) -> a -> b
$ ScalarTypeBase (ExpBase Info VName) as
-> TypeBase (ExpBase Info VName) as
forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar (ScalarTypeBase (ExpBase Info VName) as
 -> TypeBase (ExpBase Info VName) as)
-> ScalarTypeBase (ExpBase Info VName) as
-> TypeBase (ExpBase Info VName) as
forall a b. (a -> b) -> a -> b
$ PrimType -> ScalarTypeBase (ExpBase Info VName) as
forall dim u. PrimType -> ScalarTypeBase dim u
Prim PrimType
t
    onType (Scalar (TypeVar as
u QualName VName
v [StructTypeArg]
targs)) = do
      [StructTypeArg]
targs' <- (StructTypeArg -> StateT [VName] Identity StructTypeArg)
-> [StructTypeArg] -> StateT [VName] Identity [StructTypeArg]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM StructTypeArg -> StateT [VName] Identity StructTypeArg
forall {m :: * -> *}.
MonadState [VName] m =>
StructTypeArg -> m StructTypeArg
subsTypeArg [StructTypeArg]
targs
      case VName -> Maybe (Subst (RetTypeBase (ExpBase Info VName) u))
lookupSubst (VName -> Maybe (Subst (RetTypeBase (ExpBase Info VName) u)))
-> VName -> Maybe (Subst (RetTypeBase (ExpBase Info VName) u))
forall a b. (a -> b) -> a -> b
$ QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
v of
        Just (Subst [TypeParam]
ps RetTypeBase (ExpBase Info VName) u
rt) -> do
          RetType [VName]
ext TypeBase (ExpBase Info VName) u
t <- RetTypeBase (ExpBase Info VName) u
-> StateT [VName] Identity (RetTypeBase (ExpBase Info VName) u)
forall {f :: * -> *} {as}.
(MonadState [VName] f, Monoid as) =>
RetTypeBase (ExpBase Info VName) as
-> f (RetTypeBase (ExpBase Info VName) as)
freshDims RetTypeBase (ExpBase Info VName) u
rt
          ([VName] -> [VName]) -> StateT [VName] Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ([VName]
ext ++)
          TypeBase (ExpBase Info VName) as
-> StateT [VName] Identity (TypeBase (ExpBase Info VName) as)
forall a. a -> StateT [VName] Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeBase (ExpBase Info VName) as
 -> StateT [VName] Identity (TypeBase (ExpBase Info VName) as))
-> TypeBase (ExpBase Info VName) as
-> StateT [VName] Identity (TypeBase (ExpBase Info VName) as)
forall a b. (a -> b) -> a -> b
$ (as -> as)
-> TypeBase (ExpBase Info VName) as
-> TypeBase (ExpBase Info VName) as
forall b c a. (b -> c) -> TypeBase a b -> TypeBase a c
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (as -> as -> as
forall a. Semigroup a => a -> a -> a
<> as
u) (TypeBase (ExpBase Info VName) as
 -> TypeBase (ExpBase Info VName) as)
-> TypeBase (ExpBase Info VName) as
-> TypeBase (ExpBase Info VName) as
forall a b. (a -> b) -> a -> b
$ [TypeParam]
-> TypeBase (ExpBase Info VName) as
-> [StructTypeArg]
-> TypeBase (ExpBase Info VName) as
forall u.
Monoid u =>
[TypeParam]
-> TypeBase (ExpBase Info VName) u
-> [StructTypeArg]
-> TypeBase (ExpBase Info VName) u
applyType [TypeParam]
ps ((u -> as)
-> TypeBase (ExpBase Info VName) u
-> TypeBase (ExpBase Info VName) as
forall b c a. (b -> c) -> TypeBase a b -> TypeBase a c
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (as -> u -> as
forall a b. a -> b -> a
const as
u) TypeBase (ExpBase Info VName) u
t) [StructTypeArg]
targs'
        Maybe (Subst (RetTypeBase (ExpBase Info VName) u))
_ ->
          TypeBase (ExpBase Info VName) as
-> StateT [VName] Identity (TypeBase (ExpBase Info VName) as)
forall a. a -> StateT [VName] Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeBase (ExpBase Info VName) as
 -> StateT [VName] Identity (TypeBase (ExpBase Info VName) as))
-> TypeBase (ExpBase Info VName) as
-> StateT [VName] Identity (TypeBase (ExpBase Info VName) as)
forall a b. (a -> b) -> a -> b
$ ScalarTypeBase (ExpBase Info VName) as
-> TypeBase (ExpBase Info VName) as
forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar (ScalarTypeBase (ExpBase Info VName) as
 -> TypeBase (ExpBase Info VName) as)
-> ScalarTypeBase (ExpBase Info VName) as
-> TypeBase (ExpBase Info VName) as
forall a b. (a -> b) -> a -> b
$ as
-> QualName VName
-> [StructTypeArg]
-> ScalarTypeBase (ExpBase Info VName) as
forall dim u.
u -> QualName VName -> [TypeArg dim] -> ScalarTypeBase dim u
TypeVar as
u QualName VName
v [StructTypeArg]
targs'
    onType (Scalar (Record Map Name (TypeBase (ExpBase Info VName) as)
ts)) =
      ScalarTypeBase (ExpBase Info VName) as
-> TypeBase (ExpBase Info VName) as
forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar (ScalarTypeBase (ExpBase Info VName) as
 -> TypeBase (ExpBase Info VName) as)
-> (Map Name (TypeBase (ExpBase Info VName) as)
    -> ScalarTypeBase (ExpBase Info VName) as)
-> Map Name (TypeBase (ExpBase Info VName) as)
-> TypeBase (ExpBase Info VName) as
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Name (TypeBase (ExpBase Info VName) as)
-> ScalarTypeBase (ExpBase Info VName) as
forall dim u. Map Name (TypeBase dim u) -> ScalarTypeBase dim u
Record (Map Name (TypeBase (ExpBase Info VName) as)
 -> TypeBase (ExpBase Info VName) as)
-> StateT
     [VName] Identity (Map Name (TypeBase (ExpBase Info VName) as))
-> StateT [VName] Identity (TypeBase (ExpBase Info VName) as)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TypeBase (ExpBase Info VName) as
 -> StateT [VName] Identity (TypeBase (ExpBase Info VName) as))
-> Map Name (TypeBase (ExpBase Info VName) as)
-> StateT
     [VName] Identity (Map Name (TypeBase (ExpBase Info VName) as))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Map Name a -> f (Map Name b)
traverse TypeBase (ExpBase Info VName) as
-> StateT [VName] Identity (TypeBase (ExpBase Info VName) as)
forall as.
Monoid as =>
TypeBase (ExpBase Info VName) as
-> State [VName] (TypeBase (ExpBase Info VName) as)
onType Map Name (TypeBase (ExpBase Info VName) as)
ts
    onType (Scalar (Arrow as
u PName
v Diet
d StructType
t1 ResRetType
t2)) =
      ScalarTypeBase (ExpBase Info VName) as
-> TypeBase (ExpBase Info VName) as
forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar (ScalarTypeBase (ExpBase Info VName) as
 -> TypeBase (ExpBase Info VName) as)
-> StateT [VName] Identity (ScalarTypeBase (ExpBase Info VName) as)
-> StateT [VName] Identity (TypeBase (ExpBase Info VName) as)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (as
-> PName
-> Diet
-> StructType
-> ResRetType
-> ScalarTypeBase (ExpBase Info VName) as
forall dim u.
u
-> PName
-> Diet
-> TypeBase dim NoUniqueness
-> RetTypeBase dim Uniqueness
-> ScalarTypeBase dim u
Arrow as
u PName
v Diet
d (StructType
 -> ResRetType -> ScalarTypeBase (ExpBase Info VName) as)
-> StateT [VName] Identity StructType
-> StateT
     [VName]
     Identity
     (ResRetType -> ScalarTypeBase (ExpBase Info VName) as)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StructType -> StateT [VName] Identity StructType
forall as.
Monoid as =>
TypeBase (ExpBase Info VName) as
-> State [VName] (TypeBase (ExpBase Info VName) as)
onType StructType
t1 StateT
  [VName]
  Identity
  (ResRetType -> ScalarTypeBase (ExpBase Info VName) as)
-> StateT [VName] Identity ResRetType
-> StateT [VName] Identity (ScalarTypeBase (ExpBase Info VName) as)
forall a b.
StateT [VName] Identity (a -> b)
-> StateT [VName] Identity a -> StateT [VName] Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ResRetType -> StateT [VName] Identity ResRetType
forall {f :: * -> *} {as}.
(MonadState [VName] f, Monoid as) =>
RetTypeBase (ExpBase Info VName) as
-> f (RetTypeBase (ExpBase Info VName) as)
onRetType ResRetType
t2)
    onType (Scalar (Sum Map Name [TypeBase (ExpBase Info VName) as]
ts)) =
      ScalarTypeBase (ExpBase Info VName) as
-> TypeBase (ExpBase Info VName) as
forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar (ScalarTypeBase (ExpBase Info VName) as
 -> TypeBase (ExpBase Info VName) as)
-> (Map Name [TypeBase (ExpBase Info VName) as]
    -> ScalarTypeBase (ExpBase Info VName) as)
-> Map Name [TypeBase (ExpBase Info VName) as]
-> TypeBase (ExpBase Info VName) as
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Name [TypeBase (ExpBase Info VName) as]
-> ScalarTypeBase (ExpBase Info VName) as
forall dim u. Map Name [TypeBase dim u] -> ScalarTypeBase dim u
Sum (Map Name [TypeBase (ExpBase Info VName) as]
 -> TypeBase (ExpBase Info VName) as)
-> StateT
     [VName] Identity (Map Name [TypeBase (ExpBase Info VName) as])
-> StateT [VName] Identity (TypeBase (ExpBase Info VName) as)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([TypeBase (ExpBase Info VName) as]
 -> StateT [VName] Identity [TypeBase (ExpBase Info VName) as])
-> Map Name [TypeBase (ExpBase Info VName) as]
-> StateT
     [VName] Identity (Map Name [TypeBase (ExpBase Info VName) as])
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Map Name a -> f (Map Name b)
traverse ((TypeBase (ExpBase Info VName) as
 -> StateT [VName] Identity (TypeBase (ExpBase Info VName) as))
-> [TypeBase (ExpBase Info VName) as]
-> StateT [VName] Identity [TypeBase (ExpBase Info VName) as]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse TypeBase (ExpBase Info VName) as
-> StateT [VName] Identity (TypeBase (ExpBase Info VName) as)
forall as.
Monoid as =>
TypeBase (ExpBase Info VName) as
-> State [VName] (TypeBase (ExpBase Info VName) as)
onType) Map Name [TypeBase (ExpBase Info VName) as]
ts

    onRetType :: RetTypeBase (ExpBase Info VName) as
-> m (RetTypeBase (ExpBase Info VName) as)
onRetType (RetType [VName]
dims TypeBase (ExpBase Info VName) as
t) = do
      [VName]
ext <- m [VName]
forall s (m :: * -> *). MonadState s m => m s
get
      let (TypeBase (ExpBase Info VName) as
t', [VName]
ext') = State [VName] (TypeBase (ExpBase Info VName) as)
-> [VName] -> (TypeBase (ExpBase Info VName) as, [VName])
forall s a. State s a -> s -> (a, s)
runState (TypeBase (ExpBase Info VName) as
-> State [VName] (TypeBase (ExpBase Info VName) as)
forall as.
Monoid as =>
TypeBase (ExpBase Info VName) as
-> State [VName] (TypeBase (ExpBase Info VName) as)
onType TypeBase (ExpBase Info VName) as
t) [VName]
ext
          new_ext :: [VName]
new_ext = [VName]
ext' [VName] -> [VName] -> [VName]
forall a. Eq a => [a] -> [a] -> [a]
L.\\ [VName]
ext
      case TypeBase (ExpBase Info VName) as
t of
        Scalar Arrow {} -> do
          [VName] -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put [VName]
ext'
          RetTypeBase (ExpBase Info VName) as
-> m (RetTypeBase (ExpBase Info VName) as)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RetTypeBase (ExpBase Info VName) as
 -> m (RetTypeBase (ExpBase Info VName) as))
-> RetTypeBase (ExpBase Info VName) as
-> m (RetTypeBase (ExpBase Info VName) as)
forall a b. (a -> b) -> a -> b
$ [VName]
-> TypeBase (ExpBase Info VName) as
-> RetTypeBase (ExpBase Info VName) as
forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
dims TypeBase (ExpBase Info VName) as
t'
        TypeBase (ExpBase Info VName) as
_ ->
          RetTypeBase (ExpBase Info VName) as
-> m (RetTypeBase (ExpBase Info VName) as)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RetTypeBase (ExpBase Info VName) as
 -> m (RetTypeBase (ExpBase Info VName) as))
-> RetTypeBase (ExpBase Info VName) as
-> m (RetTypeBase (ExpBase Info VName) as)
forall a b. (a -> b) -> a -> b
$ [VName]
-> TypeBase (ExpBase Info VName) as
-> RetTypeBase (ExpBase Info VName) as
forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType ([VName]
new_ext [VName] -> [VName] -> [VName]
forall a. Semigroup a => a -> a -> a
<> [VName]
dims) TypeBase (ExpBase Info VName) as
t'

    subsTypeArg :: StructTypeArg -> m StructTypeArg
subsTypeArg (TypeArgType StructType
t) = do
      let RetType [VName]
dims StructType
t' = TypeSubs -> StructType -> StructRetType
forall u.
Monoid u =>
(VName -> Maybe (Subst (RetTypeBase (ExpBase Info VName) u)))
-> TypeBase (ExpBase Info VName) u
-> RetTypeBase (ExpBase Info VName) u
substTypesRet TypeSubs
lookupSubst' StructType
t
      ([VName] -> [VName]) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ([VName]
dims ++)
      StructTypeArg -> m StructTypeArg
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StructTypeArg -> m StructTypeArg)
-> StructTypeArg -> m StructTypeArg
forall a b. (a -> b) -> a -> b
$ StructType -> StructTypeArg
forall dim. TypeBase dim NoUniqueness -> TypeArg dim
TypeArgType StructType
t'
    subsTypeArg (TypeArgDim ExpBase Info VName
v) =
      StructTypeArg -> m StructTypeArg
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StructTypeArg -> m StructTypeArg)
-> StructTypeArg -> m StructTypeArg
forall a b. (a -> b) -> a -> b
$ ExpBase Info VName -> StructTypeArg
forall dim. dim -> TypeArg dim
TypeArgDim (ExpBase Info VName -> StructTypeArg)
-> ExpBase Info VName -> StructTypeArg
forall a b. (a -> b) -> a -> b
$ TypeSubs -> ExpBase Info VName -> ExpBase Info VName
forall a. Substitutable a => TypeSubs -> a -> a
applySubst TypeSubs
lookupSubst' ExpBase Info VName
v

    lookupSubst' :: TypeSubs
lookupSubst' = (Subst (RetTypeBase (ExpBase Info VName) u) -> Subst StructRetType)
-> Maybe (Subst (RetTypeBase (ExpBase Info VName) u))
-> Maybe (Subst StructRetType)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((RetTypeBase (ExpBase Info VName) u -> StructRetType)
-> Subst (RetTypeBase (ExpBase Info VName) u)
-> Subst StructRetType
forall a b. (a -> b) -> Subst a -> Subst b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((RetTypeBase (ExpBase Info VName) u -> StructRetType)
 -> Subst (RetTypeBase (ExpBase Info VName) u)
 -> Subst StructRetType)
-> (RetTypeBase (ExpBase Info VName) u -> StructRetType)
-> Subst (RetTypeBase (ExpBase Info VName) u)
-> Subst StructRetType
forall a b. (a -> b) -> a -> b
$ (u -> NoUniqueness)
-> RetTypeBase (ExpBase Info VName) u -> StructRetType
forall b c a. (b -> c) -> RetTypeBase a b -> RetTypeBase a c
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (NoUniqueness -> u -> NoUniqueness
forall a b. a -> b -> a
const NoUniqueness
NoUniqueness)) (Maybe (Subst (RetTypeBase (ExpBase Info VName) u))
 -> Maybe (Subst StructRetType))
-> (VName -> Maybe (Subst (RetTypeBase (ExpBase Info VName) u)))
-> TypeSubs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VName -> Maybe (Subst (RetTypeBase (ExpBase Info VName) u))
lookupSubst

-- | Perform substitutions, from type names to types, on a type. Works
-- regardless of what shape and uniqueness information is attached to the type.
substTypesAny ::
  (Monoid u) =>
  (VName -> Maybe (Subst (RetTypeBase Size u))) ->
  TypeBase Size u ->
  TypeBase Size u
substTypesAny :: forall u.
Monoid u =>
(VName -> Maybe (Subst (RetTypeBase (ExpBase Info VName) u)))
-> TypeBase (ExpBase Info VName) u
-> TypeBase (ExpBase Info VName) u
substTypesAny VName -> Maybe (Subst (RetTypeBase (ExpBase Info VName) u))
lookupSubst TypeBase (ExpBase Info VName) u
ot =
  case (VName -> Maybe (Subst (RetTypeBase (ExpBase Info VName) u)))
-> TypeBase (ExpBase Info VName) u
-> RetTypeBase (ExpBase Info VName) u
forall u.
Monoid u =>
(VName -> Maybe (Subst (RetTypeBase (ExpBase Info VName) u)))
-> TypeBase (ExpBase Info VName) u
-> RetTypeBase (ExpBase Info VName) u
substTypesRet VName -> Maybe (Subst (RetTypeBase (ExpBase Info VName) u))
lookupSubst TypeBase (ExpBase Info VName) u
ot of
    RetType [] TypeBase (ExpBase Info VName) u
ot' -> TypeBase (ExpBase Info VName) u
ot'
    RetType [VName]
dims TypeBase (ExpBase Info VName) u
ot' ->
      -- XXX HACK FIXME: turn any sizes that propagate to the top into
      -- AnySize.  This should _never_ happen during type-checking, but
      -- may happen as we substitute types during monomorphisation and
      -- defunctorisation later on. See Note [AnySize]
      let toAny :: ExpBase Info VName -> ExpBase Info VName
toAny (Var QualName VName
v Info StructType
_ SrcLoc
_) | QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
v VName -> [VName] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [VName]
dims = ExpBase Info VName
anySize
          toAny ExpBase Info VName
d = ExpBase Info VName
d
       in (ExpBase Info VName -> ExpBase Info VName)
-> TypeBase (ExpBase Info VName) u
-> TypeBase (ExpBase Info VName) u
forall a b c. (a -> b) -> TypeBase a c -> TypeBase b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ExpBase Info VName -> ExpBase Info VName
toAny TypeBase (ExpBase Info VName) u
ot'

-- Note [AnySize]
--
-- Consider a program:
--
-- module m : { type~ t } = { type~ t = ?[n].[n]bool }
-- let f (x: m.t) (y: m.t) = 0
--
-- After defunctorisation (and inlining the definitions of types), we
-- want this:
--
-- let f [n][m] (x: [n]bool) (y: [m]bool) = 0
--
-- But this means that defunctorisation would need to redo some amount
-- of size inference.  Not so complicated in the example above, but
-- what if loops and branches are involved?
--
-- So instead, what defunctorisation actually does is produce this:
--
-- let f (x: []bool) (y: []bool) = 0
--
-- I.e. we put in empty dimensions (AnySize), which are much later
-- turned into distinct sizes in Futhark.Internalise.Exps.  This will
-- result in unnecessary dynamic size checks, which will hopefully be
-- optimised away.
--
-- Important: The type checker will _never_ produce programs with
-- AnySize, but unfortunately some of the compilation steps
-- (defunctorisation, monomorphisation, defunctionalisation) will do
-- so.  Similarly, the core language is also perfectly well behaved.
--
-- Example with monomorphisation:
--
-- let f '~a (b: bool) (x: () -> a) (y: () -> a) : a = if b then x () else y ()
-- let g = f true (\() -> [1]) (\() -> [1,2])
--
-- This should produce:
--
-- let f (b: bool) (x: () -> ?[n].[n]i32) (y: () -> ?[m].[m]i32) : ?[k].[k]i32 =
--   if b then x () else y ()
--
-- Not so easy!  Again, what we actually produce is
--
-- let f (b: bool) (x: () -> []i32) (y: () -> []i32) : []i32 =
--   if b then x () else y ()