    -- | 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
          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 = 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 = [(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' = 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
          pure $ RetType dims' 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
      (ps, t, l) <- QualName VName -> m ([TypeParam], StructRetType, Liftedness)
    forall (m :: * -> *).
    MonadTypeChecker m =>
    QualName VName -> m ([TypeParam], StructRetType, Liftedness)
    lookupType QualName VName
    name
      t' <- renameRetType $ toResRet Nonunique t
      case 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
      (te', svars, ts, 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
      pure (TEParens te' loc, svars, ts, ls)
    --
    evalTypeExp df -> m (ExpBase Info VName)
    df (TETuple [TypeExp df VName]
    ts SrcLoc
    loc) = do
      (ts', svars, ts_s, 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
      pure
        ( TETuple ts' loc,
          mconcat svars,
          RetType (foldMap retDims ts_s) $ Scalar $ tupleRecord $ map retType ts_s,
          L.foldl' max Unlifted ls
        )
    --
    evalTypeExp df -> m (ExpBase Info VName)
    df t :: TypeExp df VName
    t@(TERecord [(L Name, TypeExp df VName)]
    fs SrcLoc
    loc) = do
      -- Check for duplicate field names.
      let field_names :: [L Name]
    field_names = ((L Name, TypeExp df VName) -> L Name)
    -> [(L Name, TypeExp df VName)] -> [L Name]
    forall a b. (a -> b) -> [a] -> [b]
    map (L Name, TypeExp df VName) -> L Name
    forall a b. (a, b) -> a
    fst [(L Name, TypeExp df VName)]
    fs
      Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([L Name] -> [L Name]
    forall a. Ord a => [a] -> [a]
    L.sort [L Name]
    field_names [L Name] -> [L Name] -> Bool
    forall a. Eq a => a -> a -> Bool
    == [L Name] -> [L Name]
    forall a. Ord a => [a] -> [a]
    L.sort ([L Name] -> [L Name]
    forall a. Ord a => [a] -> [a]
    nubOrd [L 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 ()
    "."

      checked <- (TypeExp df VName
     -> m (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
           Liftedness))
    -> Map (L Name) (TypeExp df VName)
    -> m (Map
            (L 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 (L Name) a -> f (Map (L 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 (L Name) (TypeExp df VName)
     -> m (Map
             (L Name)
             (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
              Liftedness)))
    -> Map (L Name) (TypeExp df VName)
    -> m (Map
            (L Name)
            (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
             Liftedness))
    forall a b. (a -> b) -> a -> b
    $ [(L Name, TypeExp df VName)] -> Map (L Name) (TypeExp df VName)
    forall k a. Ord k => [(k, a)] -> Map k a
    M.fromList [(L Name, TypeExp df VName)]
    fs
      let fs' = ((TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
     -> TypeExp (ExpBase Info VName) VName)
    -> Map
         (L Name)
         (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
          Liftedness)
    -> Map (L Name) (TypeExp (ExpBase Info VName) VName)
    forall a b. (a -> b) -> Map (L Name) a -> Map (L 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
      (L Name)
      (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
       Liftedness)
    checked
          fs_svars = ((TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
     -> [VName])
    -> Map
         (L Name)
         (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
          Liftedness)
    -> [VName]
    forall m a. Monoid m => (a -> m) -> Map (L 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
      (L Name)
      (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
       Liftedness)
    checked
          ts_s = ((TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
     -> ResRetType)
    -> Map
         (L Name)
         (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
          Liftedness)
    -> Map (L Name) ResRetType
    forall a b. (a -> b) -> Map (L Name) a -> Map (L 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
      (L Name)
      (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
       Liftedness)
    checked
          ls = ((TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
      Liftedness)
     -> Liftedness)
    -> Map
         (L Name)
         (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
          Liftedness)
    -> Map (L Name) Liftedness
    forall a b. (a -> b) -> Map (L Name) a -> Map (L 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
      (L Name)
      (TypeExp (ExpBase Info VName) VName, [VName], ResRetType,
       Liftedness)
    checked
      pure
        ( TERecord (M.toList fs') loc,
          fs_svars,
          RetType (foldMap retDims ts_s) . Scalar . Record $
            M.mapKeys unLoc $
              M.map retType ts_s,
          L.foldl' max Unlifted ls
        )
    --
    evalTypeExp df -> m (ExpBase Info VName)
    df (TEArray SizeExp df
    d TypeExp df VName
    t SrcLoc
    loc) = do
      (d_svars, d', d'') <- SizeExp df
    -> m ([VName], SizeExp (ExpBase Info VName), ExpBase Info VName)
    checkSizeExp SizeExp df
    d
      (t', svars, RetType dims st, l) <- evalTypeExp df t
      case (l, arrayOfWithAliases Nonunique (Shape [d'']) 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
          dv <- Name -> m VName
    forall (m :: * -> *). MonadTypeChecker m => Name -> m VName
    newTypeName Name
    "d"
          pure ([dv], SizeExpAny dloc, sizeFromName (qualName dv) dloc)
        checkSizeExp (SizeExp df
    e SrcLoc
    dloc) = do
          e' <- df -> m (ExpBase Info VName)
    df df
    e
          pure ([], SizeExp e' dloc, e')
    --
    evalTypeExp df -> m (ExpBase Info VName)
    df (TEUnique TypeExp df VName
    t SrcLoc
    loc) = do
      (t', svars, RetType dims st, 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
      unless (mayContainArray st) $
        warn loc $
          "Declaring" <+> dquotes (pretty st) <+> "as unique has no effect."
      pure (TEUnique t' loc, svars, RetType dims $ st `setUniqueness` Unique, 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
      (t1', svars1, RetType dims1 st1, _) <- (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
      bindVal v (BoundV [] $ toStruct st1) $ do
        (t2', svars2, RetType dims2 st2, _) <- evalTypeExp df t2
        pure
          ( TEArrow (Just v) t1' t2' loc,
            svars1 ++ dims1 ++ svars2,
            RetType [] $ Scalar $ Arrow Nonunique (Named v) (diet $ resToParam st1) (toStruct st1) (RetType dims2 st2),
            Lifted
          )
    --
    evalTypeExp df -> m (ExpBase Info VName)
    df (TEArrow Maybe VName
    Nothing TypeExp df VName
    t1 TypeExp df VName
    t2 SrcLoc
    loc) = do
      (t1', svars1, RetType dims1 st1, _) <- (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
      (t2', svars2, RetType dims2 st2, _) <- evalTypeExp df t2
      pure
        ( TEArrow Nothing t1' t2' loc,
          svars1 ++ dims1 ++ svars2,
          RetType [] . Scalar $
            Arrow Nonunique Unnamed (diet $ resToParam st1) (toStruct st1) $
              RetType dims2 st2,
          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
        (t', svars, RetType t_dims st, 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 (witnessed, _) = determineSizeWitnesses $ toStruct st
        case L.find (`S.notMember` witnessed) 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."

      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' = (([(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 = (([(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 = (([(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 = (([(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
      pure
        ( TESum (M.toList cs') loc,
          cs_svars,
          RetType (foldMap (foldMap retDims) ts_s) $
            Scalar $
              Sum $
                M.map (map retType) ts_s,
          L.foldl' max Unlifted ls
        )
    evalTypeExp df -> m (ExpBase Info VName)
    df ote :: TypeExp df VName
    ote@TEApply {} = do
      (tname, tname_loc, 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
      (ps, tname_t, l) <- lookupType tname
      RetType t_dims t <- renameRetType $ toResRet Nonunique tname_t
      if length ps /= length targs
        then
          typeError tloc mempty $
            "Type constructor"
              <+> dquotes (pretty tname)
              <+> "requires"
              <+> pretty (length ps)
              <+> "arguments, but provided"
              <+> pretty (length targs)
              <> "."
        else do
          (targs', dims, substs, targs_ls) <-
            L.unzip4 <$> zipWithM checkArgApply ps targs
          pure
            ( 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) (TEVar tname tname_loc) targs',
              [],
              RetType (t_dims ++ mconcat dims) $
                applySubst (`M.lookup` mconcat substs) t,
              -- XXX: this is an overapproximation of the liftedness in case one of
              -- these type parameters is a phantom type.
              maximum $ l : targs_ls
            )
      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
          (op', loc, args) <- TypeExp d vn -> f (QualName vn, SrcLoc, [TypeArgExp d vn])
    rootAndArgs TypeExp d vn
    op
          pure (op', loc, args ++ [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
          e' <- df -> m (ExpBase Info VName)
    df df
    e
          pure
            ( TypeArgExpSize (SizeExp e' dloc),
              [],
              ExpSubst e'
            )
        checkSizeExp (SizeExpAny SrcLoc
    loc) = do
          d <- Name -> m VName
    forall (m :: * -> *). MonadTypeChecker m => Name -> m VName
    newTypeName Name
    "d"
          pure
            ( TypeArgExpSize (SizeExpAny loc),
              [d],
              ExpSubst $ sizeFromName (qualName d) loc
            )

        checkArgApply :: TypeParamBase k
    -> TypeArgExp df VName
    -> m (TypeArgExp (ExpBase Info VName) VName, [VName],
          Map k (Subst StructRetType), Liftedness)
    checkArgApply (TypeParamDim k
    pv SrcLoc
    _) (TypeArgExpSize SizeExp df
    d) = do
          (d', svars, 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
          pure (d', svars, M.singleton pv subst, Unlifted)
        checkArgApply (TypeParamType Liftedness
    _ k
    pv SrcLoc
    _) (TypeArgExpType TypeExp df VName
    te) = do
          (te', svars, RetType dims st, te_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
    te
          pure
            ( TypeArgExpType te',
              svars ++ dims,
              M.singleton pv $ Subst [] $ RetType [] $ toStruct st,
              te_l
            )
        checkArgApply TypeParamBase k
    p TypeArgExp df VName
    a =
          SrcLoc
    -> Notes
    -> Doc ()
    -> m (TypeArgExp (ExpBase Info VName) VName, [VName],
          Map k (Subst StructRetType), 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 (TypeArgExp (ExpBase Info VName) VName, [VName],
           Map k (Subst StructRetType), Liftedness))
    -> Doc ()
    -> m (TypeArgExp (ExpBase Info VName) VName, [VName],
          Map k (Subst StructRetType), Liftedness)
    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, 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
          seen_ext <- f [VName]
    forall s (m :: * -> *). MonadState s m => m s
    get
          if not $ any (`elem` seen_ext) ext
            then pure $ RetType ext t
            else do
              let 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' = (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 = 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 = [(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 [] t' = substTypesRet (`M.lookup` extsubsts) t
              pure $ RetType ext' 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
          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 lookupSubst $ qualLeaf v of
            Just (Subst [TypeParam]
    ps RetTypeBase (ExpBase Info VName) u
    rt) -> do
              RetType ext 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
              modify (ext ++)
              pure $ second (<> u) $ applyType ps (second (const u) t) 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
          ext <- m [VName]
    forall s (m :: * -> *). MonadState s m => m s
    get
          let (t', ext') = runState (onType t) ext
              new_ext = [VName]
    ext' [VName] -> [VName] -> [VName]
    forall a. Eq a => [a] -> [a] -> [a]
    L.\\ [VName]
    ext
          case 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 [VName] -> [VName] -> [VName]
    forall a. [a] -> [a] -> [a]
    ++)
          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 ()