    {-# OPTIONS_GHC -Wunused-imports #-}

    {-|

    This module implements the type checking part of generalisable variables. When we get here we have
    a type checking problem for a type (or telescope) containing a known set of generalisable variables
    and we need to produce a well typed type (or telescope) with the correct generalisations. For instance,
    given

    @
    variable
      A  : Set
      n  : Nat
      xs : Vec A n

    foo : SomeType xs
    @

    generalisation should produce @{A : Set} {n : Nat} {xs : Vec A n} → SomeType xs@ for the type of
    @foo@.

    The functions `generalizeType` and `generalizeTelescope` don't have access to the abstract syntax to
    be type checked (@SomeType xs@ in the example). Instead they are provided a type checking action
    that delivers a `Type` or a `Telescope`. The challenge is setting up a context in which @SomeType
    xs@ can be type checked successfully by this action, without knowing what the telescope of
    generalised variables will be. Once we have computed this telescope the result needs to be
    transformed into a well typed type abstracted over it.

    __At no point are we allowed to cheat!__ Any transformation between well typed terms needs to be done
    by well typed substitutions.

    The key idea is to run the type checking action in the context of a single variable of an unknown
    type. Once we know what variables to generalise over this type is instantiated to a fresh record
    type with a field for each generalised variable. Turning the result of action into something valid
    in the context of the generalised variables is then a simple substitution unpacking the record
    variable.

    In more detail, generalisation proceeds as follows:

    - Add a variable @genTel@ of an unknown type to the context (`withGenRecVar`).

    @
      (genTel : _GenTel)
    @

    - Create metavariables for the generalisable variables appearing in the problem and their
      dependencies (`createGenValues`). In the example this would be

    @
      (genTel : _GenTel) ⊢
        _A  : Set
        _n  : Nat
        _xs : Vec _A _n
    @

    - Run the type checking action (`createMetasAndTypeCheck`), binding the mentioned generalisable
      variables to the corresponding newly created metavariables. This binding is stored in
      `eGeneralizedVars` and picked up in `Agda.TypeChecking.Rules.Application.inferDef`

    @
      (genTel : _GenTel) ⊢ SomeType (_xs genTel)
    @

    - Compute the telescope of generalised variables (`computeGeneralization`). This is done by taking
      the unconstrained metavariables created by `createGenValues` or created during the type checking
      action and sorting them into a well formed telescope.

    @
      {A : Set} {n : Nat} {xs : Vec A n}
    @

    - Create a record type @GeneralizeTel@ whose fields are the generalised variables and instantiate
      the type of @genTel@ to it (`createGenRecordType`).

    @
      record GeneralizeTel : Set₁ where
        constructor mkGeneralizeTel
        field
          A  : Set
          n  : Nat
          xs : Vec A n
    @

    - Solve the metavariables with their corresponding projections from @genTel@.

    @
      _A  := λ genTel → genTel .A
      _n  := λ genTel → genTel .n
      _xs := λ genTel → genTel .xs
    @

    - Build the unpacking substitution (`unpackSub`) that maps terms in @(genTel : GeneralizeTel)@ to
      terms in the context of the generalised variables by substituting a record value for @genTel@.

    @
      {A : Set} {n : Nat} {xs : Vec A n} ⊢ [mkGeneralizeTel A n xs / genTel] : (genTel : GeneralizeTel)
    @

    - Build the final result by applying the unpacking substitution to the result of the type checking
      action and abstracting over the generalised telescope.

    @
      {A : Set} {n : Nat} {xs : Vec A n} → SomeType (_xs (mkGeneralizeTel A n xs)) ==
      {A : Set} {n : Nat} {xs : Vec A n} → SomeType xs
    @

    - In case of `generalizeType` return the resulting pi type.
    - In case of `generalizeTelescope` enter the resulting context, applying the unpacking substitution
      to let bindings (TODO #6916: and also module applications!) created in the telescope, and call the
      continuation.

    -}

    module Agda.TypeChecking.Generalize
      ( generalizeType
      , generalizeType'
      , generalizeTelescope ) where

    import Prelude hiding (null)

    import Control.Monad.Except ( MonadError(..) )

    import Data.Bifunctor (first)
    import qualified Data.IntSet as IntSet
    import Data.Set (Set)
    import qualified Data.Set as Set
    import Data.Map (Map)
    import qualified Data.Map as Map
    import qualified Data.Map.Strict as MapS
    import Data.List (partition, sortBy)
    import Data.Monoid

    import Agda.Interaction.Options.Base

    import Agda.Syntax.Common
    import Agda.Syntax.Common.Pretty (prettyShow, singPlural)
    import Agda.Syntax.Concrete.Name (LensInScope(..))
    import Agda.Syntax.Position
    import Agda.Syntax.Info          (MetaNameSuggestion)
    import Agda.Syntax.Internal
    import Agda.Syntax.Internal.Generic
    import Agda.Syntax.Internal.MetaVars
    import Agda.Syntax.Scope.Monad (bindVariable, outsideLocalVars)
    import Agda.Syntax.Scope.Base (BindingSource(..))
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Constraints
    import Agda.TypeChecking.Conversion
    import Agda.TypeChecking.Free
    import Agda.TypeChecking.InstanceArguments (postponeInstanceConstraints)
    import Agda.TypeChecking.MetaVars
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Telescope
    import Agda.TypeChecking.Warnings

    import Agda.Benchmarking (Phase(Typing, Generalize))
    import Agda.Utils.Benchmark
    import qualified Agda.Utils.BiMap as BiMap
    import Agda.Utils.Function
    import Agda.Utils.Functor
    import Agda.Utils.Impossible
    import Agda.Utils.Lens
    import Agda.Utils.List (downFrom, hasElem)
    import qualified Agda.Utils.List1 as List1
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Null
    import qualified Agda.Utils.Set1 as Set1
    import Agda.Utils.Size
    import Agda.Utils.Permutation

    -- | Generalize a telescope over a set of generalizable variables.
    generalizeTelescope :: Map QName Name -> (forall a. (Telescope -> TCM a) -> TCM a) -> ([Maybe Name] -> Telescope -> TCM a) -> TCM a
    generalizeTelescope :: forall a.
    Map QName Name
    -> (forall a. (Telescope -> TCM a) -> TCM a)
    -> ([Maybe Name] -> Telescope -> TCM a)
    -> TCM a
    generalizeTelescope Map QName Name
    vars forall a. (Telescope -> TCM a) -> TCM a
    typecheckAction [Maybe Name] -> Telescope -> TCM a
    ret | Map QName Name -> Bool
    forall k a. Map k a -> Bool
    Map.null Map QName Name
    vars = (Telescope -> TCM a) -> TCM a
    forall a. (Telescope -> TCM a) -> TCM a
    typecheckAction ([Maybe Name] -> Telescope -> TCM a
    ret [])
    generalizeTelescope Map QName Name
    vars forall a. (Telescope -> TCM a) -> TCM a
    typecheckAction [Maybe Name] -> Telescope -> TCM a
    ret = Account (BenchPhase (TCMT IO)) -> TCM a -> TCM a
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    billTo [BenchPhase (TCMT IO)
    Phase
    Typing, BenchPhase (TCMT IO)
    Phase
    Generalize] (TCM a -> TCM a) -> TCM a -> TCM a
    forall a b. (a -> b) -> a -> b
    $ (Type -> TCM a) -> TCM a
    forall a. (Type -> TCM a) -> TCM a
    withGenRecVar ((Type -> TCM a) -> TCM a) -> (Type -> TCM a) -> TCM a
    forall a b. (a -> b) -> a -> b
    $ \ Type
    genRecMeta -> do
      let s :: Set QName
    s = Map QName Name -> Set QName
    forall k a. Map k a -> Set k
    Map.keysSet Map QName Name
    vars
      ((cxtNames, tel, letbinds), namedMetas, allmetas) <-
        Set QName
    -> TCM ([Name], Telescope, [(Name, LetBinding)])
    -> TCM
         (([Name], Telescope, [(Name, LetBinding)]), Map MetaId QName,
          LocalMetaStores)
    forall a.
    Set QName -> TCM a -> TCM (a, Map MetaId QName, LocalMetaStores)
    createMetasAndTypeCheck Set QName
    s (TCM ([Name], Telescope, [(Name, LetBinding)])
     -> TCM
          (([Name], Telescope, [(Name, LetBinding)]), Map MetaId QName,
           LocalMetaStores))
    -> TCM ([Name], Telescope, [(Name, LetBinding)])
    -> TCM
         (([Name], Telescope, [(Name, LetBinding)]), Map MetaId QName,
          LocalMetaStores)
    forall a b. (a -> b) -> a -> b
    $ (Telescope -> TCM ([Name], Telescope, [(Name, LetBinding)]))
    -> TCM ([Name], Telescope, [(Name, LetBinding)])
    forall a. (Telescope -> TCM a) -> TCM a
    typecheckAction ((Telescope -> TCM ([Name], Telescope, [(Name, LetBinding)]))
     -> TCM ([Name], Telescope, [(Name, LetBinding)]))
    -> (Telescope -> TCM ([Name], Telescope, [(Name, LetBinding)]))
    -> TCM ([Name], Telescope, [(Name, LetBinding)])
    forall a b. (a -> b) -> a -> b
    $ \ Telescope
    tel -> do
          xs <- Int -> [Name] -> [Name]
    forall a. Int -> [a] -> [a]
    take (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel) ([Name] -> [Name]) -> TCMT IO [Name] -> TCMT IO [Name]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO [Name]
    forall (m :: * -> *). MonadTCEnv m => m [Name]
    getContextNames'
          lbs <- getLetBindings -- This gives let-bindings valid in the current context
          return (xs, tel, lbs)

      reportSDoc "tc.generalize.metas" 60 $ vcat
        [ "open metas =" <+> (text . show . fmap ((miNameSuggestion &&& miGeneralizable) . mvInfo)) (openMetas $ allmetas)
        ]
      -- Translate the QName to the corresponding bound variable
      (genTel, genTelNames, sub) <- computeGeneralization genRecMeta namedMetas allmetas

      let boundVar QName
    q = Name -> Maybe Name -> Name
    forall a. a -> Maybe a -> a
    fromMaybe Name
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Name -> Name) -> Maybe Name -> Name
    forall a b. (a -> b) -> a -> b
    $ QName -> Map QName Name -> Maybe Name
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup QName
    q Map QName Name
    vars
          genTelVars = ((Maybe QName -> Maybe Name) -> [Maybe QName] -> [Maybe Name]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Maybe QName -> Maybe Name) -> [Maybe QName] -> [Maybe Name])
    -> ((QName -> Name) -> Maybe QName -> Maybe Name)
    -> (QName -> Name)
    -> [Maybe QName]
    -> [Maybe Name]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (QName -> Name) -> Maybe QName -> Maybe Name
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap) QName -> Name
    boundVar [Maybe QName]
    genTelNames

      tel' <- applySubst sub <$> instantiateFull tel

      -- This is not so nice. When changing the context from Γ (r : R) to Γ Δ we need to do this at the
      -- level of contexts (as a Context -> Context function), so we repeat the name logic here. Take
      -- care to preserve the name of named generalized variables.
      let setName b
    name f (p a c)
    d = (a -> b) -> p a c -> p b c
    forall a b c. (a -> b) -> p a c -> p b c
    forall (p :: * -> * -> *) a b c.
    Bifunctor p =>
    (a -> b) -> p a c -> p b c
    first (b -> a -> b
    forall a b. a -> b -> a
    const b
    name) (p a c -> p b c) -> f (p a c) -> f (p b c)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> f (p a c)
    d
          cxtEntry (Maybe Name
    mname, Dom' Term (a, Type)
    dom) = do
              let s :: a
    s = (a, Type) -> a
    forall a b. (a, b) -> a
    fst ((a, Type) -> a) -> (a, Type) -> a
    forall a b. (a -> b) -> a -> b
    $ Dom' Term (a, Type) -> (a, Type)
    forall t e. Dom' t e -> e
    unDom Dom' Term (a, Type)
    dom
              name <- m Name -> (Name -> m Name) -> Maybe Name -> m Name
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe (Name -> Name
    forall a. LensInScope a => a -> a
    setNotInScope (Name -> Name) -> m Name -> m Name
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> m Name
    forall a (m :: * -> *).
    (FreshName a, MonadFresh NameId m) =>
    a -> m Name
    forall (m :: * -> *). MonadFresh NameId m => a -> m Name
    freshName_ a
    s) Name -> m Name
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Name
    mname
              return $ CtxVar name (snd <$> dom)
          dropCxt Impossible
    err = Substitution -> (Context -> Context) -> m a -> m a
    forall a. Substitution -> (Context -> Context) -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Substitution -> (Context -> Context) -> m a -> m a
    updateContext (Impossible -> Int -> Substitution
    forall a. Impossible -> Int -> Substitution' a
    strengthenS Impossible
    err Int
    1) (Int -> Context -> Context
    forall a. Int -> [a] -> [a]
    drop Int
    1)
      genTelCxt <- dropCxt __IMPOSSIBLE__ $ mapM cxtEntry $ reverse $ zip genTelVars $ telToList genTel

      -- For the explicit module telescope we get the names from the typecheck
      -- action.
      let newTelCxt :: [ContextEntry]
          newTelCxt = (Name -> Dom Type -> ContextEntry)
    -> [Name] -> [Dom Type] -> Context
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Name -> Dom Type -> ContextEntry
    CtxVar [Name]
    cxtNames ([Dom Type] -> Context) -> [Dom Type] -> Context
    forall a b. (a -> b) -> a -> b
    $ [Dom Type] -> [Dom Type]
    forall a. [a] -> [a]
    reverse ([Dom Type] -> [Dom Type]) -> [Dom Type] -> [Dom Type]
    forall a b. (a -> b) -> a -> b
    $ (Dom (String, Type) -> Dom Type)
    -> [Dom (String, Type)] -> [Dom Type]
    forall a b. (a -> b) -> [a] -> [b]
    map (((String, Type) -> Type) -> Dom (String, Type) -> Dom Type
    forall a b. (a -> b) -> Dom' Term a -> Dom' Term b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (String, Type) -> Type
    forall a b. (a, b) -> b
    snd) ([Dom (String, Type)] -> [Dom Type])
    -> [Dom (String, Type)] -> [Dom Type]
    forall a b. (a -> b) -> a -> b
    $ Telescope -> [Dom (String, Type)]
    forall t. Tele (Dom t) -> [Dom (String, t)]
    telToList Telescope
    tel'

      -- We are in context Γ (r : R) and should call the continuation in context Γ Δ Θρ passing it Δ Θρ
      -- We have
      --   Γ (r : R) ⊢ Θ            Θ = tel
      --   Γ ⊢ Δ                    Δ = genTel
      --   Γ Δ ⊢ ρ : Γ (r : R)      ρ = sub
      --   Γ ⊢ Δ Θρ                 Θρ = tel'
      -- And we shouldn't forget about the let-bindings (#3470)
      --   Γ (r : R) Θ ⊢ letbinds
      --   Γ Δ Θρ      ⊢ letbinds' = letbinds(lift |Θ| ρ)
      -- And modules created in the telescope (#6916)
      --   TODO
      letbinds' <- applySubst (liftS (size tel) sub) <$> instantiateFull letbinds
      let addLet (Name
    x, LetBinding Origin
    o Term
    v Dom Type
    dom) = Origin -> Name -> Term -> Dom Type -> m a -> m a
    forall a. Origin -> Name -> Term -> Dom Type -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Origin -> Name -> Term -> Dom Type -> m a -> m a
    addLetBinding' Origin
    o Name
    x Term
    v Dom Type
    dom

      updateContext sub ((genTelCxt ++) . drop 1) $
        updateContext (raiseS (size tel')) (newTelCxt ++) $
          foldr addLet (ret genTelVars $ abstract genTel tel') letbinds'

    -- | Generalize a type over a set of (used) generalizable variables.
    generalizeType :: Set QName -> TCM Type -> TCM ([Maybe QName], Type)
    generalizeType :: Set QName -> TCM Type -> TCM ([Maybe QName], Type)
    generalizeType Set QName
    s TCM Type
    typecheckAction = do
      (ns, t, _) <- Set QName -> TCM (Type, ()) -> TCM ([Maybe QName], Type, ())
    forall a.
    Set QName -> TCM (Type, a) -> TCM ([Maybe QName], Type, a)
    generalizeType' Set QName
    s (TCM (Type, ()) -> TCM ([Maybe QName], Type, ()))
    -> TCM (Type, ()) -> TCM ([Maybe QName], Type, ())
    forall a b. (a -> b) -> a -> b
    $ (,()) (Type -> (Type, ())) -> TCM Type -> TCM (Type, ())
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCM Type
    typecheckAction
      return (ns, t)

    -- | Allow returning additional information from the type checking action.
    generalizeType' :: Set QName -> TCM (Type, a) -> TCM ([Maybe QName], Type, a)
    generalizeType' :: forall a.
    Set QName -> TCM (Type, a) -> TCM ([Maybe QName], Type, a)
    generalizeType' Set QName
    s TCM (Type, a)
    typecheckAction = Account (BenchPhase (TCMT IO))
    -> TCMT IO ([Maybe QName], Type, a)
    -> TCMT IO ([Maybe QName], Type, a)
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    billTo [BenchPhase (TCMT IO)
    Phase
    Typing, BenchPhase (TCMT IO)
    Phase
    Generalize] (TCMT IO ([Maybe QName], Type, a)
     -> TCMT IO ([Maybe QName], Type, a))
    -> TCMT IO ([Maybe QName], Type, a)
    -> TCMT IO ([Maybe QName], Type, a)
    forall a b. (a -> b) -> a -> b
    $ (Type -> TCMT IO ([Maybe QName], Type, a))
    -> TCMT IO ([Maybe QName], Type, a)
    forall a. (Type -> TCM a) -> TCM a
    withGenRecVar ((Type -> TCMT IO ([Maybe QName], Type, a))
     -> TCMT IO ([Maybe QName], Type, a))
    -> (Type -> TCMT IO ([Maybe QName], Type, a))
    -> TCMT IO ([Maybe QName], Type, a)
    forall a b. (a -> b) -> a -> b
    $ \ Type
    genRecMeta -> do

      ((t, userdata), namedMetas, allmetas) <- Set QName
    -> TCM (Type, a)
    -> TCM ((Type, a), Map MetaId QName, LocalMetaStores)
    forall a.
    Set QName -> TCM a -> TCM (a, Map MetaId QName, LocalMetaStores)
    createMetasAndTypeCheck Set QName
    s TCM (Type, a)
    typecheckAction

      reportSDoc "tc.generalize.metas" 60 $ vcat
        [ "open metas =" <+> (text . show . fmap ((miNameSuggestion &&& miGeneralizable) . mvInfo)) (openMetas $ allmetas)
        ]

      (genTel, genTelNames, sub) <- computeGeneralization genRecMeta namedMetas allmetas

      t' <- abstract genTel . applySubst sub <$> instantiateFull t

      reportSDoc "tc.generalize" 40 $ vcat
        [ "generalized"
        , nest 2 $ "t =" <+> escapeContext impossible 1 (prettyTCM t') ]

      return (genTelNames, t', userdata)

    -- | Create metas for the generalizable variables and run the type check action.
    createMetasAndTypeCheck ::
      Set QName -> TCM a -> TCM (a, Map MetaId QName, LocalMetaStores)
    createMetasAndTypeCheck :: forall a.
    Set QName -> TCM a -> TCM (a, Map MetaId QName, LocalMetaStores)
    createMetasAndTypeCheck Set QName
    s TCM a
    typecheckAction = do
      ((namedMetas, x), allmetas) <- TCMT IO (Map MetaId QName, a)
    -> TCMT IO ((Map MetaId QName, a), LocalMetaStores)
    forall (m :: * -> *) a.
    ReadTCState m =>
    m a -> m (a, LocalMetaStores)
    metasCreatedBy (TCMT IO (Map MetaId QName, a)
     -> TCMT IO ((Map MetaId QName, a), LocalMetaStores))
    -> TCMT IO (Map MetaId QName, a)
    -> TCMT IO ((Map MetaId QName, a), LocalMetaStores)
    forall a b. (a -> b) -> a -> b
    $ do
        (metamap, genvals) <- Set QName -> TCM (Map MetaId QName, Map QName GeneralizedValue)
    createGenValues Set QName
    s
        x <- locallyTC eGeneralizedVars (const genvals) typecheckAction
        return (metamap, x)
      return (x, namedMetas, allmetas)

    -- | Add a placeholder variable that will be substituted with a record value packing up all the
    --   generalized variables.
    withGenRecVar :: (Type -> TCM a) -> TCM a
    withGenRecVar :: forall a. (Type -> TCM a) -> TCM a
    withGenRecVar Type -> TCM a
    ret = do
      -- Create a meta type (in Set₀) for the telescope record. It won't
      -- necessarily fit in Set₀, but since it's only used locally the sort
      -- shouldn't matter. Another option would be to put it in Setω, which is a
      -- bit more honest, but this leads to performance problems (see #3306).
      genRecMeta <- Sort -> TCM Type
    newTypeMeta (Integer -> Sort
    mkType Integer
    0)
      addContext (defaultDom ("genTel" :: String, genRecMeta)) $ ret genRecMeta

    -- | Compute the generalized telescope from metas created when checking the *thing* (type or telescope) to be
    --   generalized. Called in the context extended with the telescope record variable (whose type is
    --   the first argument). Returns the telescope of generalized variables and a substitution from
    --   this telescope to the current context.
    computeGeneralization
      :: Type
           -- ^ The metavariable to be instantiated with record type containing
           --   as fields the variables generalized in the *thing*.
      -> Map MetaId name
           -- ^ Metas created from an occurrence of a @variable@. (The original free variables.)
           --   E.g. if you have
           --   @
           --     variable  l : Level; A : Set l
           --     postulate f : A → A
           --   @
           --   then @A@ would be in this @Map@, but not @l@.
      -> LocalMetaStores
           -- ^ The metas created when type-checking the *thing*.
      -> TCM (Telescope, [Maybe name], Substitution)
           -- ^ The telescope together with binder name (left-to-right order),
           --   and substitution from this telescope to the current context.
    computeGeneralization :: forall name.
    Type
    -> Map MetaId name
    -> LocalMetaStores
    -> TCM (Telescope, [Maybe name], Substitution)
    computeGeneralization Type
    genRecMeta Map MetaId name
    nameMap LocalMetaStores
    allmetas = TCM (Telescope, [Maybe name], Substitution)
    -> TCM (Telescope, [Maybe name], Substitution)
    forall a. TCM a -> TCM a
    postponeInstanceConstraints (TCM (Telescope, [Maybe name], Substitution)
     -> TCM (Telescope, [Maybe name], Substitution))
    -> TCM (Telescope, [Maybe name], Substitution)
    -> TCM (Telescope, [Maybe name], Substitution)
    forall a b. (a -> b) -> a -> b
    $ do

      String -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.generalize" Int
    10 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "computing generalization for type" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    genRecMeta

      -- Pair metas with their metaInfo
      let mvs :: [(MetaId, MetaVariable)]
          mvs :: [(MetaId, MetaVariable)]
    mvs = Map MetaId MetaVariable -> [(MetaId, MetaVariable)]
    forall k a. Map k a -> [(k, a)]
    MapS.assocs (LocalMetaStores -> Map MetaId MetaVariable
    openMetas LocalMetaStores
    allmetas) [(MetaId, MetaVariable)]
    -> [(MetaId, MetaVariable)] -> [(MetaId, MetaVariable)]
    forall a. [a] -> [a] -> [a]
    ++
                Map MetaId MetaVariable -> [(MetaId, MetaVariable)]
    forall k a. Map k a -> [(k, a)]
    MapS.assocs (LocalMetaStores -> Map MetaId MetaVariable
    solvedMetas LocalMetaStores
    allmetas)

      -- Issue 4727: filter out metavariables that were created before the
      -- current checkpoint, since they are too old to be generalized.
      -- TODO: make metasCreatedBy smarter so it doesn't see pruned
      -- versions of old metas as new metas.
      cp <- Lens' TCEnv CheckpointId -> TCMT IO CheckpointId
    forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
    viewTC (CheckpointId -> f CheckpointId) -> TCEnv -> f TCEnv
    Lens' TCEnv CheckpointId
    eCurrentCheckpoint
      let isFreshMeta :: MonadReduce m => MetaVariable -> m Bool
          isFreshMeta MetaVariable
    mv = MetaVariable -> (Range -> m Bool) -> m Bool
    forall (m :: * -> *) c a b.
    (MonadTCEnv m, ReadTCState m, LensClosure c a) =>
    c -> (a -> m b) -> m b
    enterClosure MetaVariable
    mv ((Range -> m Bool) -> m Bool) -> (Range -> m Bool) -> m Bool
    forall a b. (a -> b) -> a -> b
    $ \ Range
    _ -> Maybe Substitution -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe Substitution -> Bool) -> m (Maybe Substitution) -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> CheckpointId -> m (Maybe Substitution)
    forall (tcm :: * -> *).
    MonadTCEnv tcm =>
    CheckpointId -> tcm (Maybe Substitution)
    checkpointSubstitution' CheckpointId
    cp
      mvs :: [(MetaId, MetaVariable)] <- filterM (isFreshMeta . snd) mvs

      cs <- (++) <$> useTC stAwakeConstraints
                 <*> useTC stSleepingConstraints

      reportSDoc "tc.generalize" 50 $ "current constraints:" <?> vcat (map prettyTCM cs)

      constrainedMetas <- Set.unions <$> mapM (constraintMetas . clValue . theConstraint) cs

      reportSDoc "tc.generalize" 30 $ nest 2 $
        "constrainedMetas     = " <+> prettyList_ (map prettyTCM $ Set.toList constrainedMetas)

      let isConstrained MetaId
    x = MetaId -> Set MetaId -> Bool
    forall a. Ord a => a -> Set a -> Bool
    Set.member MetaId
    x Set MetaId
    constrainedMetas
          -- Note: Always generalize named metas even if they are constrained. We
          -- freeze them so they won't be instantiated by the constraint, and we do
          -- want the nice error from checking the constraint after generalization.
          -- See #3276.
          isGeneralizable (MetaId
    x, MetaVariable
    mv) = MetaId -> Map MetaId name -> Bool
    forall k a. Ord k => k -> Map k a -> Bool
    Map.member MetaId
    x Map MetaId name
    nameMap Bool -> Bool -> Bool
    ||
                                    Bool -> Bool
    not (MetaId -> Bool
    isConstrained MetaId
    x) Bool -> Bool -> Bool
    && DoGeneralize
    NoGeneralize DoGeneralize -> DoGeneralize -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Arg DoGeneralize -> DoGeneralize
    forall e. Arg e -> e
    unArg (MetaInfo -> Arg DoGeneralize
    miGeneralizable (MetaVariable -> MetaInfo
    mvInfo MetaVariable
    mv))
          isSort = MetaVariable -> Bool
    isSortMeta_ (MetaVariable -> Bool)
    -> ((a, MetaVariable) -> MetaVariable) -> (a, MetaVariable) -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a, MetaVariable) -> MetaVariable
    forall a b. (a, b) -> b
    snd
          isOpen = MetaInstantiation -> Bool
    isOpenMeta (MetaInstantiation -> Bool)
    -> ((a, MetaVariable) -> MetaInstantiation)
    -> (a, MetaVariable)
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . MetaVariable -> MetaInstantiation
    mvInstantiation (MetaVariable -> MetaInstantiation)
    -> ((a, MetaVariable) -> MetaVariable)
    -> (a, MetaVariable)
    -> MetaInstantiation
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a, MetaVariable) -> MetaVariable
    forall a b. (a, b) -> b
    snd

      -- Split the generalizable metas in open and closed
      let (generalizable, nongeneralizable)         = partition isGeneralizable mvs
          (generalizableOpen', generalizableClosed) = partition isOpen generalizable
          (openSortMetas, generalizableOpen)        = partition isSort generalizableOpen'
          nongeneralizableOpen                      = ((MetaId, MetaVariable) -> Bool)
    -> [(MetaId, MetaVariable)] -> [(MetaId, MetaVariable)]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (MetaId, MetaVariable) -> Bool
    forall {a}. (a, MetaVariable) -> Bool
    isOpen [(MetaId, MetaVariable)]
    nongeneralizable

      reportSDoc "tc.generalize" 30 $ nest 2 $ vcat
        [ "generalizable        = " <+> prettyList_ (map (prettyTCM . fst) generalizable)
        , "generalizableOpen    = " <+> prettyList_ (map (prettyTCM . fst) generalizableOpen)
        , "openSortMetas        = " <+> prettyList_ (map (prettyTCM . fst) openSortMetas)
        ]

      -- Issue 3301: We can't generalize over sorts
      List1.unlessNull openSortMetas $ \ List1 (MetaId, MetaVariable)
    ms ->
        Warning -> TCMT IO ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> TCMT IO ()) -> Warning -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ Set1 MetaId -> Warning
    CantGeneralizeOverSorts (Set1 MetaId -> Warning) -> Set1 MetaId -> Warning
    forall a b. (a -> b) -> a -> b
    $ NonEmpty MetaId -> Set1 MetaId
    forall a. Ord a => NonEmpty a -> NESet a
    Set1.fromList (NonEmpty MetaId -> Set1 MetaId) -> NonEmpty MetaId -> Set1 MetaId
    forall a b. (a -> b) -> a -> b
    $ ((MetaId, MetaVariable) -> MetaId)
    -> List1 (MetaId, MetaVariable) -> NonEmpty MetaId
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (MetaId, MetaVariable) -> MetaId
    forall a b. (a, b) -> a
    fst List1 (MetaId, MetaVariable)
    ms

      -- Any meta in the solution of a generalizable meta should be generalized over (if possible).
      cp <- viewTC eCurrentCheckpoint
      let canGeneralize MetaId
    x | MetaId -> Bool
    isConstrained MetaId
    x = Bool -> TCMT IO Bool
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
          canGeneralize MetaId
    x = do
              mv   <- MetaId -> TCMT IO MetaVariable
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupLocalMeta MetaId
    x
              msub <- enterClosure mv $ \ Range
    _ ->
                        CheckpointId -> TCMT IO (Maybe Substitution)
    forall (tcm :: * -> *).
    MonadTCEnv tcm =>
    CheckpointId -> tcm (Maybe Substitution)
    checkpointSubstitution' CheckpointId
    cp
              let sameContext =
                    -- We can only generalize if the metavariable takes the context variables of the
                    -- current context as arguments. This happens either when the context of the meta
                    -- is the same as the current context and there is no pruning, or the meta context
                    -- is a weakening but the extra variables have been pruned.
                    -- It would be possible to generalize also in the case when some context variables
                    -- (other than genTel) have been pruned, but it's hard to construct an example
                    -- where this actually happens.
                    case (Maybe Substitution
    msub, MetaVariable -> Permutation
    mvPermutation MetaVariable
    mv) of
                      (Just Substitution
    IdS, Perm Int
    m [Int]
    xs)        -> [Int]
    xs [Int] -> [Int] -> Bool
    forall a. Eq a => a -> a -> Bool
    == [Int
    0 .. Int
    m Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1]
                      (Just (Wk Int
    n Substitution
    IdS), Perm Int
    m [Int]
    xs) -> [Int]
    xs [Int] -> [Int] -> Bool
    forall a. Eq a => a -> a -> Bool
    == [Int
    0 .. Int
    m Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1]
                      (Maybe Substitution, Permutation)
    _                            -> Bool
    False
              unless sameContext $ reportSDoc "tc.generalize" 20 $ do
                ty <- getMetaType x
                let Perm m xs = mvPermutation mv
                vcat
                  [ text "Don't know how to generalize over"
                  , nest 2 $ prettyTCM x <+> text ":" <+> prettyTCM ty
                  , text "in context"
                  , nest 2 $ inTopContext . prettyTCM =<< getContextTelescope
                  , text "permutation:" <+> text (show (m, xs))
                  , text "subst:" <+> pretty msub ]
              return sameContext

      inherited :: Set MetaId <- Set.unions <$> forM generalizableClosed \ (MetaId
    x, MetaVariable
    mv) ->
        case MetaVariable -> MetaInstantiation
    mvInstantiation MetaVariable
    mv of
          InstV Instantiation
    inst -> do
            parentName <- MetaId -> TCMT IO String
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m String
    getMetaNameSuggestion MetaId
    x
            metas <- filterM canGeneralize . Set.toList .
                     allMetas Set.singleton =<<
                     instantiateFull (instBody inst)
            unless (null metas) do
              reportSDoc "tc.generalize" 40 $
                hcat ["Inherited metas from ", prettyTCM x, ":"] <?> prettyList_ (map prettyTCM metas)
              -- #4291: Override existing meta name suggestion.
              -- Don't suggest names for explicitly named generalizable metas.
              case filter (`Map.notMember` nameMap) metas of
                -- If we solved the parent with a new meta use the parent name for that.
                [MetaId
    m] | MetaV{} <- Instantiation -> Term
    instBody Instantiation
    inst -> MetaId -> String -> TCMT IO ()
    forall (m :: * -> *). MonadMetaSolver m => MetaId -> String -> m ()
    setMetaNameSuggestion MetaId
    m String
    parentName
                -- Otherwise suffix with a number.
                [MetaId]
    ms -> (Integer -> MetaId -> TCMT IO ())
    -> [Integer] -> [MetaId] -> TCMT IO ()
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m ()
    zipWithM_ (\ Integer
    i MetaId
    m -> MetaId -> String -> TCMT IO ()
    forall (m :: * -> *). MonadMetaSolver m => MetaId -> String -> m ()
    setMetaNameSuggestion MetaId
    m (String
    parentName String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "." String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Integer -> String
    forall a. Show a => a -> String
    show Integer
    i)) [Integer
    1..] [MetaId]
    ms
            return $ Set.fromList metas
          MetaInstantiation
    _ -> TCMT IO (Set MetaId)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

      let (alsoGeneralize, reallyDontGeneralize) = partition (`Set.member` inherited) $ map fst nongeneralizableOpen
          generalizeOver   = ((MetaId, MetaVariable) -> MetaId)
    -> [(MetaId, MetaVariable)] -> [MetaId]
    forall a b. (a -> b) -> [a] -> [b]
    map (MetaId, MetaVariable) -> MetaId
    forall a b. (a, b) -> a
    fst [(MetaId, MetaVariable)]
    generalizableOpen [MetaId] -> [MetaId] -> [MetaId]
    forall a. [a] -> [a] -> [a]
    ++ [MetaId]
    alsoGeneralize
          shouldGeneralize = ([MetaId]
    generalizeOver [MetaId] -> MetaId -> Bool
    forall a. Ord a => [a] -> a -> Bool
    `hasElem`)

      reportSDoc "tc.generalize" 30 $ nest 2 $ vcat
        [ "alsoGeneralize       = " <+> prettyList_ (map prettyTCM alsoGeneralize)
        , "reallyDontGeneralize = " <+> prettyList_ (map prettyTCM reallyDontGeneralize)
        ]

      reportSDoc "tc.generalize" 10 $ "we're generalizing over" <+> prettyList_ (map prettyTCM generalizeOver)

      -- Sort metas in dependency order. Include open metas that we are not
      -- generalizing over, since they will need to be pruned appropriately (see
      -- Issue 3672).
      allSortedMetas <- fromMaybeM (typeError GeneralizeCyclicDependency) $
        dependencySortMetas (generalizeOver ++ reallyDontGeneralize ++ map fst openSortMetas)
      let sortedMetas = (MetaId -> Bool) -> [MetaId] -> [MetaId]
    forall a. (a -> Bool) -> [a] -> [a]
    filter MetaId -> Bool
    shouldGeneralize [MetaId]
    allSortedMetas

      let dropCxt Impossible
    err = Substitution -> (Context -> Context) -> m a -> m a
    forall a. Substitution -> (Context -> Context) -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Substitution -> (Context -> Context) -> m a -> m a
    updateContext (Impossible -> Int -> Substitution
    forall a. Impossible -> Int -> Substitution' a
    strengthenS Impossible
    err Int
    1) (Int -> Context -> Context
    forall a. Int -> [a] -> [a]
    drop Int
    1)

      -- Create the pre-record type (we don't yet know the types of the fields)
      (genRecName, genRecCon, genRecFields) <- dropCxt __IMPOSSIBLE__ $
          createGenRecordType genRecMeta sortedMetas

      reportSDoc "tc.generalize" 30 $ vcat $
        [ "created genRecordType"
        , nest 2 $ "genRecName   = " <+> prettyTCM genRecName
        , nest 2 $ "genRecCon    = " <+> prettyTCM genRecCon
        , nest 2 $ "genRecFields = " <+> prettyList_ (map prettyTCM genRecFields)
        ]

      -- Solve the generalizable metas. Each generalizable meta is solved by projecting the
      -- corresponding field from the genTel record.
      cxtTel <- getContextTelescope
      let solve MetaId
    m QName
    field = do
            String -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.generalize" Int
    30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "solving generalized meta" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+>
              MetaId -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
    prettyTCM MetaId
    m TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    ":=" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM (Int -> Elims -> Term
    Var Int
    0 [ProjOrigin -> QName -> Elim' Term
    forall a. ProjOrigin -> QName -> Elim' a
    Proj ProjOrigin
    ProjSystem QName
    field])
            -- m should not be instantiated, but if we don't check constraints
            -- properly it could be (#3666 and #3667). Fail hard instead of
            -- generating bogus types.
            TCMT IO Bool -> TCMT IO () -> TCMT IO ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM (MetaId -> TCMT IO Bool
    forall a (m :: * -> *).
    (IsInstantiatedMeta a, ReadTCState m) =>
    a -> m Bool
    forall (m :: * -> *). ReadTCState m => MetaId -> m Bool
    isInstantiatedMeta MetaId
    m) TCMT IO ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
            MetaId -> [Arg String] -> Term -> TCMT IO ()
    forall (m :: * -> *).
    (MonadMetaSolver m, MonadMetaSolver m) =>
    MetaId -> [Arg String] -> Term -> m ()
    assignTerm' MetaId
    m (Telescope -> [Arg String]
    forall a. TelToArgs a => a -> [Arg String]
    telToArgs Telescope
    cxtTel) (Term -> TCMT IO ()) -> Term -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ Int -> Elims -> Term
    Var Int
    0 [ProjOrigin -> QName -> Elim' Term
    forall a. ProjOrigin -> QName -> Elim' a
    Proj ProjOrigin
    ProjSystem QName
    field]
      zipWithM_ solve sortedMetas genRecFields

      -- Record the named variables in the telescope
      let telNames = (MetaId -> Maybe name) -> [MetaId] -> [Maybe name]
    forall a b. (a -> b) -> [a] -> [b]
    map (MetaId -> Map MetaId name -> Maybe name
    forall k a. Ord k => k -> Map k a -> Maybe a
    `Map.lookup` Map MetaId name
    nameMap) [MetaId]
    sortedMetas

      -- Build the telescope of generalized metas
      teleTypes <- do
        args <- getContextArgs
        concat <$> forM sortedMetas \ MetaId
    m -> do
          mv <- MetaId -> TCMT IO MetaVariable
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupLocalMeta MetaId
    m
          let info =
                (ArgInfo -> ArgInfo
    forall a. LensHiding a => a -> a
    hideOrKeepInstance (ArgInfo -> ArgInfo) -> ArgInfo -> ArgInfo
    forall a b. (a -> b) -> a -> b
    $
                Arg DoGeneralize -> ArgInfo
    forall a. LensArgInfo a => a -> ArgInfo
    getArgInfo (Arg DoGeneralize -> ArgInfo) -> Arg DoGeneralize -> ArgInfo
    forall a b. (a -> b) -> a -> b
    $ MetaInfo -> Arg DoGeneralize
    miGeneralizable (MetaInfo -> Arg DoGeneralize) -> MetaInfo -> Arg DoGeneralize
    forall a b. (a -> b) -> a -> b
    $ MetaVariable -> MetaInfo
    mvInfo MetaVariable
    mv) { argInfoOrigin = Generalization }
              HasType{ jMetaType = t } = mvJudgement mv
              perm = MetaVariable -> Permutation
    mvPermutation MetaVariable
    mv
          t' <- piApplyM t $ permute (takeP (length args) perm) args
          return [(Arg info $ miNameSuggestion $ mvInfo mv, t')]
      let genTel = ConHead -> [(Arg String, Type)] -> Telescope
    buildGeneralizeTel ConHead
    genRecCon [(Arg String, Type)]
    teleTypes

      reportSDoc "tc.generalize" 40 $ vcat
        [ text "teleTypes =" <+> prettyTCM teleTypes
        , text "genTel    =" <+> prettyTCM genTel
        ]

      -- Now we need to prune the unsolved metas to make sure they respect the new
      -- dependencies (#3672). Also update interaction points to point to pruned metas.
      let inscope (InteractionId
    ii, InteractionPoint{ipMeta :: InteractionPoint -> Maybe MetaId
    ipMeta = Just MetaId
    x})
            | MetaId -> Map MetaId MetaVariable -> Bool
    forall k a. Ord k => k -> Map k a -> Bool
    MapS.member MetaId
    x (LocalMetaStores -> Map MetaId MetaVariable
    openMetas LocalMetaStores
    allmetas) Bool -> Bool -> Bool
    ||
              MetaId -> Map MetaId MetaVariable -> Bool
    forall k a. Ord k => k -> Map k a -> Bool
    MapS.member MetaId
    x (LocalMetaStores -> Map MetaId MetaVariable
    solvedMetas LocalMetaStores
    allmetas) =
              (MetaId, InteractionId) -> Maybe (MetaId, InteractionId)
    forall a. a -> Maybe a
    Just (MetaId
    x, InteractionId
    ii)
          inscope (InteractionId, InteractionPoint)
    _ = Maybe (MetaId, InteractionId)
    forall a. Maybe a
    Nothing
      ips <- Map.fromDistinctAscList . mapMaybe inscope . fst . BiMap.toDistinctAscendingLists <$> useTC stInteractionPoints
      pruneUnsolvedMetas genRecName genRecCon genTel genRecFields ips shouldGeneralize allSortedMetas

      -- Fill in the missing details of the telescope record.
      dropCxt __IMPOSSIBLE__ $ fillInGenRecordDetails genRecName genRecCon genRecFields genRecMeta genTel

      -- Now abstract over the telescope. We need to apply the substitution that subsitutes a record
      -- value packing up the generalized variables for the genTel variable.
      let sub = ConHead -> [ArgInfo] -> Int -> Substitution
    unpackSub ConHead
    genRecCon (((Arg String, Type) -> ArgInfo)
    -> [(Arg String, Type)] -> [ArgInfo]
    forall a b. (a -> b) -> [a] -> [b]
    map (Arg String -> ArgInfo
    forall e. Arg e -> ArgInfo
    argInfo (Arg String -> ArgInfo)
    -> ((Arg String, Type) -> Arg String)
    -> (Arg String, Type)
    -> ArgInfo
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Arg String, Type) -> Arg String
    forall a b. (a, b) -> a
    fst) [(Arg String, Type)]
    teleTypes) ([(Arg String, Type)] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [(Arg String, Type)]
    teleTypes)

      -- Instantiate all fresh meta-variables to get rid of
      -- __DUMMY_TERM__.
      genTel <- flip instantiateWhen genTel $ \MetaId
    m -> do
        mv <- MetaId -> ReduceM (Maybe (Either RemoteMetaVariable MetaVariable))
    forall (m :: * -> *).
    ReadTCState m =>
    MetaId -> m (Maybe (Either RemoteMetaVariable MetaVariable))
    lookupMeta MetaId
    m
        case mv of
          Maybe (Either RemoteMetaVariable MetaVariable)
    Nothing         -> ReduceM Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Just Left{}     -> Bool -> ReduceM Bool
    forall a. a -> ReduceM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
          Just (Right MetaVariable
    mv) -> MetaVariable -> ReduceM Bool
    forall (m :: * -> *). MonadReduce m => MetaVariable -> m Bool
    isFreshMeta MetaVariable
    mv

      return (genTel, telNames, sub)

    -- | Prune unsolved metas (#3672). The input includes also the generalized metas and is sorted in
    -- dependency order. The telescope is the generalized telescope.
    pruneUnsolvedMetas :: QName -> ConHead -> Telescope -> [QName] -> Map MetaId InteractionId -> (MetaId -> Bool) -> [MetaId] -> TCM ()
    pruneUnsolvedMetas :: QName
    -> ConHead
    -> Telescope
    -> [QName]
    -> Map MetaId InteractionId
    -> (MetaId -> Bool)
    -> [MetaId]
    -> TCMT IO ()
    pruneUnsolvedMetas QName
    genRecName ConHead
    genRecCon Telescope
    genTel [QName]
    genRecFields Map MetaId InteractionId
    interactionPoints MetaId -> Bool
    isGeneralized [MetaId]
    metas
      | (MetaId -> Bool) -> [MetaId] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all MetaId -> Bool
    isGeneralized [MetaId]
    metas = () -> TCMT IO ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      | Bool
    otherwise               = [Dom (String, Type)] -> Telescope -> [MetaId] -> TCMT IO ()
    prune [] Telescope
    genTel [MetaId]
    metas
      where
        prune :: [Dom (String, Type)] -> Telescope -> [MetaId] -> TCMT IO ()
    prune [Dom (String, Type)]
    _ Telescope
    _ [] = () -> TCMT IO ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        prune [Dom (String, Type)]
    cxt Telescope
    tel (MetaId
    x : [MetaId]
    xs) | Bool -> Bool
    not (MetaId -> Bool
    isGeneralized MetaId
    x) = do
          -- If x is a blocked term we shouldn't instantiate it.
          TCMT IO Bool -> TCMT IO () -> TCMT IO ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM (Bool -> Bool
    not (Bool -> Bool) -> TCMT IO Bool -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> TCMT IO Bool
    isBlockedTerm MetaId
    x) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ do
            x <- if Telescope -> Bool
    forall a. Null a => a -> Bool
    null Telescope
    tel then MetaId -> TCMT IO MetaId
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return MetaId
    x else MetaId -> TCMT IO MetaId
    prePrune MetaId
    x
            pruneMeta (telFromList $ reverse cxt) x
          [Dom (String, Type)] -> Telescope -> [MetaId] -> TCMT IO ()
    prune [Dom (String, Type)]
    cxt Telescope
    tel [MetaId]
    xs
        prune [Dom (String, Type)]
    cxt (ExtendTel Dom Type
    a Abs Telescope
    tel) (MetaId
    x : [MetaId]
    xs) = [Dom (String, Type)] -> Telescope -> [MetaId] -> TCMT IO ()
    prune ((Type -> (String, Type)) -> Dom Type -> Dom (String, Type)
    forall a b. (a -> b) -> Dom' Term a -> Dom' Term b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (String
    x,) Dom Type
    a Dom (String, Type) -> [Dom (String, Type)] -> [Dom (String, Type)]
    forall a. a -> [a] -> [a]
    : [Dom (String, Type)]
    cxt) (Abs Telescope -> Telescope
    forall a. Abs a -> a
    unAbs Abs Telescope
    tel) [MetaId]
    xs
          where x :: String
    x = Abs Telescope -> String
    forall a. Abs a -> String
    absName Abs Telescope
    tel
        prune [Dom (String, Type)]
    _ Telescope
    _ [MetaId]
    _ = TCMT IO ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__

        sub :: Int -> Substitution
    sub = ConHead -> [ArgInfo] -> Int -> Substitution
    unpackSub ConHead
    genRecCon ([ArgInfo] -> Int -> Substitution)
    -> [ArgInfo] -> Int -> Substitution
    forall a b. (a -> b) -> a -> b
    $ (Dom (String, Type) -> ArgInfo)
    -> [Dom (String, Type)] -> [ArgInfo]
    forall a b. (a -> b) -> [a] -> [b]
    map Dom (String, Type) -> ArgInfo
    forall a. LensArgInfo a => a -> ArgInfo
    getArgInfo ([Dom (String, Type)] -> [ArgInfo])
    -> [Dom (String, Type)] -> [ArgInfo]
    forall a b. (a -> b) -> a -> b
    $ Telescope -> [Dom (String, Type)]
    forall t. Tele (Dom t) -> [Dom (String, t)]
    telToList Telescope
    genTel

        prepruneErrorRefinedContext :: MetaId -> TCM a
    prepruneErrorRefinedContext = String -> MetaId -> TCM a
    forall a. String -> MetaId -> TCM a
    prepruneError (String -> MetaId -> TCM a) -> String -> MetaId -> TCM a
    forall a b. (a -> b) -> a -> b
    $
          String
    "Failed to generalize because some of the generalized variables depend on an " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++
          String
    "unsolved meta created in a refined context (not a simple extension of the context where " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++
          String
    "generalization happens)."

        prepruneErrorCyclicDependencies :: MetaId -> TCM a
    prepruneErrorCyclicDependencies = String -> MetaId -> TCM a
    forall a. String -> MetaId -> TCM a
    prepruneError (String -> MetaId -> TCM a) -> String -> MetaId -> TCM a
    forall a b. (a -> b) -> a -> b
    $
          String
    "Failed to generalize due to circular dependencies between the generalized " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++
          String
    "variables and an unsolved meta."

        prepruneErrorFailedToInstantiate :: MetaId -> TCM a
    prepruneErrorFailedToInstantiate = String -> MetaId -> TCM a
    forall a. String -> MetaId -> TCM a
    prepruneError (String -> MetaId -> TCM a) -> String -> MetaId -> TCM a
    forall a b. (a -> b) -> a -> b
    $
          String
    "Failed to generalize because the generalized variables depend on an unsolved meta " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++
          String
    "that could not be lifted outside the generalization."

        prepruneError :: String -> MetaId -> TCM a
        prepruneError :: forall a. String -> MetaId -> TCM a
    prepruneError String
    msg MetaId
    x = do
          r <- MetaId -> TCMT IO Range
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m Range
    getMetaRange MetaId
    x
          genericDocError =<<
            (fwords (msg ++ " The problematic unsolved meta is") $$
                     nest 2 (prettyTCM (MetaV x []) <+> "at" <+> pretty r)
            )

        -- If one of the fields depend on this meta, we have to make sure that this meta doesn't depend
        -- on any variables introduced after the genRec. See test/Fail/Issue3672b.agda for a test case.
        prePrune :: MetaId -> TCMT IO MetaId
    prePrune MetaId
    x = do
          cp <- Lens' TCEnv CheckpointId -> TCMT IO CheckpointId
    forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
    viewTC (CheckpointId -> f CheckpointId) -> TCEnv -> f TCEnv
    Lens' TCEnv CheckpointId
    eCurrentCheckpoint
          mv <- lookupLocalMeta x
          (i, _A) <- enterClosure mv $ \ Range
    _ -> do
            δ <- CheckpointId -> TCMT IO Substitution
    forall (tcm :: * -> *).
    MonadTCEnv tcm =>
    CheckpointId -> tcm Substitution
    checkpointSubstitution CheckpointId
    cp
            _A <- case mvJudgement mv of
                    IsSort{}  -> Maybe Type -> TCMT IO (Maybe Type)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Type
    forall a. Maybe a
    Nothing
                    HasType{} -> Type -> Maybe Type
    forall a. a -> Maybe a
    Just (Type -> Maybe Type) -> TCM Type -> TCMT IO (Maybe Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> TCM Type
    forall (m :: * -> *).
    (HasBuiltins m, HasCallStack, MonadDebug m, MonadReduce m,
     MonadTCEnv m, ReadTCState m) =>
    MetaId -> m Type
    getMetaTypeInContext MetaId
    x
            case δ of
              Wk Int
    n Substitution
    IdS -> (Int, Maybe Type) -> TCMT IO (Int, Maybe Type)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Int
    n, Maybe Type
    _A)
              Substitution
    IdS      -> (Int, Maybe Type) -> TCMT IO (Int, Maybe Type)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Int
    0, Maybe Type
    _A)
              Substitution
    _        -> MetaId -> TCMT IO (Int, Maybe Type)
    forall {a}. MetaId -> TCM a
    prepruneErrorRefinedContext MetaId
    x
          if i == 0 then return x else do
            reportSDoc "tc.generalize.prune.pre" 40 $ vcat
              [ "prepruning"
              , nest 2 $ pretty x <+> ":" <+> pretty (jMetaType $ mvJudgement mv)
              , nest 2 $ "|Δ| =" <+> pshow i ]

            -- We have
            --   Γ (r : GenRec)            current context
            --   Γ (r : GenRec) Δ ⊢ x : A  with |Δ| = i
            -- and we need to get rid of the dependency on Δ.

            -- We can only do this if A does not depend on Δ, so check this first.
            case IntSet.minView (allFreeVars _A) of
              Just (Int
    j, IntSet
    _) | Int
    j Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    i -> MetaId -> TCMT IO ()
    forall {a}. MetaId -> TCM a
    prepruneErrorCyclicDependencies MetaId
    x
              Maybe (Int, IntSet)
    _                   -> () -> TCMT IO ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

            -- If it doesn't we can strenghten it to the current context (this is done by
            -- newMetaFromOld).
            --   Γ (r : GenRec) ⊢ ρ : Γ (r : GenRec) Δ
            let ρ  = Impossible -> Int -> Substitution
    forall a. Impossible -> Int -> Substitution' a
    strengthenS Impossible
    HasCallStack => Impossible
    impossible Int
    i
                ρ' = Int -> Substitution
    forall a. Int -> Substitution' a
    raiseS Int
    i

            (y, u) <- newMetaFromOld mv ρ _A

            let uρ' = Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg Term)
    ρ' Term
    u

            reportSDoc "tc.generalize.prune.pre" 40 $ nest 2 $ vcat
              [ "u    =" <+> pretty u
              , "uρ⁻¹ =" <+> pretty uρ' ]

            -- To solve it we enter the context of x again
            enterClosure mv $ \ Range
    _ -> do
              -- v is x applied to the context variables
              v <- case Maybe Type
    _A of
                     Maybe Type
    Nothing -> Sort -> Term
    Sort (Sort -> Term) -> (Args -> Sort) -> Args -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . MetaId -> Elims -> Sort
    forall t. MetaId -> [Elim' t] -> Sort' t
    MetaS MetaId
    x (Elims -> Sort) -> (Args -> Elims) -> Args -> Sort
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Arg Term -> Elim' Term) -> Args -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply (Args -> Term) -> TCMT IO Args -> TCMT IO Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaVariable -> TCMT IO Args
    forall (m :: * -> *). MonadTCEnv m => MetaVariable -> m Args
    getMetaContextArgs MetaVariable
    mv
                     Just{}  -> MetaId -> Elims -> Term
    MetaV MetaId
    x (Elims -> Term) -> (Args -> Elims) -> Args -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Arg Term -> Elim' Term) -> Args -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply (Args -> Term) -> TCMT IO Args -> TCMT IO Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaVariable -> TCMT IO Args
    forall (m :: * -> *). MonadTCEnv m => MetaVariable -> m Args
    getMetaContextArgs MetaVariable
    mv
              noConstraints (doPrune x mv _A v uρ') `catchError` \ TCErr
    _ -> MetaId -> TCMT IO ()
    forall {a}. MetaId -> TCM a
    prepruneErrorFailedToInstantiate MetaId
    x
              setInteractionPoint x y
              return y

        pruneMeta :: Telescope -> MetaId -> TCMT IO ()
    pruneMeta Telescope
    _Θ MetaId
    x = do
          cp <- Lens' TCEnv CheckpointId -> TCMT IO CheckpointId
    forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
    viewTC (CheckpointId -> f CheckpointId) -> TCEnv -> f TCEnv
    Lens' TCEnv CheckpointId
    eCurrentCheckpoint
          mv <- lookupLocalMeta x
          -- The reason we are doing all this inside the closure of x is so that if x is an interaction
          -- meta we get the right context for the pruned interaction meta.
          enterClosure mv $ \ Range
    _ ->
            -- If we can't find the generalized record, it's already been pruned and we don't have to do
            -- anything.
            TCMT IO (Maybe Int) -> (Int -> TCMT IO ()) -> TCMT IO ()
    forall (m :: * -> *) a.
    Monad m =>
    m (Maybe a) -> (a -> m ()) -> m ()
    whenJustM (MetaVariable -> TCMT IO (Maybe Int)
    findGenRec MetaVariable
    mv) ((Int -> TCMT IO ()) -> TCMT IO ())
    -> (Int -> TCMT IO ()) -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ \ Int
    i -> do

            String -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.generalize.prune" Int
    30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
              [ TCMT IO Doc
    "pruning"
              , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc -> TCMT IO Doc
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Judgement MetaId -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Judgement MetaId -> m Doc
    prettyTCM (MetaVariable -> Judgement MetaId
    mvJudgement MetaVariable
    mv)
              , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "GenRecTel is var" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Int -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Int
    i ]

            _ΓrΔ <- TCMT IO Telescope
    forall (m :: * -> *). MonadTCEnv m => m Telescope
    getContextTelescope
            let (_Γ, _Δ) = (telFromList gs, telFromList ds)
                  where (gs, _ : ds) = splitAt (size _ΓrΔ - i - 1) (telToList _ΓrΔ)

            -- Get the type of x. By doing this here we let the checkpoint machinery sort out the
            _A <- case mvJudgement mv of
                    IsSort{}  -> Maybe Type -> TCMT IO (Maybe Type)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Type
    forall a. Maybe a
    Nothing
                    HasType{} -> Type -> Maybe Type
    forall a. a -> Maybe a
    Just (Type -> Maybe Type) -> TCM Type -> TCMT IO (Maybe Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> TCM Type
    forall (m :: * -> *).
    (HasBuiltins m, HasCallStack, MonadDebug m, MonadReduce m,
     MonadTCEnv m, ReadTCState m) =>
    MetaId -> m Type
    getMetaTypeInContext MetaId
    x

            -- We have
            --   Γ  (r : GenTel) Δ         current context
            --   Γ₀ (r : GenTel)           top context
            --   Γ₀ ⊢ Θ                    prefix of the generalized telescope currently in scope
            --   Γ (r : GenTel) Δ ⊢ x : A  the meta to prune

            -- Get the substitution from the point of generalization to the current context. This always
            -- succeeds since if the meta depends on GenTel it must have been created inside the
            -- generalization:
            --   Γ (r : GenTel) Δ ⊢ δ : Γ₀ (r : GenTel)
            δ <- checkpointSubstitution cp

            -- v is x applied to the context variables
            v <- case _A of
                   Maybe Type
    Nothing -> Sort -> Term
    Sort (Sort -> Term) -> (Args -> Sort) -> Args -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . MetaId -> Elims -> Sort
    forall t. MetaId -> [Elim' t] -> Sort' t
    MetaS MetaId
    x (Elims -> Sort) -> (Args -> Elims) -> Args -> Sort
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Arg Term -> Elim' Term) -> Args -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply (Args -> Term) -> TCMT IO Args -> TCMT IO Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaVariable -> TCMT IO Args
    forall (m :: * -> *). MonadTCEnv m => MetaVariable -> m Args
    getMetaContextArgs MetaVariable
    mv
                   Just{}  -> MetaId -> Elims -> Term
    MetaV MetaId
    x (Elims -> Term) -> (Args -> Elims) -> Args -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Arg Term -> Elim' Term) -> Args -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply (Args -> Term) -> TCMT IO Args -> TCMT IO Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaVariable -> TCMT IO Args
    forall (m :: * -> *). MonadTCEnv m => MetaVariable -> m Args
    getMetaContextArgs MetaVariable
    mv

            -- Now ultimately we want to create the fresh meta in the context
            --   Γ Θγ Δσ where Γ    ⊢ γ : Γ₀
            --                 Γ Θγ ⊢ σ : Γ (r : GenTel)
            -- σ is the unpacking substitution (which is polymorphic in Γ)
            let σ   = Int -> Substitution
    sub (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    _Θ)
                --    Γ <- Γ (r : GenTel) Δ <- Γ₀ (r : GenTel) <- Γ₀
                γ   = Impossible -> Int -> Substitution
    forall a. Impossible -> Int -> Substitution' a
    strengthenS Impossible
    HasCallStack => Impossible
    impossible (Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1) Substitution -> Substitution -> Substitution
    forall a.
    EndoSubst a =>
    Substitution' a -> Substitution' a -> Substitution' a
    `composeS` Substitution
    δ Substitution -> Substitution -> Substitution
    forall a.
    EndoSubst a =>
    Substitution' a -> Substitution' a -> Substitution' a
    `composeS` Int -> Substitution
    forall a. Int -> Substitution' a
    raiseS Int
    1
                _Θγ = Substitution' (SubstArg Telescope) -> Telescope -> Telescope
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg Telescope)
    γ Telescope
    _Θ
                _Δσ = Substitution' (SubstArg Telescope) -> Telescope -> Telescope
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg Telescope)
    σ Telescope
    _Δ

            -- The substitution into the new context is simply lifting σ over Δ:
            --   Γ Θγ Δσ ⊢ lift i σ : Γ (r : GenTel) Δ
            let ρ  = Int -> Substitution -> Substitution
    forall a. Int -> Substitution' a -> Substitution' a
    liftS Int
    i Substitution
    σ
                -- We also need ρ⁻¹, which is a lot easier to construct.
                ρ' = Int -> Substitution -> Substitution
    forall a. Int -> Substitution' a -> Substitution' a
    liftS Int
    i (Substitution -> Substitution) -> Substitution -> Substitution
    forall a b. (a -> b) -> a -> b
    $ [ Int -> Elims -> Term
    Var Int
    0 [ProjOrigin -> QName -> Elim' Term
    forall a. ProjOrigin -> QName -> Elim' a
    Proj ProjOrigin
    ProjSystem QName
    fld] | QName
    fld <- [QName] -> [QName]
    forall a. [a] -> [a]
    reverse ([QName] -> [QName]) -> [QName] -> [QName]
    forall a b. (a -> b) -> a -> b
    $ Int -> [QName] -> [QName]
    forall a. Int -> [a] -> [a]
    take (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    _Θ) ([QName] -> [QName]) -> [QName] -> [QName]
    forall a b. (a -> b) -> a -> b
    $ [QName]
    genRecFields ] [Term] -> Substitution -> Substitution
    forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
    ++# Int -> Substitution
    forall a. Int -> Substitution' a
    raiseS Int
    1

            reportSDoc "tc.generalize.prune" 30 $ nest 2 $ vcat
              [ "Γ   =" <+> pretty _Γ
              , "Θ   =" <+> pretty _Θ
              , "Δ   =" <+> pretty _Δ
              , "σ   =" <+> pretty σ
              , "γ   =" <+> pretty γ
              , "δ   =" <+> pretty δ
              , "ρ   =" <+> pretty ρ
              , "ρ⁻¹ =" <+> pretty ρ'
              , "Θγ  =" <+> pretty _Θγ
              , "Δσ  =" <+> pretty _Δσ
              , "_A  =" <+> pretty _A
              ]

            -- When updating the context we also need to pick names for the variables. Get them from the
            -- current context and generate fresh ones for the generalized variables in Θ.
            (newCxt, rΘ) <- do
              (rΔ, _ : rΓ) <- splitAt i <$> getContext
              let setName dom :: Dom' Term (a, Type)
    dom@(Dom {unDom :: forall t e. Dom' t e -> e
    unDom = (a
    s,Type
    ty)}) = Name -> Dom Type -> ContextEntry
    CtxVar (Name -> Dom Type -> ContextEntry)
    -> f Name -> f (Dom Type -> ContextEntry)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> f Name
    forall a (m :: * -> *).
    (FreshName a, MonadFresh NameId m) =>
    a -> m Name
    forall (m :: * -> *). MonadFresh NameId m => a -> m Name
    freshName_ a
    s f (Dom Type -> ContextEntry) -> f (Dom Type) -> f ContextEntry
    forall a b. f (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Dom Type -> f (Dom Type)
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Dom Type -> f (Dom Type)) -> Dom Type -> f (Dom Type)
    forall a b. (a -> b) -> a -> b
    $ Dom' Term (a, Type)
    dom Dom' Term (a, Type) -> Type -> Dom Type
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> Type
    ty)
              rΘ <- mapM setName $ reverse $ telToList _Θγ
              let rΔσ = (Name -> Dom (String, Type) -> ContextEntry)
    -> [Name] -> [Dom (String, Type)] -> Context
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (\ Name
    name Dom (String, Type)
    dom -> Name -> Dom Type -> ContextEntry
    CtxVar Name
    name ((String, Type) -> Type
    forall a b. (a, b) -> b
    snd ((String, Type) -> Type) -> Dom (String, Type) -> Dom Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Dom (String, Type)
    dom))
                                ((ContextEntry -> Name) -> Context -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map ContextEntry -> Name
    ctxEntryName Context
    rΔ)
                                ([Dom (String, Type)] -> [Dom (String, Type)]
    forall a. [a] -> [a]
    reverse ([Dom (String, Type)] -> [Dom (String, Type)])
    -> [Dom (String, Type)] -> [Dom (String, Type)]
    forall a b. (a -> b) -> a -> b
    $ Telescope -> [Dom (String, Type)]
    forall t. Tele (Dom t) -> [Dom (String, t)]
    telToList Telescope
    _Δσ)
              return (rΔσ ++ rΘ ++ rΓ, rΘ)

            -- Now we can enter the new context and create our meta variable.
            (y, u) <- updateContext ρ (const newCxt) $ localScope $ do

              -- First, we add the named variables to the scope, to allow
              -- them to be used in holes (#3341). These should go outside Δ (#3735).
              outsideLocalVars i $ addNamedVariablesToScope rΘ

              -- Now we can create the new meta
              newMetaFromOld mv ρ _A

            -- Finally we solve x := yρ⁻¹. The reason for solving it this way instead of xρ := y is that
            -- ρ contains dummy terms for the variables that are not in scope.
            -- If x has been instantiated by some constraint unblocked by previous pruning or
            -- generalization, use equalTerm instead of assigning to x. If this fails (see
            -- test/Fail/Issue3655b.agda for a test case), we need to give an error. This can happen if
            -- there are dependencies between generalized variables that are hidden by constraints and
            -- the dependency sorting happens to pick the wrong order. For instance, if we have
            --    α : Nat   (unsolved meta)
            --    t : F α   (named variable)
            --    n : Nat   (named variable)
            -- and a constraint F α == F n, where F does some pattern matching preventing the constraint
            -- to be solved when n is still a meta. If t appears before n in the type these will be sorted
            -- as α, t, n, but we will solve α := n before we get to the pruning here. It's good that we
            -- solve first though, because that means we can give a more informative error message than
            -- the "Cannot instantiate..." we would otherwise get.
            let uρ' = Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg Term)
    ρ' Term
    u
            reportSDoc "tc.generalize.prune" 80 $ vcat
              [ "solving"
              , nest 2 $ sep [ pretty v   <+> "=="
                             , pretty uρ' <+> ":"
                             , pretty _A ] ]
            noConstraints (doPrune x mv _A v uρ') `catchError` niceError x v

            reportSDoc "tc.generalize.prune" 80 $ vcat
              [ "solved"
              , nest 2 $ "v    =" <+> (pretty =<< instantiateFull v)
              , nest 2 $ "uρ⁻¹ =" <+> (pretty =<< instantiateFull uρ') ]

            setInteractionPoint x y

        findGenRec :: MetaVariable -> TCM (Maybe Int)
        findGenRec :: MetaVariable -> TCMT IO (Maybe Int)
    findGenRec MetaVariable
    mv = do
          cxt <- Context -> TCMT IO Context
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull (Context -> TCMT IO Context) -> TCMT IO Context -> TCMT IO Context
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCMT IO Context
    forall (m :: * -> *). MonadTCEnv m => m Context
    getContext
          let n         = Context -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length Context
    cxt
              notPruned = [Int] -> IntSet
    IntSet.fromList ([Int] -> IntSet) -> [Int] -> IntSet
    forall a b. (a -> b) -> a -> b
    $
                          Permutation -> [Int] -> [Int]
    forall a. Permutation -> [a] -> [a]
    permute (Int -> Permutation -> Permutation
    takeP Int
    n (Permutation -> Permutation) -> Permutation -> Permutation
    forall a b. (a -> b) -> a -> b
    $ MetaVariable -> Permutation
    mvPermutation MetaVariable
    mv) ([Int] -> [Int]) -> [Int] -> [Int]
    forall a b. (a -> b) -> a -> b
    $
                          Int -> [Int]
    forall a. Integral a => a -> [a]
    downFrom Int
    n
          case [ i
               | (i, CtxVar _ (Dom{unDom = (El _ (Def q _))})) <- zip [0..] cxt
               , q == genRecName
               , i `IntSet.member` notPruned
               ] of
            []    -> Maybe Int -> TCMT IO (Maybe Int)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Int
    forall a. Maybe a
    Nothing
            Int
    _:Int
    _:[Int]
    _ -> TCMT IO (Maybe Int)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
            [Int
    i]   -> Maybe Int -> TCMT IO (Maybe Int)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Int -> Maybe Int
    forall a. a -> Maybe a
    Just Int
    i)
                                                        -- Nothing if sort meta
        newMetaFromOld :: MetaVariable -> Substitution -> Maybe Type -> TCM (MetaId, Term)
        newMetaFromOld :: MetaVariable -> Substitution -> Maybe Type -> TCM (MetaId, Term)
    newMetaFromOld MetaVariable
    mv Substitution
    ρ Maybe Type
    mA = MetaVariable -> TCM (MetaId, Term) -> TCM (MetaId, Term)
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange MetaVariable
    mv (TCM (MetaId, Term) -> TCM (MetaId, Term))
    -> TCM (MetaId, Term) -> TCM (MetaId, Term)
    forall a b. (a -> b) -> a -> b
    $
          case Maybe Type
    mA of
            Maybe Type
    Nothing -> do
              s@(MetaS y _) <- TCMT IO Sort
    forall (m :: * -> *). MonadMetaSolver m => m Sort
    newSortMeta
              return (y, Sort s)
            Just Type
    _A -> do
              let _Aρ :: Type
    _Aρ = Substitution' (SubstArg Type) -> Type -> Type
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg Type)
    ρ Type
    _A
              RunMetaOccursCheck
    -> String -> Comparison -> Type -> TCM (MetaId, Term)
    forall (m :: * -> *).
    MonadMetaSolver m =>
    RunMetaOccursCheck
    -> String -> Comparison -> Type -> m (MetaId, Term)
    newNamedValueMeta RunMetaOccursCheck
    DontRunMetaOccursCheck
                                (MetaInfo -> String
    miNameSuggestion (MetaInfo -> String) -> MetaInfo -> String
    forall a b. (a -> b) -> a -> b
    $ MetaVariable -> MetaInfo
    mvInfo MetaVariable
    mv)
                                (Judgement MetaId -> Comparison
    forall a. Judgement a -> Comparison
    jComparison (Judgement MetaId -> Comparison) -> Judgement MetaId -> Comparison
    forall a b. (a -> b) -> a -> b
    $ MetaVariable -> Judgement MetaId
    mvJudgement MetaVariable
    mv) Type
    _Aρ

        -- If x is a hole, update the hole to point to y instead.
        setInteractionPoint :: MetaId -> MetaId -> TCMT IO ()
    setInteractionPoint MetaId
    x MetaId
    y =
          Maybe InteractionId -> (InteractionId -> TCMT IO ()) -> TCMT IO ()
    forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
    whenJust (MetaId -> Map MetaId InteractionId -> Maybe InteractionId
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup MetaId
    x Map MetaId InteractionId
    interactionPoints) (InteractionId -> MetaId -> TCMT IO ()
    forall (m :: * -> *).
    MonadInteractionPoints m =>
    InteractionId -> MetaId -> m ()
    `connectInteractionPoint` MetaId
    y)

        doPrune :: MetaId -> MetaVariable -> Maybe Type -> Term -> Term -> TCM ()
        doPrune :: MetaId -> MetaVariable -> Maybe Type -> Term -> Term -> TCMT IO ()
    doPrune MetaId
    x MetaVariable
    mv Maybe Type
    mt Term
    v Term
    u =
          case Maybe Type
    mt of
            Maybe Type
    _ | Bool
    isOpen -> CompareDirection
    -> MetaId -> Args -> Term -> CompareAs -> TCMT IO ()
    assign CompareDirection
    DirEq MetaId
    x (Term -> Args
    getArgs Term
    v) Term
    u (CompareAs -> TCMT IO ()) -> CompareAs -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ CompareAs -> (Type -> CompareAs) -> Maybe Type -> CompareAs
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe CompareAs
    AsTypes Type -> CompareAs
    AsTermsOf Maybe Type
    mt
            Maybe Type
    Nothing    -> Sort -> Sort -> TCMT IO ()
    forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
    equalSort (Term -> Sort
    unwrapSort Term
    v) (Term -> Sort
    unwrapSort Term
    u)
            Just Type
    t     -> Type -> Term -> Term -> TCMT IO ()
    forall (m :: * -> *).
    MonadConversion m =>
    Type -> Term -> Term -> m ()
    equalTerm Type
    t Term
    v Term
    u
          where
            isOpen :: Bool
    isOpen = MetaInstantiation -> Bool
    isOpenMeta (MetaInstantiation -> Bool) -> MetaInstantiation -> Bool
    forall a b. (a -> b) -> a -> b
    $ MetaVariable -> MetaInstantiation
    mvInstantiation MetaVariable
    mv
            getArgs :: Term -> Args
    getArgs = \case
                Sort (MetaS MetaId
    _ Elims
    es) -> Args -> Maybe Args -> Args
    forall a. a -> Maybe a -> a
    fromMaybe Args
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe Args
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es
                MetaV MetaId
    _ Elims
    es        -> Args -> Maybe Args -> Args
    forall a. a -> Maybe a -> a
    fromMaybe Args
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe Args
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es
                Term
    _                 -> Args
    forall a. HasCallStack => a
    __IMPOSSIBLE__
            unwrapSort :: Term -> Sort
    unwrapSort (Sort Sort
    s) = Sort
    s
            unwrapSort Term
    _        = Sort
    forall a. HasCallStack => a
    __IMPOSSIBLE__

        niceError :: MetaId -> Term -> TCErr -> TCMT IO ()
    niceError MetaId
    x Term
    u TCErr
    err = do
          u <- Term -> TCMT IO Term
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull Term
    u
          let err' = case TCErr
    err of
                       TypeError{tcErrClosErr :: TCErr -> Closure TypeError
    tcErrClosErr = Closure TypeError
    cl} ->
                         -- Remove the 'when' part from the error since it's most like the same as ours.
                         TCErr
    err{ tcErrClosErr = cl{ clEnv = (clEnv cl) { envCall = Nothing } } }
                       TCErr
    _ -> TCErr
    err
              telList = Telescope -> [Dom (String, Type)]
    forall t. Tele (Dom t) -> [Dom (String, t)]
    telToList Telescope
    genTel
              names   = (Dom (String, Type) -> String) -> [Dom (String, Type)] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map ((String, Type) -> String
    forall a b. (a, b) -> a
    fst ((String, Type) -> String)
    -> (Dom (String, Type) -> (String, Type))
    -> Dom (String, Type)
    -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom (String, Type) -> (String, Type)
    forall t e. Dom' t e -> e
    unDom) [Dom (String, Type)]
    telList
              late    = (Dom (String, Type) -> String) -> [Dom (String, Type)] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map ((String, Type) -> String
    forall a b. (a, b) -> a
    fst ((String, Type) -> String)
    -> (Dom (String, Type) -> (String, Type))
    -> Dom (String, Type)
    -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom (String, Type) -> (String, Type)
    forall t e. Dom' t e -> e
    unDom) ([Dom (String, Type)] -> [String])
    -> [Dom (String, Type)] -> [String]
    forall a b. (a -> b) -> a -> b
    $ (Dom (String, Type) -> Bool)
    -> [Dom (String, Type)] -> [Dom (String, Type)]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Any -> Bool
    getAny (Any -> Bool)
    -> (Dom (String, Type) -> Any) -> Dom (String, Type) -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (MetaId -> Any) -> Dom (String, Type) -> Any
    forall m. Monoid m => (MetaId -> m) -> Dom (String, Type) -> m
    forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
    allMetas (Bool -> Any
    Any (Bool -> Any) -> (MetaId -> Bool) -> MetaId -> Any
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (MetaId -> MetaId -> Bool
    forall a. Eq a => a -> a -> Bool
    == MetaId
    x))) [Dom (String, Type)]
    telList
              projs (Proj ProjOrigin
    _ QName
    q)
                | QName
    q QName -> [QName] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [QName]
    genRecFields
                , Just String
    y <- QName -> Maybe String
    getGeneralizedFieldName QName
    q
                = String -> Set String
    forall a. a -> Set a
    Set.singleton String
    y
              projs Elim' Term
    _ = Set String
    forall a. Set a
    Set.empty
              early = ((Term -> Set String) -> Term -> Set String)
    -> Term -> (Term -> Set String) -> Set String
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (Term -> Set String) -> Term -> Set String
    forall m. Monoid m => (Term -> m) -> Term -> m
    forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
    foldTerm Term
    u \case
                      Var Int
    _ Elims
    es   -> (Elim' Term -> Set String) -> Elims -> Set String
    forall m a. Monoid m => (a -> m) -> [a] -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap Elim' Term -> Set String
    projs Elims
    es
                      Def QName
    _ Elims
    es   -> (Elim' Term -> Set String) -> Elims -> Set String
    forall m a. Monoid m => (a -> m) -> [a] -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap Elim' Term -> Set String
    projs Elims
    es
                      MetaV MetaId
    _ Elims
    es -> (Elim' Term -> Set String) -> Elims -> Set String
    forall m a. Monoid m => (a -> m) -> [a] -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap Elim' Term -> Set String
    projs Elims
    es
                      Term
    _          -> Set String
    forall a. Set a
    Set.empty
              commas []       = String
    forall a. HasCallStack => a
    __IMPOSSIBLE__
              commas [String
    x]      = String
    x
              commas [String
    x, String
    y]   = String
    x String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ", and " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    y
              commas (String
    x : [String]
    xs) = String
    x String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ", " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    commas [String]
    xs
              cause = String
    "There were unsolved constraints that obscured the " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++
                      String
    "dependencies between the generalized variables."
              solution = String
    "The most reliable solution is to provide enough information to make the dependencies " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++
                         String
    "clear, but simply mentioning the variables in the right order should also work."
              order = [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    fwords String
    "Dependency analysis suggested this (likely incorrect) order:",
                            Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    fwords ([String] -> String
    unwords [String]
    names) ]
              guess = [String] -> String
    unwords
                [ String
    "After constraint solving it looks like", [String] -> String
    commas [String]
    late
                , String
    "actually"
                , [String]
    -> (String -> String) -> (String -> String) -> String -> String
    forall a c. Sized a => a -> c -> c -> c
    singPlural [String]
    late (String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> String
    "s") String -> String
    forall a. a -> a
    id String
    "depend"  -- NB: this is a singular "s"
                , String
    "on", [String] -> String
    commas ([String] -> String) -> [String] -> String
    forall a b. (a -> b) -> a -> b
    $ Set String -> [String]
    forall a. Set a -> [a]
    Set.toList Set String
    early
                ]
          genericDocError =<< vcat
            [ fwords $ "Variable generalization failed."
            , nest 2 $ sep ["- Probable cause", nest 4 $ fwords cause]
            , nest 2 $ sep ["- Suggestion", nest 4 $ fwords solution]
            , nest 2 $ sep $ ["- Further information"
                             , nest 2 $ "-" <+> order ] ++
                             [ nest 2 $ "-" <+> fwords guess | not (null late), not (null early) ] ++
                             [ nest 2 $ "-" <+> sep [ fwords "The dependency error is", prettyTCM err' ] ]
            ]

        addNamedVariablesToScope :: t ContextEntry -> TCMT IO ()
    addNamedVariablesToScope t ContextEntry
    cxt =
          t ContextEntry -> (ContextEntry -> TCMT IO ()) -> TCMT IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ t ContextEntry
    cxt ((ContextEntry -> TCMT IO ()) -> TCMT IO ())
    -> (ContextEntry -> TCMT IO ()) -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ \ (CtxVar Name
    x Dom Type
    _) -> do
            -- Recognize named variables by lack of '.' (TODO: hacky!)
            String -> Int -> String -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> String -> m ()
    reportSLn String
    "tc.generalize.eta.scope" Int
    40 (String -> TCMT IO ()) -> String -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ String
    "Adding (or not) " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Name -> String
    forall a. Pretty a => a -> String
    prettyShow (Name -> Name
    nameConcrete Name
    x) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " to the scope"
            Bool -> TCMT IO () -> TCMT IO ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    when (Char
    '.' Char -> String -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `notElem` Name -> String
    forall a. Pretty a => a -> String
    prettyShow (Name -> Name
    nameConcrete Name
    x)) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ do
              String -> Int -> String -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> String -> m ()
    reportSLn String
    "tc.generalize.eta.scope" Int
    40 String
    "  (added)"
              BindingSource -> Name -> Name -> TCMT IO ()
    bindVariable BindingSource
    LambdaBound (Name -> Name
    nameConcrete Name
    x) Name
    x

    -- | Create a substition from a context where the i first record fields are variables to a context
    --   where you have a single variable of the record type. Packs up the field variables in a record
    --   constructor and pads with __DUMMY_TERM__s for the missing fields. Important that you apply this
    --   to terms that only projects the defined fields from the record variable.
    --   Used with partial record values when building the telescope of generalized variables in which
    --   case we have done the dependency analysis that guarantees it is safe.
    unpackSub :: ConHead -> [ArgInfo] -> Int -> Substitution
    unpackSub :: ConHead -> [ArgInfo] -> Int -> Substitution
    unpackSub ConHead
    con [ArgInfo]
    infos Int
    i = Substitution
    recSub
      where
        ar :: Int
    ar = [ArgInfo] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [ArgInfo]
    infos
        appl :: ArgInfo -> a -> Elim' a
    appl ArgInfo
    info a
    v = Arg a -> Elim' a
    forall a. Arg a -> Elim' a
    Apply (ArgInfo -> a -> Arg a
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    info a
    v)
        recVal :: Term
    recVal = ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    con ConInfo
    ConOSystem (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ (ArgInfo -> Term -> Elim' Term) -> [ArgInfo] -> [Term] -> Elims
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith ArgInfo -> Term -> Elim' Term
    forall {a}. ArgInfo -> a -> Elim' a
    appl [ArgInfo]
    infos ([Term] -> Elims) -> [Term] -> Elims
    forall a b. (a -> b) -> a -> b
    $ [Int -> Term
    var Int
    j | Int
    j <- [Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1, Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    2..Int
    0]] [Term] -> [Term] -> [Term]
    forall a. [a] -> [a] -> [a]
    ++ Int -> Term -> [Term]
    forall a. Int -> a -> [a]
    replicate (Int
    ar Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    i) Term
    HasCallStack => Term
    __DUMMY_TERM__

        -- want: Γ Δᵢ ⊢ recSub i : Γ (r : R)
        -- have:
        -- Γ Δᵢ ⊢ recVal i :# σ : Θ (r : R),  if Γ Δᵢ ⊢ σ : Θ
        -- Γ Δᵢ ⊢ WkS i IdS : Γ
        recSub :: Substitution
    recSub = Term
    recVal Term -> Substitution -> Substitution
    forall a. a -> Substitution' a -> Substitution' a
    :# Int -> Substitution -> Substitution
    forall a. Int -> Substitution' a -> Substitution' a
    Wk Int
    i Substitution
    forall a. Substitution' a
    IdS

    -- | Takes the list of types
    --    A₁ []
    --    A₂ [r.f₁]
    --    A₃ [r.f₂, r.f₃]
    --    ...
    --   And builds the telescope
    --    (x₁ : A₁ [ r := c _       .. _ ])
    --    (x₂ : A₂ [ r := c x₁ _    .. _ ])
    --    (x₃ : A₃ [ r := c x₁ x₂ _ .. _ ])
    --    ...
    buildGeneralizeTel :: ConHead -> [(Arg MetaNameSuggestion, Type)] -> Telescope
    buildGeneralizeTel :: ConHead -> [(Arg String, Type)] -> Telescope
    buildGeneralizeTel ConHead
    con [(Arg String, Type)]
    xs = Int -> [(Arg String, Type)] -> Telescope
    go Int
    0 [(Arg String, Type)]
    xs
      where
        infos :: [ArgInfo]
    infos = ((Arg String, Type) -> ArgInfo)
    -> [(Arg String, Type)] -> [ArgInfo]
    forall a b. (a -> b) -> [a] -> [b]
    map (Arg String -> ArgInfo
    forall e. Arg e -> ArgInfo
    argInfo (Arg String -> ArgInfo)
    -> ((Arg String, Type) -> Arg String)
    -> (Arg String, Type)
    -> ArgInfo
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Arg String, Type) -> Arg String
    forall a b. (a, b) -> a
    fst) [(Arg String, Type)]
    xs
        recSub :: Int -> Substitution
    recSub Int
    i = ConHead -> [ArgInfo] -> Int -> Substitution
    unpackSub ConHead
    con [ArgInfo]
    infos Int
    i
        go :: Int -> [(Arg String, Type)] -> Telescope
    go Int
    _ [] = Telescope
    forall a. Tele a
    EmptyTel
        go Int
    i ((Arg String
    name, Type
    ty) : [(Arg String, Type)]
    xs) = Dom Type -> Abs Telescope -> Telescope
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel (Type -> Dom Type
    dom Type
    ty') (Abs Telescope -> Telescope) -> Abs Telescope -> Telescope
    forall a b. (a -> b) -> a -> b
    $ String -> Telescope -> Abs Telescope
    forall a. String -> a -> Abs a
    Abs (Arg String -> String
    forall e. Arg e -> e
    unArg Arg String
    name) (Telescope -> Abs Telescope) -> Telescope -> Abs Telescope
    forall a b. (a -> b) -> a -> b
    $ Int -> [(Arg String, Type)] -> Telescope
    go (Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1) [(Arg String, Type)]
    xs
          where ty' :: Type
    ty' = Substitution' (SubstArg Type) -> Type -> Type
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst (Int -> Substitution
    recSub Int
    i) Type
    ty
                dom :: Type -> Dom Type
    dom = ArgInfo -> String -> Type -> Dom Type
    forall a. ArgInfo -> String -> a -> Dom a
    defaultNamedArgDom (Arg String -> ArgInfo
    forall a. LensArgInfo a => a -> ArgInfo
    getArgInfo Arg String
    name) (Arg String -> String
    forall e. Arg e -> e
    unArg Arg String
    name)

    -- | Create metas for all used generalizable variables and their dependencies.
    createGenValues ::
         Set QName
           -- ^ Possibly empty set of generalizable variables.
      -> TCM (Map MetaId QName, Map QName GeneralizedValue)
           -- ^ A bimap from generalizable variables to their metas.
    createGenValues :: Set QName -> TCM (Map MetaId QName, Map QName GeneralizedValue)
    createGenValues Set QName
    s = do
      genvals <- Lens' TCEnv DoGeneralize
    -> (DoGeneralize -> DoGeneralize)
    -> TCMT IO [(QName, (MetaId, GeneralizedValue))]
    -> TCMT IO [(QName, (MetaId, GeneralizedValue))]
    forall (m :: * -> *) a b.
    MonadTCEnv m =>
    Lens' TCEnv a -> (a -> a) -> m b -> m b
    locallyTC (DoGeneralize -> f DoGeneralize) -> TCEnv -> f TCEnv
    Lens' TCEnv DoGeneralize
    eGeneralizeMetas (DoGeneralize -> DoGeneralize -> DoGeneralize
    forall a b. a -> b -> a
    const DoGeneralize
    YesGeneralizeVar) (TCMT IO [(QName, (MetaId, GeneralizedValue))]
     -> TCMT IO [(QName, (MetaId, GeneralizedValue))])
    -> TCMT IO [(QName, (MetaId, GeneralizedValue))]
    -> TCMT IO [(QName, (MetaId, GeneralizedValue))]
    forall a b. (a -> b) -> a -> b
    $
        [QName]
    -> (QName -> TCMT IO (QName, (MetaId, GeneralizedValue)))
    -> TCMT IO [(QName, (MetaId, GeneralizedValue))]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM ((QName -> QName -> Ordering) -> [QName] -> [QName]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    sortBy (Range -> Range -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (Range -> Range -> Ordering)
    -> (QName -> Range) -> QName -> QName -> Ordering
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` QName -> Range
    forall a. HasRange a => a -> Range
    getRange) ([QName] -> [QName]) -> [QName] -> [QName]
    forall a b. (a -> b) -> a -> b
    $ Set QName -> [QName]
    forall a. Set a -> [a]
    Set.toList Set QName
    s) \ QName
    x -> do
          (QName
    x,) ((MetaId, GeneralizedValue) -> (QName, (MetaId, GeneralizedValue)))
    -> TCMT IO (MetaId, GeneralizedValue)
    -> TCMT IO (QName, (MetaId, GeneralizedValue))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCMT IO (MetaId, GeneralizedValue)
    createGenValue QName
    x
      let metaMap = (QName -> QName -> QName) -> [(MetaId, QName)] -> Map MetaId QName
    forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
    Map.fromListWith QName -> QName -> QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__ [ (MetaId
    m, QName
    x) | (QName
    x, (MetaId
    m, GeneralizedValue
    _)) <- [(QName, (MetaId, GeneralizedValue))]
    genvals ]
          nameMap = (GeneralizedValue -> GeneralizedValue -> GeneralizedValue)
    -> [(QName, GeneralizedValue)] -> Map QName GeneralizedValue
    forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
    Map.fromListWith GeneralizedValue -> GeneralizedValue -> GeneralizedValue
    forall a. HasCallStack => a
    __IMPOSSIBLE__ [ (QName
    x, GeneralizedValue
    v) | (QName
    x, (MetaId
    _, GeneralizedValue
    v)) <- [(QName, (MetaId, GeneralizedValue))]
    genvals ]
      return (metaMap, nameMap)

    -- | Create a generalizable meta for a generalizable variable.
    createGenValue ::
         QName
           -- ^ Name of a generalizable variable.
      -> TCM (MetaId, GeneralizedValue)
           -- ^ Generated metavariable and its representation as typed term.
    createGenValue :: QName -> TCMT IO (MetaId, GeneralizedValue)
    createGenValue QName
    x = QName
    -> TCMT IO (MetaId, GeneralizedValue)
    -> TCMT IO (MetaId, GeneralizedValue)
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange QName
    x (TCMT IO (MetaId, GeneralizedValue)
     -> TCMT IO (MetaId, GeneralizedValue))
    -> TCMT IO (MetaId, GeneralizedValue)
    -> TCMT IO (MetaId, GeneralizedValue)
    forall a b. (a -> b) -> a -> b
    $ do
      cp  <- Lens' TCEnv CheckpointId -> TCMT IO CheckpointId
    forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
    viewTC (CheckpointId -> f CheckpointId) -> TCEnv -> f TCEnv
    Lens' TCEnv CheckpointId
    eCurrentCheckpoint

      def <- instantiateDef =<< getConstInfo x
      let
        nGen = case Definition -> Defn
    theDef Definition
    def of
          GeneralizableVar NumGeneralizableArgs
    NoGeneralizableArgs       -> Int
    0
          GeneralizableVar (SomeGeneralizableArgs Int
    n) -> Int
    n
          Defn
    _ -> Int
    forall a. HasCallStack => a
    __IMPOSSIBLE__

        ty         = Definition -> Type
    defType Definition
    def
        TelV tel _ = telView' ty
        -- Generalizable variables are never explicit, so if they're given as
        -- explicit we default to hidden.
        argTel     = [Dom (String, Type)] -> Telescope
    telFromList ([Dom (String, Type)] -> Telescope)
    -> [Dom (String, Type)] -> Telescope
    forall a b. (a -> b) -> a -> b
    $ (Dom (String, Type) -> Dom (String, Type))
    -> [Dom (String, Type)] -> [Dom (String, Type)]
    forall a b. (a -> b) -> [a] -> [b]
    map Dom (String, Type) -> Dom (String, Type)
    forall a. LensHiding a => a -> a
    hideExplicit ([Dom (String, Type)] -> [Dom (String, Type)])
    -> [Dom (String, Type)] -> [Dom (String, Type)]
    forall a b. (a -> b) -> a -> b
    $ Int -> [Dom (String, Type)] -> [Dom (String, Type)]
    forall a. Int -> [a] -> [a]
    take Int
    nGen ([Dom (String, Type)] -> [Dom (String, Type)])
    -> [Dom (String, Type)] -> [Dom (String, Type)]
    forall a b. (a -> b) -> a -> b
    $ Telescope -> [Dom (String, Type)]
    forall t. Tele (Dom t) -> [Dom (String, t)]
    telToList Telescope
    tel

      args <- newTelMeta argTel
      metaType <- piApplyM ty args

      let name = Name -> String
    forall a. Pretty a => a -> String
    prettyShow (Name -> String) -> Name -> String
    forall a b. (a -> b) -> a -> b
    $ Name -> Name
    nameConcrete (Name -> Name) -> Name -> Name
    forall a b. (a -> b) -> a -> b
    $ QName -> Name
    qnameName QName
    x
      (m, term) <- newNamedValueMeta DontRunMetaOccursCheck name CmpLeq metaType

      -- Freeze the meta to prevent named generalizable metas from being
      -- instantiated, and set the quantity of the meta to the declared
      -- quantity of the generalisable variable.
      updateMetaVar m $ \ MetaVariable
    mv ->
        Modality -> MetaVariable -> MetaVariable
    forall a. LensModality a => Modality -> a -> a
    setModality (ArgInfo -> Modality
    forall a. LensModality a => a -> Modality
    getModality (Definition -> ArgInfo
    defArgInfo Definition
    def)) (MetaVariable -> MetaVariable) -> MetaVariable -> MetaVariable
    forall a b. (a -> b) -> a -> b
    $
        MetaVariable
    mv { mvFrozen = Frozen }

      -- Set up names of arg metas
      forM_ (zip3 [1..] (map unArg args) (telToList argTel)) $ \ case
        (Integer
    i, MetaV MetaId
    m Elims
    _, Dom{unDom :: forall t e. Dom' t e -> e
    unDom = (String
    x, Type
    _)}) -> do
          let suf :: String -> String
    suf String
    "_" = Integer -> String
    forall a. Show a => a -> String
    show Integer
    i
              suf String
    ""  = Integer -> String
    forall a. Show a => a -> String
    show Integer
    i
              suf String
    x   = String
    x
          MetaId -> String -> TCMT IO ()
    forall (m :: * -> *). MonadMetaSolver m => MetaId -> String -> m ()
    setMetaNameSuggestion MetaId
    m (String
    name String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "." String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    suf String
    x)
        (Integer, Term, Dom (String, Type))
    _ -> () -> TCMT IO ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()  -- eta expanded

      -- Update the ArgInfos for the named meta. The argument metas are
      -- created with the correct ArgInfo.
      setMetaGeneralizableArgInfo m $ hideExplicit (defArgInfo def)

      reportSDoc "tc.generalize" 50 $ vcat
        [ "created metas for generalized variable" <+> prettyTCM x
        , nest 2 $ "top  =" <+> prettyTCM term
        , nest 2 $ "args =" <+> prettyTCM args ]

      case term of
        MetaV{} -> () -> TCMT IO ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        Term
    _       -> Doc -> TCMT IO ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    Doc -> m a
    genericDocError (Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< (TCMT IO Doc
    "Cannot generalize over" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    x TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "of eta-expandable type") TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <?>
                                        Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    metaType
      return . (m,) $ GeneralizedValue
        { genvalCheckpoint = cp
        , genvalTerm       = term
        , genvalType       = metaType
        }

      where
        hideExplicit :: LensHiding a => a -> a
        hideExplicit :: forall a. LensHiding a => a -> a
    hideExplicit = (a -> Bool) -> (a -> a) -> a -> a
    forall b a. IsBool b => (a -> b) -> (a -> a) -> a -> a
    applyWhenIts a -> Bool
    forall a. LensHiding a => a -> Bool
    visible a -> a
    forall a. LensHiding a => a -> a
    hide

    -- | Create a not-yet correct record type for the generalized telescope. It's not yet correct since
    --   we haven't computed the telescope yet, and we need the record type to do it.
    createGenRecordType :: Type -> [MetaId] -> TCM (QName, ConHead, [QName])
    createGenRecordType :: Type -> [MetaId] -> TCMT IO (QName, ConHead, [QName])
    createGenRecordType genRecMeta :: Type
    genRecMeta@(El Sort
    genRecSort Term
    _) [MetaId]
    sortedMetas = TCMT IO (QName, ConHead, [QName])
    -> TCMT IO (QName, ConHead, [QName])
    forall a. TCM a -> TCM a
    noMutualBlock (TCMT IO (QName, ConHead, [QName])
     -> TCMT IO (QName, ConHead, [QName]))
    -> TCMT IO (QName, ConHead, [QName])
    -> TCMT IO (QName, ConHead, [QName])
    forall a b. (a -> b) -> a -> b
    $ do
      current <- TCMT IO ModuleName
    forall (m :: * -> *). MonadTCEnv m => m ModuleName
    currentModule
      let freshQName String
    s = ModuleName -> Name -> QName
    qualify ModuleName
    current (Name -> QName) -> TCMT IO Name -> TCMT IO QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> String -> TCMT IO Name
    forall a (m :: * -> *).
    (FreshName a, MonadFresh NameId m) =>
    a -> m Name
    forall (m :: * -> *). MonadFresh NameId m => String -> m Name
    freshName_ (String
    s :: String)
          mkFieldName  = String -> TCMT IO QName
    freshQName (String -> TCMT IO QName)
    -> (String -> String) -> String -> TCMT IO QName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (String
    generalizedFieldName String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++) (String -> TCMT IO QName)
    -> (MetaId -> TCMT IO String) -> MetaId -> TCMT IO QName
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< MetaId -> TCMT IO String
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m String
    getMetaNameSuggestion
      genRecFields <- mapM (defaultDom <.> mkFieldName) sortedMetas
      genRecName   <- freshQName "GeneralizeTel"
      genRecCon    <- freshQName "mkGeneralizeTel" <&> \ QName
    con -> ConHead
                      { conName :: QName
    conName      = QName
    con
                      , conDataRecord :: DataOrRecord
    conDataRecord= PatternOrCopattern -> DataOrRecord
    forall p. p -> DataOrRecord' p
    IsRecord PatternOrCopattern
    CopatternMatching
                      , conInductive :: Induction
    conInductive = Induction
    Inductive
                      , conFields :: [Arg QName]
    conFields    = (Dom QName -> Arg QName) -> [Dom QName] -> [Arg QName]
    forall a b. (a -> b) -> [a] -> [b]
    map Dom QName -> Arg QName
    forall t a. Dom' t a -> Arg a
    argFromDom [Dom QName]
    genRecFields
                      }
      projIx <- succ . size <$> getContext
      erasure <- optErasure <$> pragmaOptions
      inTopContext $ forM_ (zip sortedMetas genRecFields) $ \ (MetaId
    meta, Dom QName
    fld) -> do
        fieldTy <- MetaId -> TCM Type
    forall (m :: * -> *). ReadTCState m => MetaId -> m Type
    getMetaType MetaId
    meta
        let field = Dom QName -> QName
    forall t e. Dom' t e -> e
    unDom Dom QName
    fld
        addConstant' field (getArgInfo fld) fieldTy $ FunctionDefn $
          (emptyFunctionData_ erasure)
            { _funMutual     = Just []
            , _funTerminates = Just True
            , _funProjection = Right Projection
              { projProper   = Just genRecName
              , projOrig     = field
              , projFromType = defaultArg genRecName
              , projIndex    = projIx
              , projLams     = ProjLams [defaultArg "gtel"]
              }
            }
      addConstant' (conName genRecCon) defaultArgInfo __DUMMY_TYPE__ $ -- Filled in later
        Constructor { conPars   = 0
                    , conArity  = length genRecFields
                    , conSrcCon = genRecCon
                    , conData   = genRecName
                    , conAbstr  = ConcreteDef
                    , conComp   = emptyCompKit
                    , conProj   = Nothing
                    , conForced = []
                    , conErased = Nothing
                    , conErasure = erasure
                    , conInline  = False
                    }
      let dummyTel t
    0 = Telescope
    forall a. Tele a
    EmptyTel
          dummyTel t
    n = Dom Type -> Abs Telescope -> Telescope
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel (Type -> Dom Type
    forall a. a -> Dom a
    defaultDom Type
    HasCallStack => Type
    __DUMMY_TYPE__) (Abs Telescope -> Telescope) -> Abs Telescope -> Telescope
    forall a b. (a -> b) -> a -> b
    $ String -> Telescope -> Abs Telescope
    forall a. String -> a -> Abs a
    Abs String
    "_" (Telescope -> Abs Telescope) -> Telescope -> Abs Telescope
    forall a b. (a -> b) -> a -> b
    $ t -> Telescope
    dummyTel (t
    n t -> t -> t
    forall a. Num a => a -> a -> a
    - t
    1)
      addConstant' genRecName defaultArgInfo (sort genRecSort) $
        Record { recPars         = 0
               , recClause       = Nothing
               , recConHead      = genRecCon
               , recNamedCon     = False
               , recFields       = genRecFields
               , recTel          = dummyTel (length genRecFields) -- Filled in later
               , recMutual       = Just []
               , recEtaEquality' = Inferred YesEta
               , recPatternMatching = CopatternMatching
               , recInduction    = Nothing
               , recTerminates   = Just True    -- not recursive
               , recAbstr        = ConcreteDef
               , recComp         = emptyCompKit
               }
      reportSDoc "tc.generalize" 20 $ vcat
        [ text "created genRec" <+> prettyList_ (map (text . prettyShow . unDom) genRecFields) ]
      reportSDoc "tc.generalize" 80 $ vcat
        [ text "created genRec" <+> text (prettyShow genRecFields) ]
      -- Solve the genRecMeta
      args <- getContextArgs
      let genRecTy = Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El Sort
    genRecSort (Term -> Type) -> Term -> Type
    forall a b. (a -> b) -> a -> b
    $ QName -> Elims -> Term
    Def QName
    genRecName (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> Elim' Term) -> Args -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply Args
    args
      noConstraints $ equalType genRecTy genRecMeta
      return (genRecName, genRecCon, map unDom genRecFields)

    -- | Once we have the generalized telescope we can fill in the missing details of the record type.
    fillInGenRecordDetails :: QName -> ConHead -> [QName] -> Type -> Telescope -> TCM ()
    fillInGenRecordDetails :: QName -> ConHead -> [QName] -> Type -> Telescope -> TCMT IO ()
    fillInGenRecordDetails QName
    name ConHead
    con [QName]
    fields Type
    recTy Telescope
    fieldTel = do
      cxtTel <- (Dom Type -> Dom Type) -> Telescope -> Telescope
    forall a b. (a -> b) -> Tele a -> Tele b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Dom Type -> Dom Type
    forall a. (LensHiding a, LensRelevance a) => a -> a
    hideAndRelParams (Telescope -> Telescope) -> TCMT IO Telescope -> TCMT IO Telescope
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO Telescope
    forall (m :: * -> *). MonadTCEnv m => m Telescope
    getContextTelescope
      let fullTel = Telescope
    cxtTel Telescope -> Telescope -> Telescope
    forall t. Abstract t => Telescope -> t -> t
    `abstract` Telescope
    fieldTel
      -- Field types
      let mkFieldTypes [] Telescope
    EmptyTel = []
          mkFieldTypes (QName
    fld : [QName]
    flds) (ExtendTel Dom Type
    ty Abs Telescope
    ftel) =
              Telescope -> Type -> Type
    forall t. Abstract t => Telescope -> t -> t
    abstract Telescope
    cxtTel (Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El Sort
    s (Term -> Type) -> Term -> Type
    forall a b. (a -> b) -> a -> b
    $ Dom Type -> Abs Type -> Term
    Pi (Type -> Dom Type
    forall a. a -> Dom a
    defaultDom Type
    recTy) (String -> Type -> Abs Type
    forall a. String -> a -> Abs a
    Abs String
    "r" (Type -> Abs Type) -> Type -> Abs Type
    forall a b. (a -> b) -> a -> b
    $ Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    ty)) Type -> [Type] -> [Type]
    forall a. a -> [a] -> [a]
    :
              [QName] -> Telescope -> [Type]
    mkFieldTypes [QName]
    flds (Abs Telescope -> SubstArg Telescope -> Telescope
    forall a. Subst a => Abs a -> SubstArg a -> a
    absApp Abs Telescope
    ftel Term
    SubstArg Telescope
    proj)
            where
              s :: Sort
    s = Dom Type -> Abs Type -> Sort
    mkPiSort (Type -> Dom Type
    forall a. a -> Dom a
    defaultDom Type
    recTy) (String -> Type -> Abs Type
    forall a. String -> a -> Abs a
    Abs String
    "r" (Type -> Abs Type) -> Type -> Abs Type
    forall a b. (a -> b) -> a -> b
    $ Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    ty)
              proj :: Term
    proj = Int -> Elims -> Term
    Var Int
    0 [ProjOrigin -> QName -> Elim' Term
    forall a. ProjOrigin -> QName -> Elim' a
    Proj ProjOrigin
    ProjSystem QName
    fld]
          mkFieldTypes [QName]
    _ Telescope
    _ = [Type]
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      let fieldTypes = [QName] -> Telescope -> [Type]
    mkFieldTypes [QName]
    fields (Int -> Telescope -> Telescope
    forall a. Subst a => Int -> a -> a
    raise Int
    1 Telescope
    fieldTel)
      reportSDoc "tc.generalize" 40 $ text "Field types:" <+> inTopContext (nest 2 $ vcat $ map prettyTCM fieldTypes)
      zipWithM_ setType fields fieldTypes
      -- Constructor type
      let conType = Telescope
    fullTel Telescope -> Type -> Type
    forall t. Abstract t => Telescope -> t -> t
    `abstract` Int -> Type -> Type
    forall a. Subst a => Int -> a -> a
    raise (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    fieldTel) Type
    recTy
      reportSDoc "tc.generalize" 40 $ text "Final genRecCon type:" <+> inTopContext (prettyTCM conType)
      setType (conName con) conType
      -- Record telescope: Includes both parameters and fields.
      modifyGlobalDefinition name $ set (lensTheDef . lensRecord . lensRecTel) fullTel
      -- #7380: Also add clauses to the field definitions
      let n      = [QName] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [QName]
    fields
          cpi    = ConPatternInfo
    noConPatternInfo
          fldTys = (Dom (String, Type) -> Arg Type)
    -> [Dom (String, Type)] -> [Arg Type]
    forall a b. (a -> b) -> [a] -> [b]
    map (((String, Type) -> Type) -> Arg (String, Type) -> Arg Type
    forall a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (String, Type) -> Type
    forall a b. (a, b) -> b
    snd (Arg (String, Type) -> Arg Type)
    -> (Dom (String, Type) -> Arg (String, Type))
    -> Dom (String, Type)
    -> Arg Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom (String, Type) -> Arg (String, Type)
    forall t a. Dom' t a -> Arg a
    argFromDom) ([Dom (String, Type)] -> [Arg Type])
    -> [Dom (String, Type)] -> [Arg Type]
    forall a b. (a -> b) -> a -> b
    $ Telescope -> [Dom (String, Type)]
    forall t. Tele (Dom t) -> [Dom (String, t)]
    telToList Telescope
    fieldTel
          conPat = ConHead
    -> ConPatternInfo
    -> [NamedArg (Pattern' DBPatVar)]
    -> Pattern' DBPatVar
    forall x.
    ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
    ConP ConHead
    con ConPatternInfo
    cpi [ (Pattern' DBPatVar -> Named_ (Pattern' DBPatVar))
    -> Arg (Pattern' DBPatVar) -> NamedArg (Pattern' DBPatVar)
    forall a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Pattern' DBPatVar -> Named_ (Pattern' DBPatVar)
    forall a name. a -> Named name a
    unnamed (Arg (Pattern' DBPatVar) -> NamedArg (Pattern' DBPatVar))
    -> Arg (Pattern' DBPatVar) -> NamedArg (Pattern' DBPatVar)
    forall a b. (a -> b) -> a -> b
    $ DBPatVar -> Pattern' DBPatVar
    forall a. a -> Pattern' a
    varP (String -> Int -> DBPatVar
    DBPatVar String
    "x" Int
    i) Pattern' DBPatVar -> Arg Type -> Arg (Pattern' DBPatVar)
    forall a b. a -> Arg b -> Arg a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Arg Type
    arg | (Int
    i, Arg Type
    arg) <- [Int] -> [Arg Type] -> [(Int, Arg Type)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip (Int -> [Int]
    forall a. Integral a => a -> [a]
    downFrom Int
    n) [Arg Type]
    fldTys ]
      forM_ (zip3 (downFrom n) fields fldTys) \ (Int
    i, QName
    fld, Arg Type
    fldTy) -> do
        QName -> ([Clause] -> [Clause]) -> TCMT IO ()
    modifyFunClauses QName
    fld \ [Clause]
    _ ->
          [Clause
            { clauseLHSRange :: Range
    clauseLHSRange    = Range
    forall a. Range' a
    noRange
            , clauseFullRange :: Range
    clauseFullRange   = Range
    forall a. Range' a
    noRange
            , clauseTel :: Telescope
    clauseTel         = Telescope
    fieldTel
            , namedClausePats :: [NamedArg (Pattern' DBPatVar)]
    namedClausePats   = [Pattern' DBPatVar -> NamedArg (Pattern' DBPatVar)
    forall a. a -> NamedArg a
    defaultNamedArg Pattern' DBPatVar
    conPat]
            , clauseBody :: Maybe Term
    clauseBody        = Term -> Maybe Term
    forall a. a -> Maybe a
    Just (Term -> Maybe Term) -> Term -> Maybe Term
    forall a b. (a -> b) -> a -> b
    $ Int -> Term
    var Int
    i
            , clauseType :: Maybe (Arg Type)
    clauseType        = Arg Type -> Maybe (Arg Type)
    forall a. a -> Maybe a
    Just (Arg Type -> Maybe (Arg Type)) -> Arg Type -> Maybe (Arg Type)
    forall a b. (a -> b) -> a -> b
    $ Int -> Arg Type -> Arg Type
    forall a. Subst a => Int -> a -> a
    raise (Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1) Arg Type
    fldTy
            , clauseCatchall :: Catchall
    clauseCatchall    = Catchall
    forall a. Null a => a
    empty
            , clauseRecursive :: Maybe Bool
    clauseRecursive   = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    False
            , clauseUnreachable :: Maybe Bool
    clauseUnreachable = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    False
            , clauseEllipsis :: ExpandedEllipsis
    clauseEllipsis    = ExpandedEllipsis
    NoEllipsis
            , clauseWhereModule :: Maybe ModuleName
    clauseWhereModule = Maybe ModuleName
    forall a. Maybe a
    Nothing
            }]
      where
        setType :: QName -> Type -> m ()
    setType QName
    q Type
    ty = QName -> (Definition -> Definition) -> m ()
    forall (m :: * -> *).
    MonadTCState m =>
    QName -> (Definition -> Definition) -> m ()
    modifyGlobalDefinition QName
    q ((Definition -> Definition) -> m ())
    -> (Definition -> Definition) -> m ()
    forall a b. (a -> b) -> a -> b
    $ \ Definition
    d -> Definition
    d { defType = ty }