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

    import Prelude hiding (null)

    import Control.Arrow (first)
    import Control.Monad
    import Control.Monad.Except

    import qualified Data.IntMap as IntMap
    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 Data.List (partition, sortBy)
    import Data.Monoid
    import Data.Function (on)

    import Agda.Syntax.Common
    import Agda.Syntax.Concrete.Name (LensInScope(..))
    import Agda.Syntax.Position
    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.Irrelevance
    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.Functor
    import Agda.Utils.Impossible
    import Agda.Utils.List   (hasElem)
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Null
    import Agda.Utils.Size
    import Agda.Utils.Permutation
    import Agda.Utils.Pretty (prettyShow)

    -- | 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
      (([Name]
    cxtNames, Telescope
    tel, [(Name, (Term, Dom Type))]
    letbinds), Map MetaId QName
    namedMetas, MetaStore
    allmetas) <-
        Set QName
    -> TCM ([Name], Telescope, [(Name, (Term, Dom Type))])
    -> TCM
         (([Name], Telescope, [(Name, (Term, Dom Type))]), Map MetaId QName,
          MetaStore)
    forall a.
    Set QName -> TCM a -> TCM (a, Map MetaId QName, MetaStore)
    createMetasAndTypeCheck Set QName
    s (TCM ([Name], Telescope, [(Name, (Term, Dom Type))])
     -> TCM
          (([Name], Telescope, [(Name, (Term, Dom Type))]), Map MetaId QName,
           MetaStore))
    -> TCM ([Name], Telescope, [(Name, (Term, Dom Type))])
    -> TCM
         (([Name], Telescope, [(Name, (Term, Dom Type))]), Map MetaId QName,
          MetaStore)
    forall a b. (a -> b) -> a -> b
    $ (Telescope -> TCM ([Name], Telescope, [(Name, (Term, Dom Type))]))
    -> TCM ([Name], Telescope, [(Name, (Term, Dom Type))])
    forall a. (Telescope -> TCM a) -> TCM a
    typecheckAction ((Telescope -> TCM ([Name], Telescope, [(Name, (Term, Dom Type))]))
     -> TCM ([Name], Telescope, [(Name, (Term, Dom Type))]))
    -> (Telescope
        -> TCM ([Name], Telescope, [(Name, (Term, Dom Type))]))
    -> TCM ([Name], Telescope, [(Name, (Term, Dom Type))])
    forall a b. (a -> b) -> a -> b
    $ \ Telescope
    tel -> do
          [Dom (Name, Type)]
    cxt <- Int -> [Dom (Name, Type)] -> [Dom (Name, Type)]
    forall a. Int -> [a] -> [a]
    take (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel) ([Dom (Name, Type)] -> [Dom (Name, Type)])
    -> TCMT IO [Dom (Name, Type)] -> TCMT IO [Dom (Name, Type)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO [Dom (Name, Type)]
    forall (m :: * -> *). MonadTCEnv m => m [Dom (Name, Type)]
    getContext
          [(Name, (Term, Dom Type))]
    lbs <- TCMT IO [(Name, (Term, Dom Type))]
    forall (tcm :: * -> *).
    MonadTCM tcm =>
    tcm [(Name, (Term, Dom Type))]
    getLetBindings -- This gives let-bindings valid in the current context
          ([Name], Telescope, [(Name, (Term, Dom Type))])
    -> TCM ([Name], Telescope, [(Name, (Term, Dom Type))])
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Dom (Name, Type) -> Name) -> [Dom (Name, Type)] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Name, Type) -> Name
    forall a b. (a, b) -> a
    fst ((Name, Type) -> Name)
    -> (Dom (Name, Type) -> (Name, Type)) -> Dom (Name, Type) -> Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom (Name, Type) -> (Name, Type)
    forall t e. Dom' t e -> e
    unDom) [Dom (Name, Type)]
    cxt, Telescope
    tel, [(Name, (Term, Dom Type))]
    lbs)
      -- Translate the QName to the corresponding bound variable
      (Telescope
    genTel, [Maybe QName]
    genTelNames, Substitution
    sub) <- Type
    -> Map MetaId QName
    -> MetaStore
    -> TCM (Telescope, [Maybe QName], Substitution)
    forall name.
    Type
    -> Map MetaId name
    -> MetaStore
    -> TCM (Telescope, [Maybe name], Substitution)
    computeGeneralization Type
    genRecMeta Map MetaId QName
    namedMetas MetaStore
    allmetas

      let boundVar :: QName -> Name
    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 Name]
    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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap) QName -> Name
    boundVar [Maybe QName]
    genTelNames

      Telescope
    tel' <- Substitution' (SubstArg Telescope) -> Telescope -> Telescope
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg Telescope)
    sub (Telescope -> Telescope) -> TCMT IO Telescope -> TCMT IO Telescope
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Telescope -> TCMT IO Telescope
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull Telescope
    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 :: c -> f (b, d) -> f (c, d)
    setName c
    name f (b, d)
    d = (b -> c) -> (b, d) -> (c, d)
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (b, d) (c, d)
    first (c -> b -> c
    forall a b. a -> b -> a
    const c
    name) ((b, d) -> (c, d)) -> f (b, d) -> f (c, d)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> f (b, d)
    d
          cxtEntry :: (Maybe Name, Dom' t (b, d)) -> m (Dom' t (Name, d))
    cxtEntry (Maybe Name
    mname, Dom' t (b, d)
    d) = do
              Name
    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
    <$> b -> m Name
    forall a (m :: * -> *).
    (FreshName a, MonadFresh NameId m) =>
    a -> m Name
    freshName_ b
    s) Name -> m Name
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Name
    mname
              Dom' t (Name, d) -> m (Dom' t (Name, d))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Dom' t (Name, d) -> m (Dom' t (Name, d)))
    -> Dom' t (Name, d) -> m (Dom' t (Name, d))
    forall a b. (a -> b) -> a -> b
    $ Name -> Dom' t (b, d) -> Dom' t (Name, d)
    forall {f :: * -> *} {c} {b} {d}.
    Functor f =>
    c -> f (b, d) -> f (c, d)
    setName Name
    name Dom' t (b, d)
    d
            where s :: b
    s  = (b, d) -> b
    forall a b. (a, b) -> a
    fst ((b, d) -> b) -> (b, d) -> b
    forall a b. (a -> b) -> a -> b
    $ Dom' t (b, d) -> (b, d)
    forall t e. Dom' t e -> e
    unDom Dom' t (b, d)
    d
          dropCxt :: Impossible -> m a -> m a
    dropCxt Impossible
    err = Substitution
    -> ([Dom (Name, Type)] -> [Dom (Name, Type)]) -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Substitution
    -> ([Dom (Name, Type)] -> [Dom (Name, Type)]) -> m a -> m a
    updateContext (Impossible -> Int -> Substitution
    forall a. Impossible -> Int -> Substitution' a
    strengthenS Impossible
    err Int
    1) (Int -> [Dom (Name, Type)] -> [Dom (Name, Type)]
    forall a. Int -> [a] -> [a]
    drop Int
    1)
      [Dom (Name, Type)]
    genTelCxt <- Impossible
    -> TCMT IO [Dom (Name, Type)] -> TCMT IO [Dom (Name, Type)]
    forall {m :: * -> *} {a}.
    MonadAddContext m =>
    Impossible -> m a -> m a
    dropCxt Impossible
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (TCMT IO [Dom (Name, Type)] -> TCMT IO [Dom (Name, Type)])
    -> TCMT IO [Dom (Name, Type)] -> TCMT IO [Dom (Name, Type)]
    forall a b. (a -> b) -> a -> b
    $ ((Maybe Name, Dom (String, Type)) -> TCMT IO (Dom (Name, Type)))
    -> [(Maybe Name, Dom (String, Type))] -> TCMT IO [Dom (Name, Type)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (Maybe Name, Dom (String, Type)) -> TCMT IO (Dom (Name, Type))
    forall {m :: * -> *} {b} {t} {d}.
    (FreshName b, MonadFresh NameId m) =>
    (Maybe Name, Dom' t (b, d)) -> m (Dom' t (Name, d))
    cxtEntry ([(Maybe Name, Dom (String, Type))] -> TCMT IO [Dom (Name, Type)])
    -> [(Maybe Name, Dom (String, Type))] -> TCMT IO [Dom (Name, Type)]
    forall a b. (a -> b) -> a -> b
    $ [(Maybe Name, Dom (String, Type))]
    -> [(Maybe Name, Dom (String, Type))]
    forall a. [a] -> [a]
    reverse ([(Maybe Name, Dom (String, Type))]
     -> [(Maybe Name, Dom (String, Type))])
    -> [(Maybe Name, Dom (String, Type))]
    -> [(Maybe Name, Dom (String, Type))]
    forall a b. (a -> b) -> a -> b
    $ [Maybe Name]
    -> [Dom (String, Type)] -> [(Maybe Name, Dom (String, Type))]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Maybe Name]
    genTelVars ([Dom (String, Type)] -> [(Maybe Name, Dom (String, Type))])
    -> [Dom (String, Type)] -> [(Maybe Name, Dom (String, Type))]
    forall a b. (a -> b) -> a -> b
    $ Telescope -> [Dom (String, Type)]
    forall t. Tele (Dom t) -> [Dom (String, t)]
    telToList Telescope
    genTel

      -- For the explicit module telescope we get the names from the typecheck
      -- action.
      let newTelCxt :: [Dom (Name, Type)]
    newTelCxt = (Name -> Dom (String, Type) -> Dom (Name, Type))
    -> [Name] -> [Dom (String, Type)] -> [Dom (Name, Type)]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Name -> Dom (String, Type) -> Dom (Name, Type)
    forall {f :: * -> *} {c} {b} {d}.
    Functor f =>
    c -> f (b, d) -> f (c, d)
    setName [Name]
    cxtNames ([Dom (String, Type)] -> [Dom (Name, Type)])
    -> [Dom (String, Type)] -> [Dom (Name, Type)]
    forall a b. (a -> b) -> a -> b
    $ [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
    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 |Θ| ρ)
      [(Name, (Term, Dom Type))]
    letbinds' <- Substitution' (SubstArg [(Name, (Term, Dom Type))])
    -> [(Name, (Term, Dom Type))] -> [(Name, (Term, Dom Type))]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst (Int -> Substitution -> Substitution
    forall a. Int -> Substitution' a -> Substitution' a
    liftS (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel) Substitution
    sub) ([(Name, (Term, Dom Type))] -> [(Name, (Term, Dom Type))])
    -> TCMT IO [(Name, (Term, Dom Type))]
    -> TCMT IO [(Name, (Term, Dom Type))]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [(Name, (Term, Dom Type))] -> TCMT IO [(Name, (Term, Dom Type))]
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull [(Name, (Term, Dom Type))]
    letbinds
      let addLet :: (Name, (Term, Dom Type)) -> m a -> m a
    addLet (Name
    x, (Term
    v, Dom Type
    dom)) = Name -> Term -> Dom Type -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Name -> Term -> Dom Type -> m a -> m a
    addLetBinding' Name
    x Term
    v Dom Type
    dom

      Substitution
    -> ([Dom (Name, Type)] -> [Dom (Name, Type)]) -> TCM a -> TCM a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Substitution
    -> ([Dom (Name, Type)] -> [Dom (Name, Type)]) -> m a -> m a
    updateContext Substitution
    sub (([Dom (Name, Type)]
    genTelCxt [Dom (Name, Type)] -> [Dom (Name, Type)] -> [Dom (Name, Type)]
    forall a. [a] -> [a] -> [a]
    ++) ([Dom (Name, Type)] -> [Dom (Name, Type)])
    -> ([Dom (Name, Type)] -> [Dom (Name, Type)])
    -> [Dom (Name, Type)]
    -> [Dom (Name, Type)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> [Dom (Name, Type)] -> [Dom (Name, Type)]
    forall a. Int -> [a] -> [a]
    drop Int
    1) (TCM a -> TCM a) -> TCM a -> TCM a
    forall a b. (a -> b) -> a -> b
    $
        Substitution
    -> ([Dom (Name, Type)] -> [Dom (Name, Type)]) -> TCM a -> TCM a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Substitution
    -> ([Dom (Name, Type)] -> [Dom (Name, Type)]) -> m a -> m a
    updateContext (Int -> Substitution
    forall a. Int -> Substitution' a
    raiseS (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel')) ([Dom (Name, Type)]
    newTelCxt [Dom (Name, Type)] -> [Dom (Name, Type)] -> [Dom (Name, Type)]
    forall a. [a] -> [a] -> [a]
    ++) (TCM a -> TCM a) -> TCM a -> TCM a
    forall a b. (a -> b) -> a -> b
    $
          ((Name, (Term, Dom Type)) -> TCM a -> TCM a)
    -> TCM a -> [(Name, (Term, Dom Type))] -> TCM a
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (Name, (Term, Dom Type)) -> TCM a -> TCM a
    forall {m :: * -> *} {a}.
    MonadAddContext m =>
    (Name, (Term, Dom Type)) -> m a -> m a
    addLet ([Maybe Name] -> Telescope -> TCM a
    ret [Maybe Name]
    genTelVars (Telescope -> TCM a) -> Telescope -> TCM a
    forall a b. (a -> b) -> a -> b
    $ Telescope -> Telescope -> Telescope
    forall t. Abstract t => Telescope -> t -> t
    abstract Telescope
    genTel Telescope
    tel') [(Name, (Term, Dom Type))]
    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
      ([Maybe QName]
    ns, Type
    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
      ([Maybe QName], Type) -> TCM ([Maybe QName], Type)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Maybe QName]
    ns, Type
    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

      ((Type
    t, a
    userdata), Map MetaId QName
    namedMetas, MetaStore
    allmetas) <- Set QName
    -> TCM (Type, a) -> TCM ((Type, a), Map MetaId QName, MetaStore)
    forall a.
    Set QName -> TCM a -> TCM (a, Map MetaId QName, MetaStore)
    createMetasAndTypeCheck Set QName
    s TCM (Type, a)
    typecheckAction
      (Telescope
    genTel, [Maybe QName]
    genTelNames, Substitution
    sub) <- Type
    -> Map MetaId QName
    -> MetaStore
    -> TCM (Telescope, [Maybe QName], Substitution)
    forall name.
    Type
    -> Map MetaId name
    -> MetaStore
    -> TCM (Telescope, [Maybe name], Substitution)
    computeGeneralization Type
    genRecMeta Map MetaId QName
    namedMetas MetaStore
    allmetas

      Type
    t' <- Telescope -> Type -> Type
    forall t. Abstract t => Telescope -> t -> t
    abstract Telescope
    genTel (Type -> Type) -> (Type -> Type) -> Type -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Substitution' (SubstArg Type) -> Type -> Type
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg Type)
    sub (Type -> Type) -> TCM Type -> TCM Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> TCM Type
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull Type
    t

      String -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.generalize" Int
    40 (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
    "generalized"
        , 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
    "t =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Impossible -> Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Impossible -> Int -> m a -> m a
    escapeContext Impossible
    HasCallStack => Impossible
    impossible Int
    1 (Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    t') ]

      ([Maybe QName], Type, a) -> TCMT IO ([Maybe QName], Type, a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Maybe QName]
    genTelNames, Type
    t', a
    userdata)

    -- | Create metas for the generalizable variables and run the type check action.
    createMetasAndTypeCheck ::
      Set QName -> TCM a -> TCM (a, Map MetaId QName, MetaStore)
    createMetasAndTypeCheck :: forall a.
    Set QName -> TCM a -> TCM (a, Map MetaId QName, MetaStore)
    createMetasAndTypeCheck Set QName
    s TCM a
    typecheckAction = do
      ((Map MetaId QName
    namedMetas, a
    x), MetaStore
    allmetas) <- TCMT IO (Map MetaId QName, a)
    -> TCMT IO ((Map MetaId QName, a), MetaStore)
    forall (m :: * -> *) a. ReadTCState m => m a -> m (a, MetaStore)
    metasCreatedBy (TCMT IO (Map MetaId QName, a)
     -> TCMT IO ((Map MetaId QName, a), MetaStore))
    -> TCMT IO (Map MetaId QName, a)
    -> TCMT IO ((Map MetaId QName, a), MetaStore)
    forall a b. (a -> b) -> a -> b
    $ do
        (Map MetaId QName
    metamap, Map QName GeneralizedValue
    genvals) <- Set QName -> TCM (Map MetaId QName, Map QName GeneralizedValue)
    createGenValues Set QName
    s
        a
    x <- Lens' (Map QName GeneralizedValue) TCEnv
    -> (Map QName GeneralizedValue -> Map QName GeneralizedValue)
    -> TCM a
    -> TCM a
    forall (m :: * -> *) a b.
    MonadTCEnv m =>
    Lens' a TCEnv -> (a -> a) -> m b -> m b
    locallyTC Lens' (Map QName GeneralizedValue) TCEnv
    eGeneralizedVars (Map QName GeneralizedValue
    -> Map QName GeneralizedValue -> Map QName GeneralizedValue
    forall a b. a -> b -> a
    const Map QName GeneralizedValue
    genvals) TCM a
    typecheckAction
        (Map MetaId QName, a) -> TCMT IO (Map MetaId QName, a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Map MetaId QName
    metamap, a
    x)
      (a, Map MetaId QName, MetaStore)
    -> TCM (a, Map MetaId QName, MetaStore)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (a
    x, Map MetaId QName
    namedMetas, MetaStore
    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).
      Type
    genRecMeta <- Sort -> TCM Type
    newTypeMeta (Integer -> Sort
    mkType Integer
    0)
      Dom (String, Type) -> TCM a -> TCM a
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext ((String, Type) -> Dom (String, Type)
    forall a. a -> Dom a
    defaultDom (String
    "genTel" :: String, Type
    genRecMeta)) (TCM a -> TCM a) -> TCM a -> TCM a
    forall a b. (a -> b) -> a -> b
    $ Type -> TCM a
    ret Type
    genRecMeta

    -- | Compute the generalized telescope from metas created when checking the type/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 -> Map MetaId name -> MetaStore ->
      TCM (Telescope, [Maybe name], Substitution)
    computeGeneralization :: forall name.
    Type
    -> Map MetaId name
    -> MetaStore
    -> TCM (Telescope, [Maybe name], Substitution)
    computeGeneralization Type
    genRecMeta Map MetaId name
    nameMap MetaStore
    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
    prettyTCM Type
    genRecMeta

      -- Pair metas with their metaInfo
      [(MetaId, MetaVariable)]
    mvs <- (Int -> TCMT IO (MetaId, MetaVariable))
    -> [Int] -> TCMT IO [(MetaId, MetaVariable)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM ((\ MetaId
    x -> (MetaId
    x,) (MetaVariable -> (MetaId, MetaVariable))
    -> TCMT IO MetaVariable -> TCMT IO (MetaId, MetaVariable)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> TCMT IO MetaVariable
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupMeta MetaId
    x) (MetaId -> TCMT IO (MetaId, MetaVariable))
    -> (Int -> MetaId) -> Int -> TCMT IO (MetaId, MetaVariable)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> MetaId
    MetaId) ([Int] -> TCMT IO [(MetaId, MetaVariable)])
    -> [Int] -> TCMT IO [(MetaId, MetaVariable)]
    forall a b. (a -> b) -> a -> b
    $ MetaStore -> [Int]
    forall a. IntMap a -> [Int]
    IntMap.keys MetaStore
    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.
      CheckpointId
    cp <- Lens' CheckpointId TCEnv -> TCMT IO CheckpointId
    forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
    viewTC Lens' CheckpointId TCEnv
    eCurrentCheckpoint
      let isFreshMeta :: (MetaId, MetaVariable) -> TCMT IO Bool
    isFreshMeta (MetaId
    x,MetaVariable
    mv) = MetaVariable -> (Range -> TCMT IO Bool) -> TCMT IO Bool
    forall (m :: * -> *) a c b.
    (MonadTCEnv m, ReadTCState m, LensClosure a c) =>
    c -> (a -> m b) -> m b
    enterClosure MetaVariable
    mv ((Range -> TCMT IO Bool) -> TCMT IO Bool)
    -> (Range -> TCMT IO Bool) -> TCMT IO Bool
    forall a b. (a -> b) -> a -> b
    $ \ Range
    _ -> Maybe Substitution -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe Substitution -> Bool)
    -> TCMT IO (Maybe Substitution) -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> CheckpointId -> TCMT IO (Maybe Substitution)
    forall (tcm :: * -> *).
    MonadTCEnv tcm =>
    CheckpointId -> tcm (Maybe Substitution)
    checkpointSubstitution' CheckpointId
    cp
      [(MetaId, MetaVariable)]
    mvs <- ((MetaId, MetaVariable) -> TCMT IO Bool)
    -> [(MetaId, MetaVariable)] -> TCMT IO [(MetaId, MetaVariable)]
    forall (m :: * -> *) a.
    Applicative m =>
    (a -> m Bool) -> [a] -> m [a]
    filterM (MetaId, MetaVariable) -> TCMT IO Bool
    isFreshMeta [(MetaId, MetaVariable)]
    mvs
      [ProblemConstraint]
    cs <- [ProblemConstraint] -> [ProblemConstraint] -> [ProblemConstraint]
    forall a. [a] -> [a] -> [a]
    (++) ([ProblemConstraint] -> [ProblemConstraint] -> [ProblemConstraint])
    -> TCMT IO [ProblemConstraint]
    -> TCMT IO ([ProblemConstraint] -> [ProblemConstraint])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' [ProblemConstraint] TCState -> TCMT IO [ProblemConstraint]
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' [ProblemConstraint] TCState
    stAwakeConstraints
                 TCMT IO ([ProblemConstraint] -> [ProblemConstraint])
    -> TCMT IO [ProblemConstraint] -> TCMT IO [ProblemConstraint]
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Lens' [ProblemConstraint] TCState -> TCMT IO [ProblemConstraint]
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' [ProblemConstraint] TCState
    stSleepingConstraints

      String -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.generalize" Int
    50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "current constraints:" 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
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat ((ProblemConstraint -> TCMT IO Doc)
    -> [ProblemConstraint] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map ProblemConstraint -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM [ProblemConstraint]
    cs)

      Set MetaId
    constrainedMetas <- [Set MetaId] -> Set MetaId
    forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
    Set.unions ([Set MetaId] -> Set MetaId)
    -> TCMT IO [Set MetaId] -> TCMT IO (Set MetaId)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (ProblemConstraint -> TCMT IO (Set MetaId))
    -> [ProblemConstraint] -> TCMT IO [Set MetaId]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (Constraint -> TCMT IO (Set MetaId)
    constraintMetas (Constraint -> TCMT IO (Set MetaId))
    -> (ProblemConstraint -> Constraint)
    -> ProblemConstraint
    -> TCMT IO (Set MetaId)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Closure Constraint -> Constraint
    forall a. Closure a -> a
    clValue (Closure Constraint -> Constraint)
    -> (ProblemConstraint -> Closure Constraint)
    -> ProblemConstraint
    -> Constraint
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ProblemConstraint -> Closure Constraint
    theConstraint) [ProblemConstraint]
    cs

      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
    $ 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
    "constrainedMetas     = " 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
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList_ ((MetaId -> TCMT IO Doc) -> [MetaId] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map MetaId -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM ([MetaId] -> [TCMT IO Doc]) -> [MetaId] -> [TCMT IO Doc]
    forall a b. (a -> b) -> a -> b
    $ Set MetaId -> [MetaId]
    forall a. Set a -> [a]
    Set.toList Set MetaId
    constrainedMetas)

      let isConstrained :: MetaId -> Bool
    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, MetaVariable) -> Bool
    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 :: (a, MetaVariable) -> Bool
    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 :: (a, MetaVariable) -> Bool
    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 ([(MetaId, MetaVariable)]
    generalizable, [(MetaId, MetaVariable)]
    nongeneralizable)         = ((MetaId, MetaVariable) -> Bool)
    -> [(MetaId, MetaVariable)]
    -> ([(MetaId, MetaVariable)], [(MetaId, MetaVariable)])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    partition (MetaId, MetaVariable) -> Bool
    isGeneralizable [(MetaId, MetaVariable)]
    mvs
          ([(MetaId, MetaVariable)]
    generalizableOpen', [(MetaId, MetaVariable)]
    generalizableClosed) = ((MetaId, MetaVariable) -> Bool)
    -> [(MetaId, MetaVariable)]
    -> ([(MetaId, MetaVariable)], [(MetaId, MetaVariable)])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    partition (MetaId, MetaVariable) -> Bool
    forall {a}. (a, MetaVariable) -> Bool
    isOpen [(MetaId, MetaVariable)]
    generalizable
          ([(MetaId, MetaVariable)]
    openSortMetas, [(MetaId, MetaVariable)]
    generalizableOpen)        = ((MetaId, MetaVariable) -> Bool)
    -> [(MetaId, MetaVariable)]
    -> ([(MetaId, MetaVariable)], [(MetaId, MetaVariable)])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    partition (MetaId, MetaVariable) -> Bool
    forall {a}. (a, MetaVariable) -> Bool
    isSort [(MetaId, MetaVariable)]
    generalizableOpen'
          nongeneralizableOpen :: [(MetaId, MetaVariable)]
    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

      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
    $ 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 (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
        [ TCMT IO Doc
    "generalizable        = " 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
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList_ (((MetaId, MetaVariable) -> TCMT IO Doc)
    -> [(MetaId, MetaVariable)] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (MetaId -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (MetaId -> TCMT IO Doc)
    -> ((MetaId, MetaVariable) -> MetaId)
    -> (MetaId, MetaVariable)
    -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (MetaId, MetaVariable) -> MetaId
    forall a b. (a, b) -> a
    fst) [(MetaId, MetaVariable)]
    generalizable)
        , TCMT IO Doc
    "generalizableOpen    = " 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
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList_ (((MetaId, MetaVariable) -> TCMT IO Doc)
    -> [(MetaId, MetaVariable)] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (MetaId -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (MetaId -> TCMT IO Doc)
    -> ((MetaId, MetaVariable) -> MetaId)
    -> (MetaId, MetaVariable)
    -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (MetaId, MetaVariable) -> MetaId
    forall a b. (a, b) -> a
    fst) [(MetaId, MetaVariable)]
    generalizableOpen)
        , TCMT IO Doc
    "openSortMetas        = " 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
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList_ (((MetaId, MetaVariable) -> TCMT IO Doc)
    -> [(MetaId, MetaVariable)] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (MetaId -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (MetaId -> TCMT IO Doc)
    -> ((MetaId, MetaVariable) -> MetaId)
    -> (MetaId, MetaVariable)
    -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (MetaId, MetaVariable) -> MetaId
    forall a b. (a, b) -> a
    fst) [(MetaId, MetaVariable)]
    openSortMetas)
        ]

      -- Issue 3301: We can't generalize over sorts
      [(MetaId, MetaVariable)]
    -> ([(MetaId, MetaVariable)] -> TCMT IO ()) -> TCMT IO ()
    forall (m :: * -> *) a.
    (Monad m, Null a) =>
    a -> (a -> m ()) -> m ()
    unlessNull [(MetaId, MetaVariable)]
    openSortMetas (([(MetaId, MetaVariable)] -> TCMT IO ()) -> TCMT IO ())
    -> ([(MetaId, MetaVariable)] -> TCMT IO ()) -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ \ [(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
    $ [MetaId] -> Warning
    CantGeneralizeOverSorts ([MetaId] -> Warning) -> [MetaId] -> Warning
    forall a b. (a -> b) -> a -> b
    $ ((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)]
    ms

      -- Any meta in the solution of a generalizable meta should be generalized over (if possible).
      CheckpointId
    cp <- Lens' CheckpointId TCEnv -> TCMT IO CheckpointId
    forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
    viewTC Lens' CheckpointId TCEnv
    eCurrentCheckpoint
      let canGeneralize :: MetaId -> TCMT IO Bool
    canGeneralize MetaId
    x | MetaId -> Bool
    isConstrained MetaId
    x = Bool -> TCMT IO Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
          canGeneralize MetaId
    x = do
              MetaVariable
    mv   <- MetaId -> TCMT IO MetaVariable
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupMeta MetaId
    x
              Maybe Substitution
    msub <- MetaVariable
    -> (Range -> TCMT IO (Maybe Substitution))
    -> TCMT IO (Maybe Substitution)
    forall (m :: * -> *) a c b.
    (MonadTCEnv m, ReadTCState m, LensClosure a c) =>
    c -> (a -> m b) -> m b
    enterClosure MetaVariable
    mv ((Range -> TCMT IO (Maybe Substitution))
     -> TCMT IO (Maybe Substitution))
    -> (Range -> TCMT IO (Maybe Substitution))
    -> TCMT IO (Maybe Substitution)
    forall a b. (a -> b) -> a -> b
    $ \ Range
    _ ->
                        CheckpointId -> TCMT IO (Maybe Substitution)
    forall (tcm :: * -> *).
    MonadTCEnv tcm =>
    CheckpointId -> tcm (Maybe Substitution)
    checkpointSubstitution' CheckpointId
    cp
              let sameContext :: Bool
    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
              Bool -> TCMT IO () -> TCMT IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless Bool
    sameContext (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ do
                Type
    ty <- MetaId -> TCM Type
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m Type
    getMetaType MetaId
    x
                let Perm Int
    m [Int]
    xs = MetaVariable -> Permutation
    mvPermutation MetaVariable
    mv
                String -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.generalize" Int
    20 (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
                  [ String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text String
    "Don't know how to generalize over"
                  , 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
    $ MetaId -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM MetaId
    x TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text String
    ":" 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
    prettyTCM Type
    ty
                  , String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text String
    "in context"
                  , 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)
    -> (Telescope -> TCMT IO Doc) -> Telescope -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Telescope -> TCMT IO Doc) -> TCMT IO Telescope -> TCMT IO Doc
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCMT IO Telescope
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
    getContextTelescope
                  , String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text String
    "permutation:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text ((Int, [Int]) -> String
    forall a. Show a => a -> String
    show (Int
    m, [Int]
    xs))
                  , String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text String
    "subst:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Maybe Substitution -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Maybe Substitution
    msub ]
              Bool -> TCMT IO Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    sameContext
      Set MetaId
    inherited <- ([Set MetaId] -> Set MetaId)
    -> TCMT IO [Set MetaId] -> TCMT IO (Set MetaId)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap [Set MetaId] -> Set MetaId
    forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
    Set.unions (TCMT IO [Set MetaId] -> TCMT IO (Set MetaId))
    -> TCMT IO [Set MetaId] -> TCMT IO (Set MetaId)
    forall a b. (a -> b) -> a -> b
    $ [(MetaId, MetaVariable)]
    -> ((MetaId, MetaVariable) -> TCMT IO (Set MetaId))
    -> TCMT IO [Set MetaId]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [(MetaId, MetaVariable)]
    generalizableClosed (((MetaId, MetaVariable) -> TCMT IO (Set MetaId))
     -> TCMT IO [Set MetaId])
    -> ((MetaId, MetaVariable) -> TCMT IO (Set MetaId))
    -> TCMT IO [Set MetaId]
    forall a b. (a -> b) -> a -> b
    $ \ (MetaId
    x, MetaVariable
    mv) ->
        case MetaVariable -> MetaInstantiation
    mvInstantiation MetaVariable
    mv of
          InstV [Arg String]
    _ Term
    v -> do
            String
    parentName <- MetaId -> TCMT IO String
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m String
    getMetaNameSuggestion MetaId
    x
            [MetaId]
    metas <- (MetaId -> TCMT IO Bool) -> [MetaId] -> TCMT IO [MetaId]
    forall (m :: * -> *) a.
    Applicative m =>
    (a -> m Bool) -> [a] -> m [a]
    filterM MetaId -> TCMT IO Bool
    canGeneralize ([MetaId] -> TCMT IO [MetaId])
    -> (Term -> [MetaId]) -> Term -> TCMT IO [MetaId]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Set MetaId -> [MetaId]
    forall a. Set a -> [a]
    Set.toList (Set MetaId -> [MetaId])
    -> (Term -> Set MetaId) -> Term -> [MetaId]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (MetaId -> Set MetaId) -> Term -> Set MetaId
    forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
    allMetas MetaId -> Set MetaId
    forall a. a -> Set a
    Set.singleton (Term -> TCMT IO [MetaId]) -> TCMT IO Term -> TCMT IO [MetaId]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Term -> TCMT IO Term
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull Term
    v
            let suggestNames :: Integer -> [MetaId] -> TCMT IO ()
    suggestNames Integer
    i [] = () -> TCMT IO ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
                suggestNames Integer
    i (MetaId
    m : [MetaId]
    ms) = do
                  -- #4291: Override existing meta name suggestion. If we solved the parent with a new
                  --        meta use the parent name for that, otherwise suffix with a number.
                  let suf :: String
    suf | [MetaId] -> Bool
    forall a. Null a => a -> Bool
    null [MetaId]
    ms Bool -> Bool -> Bool
    && Integer
    i Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    1, MetaV{} <- Term
    v = String
    ""
                          | Bool
    otherwise                       = String
    "." String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Integer -> String
    forall a. Show a => a -> String
    show Integer
    i
                  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
    suf)
                  Integer -> [MetaId] -> TCMT IO ()
    suggestNames (Integer
    i Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    1) [MetaId]
    ms
            Bool -> TCMT IO () -> TCMT IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([MetaId] -> Bool
    forall a. Null a => a -> Bool
    null [MetaId]
    metas) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
              String -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.generalize" Int
    40 (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
    hcat [TCMT IO Doc
    "Inherited metas from ", MetaId -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM MetaId
    x, TCMT IO Doc
    ":"] 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
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList_ ((MetaId -> TCMT IO Doc) -> [MetaId] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map MetaId -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM [MetaId]
    metas)
                                        -- Don't suggest names for explicitly named generalizable metas
            [MetaId] -> Set MetaId
    forall a. Ord a => [a] -> Set a
    Set.fromList [MetaId]
    metas Set MetaId -> TCMT IO () -> TCMT IO (Set MetaId)
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Integer -> [MetaId] -> TCMT IO ()
    suggestNames Integer
    1 ((MetaId -> Bool) -> [MetaId] -> [MetaId]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (MetaId -> Map MetaId name -> Bool
    forall k a. Ord k => k -> Map k a -> Bool
    `Map.notMember` Map MetaId name
    nameMap) [MetaId]
    metas)
          MetaInstantiation
    _ -> TCMT IO (Set MetaId)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

      let ([MetaId]
    alsoGeneralize, [MetaId]
    reallyDontGeneralize) = (MetaId -> Bool) -> [MetaId] -> ([MetaId], [MetaId])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    partition (MetaId -> Set MetaId -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set MetaId
    inherited) ([MetaId] -> ([MetaId], [MetaId]))
    -> [MetaId] -> ([MetaId], [MetaId])
    forall a b. (a -> b) -> a -> b
    $ ((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)]
    nongeneralizableOpen
          generalizeOver :: [MetaId]
    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 -> Bool
    shouldGeneralize = ([MetaId]
    generalizeOver [MetaId] -> MetaId -> Bool
    forall a. Ord a => [a] -> a -> Bool
    `hasElem`)

      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
    $ 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 (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
        [ TCMT IO Doc
    "alsoGeneralize       = " 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
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList_ ((MetaId -> TCMT IO Doc) -> [MetaId] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map MetaId -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM [MetaId]
    alsoGeneralize)
        , TCMT IO Doc
    "reallyDontGeneralize = " 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
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList_ ((MetaId -> TCMT IO Doc) -> [MetaId] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map MetaId -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM [MetaId]
    reallyDontGeneralize)
        ]

      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
    "we're generalizing over" 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
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList_ ((MetaId -> TCMT IO Doc) -> [MetaId] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map MetaId -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM [MetaId]
    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).
      [MetaId]
    allSortedMetas <- TCMT IO [MetaId] -> TCMT IO (Maybe [MetaId]) -> TCMT IO [MetaId]
    forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
    fromMaybeM (TypeError -> TCMT IO [MetaId]
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError TypeError
    GeneralizeCyclicDependency) (TCMT IO (Maybe [MetaId]) -> TCMT IO [MetaId])
    -> TCMT IO (Maybe [MetaId]) -> TCMT IO [MetaId]
    forall a b. (a -> b) -> a -> b
    $
        [MetaId] -> TCMT IO (Maybe [MetaId])
    dependencySortMetas ([MetaId]
    generalizeOver [MetaId] -> [MetaId] -> [MetaId]
    forall a. [a] -> [a] -> [a]
    ++ [MetaId]
    reallyDontGeneralize [MetaId] -> [MetaId] -> [MetaId]
    forall a. [a] -> [a] -> [a]
    ++ ((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)]
    openSortMetas)
      let sortedMetas :: [MetaId]
    sortedMetas = (MetaId -> Bool) -> [MetaId] -> [MetaId]
    forall a. (a -> Bool) -> [a] -> [a]
    filter MetaId -> Bool
    shouldGeneralize [MetaId]
    allSortedMetas

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

      -- Create the pre-record type (we don't yet know the types of the fields)
      (QName
    genRecName, ConHead
    genRecCon, [QName]
    genRecFields) <- Impossible
    -> TCMT IO (QName, ConHead, [QName])
    -> TCMT IO (QName, ConHead, [QName])
    forall {m :: * -> *} {a}.
    MonadAddContext m =>
    Impossible -> m a -> m a
    dropCxt Impossible
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (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
    $
          Type -> [MetaId] -> TCMT IO (QName, ConHead, [QName])
    createGenRecordType Type
    genRecMeta [MetaId]
    sortedMetas

      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] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $
        [ TCMT IO Doc
    "created genRecordType"
        , 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
    "genRecName   = " 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
    prettyTCM QName
    genRecName
        , 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
    "genRecCon    = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ConHead -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM ConHead
    genRecCon
        , 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
    "genRecFields = " 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
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList_ ((QName -> TCMT IO Doc) -> [QName] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM [QName]
    genRecFields)
        ]

      -- Solve the generalizable metas. Each generalizable meta is solved by projecting the
      -- corresponding field from the genTel record.
      Telescope
    cxtTel <- TCMT IO Telescope
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
    getContextTelescope
      let solve :: MetaId -> QName -> TCMT IO ()
    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
    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
    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, MonadFail m, ReadTCState m) =>
    a -> 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]
      (MetaId -> QName -> TCMT IO ())
    -> [MetaId] -> [QName] -> TCMT IO ()
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m ()
    zipWithM_ MetaId -> QName -> TCMT IO ()
    solve [MetaId]
    sortedMetas [QName]
    genRecFields

      -- Record the named variables in the telescope
      let telNames :: [Maybe name]
    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
      [(Arg String, Type)]
    teleTypes <- do
        Args
    args <- TCMT IO Args
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
    getContextArgs
        ([[(Arg String, Type)]] -> [(Arg String, Type)])
    -> TCMT IO [[(Arg String, Type)]] -> TCMT IO [(Arg String, Type)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap [[(Arg String, Type)]] -> [(Arg String, Type)]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat (TCMT IO [[(Arg String, Type)]] -> TCMT IO [(Arg String, Type)])
    -> TCMT IO [[(Arg String, Type)]] -> TCMT IO [(Arg String, Type)]
    forall a b. (a -> b) -> a -> b
    $ [MetaId]
    -> (MetaId -> TCMT IO [(Arg String, Type)])
    -> TCMT IO [[(Arg String, Type)]]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [MetaId]
    sortedMetas ((MetaId -> TCMT IO [(Arg String, Type)])
     -> TCMT IO [[(Arg String, Type)]])
    -> (MetaId -> TCMT IO [(Arg String, Type)])
    -> TCMT IO [[(Arg String, Type)]]
    forall a b. (a -> b) -> a -> b
    $ \ MetaId
    m -> do
          MetaVariable
    mv   <- MetaId -> TCMT IO MetaVariable
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupMeta MetaId
    m
          let info :: ArgInfo
    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
              HasType{ jMetaType :: forall a. Judgement a -> Type
    jMetaType = Type
    t } = MetaVariable -> Judgement MetaId
    mvJudgement MetaVariable
    mv
              perm :: Permutation
    perm = MetaVariable -> Permutation
    mvPermutation MetaVariable
    mv
          Type
    t' <- Type -> Args -> TCM Type
    forall a (m :: * -> *).
    (PiApplyM a, MonadReduce m, HasBuiltins m) =>
    Type -> a -> m Type
    piApplyM Type
    t (Args -> TCM Type) -> Args -> TCM Type
    forall a b. (a -> b) -> a -> b
    $ Permutation -> Args -> Args
    forall a. Permutation -> [a] -> [a]
    permute (Int -> Permutation -> Permutation
    takeP (Args -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length Args
    args) Permutation
    perm) Args
    args
          [(Arg String, Type)] -> TCMT IO [(Arg String, Type)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [(ArgInfo -> String -> Arg String
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    info (String -> Arg String) -> String -> Arg String
    forall a b. (a -> b) -> a -> b
    $ MetaInfo -> String
    miNameSuggestion (MetaInfo -> String) -> MetaInfo -> String
    forall a b. (a -> b) -> a -> b
    $ MetaVariable -> MetaInfo
    mvInfo MetaVariable
    mv, Type
    t')]
      let genTel :: Telescope
    genTel = ConHead -> [(Arg String, Type)] -> Telescope
    buildGeneralizeTel ConHead
    genRecCon [(Arg String, Type)]
    teleTypes

      String -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.generalize" Int
    40 (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
        [ String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text String
    "genTel =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Telescope
    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, InteractionPoint) -> Maybe (MetaId, InteractionId)
    inscope (InteractionId
    ii, InteractionPoint{ipMeta :: InteractionPoint -> Maybe MetaId
    ipMeta = Just MetaId
    x})
            | Int -> MetaStore -> Bool
    forall a. Int -> IntMap a -> Bool
    IntMap.member (MetaId -> Int
    metaId MetaId
    x) MetaStore
    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
      Map MetaId InteractionId
    ips <- [(MetaId, InteractionId)] -> Map MetaId InteractionId
    forall k a. [(k, a)] -> Map k a
    Map.fromDistinctAscList ([(MetaId, InteractionId)] -> Map MetaId InteractionId)
    -> (BiMap InteractionId InteractionPoint
        -> [(MetaId, InteractionId)])
    -> BiMap InteractionId InteractionPoint
    -> Map MetaId InteractionId
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((InteractionId, InteractionPoint)
     -> Maybe (MetaId, InteractionId))
    -> [(InteractionId, InteractionPoint)] -> [(MetaId, InteractionId)]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe (InteractionId, InteractionPoint) -> Maybe (MetaId, InteractionId)
    inscope ([(InteractionId, InteractionPoint)] -> [(MetaId, InteractionId)])
    -> (BiMap InteractionId InteractionPoint
        -> [(InteractionId, InteractionPoint)])
    -> BiMap InteractionId InteractionPoint
    -> [(MetaId, InteractionId)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ([(InteractionId, InteractionPoint)], [(MetaId, InteractionId)])
    -> [(InteractionId, InteractionPoint)]
    forall a b. (a, b) -> a
    fst (([(InteractionId, InteractionPoint)], [(MetaId, InteractionId)])
     -> [(InteractionId, InteractionPoint)])
    -> (BiMap InteractionId InteractionPoint
        -> ([(InteractionId, InteractionPoint)],
            [(MetaId, InteractionId)]))
    -> BiMap InteractionId InteractionPoint
    -> [(InteractionId, InteractionPoint)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BiMap InteractionId InteractionPoint
    -> ([(InteractionId, InteractionPoint)], [(MetaId, InteractionId)])
    forall k v. BiMap k v -> ([(k, v)], [(Tag v, k)])
    BiMap.toDistinctAscendingLists (BiMap InteractionId InteractionPoint -> Map MetaId InteractionId)
    -> TCMT IO (BiMap InteractionId InteractionPoint)
    -> TCMT IO (Map MetaId InteractionId)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' (BiMap InteractionId InteractionPoint) TCState
    -> TCMT IO (BiMap InteractionId InteractionPoint)
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' (BiMap InteractionId InteractionPoint) TCState
    stInteractionPoints
      QName
    -> ConHead
    -> Telescope
    -> [QName]
    -> Map MetaId InteractionId
    -> (MetaId -> Bool)
    -> [MetaId]
    -> TCMT IO ()
    pruneUnsolvedMetas QName
    genRecName ConHead
    genRecCon Telescope
    genTel [QName]
    genRecFields Map MetaId InteractionId
    ips MetaId -> Bool
    shouldGeneralize [MetaId]
    allSortedMetas

      -- Fill in the missing details of the telescope record.
      Impossible -> TCMT IO () -> TCMT IO ()
    forall {m :: * -> *} {a}.
    MonadAddContext m =>
    Impossible -> m a -> m a
    dropCxt Impossible
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ QName -> ConHead -> [QName] -> Type -> Telescope -> TCMT IO ()
    fillInGenRecordDetails QName
    genRecName ConHead
    genRecCon [QName]
    genRecFields Type
    genRecMeta Telescope
    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 :: Substitution
    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 (t :: * -> *) a. Foldable t => t a -> Int
    length [(Arg String, Type)]
    teleTypes)

      (Telescope, [Maybe name], Substitution)
    -> TCM (Telescope, [Maybe name], Substitution)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Telescope
    genTel, [Maybe name]
    telNames, Substitution
    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 (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 (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
            MetaId
    x <- if Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    0 then MetaId -> TCMT IO MetaId
    prePrune MetaId
    x
                                 else MetaId -> TCMT IO MetaId
    forall (m :: * -> *) a. Monad m => a -> m a
    return MetaId
    x
            Telescope -> MetaId -> TCMT IO ()
    pruneMeta ([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)]
    forall a. [a] -> [a]
    reverse [Dom (String, Type)]
    cxt) MetaId
    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 (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
          Range
    r <- MetaId -> TCMT IO Range
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m Range
    getMetaRange MetaId
    x
          Doc -> TCM a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    Doc -> m a
    genericDocError (Doc -> TCM a) -> TCMT IO Doc -> TCM a
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<<
            (String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    fwords (String
    msg String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " The problematic unsolved meta is") TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    $$
                     (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
    $ Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (MetaId -> Elims -> Term
    MetaV MetaId
    x []) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "at" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Range -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Range
    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
          CheckpointId
    cp <- Lens' CheckpointId TCEnv -> TCMT IO CheckpointId
    forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
    viewTC Lens' CheckpointId TCEnv
    eCurrentCheckpoint
          MetaVariable
    mv <- MetaId -> TCMT IO MetaVariable
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupMeta MetaId
    x
          (Int
    i, Maybe Type
    _A) <- MetaVariable
    -> (Range -> TCMT IO (Int, Maybe Type))
    -> TCMT IO (Int, Maybe Type)
    forall (m :: * -> *) a c b.
    (MonadTCEnv m, ReadTCState m, LensClosure a c) =>
    c -> (a -> m b) -> m b
    enterClosure MetaVariable
    mv ((Range -> TCMT IO (Int, Maybe Type)) -> TCMT IO (Int, Maybe Type))
    -> (Range -> TCMT IO (Int, Maybe Type))
    -> TCMT IO (Int, Maybe Type)
    forall a b. (a -> b) -> a -> b
    $ \ Range
    _ -> do
            Substitution
    δ <- CheckpointId -> TCMT IO Substitution
    forall (tcm :: * -> *).
    MonadTCEnv tcm =>
    CheckpointId -> tcm Substitution
    checkpointSubstitution CheckpointId
    cp
            Maybe Type
    _A <- case MetaVariable -> Judgement MetaId
    mvJudgement MetaVariable
    mv of
                    IsSort{}  -> Maybe Type -> TCMT IO (Maybe Type)
    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 :: * -> *).
    (MonadFail m, MonadTCEnv m, ReadTCState m, MonadReduce m,
     HasBuiltins m) =>
    MetaId -> m Type
    getMetaTypeInContext MetaId
    x
            case Substitution
    δ of
              Wk Int
    n Substitution
    IdS -> (Int, Maybe Type) -> TCMT IO (Int, Maybe Type)
    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 (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 Int
    i Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    0 then MetaId -> TCMT IO MetaId
    forall (m :: * -> *) a. Monad m => a -> m a
    return MetaId
    x else do
            String -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.generalize.prune.pre" Int
    40 (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
    "prepruning"
              , 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
    $ MetaId -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty MetaId
    x 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
    <+> Type -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty (Judgement MetaId -> Type
    forall a. Judgement a -> Type
    jMetaType (Judgement MetaId -> Type) -> Judgement MetaId -> Type
    forall a b. (a -> b) -> a -> b
    $ 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
    "|Δ| =" 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, Show a) => a -> m Doc
    pshow Int
    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 -> Maybe (Int, IntSet)
    IntSet.minView (Maybe Type -> IntSet
    forall t. Free t => t -> IntSet
    allFreeVars Maybe Type
    _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 (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 ρ :: Substitution
    ρ  = Impossible -> Int -> Substitution
    forall a. Impossible -> Int -> Substitution' a
    strengthenS Impossible
    HasCallStack => Impossible
    impossible Int
    i
                ρ' :: Substitution
    ρ' = Int -> Substitution
    forall a. Int -> Substitution' a
    raiseS Int
    i

            (MetaId
    y, Term
    u) <- MetaVariable -> Substitution -> Maybe Type -> TCM (MetaId, Term)
    newMetaFromOld MetaVariable
    mv Substitution
    ρ Maybe Type
    _A

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

            String -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.generalize.prune.pre" Int
    40 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ 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 (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
              [ TCMT IO Doc
    "u    =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Term
    u
              , TCMT IO Doc
    "uρ⁻¹ =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Term
    uρ' ]

            -- To solve it we enter the context of x again
            MetaVariable -> (Range -> TCMT IO MetaId) -> TCMT IO MetaId
    forall (m :: * -> *) a c b.
    (MonadTCEnv m, ReadTCState m, LensClosure a c) =>
    c -> (a -> m b) -> m b
    enterClosure MetaVariable
    mv ((Range -> TCMT IO MetaId) -> TCMT IO MetaId)
    -> (Range -> TCMT IO MetaId) -> TCMT IO MetaId
    forall a b. (a -> b) -> a -> b
    $ \ Range
    _ -> do
              -- v is x applied to the context variables
              Term
    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
              TCMT IO () -> TCMT IO ()
    forall (m :: * -> *) a.
    (MonadConstraint m, MonadWarning m, MonadError TCErr m,
     MonadFresh ProblemId m) =>
    m a -> m a
    noConstraints (MetaId -> MetaVariable -> Maybe Type -> Term -> Term -> TCMT IO ()
    doPrune MetaId
    x MetaVariable
    mv Maybe Type
    _A Term
    v Term
    uρ') TCMT IO () -> (TCErr -> TCMT IO ()) -> TCMT IO ()
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    `catchError` \ TCErr
    _ -> MetaId -> TCMT IO ()
    forall {a}. MetaId -> TCM a
    prepruneErrorFailedToInstantiate MetaId
    x
              MetaId -> MetaId -> TCMT IO ()
    setInteractionPoint MetaId
    x MetaId
    y
              MetaId -> TCMT IO MetaId
    forall (m :: * -> *) a. Monad m => a -> m a
    return MetaId
    y

        pruneMeta :: Telescope -> MetaId -> TCMT IO ()
    pruneMeta Telescope
    _Θ MetaId
    x = do
          CheckpointId
    cp <- Lens' CheckpointId TCEnv -> TCMT IO CheckpointId
    forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
    viewTC Lens' CheckpointId TCEnv
    eCurrentCheckpoint
          MetaVariable
    mv <- MetaId -> TCMT IO MetaVariable
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupMeta MetaId
    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.
          MetaVariable -> (Range -> TCMT IO ()) -> TCMT IO ()
    forall (m :: * -> *) a c b.
    (MonadTCEnv m, ReadTCState m, LensClosure a c) =>
    c -> (a -> m b) -> m b
    enterClosure MetaVariable
    mv ((Range -> TCMT IO ()) -> TCMT IO ())
    -> (Range -> TCMT IO ()) -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ \ 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
    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 ]

            Telescope
    _ΓrΔ <- TCMT IO Telescope
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
    getContextTelescope
            let (Telescope
    _Γ, Telescope
    _Δ) = ([Dom (String, Type)] -> Telescope
    telFromList [Dom (String, Type)]
    gs, [Dom (String, Type)] -> Telescope
    telFromList [Dom (String, Type)]
    ds)
                  where ([Dom (String, Type)]
    gs, Dom (String, Type)
    _ : [Dom (String, Type)]
    ds) = Int
    -> [Dom (String, Type)]
    -> ([Dom (String, Type)], [Dom (String, Type)])
    forall a. Int -> [a] -> ([a], [a])
    splitAt (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    _ΓrΔ Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1) (Telescope -> [Dom (String, Type)]
    forall t. Tele (Dom t) -> [Dom (String, t)]
    telToList Telescope
    _ΓrΔ)

            -- Get the type of x. By doing this here we let the checkpoint machinery sort out the
            Maybe Type
    _A <- case MetaVariable -> Judgement MetaId
    mvJudgement MetaVariable
    mv of
                    IsSort{}  -> Maybe Type -> TCMT IO (Maybe Type)
    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 :: * -> *).
    (MonadFail m, MonadTCEnv m, ReadTCState m, MonadReduce m,
     HasBuiltins 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)
            Substitution
    δ <- CheckpointId -> TCMT IO Substitution
    forall (tcm :: * -> *).
    MonadTCEnv tcm =>
    CheckpointId -> tcm Substitution
    checkpointSubstitution CheckpointId
    cp

            -- v is x applied to the context variables
            Term
    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

            -- Now ultimately we want to create the fresh meta in the context
            --   Γ Θγ Δσ where Γ    ⊢ γ : Γ₀
            --                 Γ Θγ ⊢ σ : Γ (r : GenTel)
            -- σ is the unpacking substitution (which is polymorphic in Γ)
            let σ :: Substitution
    σ   = Int -> Substitution
    sub (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    _Θ)
                --    Γ <- Γ (r : GenTel) Δ <- Γ₀ (r : GenTel) <- Γ₀
                γ :: Substitution
    γ   = 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
                _Θγ :: Telescope
    _Θγ = Substitution' (SubstArg Telescope) -> Telescope -> Telescope
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg Telescope)
    γ 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 ρ :: Substitution
    ρ  = Int -> Substitution -> Substitution
    forall a. Int -> Substitution' a -> Substitution' a
    liftS Int
    i Substitution
    σ
                -- We also need ρ⁻¹, which is a lot easier to construct.
                ρ' :: Substitution
    ρ' = 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

            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
    $ 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 (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
              [ TCMT IO Doc
    "Γ   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Telescope
    _Γ
              , TCMT IO Doc
    "Θ   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Telescope
    _Θ
              , TCMT IO Doc
    "Δ   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Telescope
    _Δ
              , TCMT IO Doc
    "σ   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Substitution -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Substitution
    σ
              , TCMT IO Doc
    "γ   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Substitution -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Substitution
    γ
              , TCMT IO Doc
    "δ   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Substitution -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Substitution
    δ
              , TCMT IO Doc
    "ρ   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Substitution -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Substitution
    ρ
              , TCMT IO Doc
    "ρ⁻¹ =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Substitution -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Substitution
    ρ'
              , TCMT IO Doc
    "Θγ  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Telescope
    _Θγ
              , TCMT IO Doc
    "Δσ  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Telescope
    _Δσ
              , TCMT IO Doc
    "_A  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Maybe Type -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Maybe Type
    _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 Θ.
            ([Dom (Name, Type)]
    newCxt, [Dom (Name, Type)]
    rΘ) <- do
              ([Dom (Name, Type)]
    rΔ, Dom (Name, Type)
    _ : [Dom (Name, Type)]
    rΓ) <- Int
    -> [Dom (Name, Type)] -> ([Dom (Name, Type)], [Dom (Name, Type)])
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    i ([Dom (Name, Type)] -> ([Dom (Name, Type)], [Dom (Name, Type)]))
    -> TCMT IO [Dom (Name, Type)]
    -> TCMT IO ([Dom (Name, Type)], [Dom (Name, Type)])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO [Dom (Name, Type)]
    forall (m :: * -> *). MonadTCEnv m => m [Dom (Name, Type)]
    getContext
              let setName :: Dom' Term (String, t) -> TCMT IO (Dom' Term (Name, t))
    setName = ((String, t) -> TCMT IO (Name, t))
    -> Dom' Term (String, t) -> TCMT IO (Dom' Term (Name, t))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse (((String, t) -> TCMT IO (Name, t))
     -> Dom' Term (String, t) -> TCMT IO (Dom' Term (Name, t)))
    -> ((String, t) -> TCMT IO (Name, t))
    -> Dom' Term (String, t)
    -> TCMT IO (Dom' Term (Name, t))
    forall a b. (a -> b) -> a -> b
    $ \ (String
    s, t
    ty) -> (,t
    ty) (Name -> (Name, t)) -> TCMT IO Name -> TCMT IO (Name, t)
    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
    freshName_ String
    s
              [Dom (Name, Type)]
    rΘ <- (Dom (String, Type) -> TCMT IO (Dom (Name, Type)))
    -> [Dom (String, Type)] -> TCMT IO [Dom (Name, Type)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM Dom (String, Type) -> TCMT IO (Dom (Name, Type))
    forall {t}. Dom' Term (String, t) -> TCMT IO (Dom' Term (Name, t))
    setName ([Dom (String, Type)] -> TCMT IO [Dom (Name, Type)])
    -> [Dom (String, Type)] -> TCMT IO [Dom (Name, Type)]
    forall a b. (a -> b) -> a -> b
    $ [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
    _Θγ
              let rΔσ :: [Dom (Name, Type)]
    rΔσ = (Name -> Dom (String, Type) -> Dom (Name, Type))
    -> [Name] -> [Dom (String, Type)] -> [Dom (Name, Type)]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (\ Name
    name Dom (String, Type)
    dom -> (String -> Name) -> (String, Type) -> (Name, Type)
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (b, d) (c, d)
    first (Name -> String -> Name
    forall a b. a -> b -> a
    const Name
    name) ((String, Type) -> (Name, Type))
    -> Dom (String, Type) -> Dom (Name, Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Dom (String, Type)
    dom)
                                ((Dom (Name, Type) -> Name) -> [Dom (Name, Type)] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Name, Type) -> Name
    forall a b. (a, b) -> a
    fst ((Name, Type) -> Name)
    -> (Dom (Name, Type) -> (Name, Type)) -> Dom (Name, Type) -> Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom (Name, Type) -> (Name, Type)
    forall t e. Dom' t e -> e
    unDom) [Dom (Name, Type)]
    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
    _Δσ)
              ([Dom (Name, Type)], [Dom (Name, Type)])
    -> TCMT IO ([Dom (Name, Type)], [Dom (Name, Type)])
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Dom (Name, Type)]
    rΔσ [Dom (Name, Type)] -> [Dom (Name, Type)] -> [Dom (Name, Type)]
    forall a. [a] -> [a] -> [a]
    ++ [Dom (Name, Type)]
    rΘ [Dom (Name, Type)] -> [Dom (Name, Type)] -> [Dom (Name, Type)]
    forall a. [a] -> [a] -> [a]
    ++ [Dom (Name, Type)]
    rΓ, [Dom (Name, Type)]
    rΘ)

            -- Now we can enter the new context and create our meta variable.
            (MetaId
    y, Term
    u) <- Substitution
    -> ([Dom (Name, Type)] -> [Dom (Name, Type)])
    -> TCM (MetaId, Term)
    -> TCM (MetaId, Term)
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Substitution
    -> ([Dom (Name, Type)] -> [Dom (Name, Type)]) -> m a -> m a
    updateContext Substitution
    ρ ([Dom (Name, Type)] -> [Dom (Name, Type)] -> [Dom (Name, Type)]
    forall a b. a -> b -> a
    const [Dom (Name, Type)]
    newCxt) (TCM (MetaId, Term) -> TCM (MetaId, Term))
    -> TCM (MetaId, Term) -> TCM (MetaId, Term)
    forall a b. (a -> b) -> a -> b
    $ TCM (MetaId, Term) -> TCM (MetaId, Term)
    forall a. TCM a -> TCM a
    localScope (TCM (MetaId, Term) -> TCM (MetaId, Term))
    -> TCM (MetaId, Term) -> TCM (MetaId, Term)
    forall a b. (a -> b) -> a -> b
    $ do

              -- First, we add the named variables to the scope, to allow
              -- them to be used in holes (#3341). These should go outside Δ (#3735).
              Int -> TCMT IO () -> TCMT IO ()
    forall a. Int -> ScopeM a -> ScopeM a
    outsideLocalVars Int
    i (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [Dom (Name, Type)] -> TCMT IO ()
    forall {t :: * -> *} {t} {b}.
    Foldable t =>
    t (Dom' t (Name, b)) -> TCMT IO ()
    addNamedVariablesToScope [Dom (Name, Type)]
    rΘ

              -- Now we can create the new meta
              MetaVariable -> Substitution -> Maybe Type -> TCM (MetaId, Term)
    newMetaFromOld MetaVariable
    mv Substitution
    ρ Maybe Type
    _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ρ' :: Term
    uρ' = Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg Term)
    ρ' Term
    u
            String -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.generalize.prune" Int
    80 (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
    "solving"
              , 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 (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ Term -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Term
    v   TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "=="
                             , Term -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Term
    uρ' TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    ":"
                             , Maybe Type -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Maybe Type
    _A ] ]
            TCMT IO () -> TCMT IO ()
    forall (m :: * -> *) a.
    (MonadConstraint m, MonadWarning m, MonadError TCErr m,
     MonadFresh ProblemId m) =>
    m a -> m a
    noConstraints (MetaId -> MetaVariable -> Maybe Type -> Term -> Term -> TCMT IO ()
    doPrune MetaId
    x MetaVariable
    mv Maybe Type
    _A Term
    v Term
    uρ') TCMT IO () -> (TCErr -> TCMT IO ()) -> TCMT IO ()
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    `catchError` MetaId -> Term -> TCErr -> TCMT IO ()
    niceError MetaId
    x Term
    v

            String -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.generalize.prune" Int
    80 (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
    "solved"
              , 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
    "v    =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (Term -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty (Term -> TCMT IO Doc) -> TCMT IO Term -> TCMT IO Doc
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Term -> TCMT IO Term
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull Term
    v)
              , 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
    "uρ⁻¹ =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (Term -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty (Term -> TCMT IO Doc) -> TCMT IO Term -> TCMT IO Doc
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Term -> TCMT IO Term
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull Term
    uρ') ]

            MetaId -> MetaId -> TCMT IO ()
    setInteractionPoint MetaId
    x MetaId
    y

        findGenRec :: MetaVariable -> TCM (Maybe Int)
        findGenRec :: MetaVariable -> TCMT IO (Maybe Int)
    findGenRec MetaVariable
    mv = do
          [Dom (Name, Type)]
    cxt <- [Dom (Name, Type)] -> TCMT IO [Dom (Name, Type)]
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull ([Dom (Name, Type)] -> TCMT IO [Dom (Name, Type)])
    -> TCMT IO [Dom (Name, Type)] -> TCMT IO [Dom (Name, Type)]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCMT IO [Dom (Name, Type)]
    forall (m :: * -> *). MonadTCEnv m => m [Dom (Name, Type)]
    getContext
          let notPruned :: [Int]
    notPruned = Permutation -> [Int] -> [Int]
    forall a. Permutation -> [a] -> [a]
    permute (Int -> Permutation -> Permutation
    takeP ([Dom (Name, Type)] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Dom (Name, Type)]
    cxt) (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. [a] -> [a]
    reverse ([Int] -> [Int]) -> [Int] -> [Int]
    forall a b. (a -> b) -> a -> b
    $ (Int -> Dom (Name, Type) -> Int)
    -> [Int] -> [Dom (Name, Type)] -> [Int]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Int -> Dom (Name, Type) -> Int
    forall a b. a -> b -> a
    const [Int
    0..] [Dom (Name, Type)]
    cxt
          case [ Int
    i | (Int
    i, Dom{unDom :: forall t e. Dom' t e -> e
    unDom = (Name
    _, El Sort
    _ (Def QName
    q Elims
    _))}) <- [Int] -> [Dom (Name, Type)] -> [(Int, Dom (Name, Type))]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Int
    0..] [Dom (Name, Type)]
    cxt,
                     QName
    q QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    genRecName, Int
    i Int -> [Int] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [Int]
    notPruned ] of
            []    -> Maybe Int -> TCMT IO (Maybe Int)
    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 (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 :: Sort
    s@(MetaS MetaId
    y Elims
    _) <- TCMT IO Sort
    forall (m :: * -> *). MonadMetaSolver m => m Sort
    newSortMeta
              (MetaId, Term) -> TCM (MetaId, Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (MetaId
    y, Sort -> Term
    Sort 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
          Term
    u <- Term -> TCMT IO Term
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull Term
    u
          let err' :: TCErr
    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 :: Closure TypeError
    tcErrClosErr = Closure TypeError
    cl{ clEnv :: TCEnv
    clEnv = (Closure TypeError -> TCEnv
    forall a. Closure a -> TCEnv
    clEnv Closure TypeError
    cl) { envCall :: Maybe (Closure Call)
    envCall = Maybe (Closure Call)
    forall a. Maybe a
    Nothing } } }
                       TCErr
    _ -> TCErr
    err
              telList :: [Dom (String, Type)]
    telList = Telescope -> [Dom (String, Type)]
    forall t. Tele (Dom t) -> [Dom (String, t)]
    telToList Telescope
    genTel
              names :: [String]
    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 :: [String]
    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 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 :: Elim' Term -> Set String
    projs (Proj ProjOrigin
    _ QName
    q)
                | QName
    q QName -> [QName] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [QName]
    genRecFields = [String] -> Set String
    forall a. Ord a => [a] -> Set a
    Set.fromList ([String] -> Set String) -> [String] -> Set String
    forall a b. (a -> b) -> a -> b
    $ [Maybe String] -> [String]
    forall a. [Maybe a] -> [a]
    catMaybes [QName -> Maybe String
    getGeneralizedFieldName QName
    q]
              projs Elim' Term
    _                 = Set String
    forall a. Set a
    Set.empty
              early :: [String]
    early = Set String -> [String]
    forall a. Set a -> [a]
    Set.toList (Set String -> [String]) -> Set String -> [String]
    forall a b. (a -> b) -> a -> b
    $ ((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 a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
    foldTerm Term
    u ((Term -> Set String) -> Set String)
    -> (Term -> Set String) -> Set String
    forall a b. (a -> b) -> a -> b
    $ \ case
                      Var Int
    _ Elims
    es   -> (Elim' Term -> Set String) -> Elims -> Set String
    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 (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 (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] -> String
    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
    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
    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
    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
    guess = String
    "After constraint solving it looks like " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    commas [String]
    late String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " actually depend" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++
                      String
    " on " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    commas [String]
    early
                where
                  s :: String
    s | [String] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [String]
    late Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    1 = String
    "s"
                    | Bool
    otherwise        = String
    ""
          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] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
            [ String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    fwords (String -> TCMT IO Doc) -> String -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ String
    "Variable generalization failed."
            , 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 (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [TCMT IO Doc
    "- Probable cause", Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    4 (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
    cause]
            , 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 (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [TCMT IO Doc
    "- Suggestion", Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    4 (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
    solution]
            , 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 (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc
    "- Further information"
                             , 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 -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    order ] [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a. [a] -> [a] -> [a]
    ++
                             [ 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 -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    fwords String
    guess | Bool -> Bool
    not ([String] -> Bool
    forall a. Null a => a -> Bool
    null [String]
    late), Bool -> Bool
    not ([String] -> Bool
    forall a. Null a => a -> Bool
    null [String]
    early) ] [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a. [a] -> [a] -> [a]
    ++
                             [ 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 -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [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
    "The dependency I error is", TCErr -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM TCErr
    err' ] ]
            ]

        addNamedVariablesToScope :: t (Dom' t (Name, b)) -> TCMT IO ()
    addNamedVariablesToScope t (Dom' t (Name, b))
    cxt =
          t (Dom' t (Name, b))
    -> (Dom' t (Name, b) -> TCMT IO ()) -> TCMT IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ t (Dom' t (Name, b))
    cxt ((Dom' t (Name, b) -> TCMT IO ()) -> TCMT IO ())
    -> (Dom' t (Name, b) -> TCMT IO ()) -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ \ Dom{ unDom :: forall t e. Dom' t e -> e
    unDom = (Name
    x, b
    _) } -> 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 (f :: * -> *). Applicative f => Bool -> f () -> f ()
    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 (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 String, 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 -> TCM (Map MetaId QName, Map QName GeneralizedValue)
    createGenValues :: Set QName -> TCM (Map MetaId QName, Map QName GeneralizedValue)
    createGenValues Set QName
    s = do
      [(QName, MetaId, GeneralizedValue)]
    genvals <- Lens' DoGeneralize TCEnv
    -> (DoGeneralize -> DoGeneralize)
    -> TCMT IO [(QName, MetaId, GeneralizedValue)]
    -> TCMT IO [(QName, MetaId, GeneralizedValue)]
    forall (m :: * -> *) a b.
    MonadTCEnv m =>
    Lens' a TCEnv -> (a -> a) -> m b -> m b
    locallyTC Lens' DoGeneralize TCEnv
    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 -> TCMT IO (QName, MetaId, GeneralizedValue))
    -> [QName] -> TCMT IO [(QName, MetaId, GeneralizedValue)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM QName -> TCMT IO (QName, MetaId, GeneralizedValue)
    createGenValue ([QName] -> TCMT IO [(QName, MetaId, GeneralizedValue)])
    -> [QName] -> TCMT IO [(QName, MetaId, GeneralizedValue)]
    forall a b. (a -> b) -> a -> b
    $ (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
      let metaMap :: Map MetaId QName
    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 :: Map QName GeneralizedValue
    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 ]
      (Map MetaId QName, Map QName GeneralizedValue)
    -> TCM (Map MetaId QName, Map QName GeneralizedValue)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Map MetaId QName
    metaMap, Map QName GeneralizedValue
    nameMap)

    -- | Create a generalisable meta for a generalisable variable.
    createGenValue :: QName -> TCM (QName, MetaId, GeneralizedValue)
    createGenValue :: QName -> TCMT IO (QName, MetaId, GeneralizedValue)
    createGenValue QName
    x = QName
    -> TCMT IO (QName, MetaId, GeneralizedValue)
    -> TCMT IO (QName, MetaId, GeneralizedValue)
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange QName
    x (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
    $ do
      CheckpointId
    cp  <- Lens' CheckpointId TCEnv -> TCMT IO CheckpointId
    forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
    viewTC Lens' CheckpointId TCEnv
    eCurrentCheckpoint
      Definition
    def <- Definition -> TCMT IO Definition
    forall (m :: * -> *).
    (Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
     MonadTCEnv m, MonadDebug m) =>
    Definition -> m Definition
    instantiateDef (Definition -> TCMT IO Definition)
    -> TCMT IO Definition -> TCMT IO Definition
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    x
                       -- Only prefix of generalizable arguments (for now?)
      let nGen :: Int
    nGen       = case Definition -> NumGeneralizableArgs
    defArgGeneralizable Definition
    def of
                         NumGeneralizableArgs
    NoGeneralizableArgs     -> Int
    0
                         SomeGeneralizableArgs Int
    n -> Int
    n
          ty :: Type
    ty         = Definition -> Type
    defType Definition
    def
          TelV Telescope
    tel Type
    _ = Type -> TelV Type
    telView' Type
    ty
          -- Generalizable variables are never explicit, so if they're given as
          -- explicit we default to hidden.
          hideExplicit :: a -> a
    hideExplicit a
    arg | a -> Bool
    forall a. LensHiding a => a -> Bool
    visible a
    arg = a -> a
    forall a. LensHiding a => a -> a
    hide a
    arg
                           | Bool
    otherwise   = a
    arg
          argTel :: Telescope
    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
    args <- Telescope -> TCMT IO Args
    forall (m :: * -> *). MonadMetaSolver m => Telescope -> m Args
    newTelMeta Telescope
    argTel
      Type
    metaType <- Type -> Args -> TCM Type
    forall a (m :: * -> *).
    (PiApplyM a, MonadReduce m, HasBuiltins m) =>
    Type -> a -> m Type
    piApplyM Type
    ty Args
    args

      let name :: String
    name     = Name -> String
    forall a. Pretty a => a -> String
    prettyShow (Name -> Name
    nameConcrete (Name -> Name) -> Name -> Name
    forall a b. (a -> b) -> a -> b
    $ QName -> Name
    qnameName QName
    x)
      (MetaId
    m, Term
    term) <- RunMetaOccursCheck
    -> String -> Comparison -> Type -> TCM (MetaId, Term)
    forall (m :: * -> *).
    MonadMetaSolver m =>
    RunMetaOccursCheck
    -> String -> Comparison -> Type -> m (MetaId, Term)
    newNamedValueMeta RunMetaOccursCheck
    DontRunMetaOccursCheck String
    name Comparison
    CmpLeq Type
    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.
      MetaId -> (MetaVariable -> MetaVariable) -> TCMT IO ()
    forall (m :: * -> *).
    MonadMetaSolver m =>
    MetaId -> (MetaVariable -> MetaVariable) -> m ()
    updateMetaVar MetaId
    m ((MetaVariable -> MetaVariable) -> TCMT IO ())
    -> (MetaVariable -> MetaVariable) -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ \ MetaVariable
    mv ->
        Quantity -> MetaVariable -> MetaVariable
    forall a. LensQuantity a => Quantity -> a -> a
    setQuantity (ArgInfo -> Quantity
    forall a. LensQuantity a => a -> Quantity
    getQuantity (Definition -> ArgInfo
    defArgInfo Definition
    def)) (MetaVariable -> MetaVariable) -> MetaVariable -> MetaVariable
    forall a b. (a -> b) -> a -> b
    $
        MetaVariable
    mv { mvFrozen :: Frozen
    mvFrozen = Frozen
    Frozen }

      -- Set up names of arg metas
      [(Integer, Term, Dom (String, Type))]
    -> ((Integer, Term, Dom (String, Type)) -> TCMT IO ())
    -> TCMT IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ ([Integer]
    -> [Term]
    -> [Dom (String, Type)]
    -> [(Integer, Term, Dom (String, Type))]
    forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
    zip3 [Integer
    1..] ((Arg Term -> Term) -> Args -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Term
    forall e. Arg e -> e
    unArg Args
    args) (Telescope -> [Dom (String, Type)]
    forall t. Tele (Dom t) -> [Dom (String, t)]
    telToList Telescope
    argTel)) (((Integer, Term, Dom (String, Type)) -> TCMT IO ()) -> TCMT IO ())
    -> ((Integer, Term, Dom (String, Type)) -> TCMT IO ())
    -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ \ 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 (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.
      MetaId -> ArgInfo -> TCMT IO ()
    forall (m :: * -> *).
    MonadMetaSolver m =>
    MetaId -> ArgInfo -> m ()
    setMetaGeneralizableArgInfo MetaId
    m (ArgInfo -> TCMT IO ()) -> ArgInfo -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> ArgInfo
    forall a. LensHiding a => a -> a
    hideExplicit (Definition -> ArgInfo
    defArgInfo Definition
    def)

      String -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.generalize" Int
    50 (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
    "created metas for generalized variable" 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
    prettyTCM QName
    x
        , 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
    "top  =" 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
    prettyTCM Term
    term
        , 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
    "args =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Args -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Args
    args ]

      case Term
    term of
        MetaV{} -> () -> TCMT IO ()
    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
    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
    prettyTCM Type
    metaType
      (QName, MetaId, GeneralizedValue)
    -> TCMT IO (QName, MetaId, GeneralizedValue)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (QName
    x, MetaId
    m, GeneralizedValue :: CheckpointId -> Term -> Type -> GeneralizedValue
    GeneralizedValue{ genvalCheckpoint :: CheckpointId
    genvalCheckpoint = CheckpointId
    cp
                                    , genvalTerm :: Term
    genvalTerm       = Term
    term
                                    , genvalType :: Type
    genvalType       = Type
    metaType })

    -- | 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 = do
      ModuleName
    current <- TCMT IO ModuleName
    forall (m :: * -> *). MonadTCEnv m => m ModuleName
    currentModule
      let freshQName :: String -> TCMT IO QName
    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
    freshName_ (String
    s :: String)
          mkFieldName :: MetaId -> TCMT IO QName
    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 :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m String
    getMetaNameSuggestion
      [Dom QName]
    genRecFields <- (MetaId -> TCMT IO (Dom QName)) -> [MetaId] -> TCMT IO [Dom QName]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (QName -> Dom QName
    forall a. a -> Dom a
    defaultDom (QName -> Dom QName)
    -> (MetaId -> TCMT IO QName) -> MetaId -> TCMT IO (Dom QName)
    forall (m :: * -> *) b c a.
    Functor m =>
    (b -> c) -> (a -> m b) -> a -> m c
    <.> MetaId -> TCMT IO QName
    mkFieldName) [MetaId]
    sortedMetas
      QName
    genRecName   <- String -> TCMT IO QName
    freshQName String
    "GeneralizeTel"
      ConHead
    genRecCon    <- String -> TCMT IO QName
    freshQName String
    "mkGeneralizeTel" TCMT IO QName -> (QName -> ConHead) -> TCMT IO ConHead
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \ QName
    con -> ConHead :: QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
    ConHead
                      { conName :: QName
    conName      = QName
    con
                      , conDataRecord :: DataOrRecord
    conDataRecord= PatternOrCopattern -> DataOrRecord
    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
                      }
      Int
    projIx <- Int -> Int
    forall a. Enum a => a -> a
    succ (Int -> Int)
    -> ([Dom (Name, Type)] -> Int) -> [Dom (Name, Type)] -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Dom (Name, Type)] -> Int
    forall a. Sized a => a -> Int
    size ([Dom (Name, Type)] -> Int)
    -> TCMT IO [Dom (Name, Type)] -> TCMT IO Int
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO [Dom (Name, Type)]
    forall (m :: * -> *). MonadTCEnv m => m [Dom (Name, Type)]
    getContext
      TCMT IO () -> TCMT IO ()
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [(MetaId, Dom QName)]
    -> ((MetaId, Dom QName) -> TCMT IO ()) -> TCMT IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ ([MetaId] -> [Dom QName] -> [(MetaId, Dom QName)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [MetaId]
    sortedMetas [Dom QName]
    genRecFields) (((MetaId, Dom QName) -> TCMT IO ()) -> TCMT IO ())
    -> ((MetaId, Dom QName) -> TCMT IO ()) -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ \ (MetaId
    meta, Dom QName
    fld) -> do
        Type
    fieldTy <- MetaId -> TCM Type
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m Type
    getMetaType MetaId
    meta
        let field :: QName
    field = Dom QName -> QName
    forall t e. Dom' t e -> e
    unDom Dom QName
    fld
        QName -> ArgInfo -> QName -> Type -> Defn -> TCMT IO ()
    addConstant' QName
    field (Dom QName -> ArgInfo
    forall a. LensArgInfo a => a -> ArgInfo
    getArgInfo Dom QName
    fld) QName
    field Type
    fieldTy (Defn -> TCMT IO ()) -> Defn -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
          let proj :: Projection
    proj = Projection :: Maybe QName -> QName -> Arg QName -> Int -> ProjLams -> Projection
    Projection { projProper :: Maybe QName
    projProper   = QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    genRecName
                                , projOrig :: QName
    projOrig     = QName
    field
                                , projFromType :: Arg QName
    projFromType = QName -> Arg QName
    forall a. a -> Arg a
    defaultArg QName
    genRecName
                                , projIndex :: Int
    projIndex    = Int
    projIx
                                , projLams :: ProjLams
    projLams     = [Arg String] -> ProjLams
    ProjLams [String -> Arg String
    forall a. a -> Arg a
    defaultArg String
    "gtel"] } in
          Function :: [Clause]
    -> Maybe CompiledClauses
    -> Maybe SplitTree
    -> Maybe Compiled
    -> [Clause]
    -> FunctionInverse
    -> Maybe [QName]
    -> IsAbstract
    -> Delayed
    -> Maybe Projection
    -> Set FunctionFlag
    -> Maybe Bool
    -> Maybe ExtLamInfo
    -> Maybe QName
    -> Defn
    Function { funClauses :: [Clause]
    funClauses      = []
                   , funCompiled :: Maybe CompiledClauses
    funCompiled     = Maybe CompiledClauses
    forall a. Maybe a
    Nothing
                   , funSplitTree :: Maybe SplitTree
    funSplitTree    = Maybe SplitTree
    forall a. Maybe a
    Nothing
                   , funTreeless :: Maybe Compiled
    funTreeless     = Maybe Compiled
    forall a. Maybe a
    Nothing
                   , funInv :: FunctionInverse
    funInv          = FunctionInverse
    forall c. FunctionInverse' c
    NotInjective
                   , funMutual :: Maybe [QName]
    funMutual       = [QName] -> Maybe [QName]
    forall a. a -> Maybe a
    Just []
                   , funAbstr :: IsAbstract
    funAbstr        = IsAbstract
    ConcreteDef
                   , funDelayed :: Delayed
    funDelayed      = Delayed
    NotDelayed
                   , funProjection :: Maybe Projection
    funProjection   = Projection -> Maybe Projection
    forall a. a -> Maybe a
    Just Projection
    proj
                   , funFlags :: Set FunctionFlag
    funFlags        = Set FunctionFlag
    forall a. Set a
    Set.empty
                   , funTerminates :: Maybe Bool
    funTerminates   = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    True
                   , funExtLam :: Maybe ExtLamInfo
    funExtLam       = Maybe ExtLamInfo
    forall a. Maybe a
    Nothing
                   , funWith :: Maybe QName
    funWith         = Maybe QName
    forall a. Maybe a
    Nothing
                   , funCovering :: [Clause]
    funCovering     = []
                   }
      QName -> ArgInfo -> QName -> Type -> Defn -> TCMT IO ()
    addConstant' (ConHead -> QName
    conName ConHead
    genRecCon) ArgInfo
    defaultArgInfo (ConHead -> QName
    conName ConHead
    genRecCon) Type
    HasCallStack => Type
    __DUMMY_TYPE__ (Defn -> TCMT IO ()) -> Defn -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ -- Filled in later
        Constructor :: Int
    -> Int
    -> ConHead
    -> QName
    -> IsAbstract
    -> Induction
    -> CompKit
    -> Maybe [QName]
    -> [IsForced]
    -> Maybe [Bool]
    -> Defn
    Constructor { conPars :: Int
    conPars   = Int
    0
                    , conArity :: Int
    conArity  = [Dom QName] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Dom QName]
    genRecFields
                    , conSrcCon :: ConHead
    conSrcCon = ConHead
    genRecCon
                    , conData :: QName
    conData   = QName
    genRecName
                    , conAbstr :: IsAbstract
    conAbstr  = IsAbstract
    ConcreteDef
                    , conInd :: Induction
    conInd    = Induction
    Inductive
                    , conComp :: CompKit
    conComp   = CompKit
    emptyCompKit
                    , conProj :: Maybe [QName]
    conProj   = Maybe [QName]
    forall a. Maybe a
    Nothing
                    , conForced :: [IsForced]
    conForced = []
                    , conErased :: Maybe [Bool]
    conErased = Maybe [Bool]
    forall a. Maybe a
    Nothing
                    }
      let dummyTel :: t -> Telescope
    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)
      QName -> ArgInfo -> QName -> Type -> Defn -> TCMT IO ()
    addConstant' QName
    genRecName ArgInfo
    defaultArgInfo QName
    genRecName (Sort -> Type
    sort Sort
    genRecSort) (Defn -> TCMT IO ()) -> Defn -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
        Record :: Int
    -> Maybe Clause
    -> ConHead
    -> Bool
    -> [Dom QName]
    -> Telescope
    -> Maybe [QName]
    -> EtaEquality
    -> PatternOrCopattern
    -> Maybe Induction
    -> IsAbstract
    -> CompKit
    -> Defn
    Record { recPars :: Int
    recPars         = Int
    0
               , recClause :: Maybe Clause
    recClause       = Maybe Clause
    forall a. Maybe a
    Nothing
               , recConHead :: ConHead
    recConHead      = ConHead
    genRecCon
               , recNamedCon :: Bool
    recNamedCon     = Bool
    False
               , recFields :: [Dom QName]
    recFields       = [Dom QName]
    genRecFields
               , recTel :: Telescope
    recTel          = Int -> Telescope
    forall {t}. (Eq t, Num t) => t -> Telescope
    dummyTel ([Dom QName] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Dom QName]
    genRecFields) -- Filled in later
               , recMutual :: Maybe [QName]
    recMutual       = [QName] -> Maybe [QName]
    forall a. a -> Maybe a
    Just []
               , recEtaEquality' :: EtaEquality
    recEtaEquality' = HasEta -> EtaEquality
    Inferred HasEta
    forall a. HasEta' a
    YesEta
               , recPatternMatching :: PatternOrCopattern
    recPatternMatching = PatternOrCopattern
    CopatternMatching
               , recInduction :: Maybe Induction
    recInduction    = Maybe Induction
    forall a. Maybe a
    Nothing
               , recAbstr :: IsAbstract
    recAbstr        = IsAbstract
    ConcreteDef
               , recComp :: CompKit
    recComp         = CompKit
    emptyCompKit
               }
      String -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.generalize" Int
    20 (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
        [ String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text String
    "created genRec" 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
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList_ ((Dom QName -> TCMT IO Doc) -> [Dom QName] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (String -> TCMT IO Doc)
    -> (Dom QName -> String) -> Dom QName -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> String
    forall a. Pretty a => a -> String
    prettyShow (QName -> String) -> (Dom QName -> QName) -> Dom QName -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom QName -> QName
    forall t e. Dom' t e -> e
    unDom) [Dom QName]
    genRecFields) ]
      String -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.generalize" Int
    80 (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
        [ String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text String
    "created genRec" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text ([Dom QName] -> String
    forall a. Pretty a => a -> String
    prettyShow [Dom QName]
    genRecFields) ]
      -- Solve the genRecMeta
      Args
    args <- TCMT IO Args
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
    getContextArgs
      let genRecTy :: Type
    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
      TCMT IO () -> TCMT IO ()
    forall (m :: * -> *) a.
    (MonadConstraint m, MonadWarning m, MonadError TCErr m,
     MonadFresh ProblemId m) =>
    m a -> m a
    noConstraints (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ Type -> Type -> TCMT IO ()
    forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
    equalType Type
    genRecTy Type
    genRecMeta
      (QName, ConHead, [QName]) -> TCMT IO (QName, ConHead, [QName])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (QName
    genRecName, ConHead
    genRecCon, (Dom QName -> QName) -> [Dom QName] -> [QName]
    forall a b. (a -> b) -> [a] -> [b]
    map Dom QName -> QName
    forall t e. Dom' t e -> e
    unDom [Dom QName]
    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
      Telescope
    cxtTel <- (Dom Type -> Dom Type) -> Telescope -> Telescope
    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 :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
    getContextTelescope
      let fullTel :: Telescope
    fullTel = Telescope
    cxtTel Telescope -> Telescope -> Telescope
    forall t. Abstract t => Telescope -> t -> t
    `abstract` Telescope
    fieldTel
      -- Field types
      let mkFieldTypes :: [QName] -> Telescope -> [Type]
    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 :: [Type]
    fieldTypes = [QName] -> Telescope -> [Type]
    mkFieldTypes [QName]
    fields (Int -> Telescope -> Telescope
    forall a. Subst a => Int -> a -> a
    raise Int
    1 Telescope
    fieldTel)
      String -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.generalize" Int
    40 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text String
    "Field types:" 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
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (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 (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ (Type -> TCMT IO Doc) -> [Type] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM [Type]
    fieldTypes)
      (QName -> Type -> TCMT IO ()) -> [QName] -> [Type] -> TCMT IO ()
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m ()
    zipWithM_ QName -> Type -> TCMT IO ()
    forall {m :: * -> *}. MonadTCState m => QName -> Type -> m ()
    setType [QName]
    fields [Type]
    fieldTypes
      -- Constructor type
      let conType :: Type
    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
      String -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.generalize" Int
    40 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text String
    "Final genRecCon type:" 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
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    conType)
      QName -> Type -> TCMT IO ()
    forall {m :: * -> *}. MonadTCState m => QName -> Type -> m ()
    setType (ConHead -> QName
    conName ConHead
    con) Type
    conType
      -- Record telescope: Includes both parameters and fields.
      QName -> (Definition -> Definition) -> TCMT IO ()
    forall (m :: * -> *).
    MonadTCState m =>
    QName -> (Definition -> Definition) -> m ()
    modifyGlobalDefinition QName
    name ((Definition -> Definition) -> TCMT IO ())
    -> (Definition -> Definition) -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ \ Definition
    r ->
        Definition
    r { theDef :: Defn
    theDef = (Definition -> Defn
    theDef Definition
    r) { recTel :: Telescope
    recTel = Telescope
    fullTel } }
      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 :: Type
    defType = Type
    ty }