    {-# LANGUAGE NondecreasingIndentation #-}

    -- | Solving size constraints under hypotheses.
    --
    -- The size solver proceeds as follows:
    --
    -- 1. Get size constraints, cluster into connected components.
    --
    --    All size constraints that mention the same metas go into the same
    --    cluster.  Each cluster can be solved by itself.
    --
    --    Constraints that do not fit our format are ignored.
    --    We check whether our computed solution fulfills them as well
    --    in the last step.
    --
    -- 2. Find a joint context for each cluster.
    --
    --    Each constraint comes with its own typing context, which
    --    contains size hypotheses @j : Size< i@.  We need to find a
    --    common super context in which all constraints of a cluster live,
    --    and raise all constraints to this context.
    --
    --    There might not be a common super context.  Then we are screwed,
    --    since our solver is not ready to deal with such a situation.  We
    --    will blatantly refuse to solve this cluster and blame it on the
    --    user.
    --
    -- 3. Convert the joint context into a hypothesis graph.
    --
    --    This is straightforward.  Each de Bruijn index becomes a
    --    rigid variable, each typing assumption @j : Size< i@ becomes an
    --    arc.
    --
    -- 4. Convert the constraints into a constraint graph.
    --
    --    Here we need to convert @MetaV@s into flexible variables.
    --
    -- 5. Run the solver
    --
    -- 6. Convert the solution into meta instantiations.
    --
    -- 7. Double-check whether the constraints are solved.

    -- Opportunities for optimization:
    --
    -- - NamedRigids has some cost to retrieve variable names
    --   just for the sake of debug printing.

    module Agda.TypeChecking.SizedTypes.Solve where

    import Prelude hiding (null)

    import Control.Monad hiding (forM, forM_)
    import Control.Monad.Except
    import Control.Monad.Trans.Maybe

    import Data.Either
    import Data.Foldable (forM_)
    import qualified Data.Foldable as Fold
    import Data.Function
    import qualified Data.List as List
    import Data.Monoid
    import qualified Data.Map as Map
    import Data.Set (Set)
    import qualified Data.Set as Set
    import Data.Traversable (forM)

    import Agda.Syntax.Common
    import Agda.Syntax.Internal
    import Agda.Syntax.Internal.MetaVars

    import Agda.TypeChecking.Monad as TCM hiding (Offset)
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Free
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.MetaVars
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Telescope
    import Agda.TypeChecking.Constraints as C

    import qualified Agda.TypeChecking.SizedTypes as S
    import Agda.TypeChecking.SizedTypes.Syntax as Size
    import Agda.TypeChecking.SizedTypes.Utils
    import Agda.TypeChecking.SizedTypes.WarshallSolver as Size

    import Agda.Utils.Cluster
    import Agda.Utils.Function
    import Agda.Utils.Functor
    import Agda.Utils.Lens
    import Agda.Utils.List1 (List1, pattern (:|), nonEmpty, (<|))
    import qualified Agda.Utils.List as List
    import qualified Agda.Utils.List1 as List1
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Null
    import Agda.Utils.Pretty (Pretty, prettyShow)
    import qualified Agda.Utils.Pretty as P
    import Agda.Utils.Singleton
    import Agda.Utils.Size
    import qualified Agda.Utils.VarSet as VarSet

    import Agda.Utils.Impossible

    type CC = ProblemConstraint

    -- | Flag to control the behavior of size solver.
    data DefaultToInfty
      = DefaultToInfty      -- ^ Instantiate all unconstrained size variables to ∞.
      | DontDefaultToInfty  -- ^ Leave unconstrained size variables unsolved.
      deriving (DefaultToInfty -> DefaultToInfty -> Bool
    (DefaultToInfty -> DefaultToInfty -> Bool)
    -> (DefaultToInfty -> DefaultToInfty -> Bool) -> Eq DefaultToInfty
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: DefaultToInfty -> DefaultToInfty -> Bool
    $c/= :: DefaultToInfty -> DefaultToInfty -> Bool
    == :: DefaultToInfty -> DefaultToInfty -> Bool
    $c== :: DefaultToInfty -> DefaultToInfty -> Bool
    Eq, Eq DefaultToInfty
    Eq DefaultToInfty
    -> (DefaultToInfty -> DefaultToInfty -> Ordering)
    -> (DefaultToInfty -> DefaultToInfty -> Bool)
    -> (DefaultToInfty -> DefaultToInfty -> Bool)
    -> (DefaultToInfty -> DefaultToInfty -> Bool)
    -> (DefaultToInfty -> DefaultToInfty -> Bool)
    -> (DefaultToInfty -> DefaultToInfty -> DefaultToInfty)
    -> (DefaultToInfty -> DefaultToInfty -> DefaultToInfty)
    -> Ord DefaultToInfty
    DefaultToInfty -> DefaultToInfty -> Bool
    DefaultToInfty -> DefaultToInfty -> Ordering
    DefaultToInfty -> DefaultToInfty -> DefaultToInfty
    forall a.
    Eq a
    -> (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: DefaultToInfty -> DefaultToInfty -> DefaultToInfty
    $cmin :: DefaultToInfty -> DefaultToInfty -> DefaultToInfty
    max :: DefaultToInfty -> DefaultToInfty -> DefaultToInfty
    $cmax :: DefaultToInfty -> DefaultToInfty -> DefaultToInfty
    >= :: DefaultToInfty -> DefaultToInfty -> Bool
    $c>= :: DefaultToInfty -> DefaultToInfty -> Bool
    > :: DefaultToInfty -> DefaultToInfty -> Bool
    $c> :: DefaultToInfty -> DefaultToInfty -> Bool
    <= :: DefaultToInfty -> DefaultToInfty -> Bool
    $c<= :: DefaultToInfty -> DefaultToInfty -> Bool
    < :: DefaultToInfty -> DefaultToInfty -> Bool
    $c< :: DefaultToInfty -> DefaultToInfty -> Bool
    compare :: DefaultToInfty -> DefaultToInfty -> Ordering
    $ccompare :: DefaultToInfty -> DefaultToInfty -> Ordering
    Ord, Int -> DefaultToInfty -> ShowS
    [DefaultToInfty] -> ShowS
    DefaultToInfty -> [Char]
    (Int -> DefaultToInfty -> ShowS)
    -> (DefaultToInfty -> [Char])
    -> ([DefaultToInfty] -> ShowS)
    -> Show DefaultToInfty
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    showList :: [DefaultToInfty] -> ShowS
    $cshowList :: [DefaultToInfty] -> ShowS
    show :: DefaultToInfty -> [Char]
    $cshow :: DefaultToInfty -> [Char]
    showsPrec :: Int -> DefaultToInfty -> ShowS
    $cshowsPrec :: Int -> DefaultToInfty -> ShowS
    Show)

    -- | Solve size constraints involving hypotheses.

    solveSizeConstraints :: DefaultToInfty -> TCM ()
    solveSizeConstraints :: DefaultToInfty -> TCM ()
    solveSizeConstraints DefaultToInfty
    flag =  do

      -- 1. Take out the size constraints normalised.

      let norm :: ProblemConstraint -> m ProblemConstraint
    norm ProblemConstraint
    c = (Constraint -> m Constraint)
    -> Closure Constraint -> m (Closure Constraint)
    forall (m :: * -> *) a b.
    (MonadTCEnv m, ReadTCState m) =>
    (a -> m b) -> Closure a -> m (Closure b)
    mapClosure Constraint -> m Constraint
    forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
    normalise (ProblemConstraint -> Closure Constraint
    theConstraint ProblemConstraint
    c) m (Closure Constraint)
    -> (Closure Constraint -> ProblemConstraint) -> m ProblemConstraint
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \ Closure Constraint
    cl -> ProblemConstraint
    c { theConstraint :: Closure Constraint
    theConstraint = Closure Constraint
    cl }
      [ProblemConstraint]
    cs0 <- (ProblemConstraint -> TCMT IO ProblemConstraint)
    -> [ProblemConstraint] -> TCMT IO [ProblemConstraint]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM ProblemConstraint -> TCMT IO ProblemConstraint
    forall {m :: * -> *}.
    MonadReduce m =>
    ProblemConstraint -> m ProblemConstraint
    norm ([ProblemConstraint] -> TCMT IO [ProblemConstraint])
    -> TCMT IO [ProblemConstraint] -> TCMT IO [ProblemConstraint]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< (Comparison -> Bool) -> TCMT IO [ProblemConstraint]
    S.takeSizeConstraints (Comparison -> Comparison -> Bool
    forall a. Eq a => a -> a -> Bool
    == Comparison
    CmpLeq)
        -- NOTE: this deletes the size constraints from the constraint set!
      Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([ProblemConstraint] -> Bool
    forall a. Null a => a -> Bool
    null [ProblemConstraint]
    cs0) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
        [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.size.solve" Int
    40 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    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
    $
          [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ( [Char]
    "Solving constraints (" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ DefaultToInfty -> [Char]
    forall a. Show a => a -> [Char]
    show DefaultToInfty
    flag [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ")" ) TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a. a -> [a] -> [a]
    : (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]
    cs0
      let -- Error for giving up
          cannotSolve :: TCM a -- Defined, but not currently used
          cannotSolve :: forall a. TCM a
    cannotSolve = TypeError -> TCMT IO a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO a) -> (Doc -> TypeError) -> Doc -> TCMT IO a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> TypeError
    GenericDocError (Doc -> TCMT IO a) -> TCMT IO Doc -> TCMT IO a
    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 (TCMT IO Doc
    "Cannot solve size constraints" TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a. a -> [a] -> [a]
    : (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]
    cs0)

      -- 2. Cluster the constraints by common size metas.

      -- Get all size metas.
      Set MetaId
    sizeMetaSet <- [MetaId] -> Set MetaId
    forall a. Ord a => [a] -> Set a
    Set.fromList ([MetaId] -> Set MetaId)
    -> ([(MetaId, Type, Tele (Dom Type))] -> [MetaId])
    -> [(MetaId, Type, Tele (Dom Type))]
    -> Set MetaId
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((MetaId, Type, Tele (Dom Type)) -> MetaId)
    -> [(MetaId, Type, Tele (Dom Type))] -> [MetaId]
    forall a b. (a -> b) -> [a] -> [b]
    map (\ (MetaId
    x, Type
    _t, Tele (Dom Type)
    _tel) -> MetaId
    x) ([(MetaId, Type, Tele (Dom Type))] -> Set MetaId)
    -> TCMT IO [(MetaId, Type, Tele (Dom Type))]
    -> TCMT IO (Set MetaId)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Bool -> TCMT IO [(MetaId, Type, Tele (Dom Type))]
    S.getSizeMetas Bool
    True

      -- Pair each constraint with its list of size metas occurring in it.
      [(ProblemConstraint, [Int])]
    cms <- [ProblemConstraint]
    -> (ProblemConstraint -> TCMT IO (ProblemConstraint, [Int]))
    -> TCMT IO [(ProblemConstraint, [Int])]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [ProblemConstraint]
    cs0 ((ProblemConstraint -> TCMT IO (ProblemConstraint, [Int]))
     -> TCMT IO [(ProblemConstraint, [Int])])
    -> (ProblemConstraint -> TCMT IO (ProblemConstraint, [Int]))
    -> TCMT IO [(ProblemConstraint, [Int])]
    forall a b. (a -> b) -> a -> b
    $ \ ProblemConstraint
    cl -> Closure Constraint
    -> (Constraint -> TCMT IO (ProblemConstraint, [Int]))
    -> TCMT IO (ProblemConstraint, [Int])
    forall (m :: * -> *) a c b.
    (MonadTCEnv m, ReadTCState m, LensClosure a c) =>
    c -> (a -> m b) -> m b
    enterClosure (ProblemConstraint -> Closure Constraint
    theConstraint ProblemConstraint
    cl) ((Constraint -> TCMT IO (ProblemConstraint, [Int]))
     -> TCMT IO (ProblemConstraint, [Int]))
    -> (Constraint -> TCMT IO (ProblemConstraint, [Int]))
    -> TCMT IO (ProblemConstraint, [Int])
    forall a b. (a -> b) -> a -> b
    $ \ Constraint
    c -> do

        -- @allMetas@ does not reduce or instantiate;
        -- this is why we require the size constraints to be normalised.
        (ProblemConstraint, [Int]) -> TCMT IO (ProblemConstraint, [Int])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ProblemConstraint
    cl, (MetaId -> Int) -> [MetaId] -> [Int]
    forall a b. (a -> b) -> [a] -> [b]
    map MetaId -> Int
    metaId ([MetaId] -> [Int])
    -> (Set MetaId -> [MetaId]) -> Set MetaId -> [Int]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Set MetaId -> [MetaId]
    forall a. Set a -> [a]
    Set.toList (Set MetaId -> [Int]) -> Set MetaId -> [Int]
    forall a b. (a -> b) -> a -> b
    $
          Set MetaId
    sizeMetaSet Set MetaId -> Set MetaId -> Set MetaId
    forall a. Ord a => Set a -> Set a -> Set a
    `Set.intersection` (MetaId -> Set MetaId) -> Constraint -> Set MetaId
    forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
    allMetas MetaId -> Set MetaId
    forall el coll. Singleton el coll => el -> coll
    singleton Constraint
    c)

      -- Now, some constraints may have no metas (clcs), the others have at least one (othercs).
      let classify :: (a, [b]) -> Either a (a, List1 b)
          classify :: forall a b. (a, [b]) -> Either a (a, List1 b)
    classify (a
    cl, [])     = a -> Either a (a, List1 b)
    forall a b. a -> Either a b
    Left  a
    cl
          classify (a
    cl, (b
    x:[b]
    xs)) = (a, List1 b) -> Either a (a, List1 b)
    forall a b. b -> Either a b
    Right (a
    cl, b
    x b -> [b] -> List1 b
    forall a. a -> [a] -> NonEmpty a
    :| [b]
    xs)
      let ([ProblemConstraint]
    clcs, [(ProblemConstraint, List1 Int)]
    othercs) = [Either ProblemConstraint (ProblemConstraint, List1 Int)]
    -> ([ProblemConstraint], [(ProblemConstraint, List1 Int)])
    forall a b. [Either a b] -> ([a], [b])
    partitionEithers ([Either ProblemConstraint (ProblemConstraint, List1 Int)]
     -> ([ProblemConstraint], [(ProblemConstraint, List1 Int)]))
    -> [Either ProblemConstraint (ProblemConstraint, List1 Int)]
    -> ([ProblemConstraint], [(ProblemConstraint, List1 Int)])
    forall a b. (a -> b) -> a -> b
    $ ((ProblemConstraint, [Int])
     -> Either ProblemConstraint (ProblemConstraint, List1 Int))
    -> [(ProblemConstraint, [Int])]
    -> [Either ProblemConstraint (ProblemConstraint, List1 Int)]
    forall a b. (a -> b) -> [a] -> [b]
    map (ProblemConstraint, [Int])
    -> Either ProblemConstraint (ProblemConstraint, List1 Int)
    forall a b. (a, [b]) -> Either a (a, List1 b)
    classify [(ProblemConstraint, [Int])]
    cms

      -- We cluster the constraints by their metas.
      let ccs :: [NonEmpty ProblemConstraint]
    ccs = [(ProblemConstraint, List1 Int)] -> [NonEmpty ProblemConstraint]
    forall a. [(a, List1 Int)] -> [NonEmpty a]
    cluster' [(ProblemConstraint, List1 Int)]
    othercs

      -- 3. Solve each cluster

      -- Solve the closed constraints, one by one.

      [ProblemConstraint] -> (ProblemConstraint -> TCM ()) -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [ProblemConstraint]
    clcs ((ProblemConstraint -> TCM ()) -> TCM ())
    -> (ProblemConstraint -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ ProblemConstraint
    c -> () () -> TCMT IO (Set MetaId) -> TCM ()
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ DefaultToInfty -> [ProblemConstraint] -> TCMT IO (Set MetaId)
    solveSizeConstraints_ DefaultToInfty
    flag [ProblemConstraint
    c]

      -- Solve the clusters.

      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)
    -> TCM [Set MetaId] -> TCMT IO (Set MetaId)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
        [NonEmpty ProblemConstraint]
    -> (NonEmpty ProblemConstraint -> TCMT IO (Set MetaId))
    -> TCM [Set MetaId]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM  ([NonEmpty ProblemConstraint]
    ccs) ((NonEmpty ProblemConstraint -> TCMT IO (Set MetaId))
     -> TCM [Set MetaId])
    -> (NonEmpty ProblemConstraint -> TCMT IO (Set MetaId))
    -> TCM [Set MetaId]
    forall a b. (a -> b) -> a -> b
    $ \ (NonEmpty ProblemConstraint
    cs :: List1 CC) -> do

          [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.size.solve" Int
    60 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ NonEmpty (TCMT IO Doc) -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat (NonEmpty (TCMT IO Doc) -> TCMT IO Doc)
    -> NonEmpty (TCMT IO Doc) -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $
            TCMT IO Doc
    "size constraint cluster:" TCMT IO Doc -> NonEmpty (TCMT IO Doc) -> NonEmpty (TCMT IO Doc)
    forall a. a -> NonEmpty a -> NonEmpty a
    <| (ProblemConstraint -> TCMT IO Doc)
    -> NonEmpty ProblemConstraint -> NonEmpty (TCMT IO Doc)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ([Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc)
    -> (ProblemConstraint -> [Char])
    -> ProblemConstraint
    -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ProblemConstraint -> [Char]
    forall a. Show a => a -> [Char]
    show) NonEmpty ProblemConstraint
    cs

          -- Convert each constraint in the cluster to the largest context.
          -- (Keep fingers crossed).

          Closure Constraint
    -> (Constraint -> TCMT IO (Set MetaId)) -> TCMT IO (Set MetaId)
    forall (m :: * -> *) a c b.
    (MonadTCEnv m, ReadTCState m, LensClosure a c) =>
    c -> (a -> m b) -> m b
    enterClosure ((Closure Constraint -> Closure Constraint -> Ordering)
    -> NonEmpty (Closure Constraint) -> Closure Constraint
    forall (t :: * -> *) a.
    Foldable t =>
    (a -> a -> Ordering) -> t a -> a
    Fold.maximumBy (Int -> Int -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (Int -> Int -> Ordering)
    -> (Closure Constraint -> Int)
    -> Closure Constraint
    -> Closure Constraint
    -> Ordering
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` (Context -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length (Context -> Int)
    -> (Closure Constraint -> Context) -> Closure Constraint -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TCEnv -> Context
    envContext (TCEnv -> Context)
    -> (Closure Constraint -> TCEnv) -> Closure Constraint -> Context
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Closure Constraint -> TCEnv
    forall a. Closure a -> TCEnv
    clEnv)) (NonEmpty (Closure Constraint) -> Closure Constraint)
    -> NonEmpty (Closure Constraint) -> Closure Constraint
    forall a b. (a -> b) -> a -> b
    $ (ProblemConstraint -> Closure Constraint)
    -> NonEmpty ProblemConstraint -> NonEmpty (Closure Constraint)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ProblemConstraint -> Closure Constraint
    theConstraint NonEmpty ProblemConstraint
    cs) ((Constraint -> TCMT IO (Set MetaId)) -> TCMT IO (Set MetaId))
    -> (Constraint -> TCMT IO (Set MetaId)) -> TCMT IO (Set MetaId)
    forall a b. (a -> b) -> a -> b
    $ \ Constraint
    _ -> do
            -- Get all constraints that can be cast to the longest context.
            [ProblemConstraint]
    cs' :: [ProblemConstraint] <- List1 (Maybe ProblemConstraint) -> [ProblemConstraint]
    forall a. List1 (Maybe a) -> [a]
    List1.catMaybes (List1 (Maybe ProblemConstraint) -> [ProblemConstraint])
    -> TCM (List1 (Maybe ProblemConstraint))
    -> TCMT IO [ProblemConstraint]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
              (ProblemConstraint -> TCM (Maybe ProblemConstraint))
    -> NonEmpty ProblemConstraint
    -> TCM (List1 (Maybe ProblemConstraint))
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (MaybeT (TCMT IO) ProblemConstraint -> TCM (Maybe ProblemConstraint)
    forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
    runMaybeT (MaybeT (TCMT IO) ProblemConstraint
     -> TCM (Maybe ProblemConstraint))
    -> (ProblemConstraint -> MaybeT (TCMT IO) ProblemConstraint)
    -> ProblemConstraint
    -> TCM (Maybe ProblemConstraint)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ProblemConstraint -> MaybeT (TCMT IO) ProblemConstraint
    castConstraintToCurrentContext) NonEmpty ProblemConstraint
    cs

            [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.size.solve" Int
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    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
    "converted size constraints to context: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> do
                  Tele (Dom Type)
    tel <- TCMT IO (Tele (Dom Type))
    forall (m :: * -> *).
    (Applicative m, MonadTCEnv m) =>
    m (Tele (Dom Type))
    getContextTelescope
                  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
    $ Tele (Dom Type) -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Tele (Dom Type)
    tel
              ) TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a. a -> [a] -> [a]
    : (ProblemConstraint -> TCMT IO Doc)
    -> [ProblemConstraint] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (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)
    -> (ProblemConstraint -> TCMT IO Doc)
    -> ProblemConstraint
    -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ProblemConstraint -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM) [ProblemConstraint]
    cs'

            -- Solve the converted constraints.
            DefaultToInfty -> [ProblemConstraint] -> TCMT IO (Set MetaId)
    solveSizeConstraints_ DefaultToInfty
    flag [ProblemConstraint]
    cs'

      -- 4. Possibly set remaining metas to infinity.

      -- Andreas, issue 1862: do not default to ∞ always, could be too early.
      Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (DefaultToInfty
    flag DefaultToInfty -> DefaultToInfty -> Bool
    forall a. Eq a => a -> a -> Bool
    == DefaultToInfty
    DefaultToInfty) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do

        -- let constrainedMetas = Set.fromList $ concat $
        --       for cs0 $ \ Closure{ clValue = ValueCmp _ _ u v } ->
        --         allMetas u ++ allMetas v

        -- Set the unconstrained, open size metas to ∞.
        [(MetaId, Type, Tele (Dom Type))]
    ms <- Bool -> TCMT IO [(MetaId, Type, Tele (Dom Type))]
    S.getSizeMetas Bool
    False -- do not get interaction metas
        Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([(MetaId, Type, Tele (Dom Type))] -> Bool
    forall a. Null a => a -> Bool
    null [(MetaId, Type, Tele (Dom Type))]
    ms) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
          Term
    inf <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primSizeInf
          [(MetaId, Type, Tele (Dom Type))]
    -> ((MetaId, Type, Tele (Dom Type)) -> TCM ()) -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [(MetaId, Type, Tele (Dom Type))]
    ms (((MetaId, Type, Tele (Dom Type)) -> TCM ()) -> TCM ())
    -> ((MetaId, Type, Tele (Dom Type)) -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ (MetaId
    m, Type
    t, Tele (Dom Type)
    tel) -> do
            Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (MetaId
    m MetaId -> Set MetaId -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set MetaId
    constrainedMetas) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
            TCMT IO Bool -> TCM () -> TCM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    unlessM (MetaId -> TCMT IO Bool
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m Bool
    isFrozen MetaId
    m) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
            [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.size.solve" Int
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
              TCMT IO Doc
    "solution " 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 (MetaId -> Elims -> Term
    MetaV 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 Term
    inf
            Int -> MetaId -> Type -> [Int] -> Term -> TCM ()
    assignMeta Int
    0 MetaId
    m Type
    t (Int -> [Int]
    forall a. Integral a => a -> [a]
    List.downFrom (Int -> [Int]) -> Int -> [Int]
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    tel) Term
    inf

      -- -- Double check.
      -- unless (null cs0 && null ms) $ do
      --   flip catchError (const cannotSolve) $
      --     noConstraints $
      --       forM_ cs0 $ \ cl -> enterClosure cl solveConstraint

      -- 5. Make sure we did not lose any constraints.

      -- This is necessary since we have removed the size constraints.
      [ProblemConstraint] -> (ProblemConstraint -> TCM ()) -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [ProblemConstraint]
    cs0 ((ProblemConstraint -> TCM ()) -> TCM ())
    -> (ProblemConstraint -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ (Constraint -> TCM ()) -> ProblemConstraint -> TCM ()
    forall (m :: * -> *) a.
    MonadConstraint m =>
    (Constraint -> m a) -> ProblemConstraint -> m a
    withConstraint Constraint -> TCM ()
    forall (m :: * -> *). MonadConstraint m => Constraint -> m ()
    solveConstraint

    -- | TODO: this does not actually work!
    --
    --   We would like to use a constraint @c@ created in context @Δ@ from module @N@
    --   in the current context @Γ@ and current module @M@.
    --
    --   @Δ@ is module tel @Δ₁@ of @N@ extended by some local bindings @Δ₂@.
    --   @Γ@ is the current context.
    --   The module parameter substitution from current @M@ to @N@ be
    --   @Γ ⊢ σ : Δ₁@.
    --
    --   If @M == N@, we do not need the parameter substitution.  We try raising.
    --
    --   We first strengthen @Δ ⊢ c@ to live in @Δ₁@ and obtain @c₁ = strengthen Δ₂ c@.
    --   We then transport @c₁@ to @Γ@ and obtain @c₂ = applySubst σ c₁@.
    --
    --   This works for different modules, but if @M == N@ we should not strengthen
    --   and then weaken, because strengthening is a partial operation.
    --   We should rather lift the substitution @σ@ by @Δ₂@ and then
    --   raise by @Γ₂ - Δ₂@.
    --   This "raising" might be a strengthening if @Γ₂@ is shorter than @Δ₂@.
    --
    --   (TODO: If the module substitution does not exist, because @N@ is not
    --   a parent of @M@, we cannot use the constraint, as it has been created
    --   in an unrelated context.)

    castConstraintToCurrentContext' :: Closure TCM.Constraint -> MaybeT TCM TCM.Constraint
    castConstraintToCurrentContext' :: Closure Constraint -> MaybeT (TCMT IO) Constraint
    castConstraintToCurrentContext' Closure Constraint
    cl = do
      let modN :: ModuleName
    modN  = TCEnv -> ModuleName
    envCurrentModule (TCEnv -> ModuleName) -> TCEnv -> ModuleName
    forall a b. (a -> b) -> a -> b
    $ Closure Constraint -> TCEnv
    forall a. Closure a -> TCEnv
    clEnv Closure Constraint
    cl
          delta :: Context
    delta = TCEnv -> Context
    envContext (TCEnv -> Context) -> TCEnv -> Context
    forall a b. (a -> b) -> a -> b
    $ Closure Constraint -> TCEnv
    forall a. Closure a -> TCEnv
    clEnv Closure Constraint
    cl
      -- The module telescope of the constraint.
      -- The constraint could come from the module telescope of the top level module.
      -- In this case, it does not live in any module!
      -- Thus, getSection can return Nothing.
      Tele (Dom Type)
    delta1 <- TCMT IO (Tele (Dom Type)) -> MaybeT (TCMT IO) (Tele (Dom Type))
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO (Tele (Dom Type)) -> MaybeT (TCMT IO) (Tele (Dom Type)))
    -> TCMT IO (Tele (Dom Type)) -> MaybeT (TCMT IO) (Tele (Dom Type))
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type)
    -> (Section -> Tele (Dom Type)) -> Maybe Section -> Tele (Dom Type)
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Tele (Dom Type)
    forall a. Null a => a
    empty (Section -> Lens' (Tele (Dom Type)) Section -> Tele (Dom Type)
    forall o i. o -> Lens' i o -> i
    ^. Lens' (Tele (Dom Type)) Section
    secTelescope) (Maybe Section -> Tele (Dom Type))
    -> TCMT IO (Maybe Section) -> TCMT IO (Tele (Dom Type))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ModuleName -> TCMT IO (Maybe Section)
    forall (m :: * -> *).
    (Functor m, ReadTCState m) =>
    ModuleName -> m (Maybe Section)
    getSection ModuleName
    modN
      -- The number of locals of the constraint.
      let delta2 :: Int
    delta2 = Context -> Int
    forall a. Sized a => a -> Int
    size Context
    delta Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    delta1
      Bool -> MaybeT (TCMT IO) () -> MaybeT (TCMT IO) ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Int
    delta2 Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    0) MaybeT (TCMT IO) ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__

      -- The current module M and context Γ.
      ModuleName
    modM  <- MaybeT (TCMT IO) ModuleName
    forall (m :: * -> *). MonadTCEnv m => m ModuleName
    currentModule
      Int
    gamma <- TCM Int -> MaybeT (TCMT IO) Int
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM Int -> MaybeT (TCMT IO) Int)
    -> TCM Int -> MaybeT (TCMT IO) Int
    forall a b. (a -> b) -> a -> b
    $ TCM Int
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Int
    getContextSize
      -- The current module telescope.
      -- Could also be empty, if we are in the front matter or telescope of the top-level module.
      Tele (Dom Type)
    gamma1 <-TCMT IO (Tele (Dom Type)) -> MaybeT (TCMT IO) (Tele (Dom Type))
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO (Tele (Dom Type)) -> MaybeT (TCMT IO) (Tele (Dom Type)))
    -> TCMT IO (Tele (Dom Type)) -> MaybeT (TCMT IO) (Tele (Dom Type))
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type)
    -> (Section -> Tele (Dom Type)) -> Maybe Section -> Tele (Dom Type)
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Tele (Dom Type)
    forall a. Null a => a
    empty (Section -> Lens' (Tele (Dom Type)) Section -> Tele (Dom Type)
    forall o i. o -> Lens' i o -> i
    ^. Lens' (Tele (Dom Type)) Section
    secTelescope) (Maybe Section -> Tele (Dom Type))
    -> TCMT IO (Maybe Section) -> TCMT IO (Tele (Dom Type))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ModuleName -> TCMT IO (Maybe Section)
    forall (m :: * -> *).
    (Functor m, ReadTCState m) =>
    ModuleName -> m (Maybe Section)
    getSection ModuleName
    modM
      -- The current locals.
      let gamma2 :: Int
    gamma2 = Int
    gamma Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    gamma1

      -- Γ ⊢ σ : Δ₁
      Substitution' Term
    sigma <- TCM (Substitution' Term) -> MaybeT (TCMT IO) (Substitution' Term)
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM (Substitution' Term) -> MaybeT (TCMT IO) (Substitution' Term))
    -> TCM (Substitution' Term)
    -> MaybeT (TCMT IO) (Substitution' Term)
    forall a b. (a -> b) -> a -> b
    $ Substitution' Term
    -> Maybe (Substitution' Term) -> Substitution' Term
    forall a. a -> Maybe a -> a
    fromMaybe Substitution' Term
    forall a. Substitution' a
    idS (Maybe (Substitution' Term) -> Substitution' Term)
    -> TCMT IO (Maybe (Substitution' Term)) -> TCM (Substitution' Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ModuleName -> TCMT IO (Maybe (Substitution' Term))
    forall (m :: * -> *).
    (MonadTCEnv m, ReadTCState m) =>
    ModuleName -> m (Maybe (Substitution' Term))
    getModuleParameterSub ModuleName
    modN

      -- Debug printing.
      [Char] -> Int -> TCMT IO Doc -> MaybeT (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.constr.cast" Int
    40 (TCMT IO Doc -> MaybeT (TCMT IO) ())
    -> TCMT IO Doc -> MaybeT (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "casting constraint" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    $$ do
        Tele (Dom Type)
    tel <- TCMT IO (Tele (Dom Type))
    forall (m :: * -> *).
    (Applicative m, MonadTCEnv m) =>
    m (Tele (Dom Type))
    getContextTelescope
        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
    $ 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
    $
          [ TCMT IO Doc
    "current module                = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ModuleName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM ModuleName
    modM
          , TCMT IO Doc
    "current module telescope      = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Tele (Dom Type) -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Tele (Dom Type)
    gamma1
          , TCMT IO Doc
    "current context               = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Tele (Dom Type) -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Tele (Dom Type)
    tel
          , TCMT IO Doc
    "constraint module             = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ModuleName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM ModuleName
    modN
          , TCMT IO Doc
    "constraint module telescope   = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Tele (Dom Type) -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Tele (Dom Type)
    delta1
          , TCMT IO Doc
    "constraint context            = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (Tele (Dom Type) -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Tele (Dom Type) -> TCMT IO Doc)
    -> TCMT IO (Tele (Dom Type)) -> TCMT IO Doc
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Closure Constraint
    -> (Constraint -> TCMT IO (Tele (Dom Type)))
    -> TCMT IO (Tele (Dom Type))
    forall (m :: * -> *) a c b.
    (MonadTCEnv m, ReadTCState m, LensClosure a c) =>
    c -> (a -> m b) -> m b
    enterClosure Closure Constraint
    cl (TCMT IO (Tele (Dom Type))
    -> Constraint -> TCMT IO (Tele (Dom Type))
    forall a b. a -> b -> a
    const (TCMT IO (Tele (Dom Type))
     -> Constraint -> TCMT IO (Tele (Dom Type)))
    -> TCMT IO (Tele (Dom Type))
    -> Constraint
    -> TCMT IO (Tele (Dom Type))
    forall a b. (a -> b) -> a -> b
    $ TCMT IO (Tele (Dom Type))
    forall (m :: * -> *).
    (Applicative m, MonadTCEnv m) =>
    m (Tele (Dom Type))
    getContextTelescope))
          , TCMT IO Doc
    "constraint                    = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Closure Constraint -> (Constraint -> TCMT IO Doc) -> TCMT IO Doc
    forall (m :: * -> *) a c b.
    (MonadTCEnv m, ReadTCState m, LensClosure a c) =>
    c -> (a -> m b) -> m b
    enterClosure Closure Constraint
    cl Constraint -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM
          , TCMT IO Doc
    "module parameter substitution = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Substitution' Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Substitution' Term
    sigma
          ]

      -- If gamma2 < 0, we must be in the wrong context.
      -- E.g. we could have switched to the empty context even though
      -- we are still inside a module with parameters.
      -- In this case, we cannot safely convert the constraint,
      -- since the module parameter substitution may be wrong.
      Bool -> MaybeT (TCMT IO) ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Int
    gamma2 Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    0)

      -- Shortcut for modN == modM:
      -- Raise constraint from Δ to Γ, if possible.
      -- This might save us some strengthening.
      if ModuleName
    modN ModuleName -> ModuleName -> Bool
    forall a. Eq a => a -> a -> Bool
    == ModuleName
    modM then Int -> Constraint -> MaybeT (TCMT IO) Constraint
    forall {m :: * -> *} {b}.
    (Monad m, Alternative m, Free b, Subst b) =>
    Int -> b -> m b
    raiseMaybe (Int
    gamma Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Context -> Int
    forall a. Sized a => a -> Int
    size Context
    delta) (Constraint -> MaybeT (TCMT IO) Constraint)
    -> Constraint -> MaybeT (TCMT IO) Constraint
    forall a b. (a -> b) -> a -> b
    $ Closure Constraint -> Constraint
    forall a. Closure a -> a
    clValue Closure Constraint
    cl else do

      -- Strengthen constraint to Δ₁ ⊢ c
      Constraint
    c <- Int -> Constraint -> MaybeT (TCMT IO) Constraint
    forall {m :: * -> *} {b}.
    (Monad m, Alternative m, Free b, Subst b) =>
    Int -> b -> m b
    raiseMaybe (-Int
    delta2) (Constraint -> MaybeT (TCMT IO) Constraint)
    -> Constraint -> MaybeT (TCMT IO) Constraint
    forall a b. (a -> b) -> a -> b
    $ Closure Constraint -> Constraint
    forall a. Closure a -> a
    clValue Closure Constraint
    cl

      -- Ulf, 2016-11-09: I don't understand what this function does when M and N
      -- are not related. Certainly things can go terribly wrong (see
      -- test/Succeed/Issue2223b.agda)
      Int
    fv <- TCM Int -> MaybeT (TCMT IO) Int
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM Int -> MaybeT (TCMT IO) Int)
    -> TCM Int -> MaybeT (TCMT IO) Int
    forall a b. (a -> b) -> a -> b
    $ ModuleName -> TCM Int
    forall (m :: * -> *).
    (Functor m, Applicative m, MonadTCEnv m, ReadTCState m) =>
    ModuleName -> m Int
    getModuleFreeVars ModuleName
    modN
      Bool -> MaybeT (TCMT IO) ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Bool -> MaybeT (TCMT IO) ()) -> Bool -> MaybeT (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ Int
    fv Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    delta1

      -- Γ ⊢ c[σ]
      Constraint -> MaybeT (TCMT IO) Constraint
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Constraint -> MaybeT (TCMT IO) Constraint)
    -> Constraint -> MaybeT (TCMT IO) Constraint
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg Constraint) -> Constraint -> Constraint
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' Term
    Substitution' (SubstArg Constraint)
    sigma Constraint
    c
      where
        raiseMaybe :: Int -> b -> m b
    raiseMaybe Int
    n b
    c = do
          -- Fine if we have to weaken or strengthening is safe.
          Bool -> m ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Bool -> m ()) -> Bool -> m ()
    forall a b. (a -> b) -> a -> b
    $ Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    0 Bool -> Bool -> Bool
    || (Int -> Bool) -> [Int] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    List.all (Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= -Int
    n) (IntSet -> [Int]
    VarSet.toList (IntSet -> [Int]) -> IntSet -> [Int]
    forall a b. (a -> b) -> a -> b
    $ b -> IntSet
    forall t. Free t => t -> IntSet
    allFreeVars b
    c)
          b -> m b
    forall (m :: * -> *) a. Monad m => a -> m a
    return (b -> m b) -> b -> m b
    forall a b. (a -> b) -> a -> b
    $ Int -> b -> b
    forall a. Subst a => Int -> a -> a
    raise Int
    n b
    c

    -- | A hazardous hack, may the Gods have mercy on us.
    --
    --   To cast to the current context, we match the context of the
    --   given constraint by 'CtxId', and as fallback, by variable name (douh!).
    --
    --   This hack lets issue 2046 go through.

    castConstraintToCurrentContext :: ProblemConstraint -> MaybeT TCM ProblemConstraint
    castConstraintToCurrentContext :: ProblemConstraint -> MaybeT (TCMT IO) ProblemConstraint
    castConstraintToCurrentContext ProblemConstraint
    c = do
      -- The checkpoint of the contraint
      let cl :: Closure Constraint
    cl = ProblemConstraint -> Closure Constraint
    theConstraint ProblemConstraint
    c
          cp :: CheckpointId
    cp = TCEnv -> CheckpointId
    envCurrentCheckpoint (TCEnv -> CheckpointId) -> TCEnv -> CheckpointId
    forall a b. (a -> b) -> a -> b
    $ Closure Constraint -> TCEnv
    forall a. Closure a -> TCEnv
    clEnv Closure Constraint
    cl
      Substitution' Term
    sigma <- MaybeT (TCMT IO) (Maybe (Substitution' Term))
    -> MaybeT (TCMT IO) (Substitution' Term)
    -> (Substitution' Term -> MaybeT (TCMT IO) (Substitution' Term))
    -> MaybeT (TCMT IO) (Substitution' Term)
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (Lens' (Maybe (Substitution' Term)) TCEnv
    -> MaybeT (TCMT IO) (Maybe (Substitution' Term))
    forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
    viewTC (Lens' (Maybe (Substitution' Term)) TCEnv
     -> MaybeT (TCMT IO) (Maybe (Substitution' Term)))
    -> Lens' (Maybe (Substitution' Term)) TCEnv
    -> MaybeT (TCMT IO) (Maybe (Substitution' Term))
    forall a b. (a -> b) -> a -> b
    $ (Map CheckpointId (Substitution' Term)
     -> f (Map CheckpointId (Substitution' Term)))
    -> TCEnv -> f TCEnv
    Lens' (Map CheckpointId (Substitution' Term)) TCEnv
    eCheckpoints ((Map CheckpointId (Substitution' Term)
      -> f (Map CheckpointId (Substitution' Term)))
     -> TCEnv -> f TCEnv)
    -> ((Maybe (Substitution' Term) -> f (Maybe (Substitution' Term)))
        -> Map CheckpointId (Substitution' Term)
        -> f (Map CheckpointId (Substitution' Term)))
    -> (Maybe (Substitution' Term) -> f (Maybe (Substitution' Term)))
    -> TCEnv
    -> f TCEnv
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CheckpointId
    -> Lens'
         (Maybe (Substitution' Term))
         (Map CheckpointId (Substitution' Term))
    forall k v. Ord k => k -> Lens' (Maybe v) (Map k v)
    key CheckpointId
    cp)
              (do
                -- We are not in a descendant of the constraint checkpoint.
                -- Here be dragons!!
                Context
    gamma <- (TCEnv -> Context) -> MaybeT (TCMT IO) Context
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Context
    envContext -- The target context
                let findInGamma :: Dom' Term (Name, Type) -> Maybe Int
    findInGamma (Dom {unDom :: forall t e. Dom' t e -> e
    unDom = (Name
    x, Type
    t)}) =
                      -- match by name (hazardous)
                      -- This is one of the seven deadly sins (not respecting alpha).
                      (Dom' Term (Name, Type) -> Bool) -> Context -> Maybe Int
    forall a. (a -> Bool) -> [a] -> Maybe Int
    List.findIndex ((Name
    x Name -> Name -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (Name -> Bool)
    -> (Dom' Term (Name, Type) -> Name)
    -> Dom' Term (Name, Type)
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Name, Type) -> Name
    forall a b. (a, b) -> a
    fst ((Name, Type) -> Name)
    -> (Dom' Term (Name, Type) -> (Name, Type))
    -> Dom' Term (Name, Type)
    -> Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom' Term (Name, Type) -> (Name, Type)
    forall t e. Dom' t e -> e
    unDom) Context
    gamma
                let delta :: Context
    delta = TCEnv -> Context
    envContext (TCEnv -> Context) -> TCEnv -> Context
    forall a b. (a -> b) -> a -> b
    $ Closure Constraint -> TCEnv
    forall a. Closure a -> TCEnv
    clEnv Closure Constraint
    cl
                    cand :: [Maybe Int]
    cand  = (Dom' Term (Name, Type) -> Maybe Int) -> Context -> [Maybe Int]
    forall a b. (a -> b) -> [a] -> [b]
    map Dom' Term (Name, Type) -> Maybe Int
    findInGamma Context
    delta
                -- The domain of our substitution
                let coveredVars :: IntSet
    coveredVars = [Int] -> IntSet
    VarSet.fromList ([Int] -> IntSet) -> [Int] -> IntSet
    forall a b. (a -> b) -> a -> b
    $ [Maybe Int] -> [Int]
    forall a. [Maybe a] -> [a]
    catMaybes ([Maybe Int] -> [Int]) -> [Maybe Int] -> [Int]
    forall a b. (a -> b) -> a -> b
    $ (Maybe Int -> Int -> Maybe Int)
    -> [Maybe Int] -> [Int] -> [Maybe Int]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Maybe Int -> Int -> Maybe Int
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    ($>) [Maybe Int]
    cand [Int
    0..]
                -- Check that all the free variables of the constraint are contained in
                -- coveredVars.
                -- We ignore the free variables occurring in sorts.
                Bool -> MaybeT (TCMT IO) ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Bool -> MaybeT (TCMT IO) ()) -> Bool -> MaybeT (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ All -> Bool
    getAll (All -> Bool) -> All -> Bool
    forall a b. (a -> b) -> a -> b
    $ SingleVar All -> IgnoreSorts -> Constraint -> All
    forall a c t.
    (IsVarSet a c, Free t) =>
    SingleVar c -> IgnoreSorts -> t -> c
    runFree (Bool -> All
    All (Bool -> All) -> (Int -> Bool) -> SingleVar All
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Int -> IntSet -> Bool
    `VarSet.member` IntSet
    coveredVars)) IgnoreSorts
    IgnoreAll (Closure Constraint -> Constraint
    forall a. Closure a -> a
    clValue Closure Constraint
    cl)
                -- Turn cand into a substitution.
                -- Since we ignored the free variables in sorts, we better patch up
                -- the substitution with some dummy term rather than __IMPOSSIBLE__.
                Substitution' Term -> MaybeT (TCMT IO) (Substitution' Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Substitution' Term -> MaybeT (TCMT IO) (Substitution' Term))
    -> Substitution' Term -> MaybeT (TCMT IO) (Substitution' Term)
    forall a b. (a -> b) -> a -> b
    $ [Term] -> Substitution' Term
    forall a. DeBruijn a => [a] -> Substitution' a
    parallelS ([Term] -> Substitution' Term) -> [Term] -> Substitution' Term
    forall a b. (a -> b) -> a -> b
    $ (Maybe Int -> Term) -> [Maybe Int] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map (Term -> (Int -> Term) -> Maybe Int -> Term
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Term
    HasCallStack => Term
    __DUMMY_TERM__ Int -> Term
    var) [Maybe Int]
    cand
              ) Substitution' Term -> MaybeT (TCMT IO) (Substitution' Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return -- Phew, we've got the checkpoint! All is well.
      -- Apply substitution to constraint and pray that the Gods are merciful on us.
      Closure Constraint
    cl' <- Constraint -> MaybeT (TCMT IO) (Closure Constraint)
    forall (m :: * -> *) a.
    (MonadTCEnv m, ReadTCState m) =>
    a -> m (Closure a)
    buildClosure (Constraint -> MaybeT (TCMT IO) (Closure Constraint))
    -> Constraint -> MaybeT (TCMT IO) (Closure Constraint)
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg Constraint) -> Constraint -> Constraint
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' Term
    Substitution' (SubstArg Constraint)
    sigma (Closure Constraint -> Constraint
    forall a. Closure a -> a
    clValue Closure Constraint
    cl)
      ProblemConstraint -> MaybeT (TCMT IO) ProblemConstraint
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ProblemConstraint -> MaybeT (TCMT IO) ProblemConstraint)
    -> ProblemConstraint -> MaybeT (TCMT IO) ProblemConstraint
    forall a b. (a -> b) -> a -> b
    $ ProblemConstraint
    c { theConstraint :: Closure Constraint
    theConstraint = Closure Constraint
    cl' }
      -- Note: the resulting constraint may not well-typed.
      -- Even if it is, it may map variables to their wrong counterpart.

    -- | Return the size metas occurring in the simplified constraints.
    --   A constraint like @↑ _j =< ∞ : Size@ simplifies to nothing,
    --   so @_j@ would not be in this set.
    solveSizeConstraints_ :: DefaultToInfty -> [CC] -> TCM (Set MetaId)
    solveSizeConstraints_ :: DefaultToInfty -> [ProblemConstraint] -> TCMT IO (Set MetaId)
    solveSizeConstraints_ DefaultToInfty
    flag [ProblemConstraint]
    cs0 = do
      -- Pair constraints with their representation as size constraints.
      -- Discard constraints that do not have such a representation.
      [(ProblemConstraint, HypSizeConstraint)]
    ccs :: [(CC,HypSizeConstraint)] <- [Maybe (ProblemConstraint, HypSizeConstraint)]
    -> [(ProblemConstraint, HypSizeConstraint)]
    forall a. [Maybe a] -> [a]
    catMaybes ([Maybe (ProblemConstraint, HypSizeConstraint)]
     -> [(ProblemConstraint, HypSizeConstraint)])
    -> TCMT IO [Maybe (ProblemConstraint, HypSizeConstraint)]
    -> TCMT IO [(ProblemConstraint, HypSizeConstraint)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
        [ProblemConstraint]
    -> (ProblemConstraint
        -> TCMT IO (Maybe (ProblemConstraint, HypSizeConstraint)))
    -> TCMT IO [Maybe (ProblemConstraint, HypSizeConstraint)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [ProblemConstraint]
    cs0 ((ProblemConstraint
      -> TCMT IO (Maybe (ProblemConstraint, HypSizeConstraint)))
     -> TCMT IO [Maybe (ProblemConstraint, HypSizeConstraint)])
    -> (ProblemConstraint
        -> TCMT IO (Maybe (ProblemConstraint, HypSizeConstraint)))
    -> TCMT IO [Maybe (ProblemConstraint, HypSizeConstraint)]
    forall a b. (a -> b) -> a -> b
    $ \ ProblemConstraint
    c0 -> (HypSizeConstraint -> (ProblemConstraint, HypSizeConstraint))
    -> Maybe HypSizeConstraint
    -> Maybe (ProblemConstraint, HypSizeConstraint)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (ProblemConstraint
    c0,) (Maybe HypSizeConstraint
     -> Maybe (ProblemConstraint, HypSizeConstraint))
    -> TCMT IO (Maybe HypSizeConstraint)
    -> TCMT IO (Maybe (ProblemConstraint, HypSizeConstraint))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ProblemConstraint -> TCMT IO (Maybe HypSizeConstraint)
    computeSizeConstraint ProblemConstraint
    c0

      -- Simplify constraints and check for obvious inconsistencies.
      [(ProblemConstraint, HypSizeConstraint)]
    ccs' <- [[(ProblemConstraint, HypSizeConstraint)]]
    -> [(ProblemConstraint, HypSizeConstraint)]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat ([[(ProblemConstraint, HypSizeConstraint)]]
     -> [(ProblemConstraint, HypSizeConstraint)])
    -> TCMT IO [[(ProblemConstraint, HypSizeConstraint)]]
    -> TCMT IO [(ProblemConstraint, HypSizeConstraint)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
        [(ProblemConstraint, HypSizeConstraint)]
    -> ((ProblemConstraint, HypSizeConstraint)
        -> TCMT IO [(ProblemConstraint, HypSizeConstraint)])
    -> TCMT IO [[(ProblemConstraint, HypSizeConstraint)]]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [(ProblemConstraint, HypSizeConstraint)]
    ccs (((ProblemConstraint, HypSizeConstraint)
      -> TCMT IO [(ProblemConstraint, HypSizeConstraint)])
     -> TCMT IO [[(ProblemConstraint, HypSizeConstraint)]])
    -> ((ProblemConstraint, HypSizeConstraint)
        -> TCMT IO [(ProblemConstraint, HypSizeConstraint)])
    -> TCMT IO [[(ProblemConstraint, HypSizeConstraint)]]
    forall a b. (a -> b) -> a -> b
    $ \ (ProblemConstraint
    c0, HypSizeConstraint Context
    cxt [Int]
    hids [SizeConstraint]
    hs SizeConstraint
    sc) -> do
          case CTrans NamedRigid SizeMeta -> CTrans NamedRigid SizeMeta
    forall f r. (Pretty f, Pretty r, Eq r) => CTrans r f -> CTrans r f
    simplify1 (\ SizeConstraint
    sc -> [SizeConstraint] -> Either [Char] [SizeConstraint]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [SizeConstraint
    sc]) SizeConstraint
    sc of
            Left [Char]
    _ -> TypeError -> TCMT IO [(ProblemConstraint, HypSizeConstraint)]
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO [(ProblemConstraint, HypSizeConstraint)])
    -> (Doc -> TypeError)
    -> Doc
    -> TCMT IO [(ProblemConstraint, HypSizeConstraint)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> TypeError
    GenericDocError (Doc -> TCMT IO [(ProblemConstraint, HypSizeConstraint)])
    -> TCMT IO Doc -> TCMT IO [(ProblemConstraint, HypSizeConstraint)]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< do
              TCMT IO Doc
    "Contradictory size constraint" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ProblemConstraint -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM ProblemConstraint
    c0
            Right [SizeConstraint]
    cs -> [(ProblemConstraint, HypSizeConstraint)]
    -> TCMT IO [(ProblemConstraint, HypSizeConstraint)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([(ProblemConstraint, HypSizeConstraint)]
     -> TCMT IO [(ProblemConstraint, HypSizeConstraint)])
    -> [(ProblemConstraint, HypSizeConstraint)]
    -> TCMT IO [(ProblemConstraint, HypSizeConstraint)]
    forall a b. (a -> b) -> a -> b
    $ (ProblemConstraint
    c0,) (HypSizeConstraint -> (ProblemConstraint, HypSizeConstraint))
    -> (SizeConstraint -> HypSizeConstraint)
    -> SizeConstraint
    -> (ProblemConstraint, HypSizeConstraint)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Context
    -> [Int] -> [SizeConstraint] -> SizeConstraint -> HypSizeConstraint
    HypSizeConstraint Context
    cxt [Int]
    hids [SizeConstraint]
    hs (SizeConstraint -> (ProblemConstraint, HypSizeConstraint))
    -> [SizeConstraint] -> [(ProblemConstraint, HypSizeConstraint)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [SizeConstraint]
    cs

      -- Cluster constraints according to the meta variables they mention.
      -- @csNoM@ are the constraints that do not mention any meta.
      let ([(ProblemConstraint, HypSizeConstraint)]
    csNoM, [((ProblemConstraint, HypSizeConstraint), List1 Int)]
    csMs) = (((ProblemConstraint, HypSizeConstraint)
     -> Maybe ((ProblemConstraint, HypSizeConstraint), List1 Int))
    -> [(ProblemConstraint, HypSizeConstraint)]
    -> ([(ProblemConstraint, HypSizeConstraint)],
        [((ProblemConstraint, HypSizeConstraint), List1 Int)])
    forall a b. (a -> Maybe b) -> [a] -> ([a], [b])
    `List.partitionMaybe` [(ProblemConstraint, HypSizeConstraint)]
    ccs') (((ProblemConstraint, HypSizeConstraint)
      -> Maybe ((ProblemConstraint, HypSizeConstraint), List1 Int))
     -> ([(ProblemConstraint, HypSizeConstraint)],
         [((ProblemConstraint, HypSizeConstraint), List1 Int)]))
    -> ((ProblemConstraint, HypSizeConstraint)
        -> Maybe ((ProblemConstraint, HypSizeConstraint), List1 Int))
    -> ([(ProblemConstraint, HypSizeConstraint)],
        [((ProblemConstraint, HypSizeConstraint), List1 Int)])
    forall a b. (a -> b) -> a -> b
    $ \ p :: (ProblemConstraint, HypSizeConstraint)
    p@(ProblemConstraint
    c0, HypSizeConstraint
    c) ->
            (List1 Int -> ((ProblemConstraint, HypSizeConstraint), List1 Int))
    -> Maybe (List1 Int)
    -> Maybe ((ProblemConstraint, HypSizeConstraint), List1 Int)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((ProblemConstraint, HypSizeConstraint)
    p,) (Maybe (List1 Int)
     -> Maybe ((ProblemConstraint, HypSizeConstraint), List1 Int))
    -> Maybe (List1 Int)
    -> Maybe ((ProblemConstraint, HypSizeConstraint), List1 Int)
    forall a b. (a -> b) -> a -> b
    $ [Int] -> Maybe (List1 Int)
    forall a. [a] -> Maybe (NonEmpty a)
    nonEmpty ([Int] -> Maybe (List1 Int)) -> [Int] -> Maybe (List1 Int)
    forall a b. (a -> b) -> a -> b
    $ (SizeMeta -> Int) -> [SizeMeta] -> [Int]
    forall a b. (a -> b) -> [a] -> [b]
    map (MetaId -> Int
    metaId (MetaId -> Int) -> (SizeMeta -> MetaId) -> SizeMeta -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SizeMeta -> MetaId
    sizeMetaId) ([SizeMeta] -> [Int]) -> [SizeMeta] -> [Int]
    forall a b. (a -> b) -> a -> b
    $ Set SizeMeta -> [SizeMeta]
    forall a. Set a -> [a]
    Set.toList (Set SizeMeta -> [SizeMeta]) -> Set SizeMeta -> [SizeMeta]
    forall a b. (a -> b) -> a -> b
    $ HypSizeConstraint -> Set (FlexOf HypSizeConstraint)
    forall a. Flexs a => a -> Set (FlexOf a)
    flexs HypSizeConstraint
    c
      -- @css@ are the clusters of constraints.
          css :: [List1 (CC,HypSizeConstraint)]
          css :: [List1 (ProblemConstraint, HypSizeConstraint)]
    css = [((ProblemConstraint, HypSizeConstraint), List1 Int)]
    -> [List1 (ProblemConstraint, HypSizeConstraint)]
    forall a. [(a, List1 Int)] -> [NonEmpty a]
    cluster' [((ProblemConstraint, HypSizeConstraint), List1 Int)]
    csMs

      -- Check that the closed constraints are valid.
      Maybe (List1 (ProblemConstraint, HypSizeConstraint))
    -> (List1 (ProblemConstraint, HypSizeConstraint) -> TCM ())
    -> TCM ()
    forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
    whenJust ([(ProblemConstraint, HypSizeConstraint)]
    -> Maybe (List1 (ProblemConstraint, HypSizeConstraint))
    forall a. [a] -> Maybe (NonEmpty a)
    nonEmpty [(ProblemConstraint, HypSizeConstraint)]
    csNoM) ((List1 (ProblemConstraint, HypSizeConstraint) -> TCM ())
     -> TCM ())
    -> (List1 (ProblemConstraint, HypSizeConstraint) -> TCM ())
    -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ DefaultToInfty
    -> List1 (ProblemConstraint, HypSizeConstraint) -> TCM ()
    solveCluster DefaultToInfty
    flag

      -- Now, process the clusters.
      [List1 (ProblemConstraint, HypSizeConstraint)]
    -> (List1 (ProblemConstraint, HypSizeConstraint) -> TCM ())
    -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [List1 (ProblemConstraint, HypSizeConstraint)]
    css ((List1 (ProblemConstraint, HypSizeConstraint) -> TCM ())
     -> TCM ())
    -> (List1 (ProblemConstraint, HypSizeConstraint) -> TCM ())
    -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ DefaultToInfty
    -> List1 (ProblemConstraint, HypSizeConstraint) -> TCM ()
    solveCluster DefaultToInfty
    flag

      Set MetaId -> TCMT IO (Set MetaId)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Set MetaId -> TCMT IO (Set MetaId))
    -> Set MetaId -> TCMT IO (Set MetaId)
    forall a b. (a -> b) -> a -> b
    $ (SizeMeta -> MetaId) -> Set SizeMeta -> Set MetaId
    forall a b. (a -> b) -> Set a -> Set b
    Set.mapMonotonic SizeMeta -> MetaId
    sizeMetaId (Set SizeMeta -> Set MetaId) -> Set SizeMeta -> Set MetaId
    forall a b. (a -> b) -> a -> b
    $ [HypSizeConstraint] -> Set (FlexOf [HypSizeConstraint])
    forall a. Flexs a => a -> Set (FlexOf a)
    flexs ([HypSizeConstraint] -> Set (FlexOf [HypSizeConstraint]))
    -> [HypSizeConstraint] -> Set (FlexOf [HypSizeConstraint])
    forall a b. (a -> b) -> a -> b
    $ (((ProblemConstraint, HypSizeConstraint), List1 Int)
     -> HypSizeConstraint)
    -> [((ProblemConstraint, HypSizeConstraint), List1 Int)]
    -> [HypSizeConstraint]
    forall a b. (a -> b) -> [a] -> [b]
    map ((ProblemConstraint, HypSizeConstraint) -> HypSizeConstraint
    forall a b. (a, b) -> b
    snd ((ProblemConstraint, HypSizeConstraint) -> HypSizeConstraint)
    -> (((ProblemConstraint, HypSizeConstraint), List1 Int)
        -> (ProblemConstraint, HypSizeConstraint))
    -> ((ProblemConstraint, HypSizeConstraint), List1 Int)
    -> HypSizeConstraint
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((ProblemConstraint, HypSizeConstraint), List1 Int)
    -> (ProblemConstraint, HypSizeConstraint)
    forall a b. (a, b) -> a
    fst) [((ProblemConstraint, HypSizeConstraint), List1 Int)]
    csMs

    -- | Solve a cluster of constraints sharing some metas.
    --
    solveCluster :: DefaultToInfty -> List1 (CC, HypSizeConstraint) -> TCM ()
    solveCluster :: DefaultToInfty
    -> List1 (ProblemConstraint, HypSizeConstraint) -> TCM ()
    solveCluster DefaultToInfty
    flag List1 (ProblemConstraint, HypSizeConstraint)
    ccs = do
      let cs :: NonEmpty HypSizeConstraint
    cs = ((ProblemConstraint, HypSizeConstraint) -> HypSizeConstraint)
    -> List1 (ProblemConstraint, HypSizeConstraint)
    -> NonEmpty HypSizeConstraint
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (ProblemConstraint, HypSizeConstraint) -> HypSizeConstraint
    forall a b. (a, b) -> b
    snd List1 (ProblemConstraint, HypSizeConstraint)
    ccs
      let prettyCs :: [TCMT IO Doc]
    prettyCs   = (HypSizeConstraint -> TCMT IO Doc)
    -> [HypSizeConstraint] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map HypSizeConstraint -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM ([HypSizeConstraint] -> [TCMT IO Doc])
    -> [HypSizeConstraint] -> [TCMT IO Doc]
    forall a b. (a -> b) -> a -> b
    $ NonEmpty HypSizeConstraint -> [HypSizeConstraint]
    forall a. NonEmpty a -> [a]
    List1.toList NonEmpty HypSizeConstraint
    cs
      let err :: [Char] -> TCMT IO (Solution NamedRigid Int)
    err [Char]
    reason = TypeError -> TCMT IO (Solution NamedRigid Int)
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO (Solution NamedRigid Int))
    -> (Doc -> TypeError) -> Doc -> TCMT IO (Solution NamedRigid Int)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> TypeError
    GenericDocError (Doc -> TCMT IO (Solution NamedRigid Int))
    -> TCMT IO Doc -> TCMT IO (Solution NamedRigid Int)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< do
            [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
    $
              [ [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Cannot solve size constraints" ] [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a. [a] -> [a] -> [a]
    ++ [TCMT IO Doc]
    prettyCs [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a. [a] -> [a] -> [a]
    ++
              [ [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Reason: " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    reason ]
      [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.size.solve" Int
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    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
    "Solving constraint cluster" TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a. a -> [a] -> [a]
    : [TCMT IO Doc]
    prettyCs
      -- Find the super context of all contexts.
    {-
      -- We use the @'ctxId'@s.
      let cis@(ci:cis') = for cs $ \ c -> (c, reverse $ map ctxId $ sizeContext c)
    --  let cis@(ci:cis') = for cs $ \ c -> (c, reverse $ sizeHypIds c)
          max a@Left{}            _            = a
          max a@(Right ci@(c,is)) ci'@(c',is') =
            case preOrSuffix is is' of
              -- No common context:
              IsNofix    -> Left (ci, ci')
              IsPrefix{} -> Right ci'
              _          -> a
          res = foldl' max (Right ci) cis'
          noContext ((c,is),(c',is')) = typeError . GenericDocError =<< vcat
            [ "Cannot solve size constraints; the following constraints have no common typing context:"
            , prettyTCM c
            , prettyTCM c'
            ]
      flip (either noContext) res $ \ (HypSizeConstraint gamma hids hs _, _) -> do
    -}
      -- We rely on the fact that contexts are only extended...
      -- Just take the longest context.
      let HypSizeConstraint Context
    gamma [Int]
    hids [SizeConstraint]
    hs SizeConstraint
    _ = (HypSizeConstraint -> HypSizeConstraint -> Ordering)
    -> NonEmpty HypSizeConstraint -> HypSizeConstraint
    forall (t :: * -> *) a.
    Foldable t =>
    (a -> a -> Ordering) -> t a -> a
    Fold.maximumBy (Int -> Int -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (Int -> Int -> Ordering)
    -> (HypSizeConstraint -> Int)
    -> HypSizeConstraint
    -> HypSizeConstraint
    -> Ordering
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` (Context -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length (Context -> Int)
    -> (HypSizeConstraint -> Context) -> HypSizeConstraint -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . HypSizeConstraint -> Context
    sizeContext)) NonEmpty HypSizeConstraint
    cs
      -- Length of longest context.
      let n :: Int
    n = Context -> Int
    forall a. Sized a => a -> Int
    size Context
    gamma

      -- Now convert all size constraints to the largest context.
          csL :: NonEmpty SizeConstraint
    csL = NonEmpty HypSizeConstraint
    -> (HypSizeConstraint -> SizeConstraint) -> NonEmpty SizeConstraint
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    for NonEmpty HypSizeConstraint
    cs ((HypSizeConstraint -> SizeConstraint) -> NonEmpty SizeConstraint)
    -> (HypSizeConstraint -> SizeConstraint) -> NonEmpty SizeConstraint
    forall a b. (a -> b) -> a -> b
    $ \ (HypSizeConstraint Context
    cxt [Int]
    _ [SizeConstraint]
    _ SizeConstraint
    c) -> Int -> SizeConstraint -> SizeConstraint
    forall a. Subst a => Int -> a -> a
    raise (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Context -> Int
    forall a. Sized a => a -> Int
    size Context
    cxt) SizeConstraint
    c
      -- Canonicalize the constraints.
      -- This is unsound in the presence of hypotheses.
          csC :: [SizeConstraint]
          csC :: [SizeConstraint]
    csC = Bool
    -> ([SizeConstraint] -> [SizeConstraint])
    -> [SizeConstraint]
    -> [SizeConstraint]
    forall a. Bool -> (a -> a) -> a -> a
    applyWhen ([SizeConstraint] -> Bool
    forall a. Null a => a -> Bool
    null [SizeConstraint]
    hs) ((SizeConstraint -> Maybe SizeConstraint)
    -> [SizeConstraint] -> [SizeConstraint]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe SizeConstraint -> Maybe SizeConstraint
    canonicalizeSizeConstraint) ([SizeConstraint] -> [SizeConstraint])
    -> [SizeConstraint] -> [SizeConstraint]
    forall a b. (a -> b) -> a -> b
    $ NonEmpty SizeConstraint -> [SizeConstraint]
    forall a. NonEmpty a -> [a]
    List1.toList NonEmpty SizeConstraint
    csL
      [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.size.solve" Int
    30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    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
    "Size hypotheses" ] [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a. [a] -> [a] -> [a]
    ++
        (SizeConstraint -> TCMT IO Doc)
    -> [SizeConstraint] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (HypSizeConstraint -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (HypSizeConstraint -> TCMT IO Doc)
    -> (SizeConstraint -> HypSizeConstraint)
    -> SizeConstraint
    -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Context
    -> [Int] -> [SizeConstraint] -> SizeConstraint -> HypSizeConstraint
    HypSizeConstraint Context
    gamma [Int]
    hids [SizeConstraint]
    hs) [SizeConstraint]
    hs [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a. [a] -> [a] -> [a]
    ++
        [ TCMT IO Doc
    "Canonicalized constraints" ] [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a. [a] -> [a] -> [a]
    ++
        (SizeConstraint -> TCMT IO Doc)
    -> [SizeConstraint] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (HypSizeConstraint -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (HypSizeConstraint -> TCMT IO Doc)
    -> (SizeConstraint -> HypSizeConstraint)
    -> SizeConstraint
    -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Context
    -> [Int] -> [SizeConstraint] -> SizeConstraint -> HypSizeConstraint
    HypSizeConstraint Context
    gamma [Int]
    hids [SizeConstraint]
    hs) [SizeConstraint]
    csC

      -- -- ALT:
      -- -- Now convert all size constraints to de Bruijn levels.

      -- -- To get from indices in a context of length m <= n
      -- -- to levels into the target context of length n,
      -- -- we apply the following substitution:
      -- -- Index m-1 needs to be mapped to level 0,
      -- -- index m-2 needs to be mapped to level 1,
      -- -- index 0 needs to be mapped to level m-1,
      -- -- so the desired substitution is @downFrom m@.
      -- let sub m = applySubst $ parallelS $ map var $ downFrom m

      -- -- We simply reverse the context to get to de Bruijn levels.
      -- -- Of course, all types in the context are broken, but
      -- -- only need it for pretty printing constraints.
      -- gamma <- return $ reverse gamma

      -- -- We convert the hypotheses to de Bruijn levels.
      -- hs <- return $ sub n hs

      -- -- We get a form for pretty-printing
      -- let prettyC = prettyTCM . HypSizeConstraint gamma hids hs

      -- -- We convert the constraints to de Bruijn level format.
      -- let csC :: [SizeConstraint]
      --     csC = for cs $ \ (HypSizeConstraint cxt _ _ c) -> sub (size cxt) c

      -- reportSDoc "tc.size.solve" 30 $ vcat $
      --   [ "Size hypotheses" ]           ++ map prettyC hs ++
      --   [ "Canonicalized constraints" ] ++ map prettyC csC

      -- Convert size metas to flexible vars.
      let metas :: [SizeMeta]
          metas :: [SizeMeta]
    metas = (SizeConstraint -> [SizeMeta]) -> [SizeConstraint] -> [SizeMeta]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap ((SizeMeta -> [SizeMeta]) -> SizeConstraint -> [SizeMeta]
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap (SizeMeta -> [SizeMeta] -> [SizeMeta]
    forall a. a -> [a] -> [a]
    :[])) [SizeConstraint]
    csC
          csF   :: [Size.Constraint' NamedRigid Int]
          csF :: [Constraint' NamedRigid Int]
    csF   = (SizeConstraint -> Constraint' NamedRigid Int)
    -> [SizeConstraint] -> [Constraint' NamedRigid Int]
    forall a b. (a -> b) -> [a] -> [b]
    map ((SizeMeta -> Int) -> SizeConstraint -> Constraint' NamedRigid Int
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (MetaId -> Int
    metaId (MetaId -> Int) -> (SizeMeta -> MetaId) -> SizeMeta -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SizeMeta -> MetaId
    sizeMetaId)) [SizeConstraint]
    csC

      -- Construct the hypotheses graph.
      let hyps :: [Constraint' NamedRigid Int]
    hyps = (SizeConstraint -> Constraint' NamedRigid Int)
    -> [SizeConstraint] -> [Constraint' NamedRigid Int]
    forall a b. (a -> b) -> [a] -> [b]
    map ((SizeMeta -> Int) -> SizeConstraint -> Constraint' NamedRigid Int
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (MetaId -> Int
    metaId (MetaId -> Int) -> (SizeMeta -> MetaId) -> SizeMeta -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SizeMeta -> MetaId
    sizeMetaId)) [SizeConstraint]
    hs
      -- There cannot be negative cycles in hypotheses graph due to scoping.
      let hg :: HypGraph NamedRigid Int
    hg = ([Char] -> HypGraph NamedRigid Int)
    -> (HypGraph NamedRigid Int -> HypGraph NamedRigid Int)
    -> Either [Char] (HypGraph NamedRigid Int)
    -> HypGraph NamedRigid Int
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either [Char] -> HypGraph NamedRigid Int
    forall a. HasCallStack => a
    __IMPOSSIBLE__ HypGraph NamedRigid Int -> HypGraph NamedRigid Int
    forall a. a -> a
    id (Either [Char] (HypGraph NamedRigid Int)
     -> HypGraph NamedRigid Int)
    -> Either [Char] (HypGraph NamedRigid Int)
    -> HypGraph NamedRigid Int
    forall a b. (a -> b) -> a -> b
    $ Set NamedRigid
    -> [Constraint' NamedRigid Int]
    -> Either [Char] (HypGraph NamedRigid Int)
    forall rigid flex.
    (Ord rigid, Ord flex, Pretty rigid, Pretty flex) =>
    Set rigid
    -> [Hyp' rigid flex] -> Either [Char] (HypGraph rigid flex)
    hypGraph ([Constraint' NamedRigid Int]
    -> Set (RigidOf [Constraint' NamedRigid Int])
    forall a. Rigids a => a -> Set (RigidOf a)
    rigids [Constraint' NamedRigid Int]
    csF) [Constraint' NamedRigid Int]
    hyps

      -- -- Construct the constraint graph.
      -- --    g :: Size.Graph NamedRigid Int Label
      -- g <- either err return $ constraintGraph csF hg
      -- reportSDoc "tc.size.solve" 40 $ vcat $
      --   [ "Constraint graph"
      --   , text (show g)
      --   ]

      -- sol :: Solution NamedRigid Int <- either err return $ solveGraph Map.empty hg g
      -- either err return $ verifySolution hg csF sol

      -- Andreas, 2016-07-13, issue 2096.
      -- Running the solver once might result in unsolvable left-over constraints.
      -- We need to iterate the solver to detect this.
      Solution NamedRigid Int
    sol :: Solution NamedRigid Int <- ([Char] -> TCMT IO (Solution NamedRigid Int))
    -> (Solution NamedRigid Int -> TCMT IO (Solution NamedRigid Int))
    -> Either [Char] (Solution NamedRigid Int)
    -> TCMT IO (Solution NamedRigid Int)
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either [Char] -> TCMT IO (Solution NamedRigid Int)
    err Solution NamedRigid Int -> TCMT IO (Solution NamedRigid Int)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either [Char] (Solution NamedRigid Int)
     -> TCMT IO (Solution NamedRigid Int))
    -> Either [Char] (Solution NamedRigid Int)
    -> TCMT IO (Solution NamedRigid Int)
    forall a b. (a -> b) -> a -> b
    $
        Polarities Int
    -> HypGraph NamedRigid Int
    -> [Constraint' NamedRigid Int]
    -> Solution NamedRigid Int
    -> Either [Char] (Solution NamedRigid Int)
    forall r f.
    (Ord r, Ord f, Pretty r, Pretty f, Show r, Show f) =>
    Polarities f
    -> HypGraph r f
    -> [Constraint' r f]
    -> Solution r f
    -> Either [Char] (Solution r f)
    iterateSolver Polarities Int
    forall k a. Map k a
    Map.empty HypGraph NamedRigid Int
    hg [Constraint' NamedRigid Int]
    csF Solution NamedRigid Int
    forall r f. Solution r f
    emptySolution

      -- Convert solution to meta instantiation.
      Set MetaId
    solved <- ([Set MetaId] -> Set MetaId)
    -> TCM [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 (TCM [Set MetaId] -> TCMT IO (Set MetaId))
    -> TCM [Set MetaId] -> TCMT IO (Set MetaId)
    forall a b. (a -> b) -> a -> b
    $ [(Int, SizeExpr' NamedRigid Int)]
    -> ((Int, SizeExpr' NamedRigid Int) -> TCMT IO (Set MetaId))
    -> TCM [Set MetaId]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM (Map Int (SizeExpr' NamedRigid Int)
    -> [(Int, SizeExpr' NamedRigid Int)]
    forall k a. Map k a -> [(k, a)]
    Map.assocs (Map Int (SizeExpr' NamedRigid Int)
     -> [(Int, SizeExpr' NamedRigid Int)])
    -> Map Int (SizeExpr' NamedRigid Int)
    -> [(Int, SizeExpr' NamedRigid Int)]
    forall a b. (a -> b) -> a -> b
    $ Solution NamedRigid Int -> Map Int (SizeExpr' NamedRigid Int)
    forall rigid flex.
    Solution rigid flex -> Map flex (SizeExpr' rigid flex)
    theSolution Solution NamedRigid Int
    sol) (((Int, SizeExpr' NamedRigid Int) -> TCMT IO (Set MetaId))
     -> TCM [Set MetaId])
    -> ((Int, SizeExpr' NamedRigid Int) -> TCMT IO (Set MetaId))
    -> TCM [Set MetaId]
    forall a b. (a -> b) -> a -> b
    $ \ (Int
    m, SizeExpr' NamedRigid Int
    a) -> do
        Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (SizeExpr' NamedRigid Int -> Bool
    forall a. ValidOffset a => a -> Bool
    validOffset SizeExpr' NamedRigid Int
    a) TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        -- Solution does not contain metas
        Term
    u <- DBSizeExpr -> TCMT IO Term
    forall (m :: * -> *). HasBuiltins m => DBSizeExpr -> m Term
    unSizeExpr (DBSizeExpr -> TCMT IO Term) -> DBSizeExpr -> TCMT IO Term
    forall a b. (a -> b) -> a -> b
    $ (Int -> SizeMeta) -> SizeExpr' NamedRigid Int -> DBSizeExpr
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Int -> SizeMeta
    forall a. HasCallStack => a
    __IMPOSSIBLE__ SizeExpr' NamedRigid Int
    a
        let x :: MetaId
    x = Int -> MetaId
    MetaId Int
    m
        let SizeMeta MetaId
    _ [Int]
    xs = SizeMeta -> Maybe SizeMeta -> SizeMeta
    forall a. a -> Maybe a -> a
    fromMaybe SizeMeta
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe SizeMeta -> SizeMeta) -> Maybe SizeMeta -> SizeMeta
    forall a b. (a -> b) -> a -> b
    $
              (SizeMeta -> Bool) -> [SizeMeta] -> Maybe SizeMeta
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
    List.find ((Int
    mInt -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (Int -> Bool) -> (SizeMeta -> Int) -> SizeMeta -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . MetaId -> Int
    metaId (MetaId -> Int) -> (SizeMeta -> MetaId) -> SizeMeta -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SizeMeta -> MetaId
    sizeMetaId) [SizeMeta]
    metas
        -- Check that solution is well-scoped
        let ys :: [Int]
    ys = NamedRigid -> Int
    rigidIndex (NamedRigid -> Int) -> [NamedRigid] -> [Int]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Set NamedRigid -> [NamedRigid]
    forall a. Set a -> [a]
    Set.toList (SizeExpr' NamedRigid Int
    -> Set (RigidOf (SizeExpr' NamedRigid Int))
    forall a. Rigids a => a -> Set (RigidOf a)
    rigids SizeExpr' NamedRigid Int
    a)
            ok :: Bool
    ok = (Int -> Bool) -> [Int] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (Int -> [Int] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [Int]
    xs) [Int]
    ys -- TODO: more efficient
        -- unless ok $ err "ill-scoped solution for size meta variable"
        Term
    u <- if Bool
    ok then Term -> TCMT IO Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    u else TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primSizeInf
        Type
    t <- MetaId -> TCMT IO Type
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m Type
    getMetaType MetaId
    x
        [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.size.solve" Int
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ (Context -> Context) -> TCMT IO Doc -> TCMT IO Doc
    forall (tcm :: * -> *) a.
    MonadTCEnv tcm =>
    (Context -> Context) -> tcm a -> tcm a
    unsafeModifyContext (Context -> Context -> Context
    forall a b. a -> b -> a
    const Context
    gamma) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ do
          let args :: Elims
    args = (Int -> Elim' Term) -> [Int] -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map (Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply (Arg Term -> Elim' Term) -> (Int -> Arg Term) -> Int -> Elim' Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> Arg Term
    forall a. a -> Arg a
    defaultArg (Term -> Arg Term) -> (Int -> Term) -> Int -> Arg Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Term
    var) [Int]
    xs
          TCMT IO Doc
    "solution " 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 (MetaId -> Elims -> Term
    MetaV MetaId
    x Elims
    args) 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 Term
    u
        [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.size.solve" Int
    60 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    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
          [ [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "  xs = " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Int] -> [Char]
    forall a. Show a => a -> [Char]
    show [Int]
    xs
          , [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "  u  = " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Term -> [Char]
    forall a. Show a => a -> [Char]
    show Term
    u
          ]
        TCMT IO Bool
    -> TCMT IO (Set MetaId)
    -> TCMT IO (Set MetaId)
    -> TCMT IO (Set MetaId)
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (MetaId -> TCMT IO Bool
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m Bool
    isFrozen MetaId
    x TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `or2M` (Bool -> Bool
    not (Bool -> Bool) -> TCMT IO Bool -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (TCEnv -> Bool) -> TCMT IO Bool
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Bool
    envAssignMetas)) (Set MetaId -> TCMT IO (Set MetaId)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Set MetaId
    forall a. Set a
    Set.empty) (TCMT IO (Set MetaId) -> TCMT IO (Set MetaId))
    -> TCMT IO (Set MetaId) -> TCMT IO (Set MetaId)
    forall a b. (a -> b) -> a -> b
    $ do
          Int -> MetaId -> Type -> [Int] -> Term -> TCM ()
    assignMeta Int
    n MetaId
    x Type
    t [Int]
    xs Term
    u
          Set MetaId -> TCMT IO (Set MetaId)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Set MetaId -> TCMT IO (Set MetaId))
    -> Set MetaId -> TCMT IO (Set MetaId)
    forall a b. (a -> b) -> a -> b
    $ MetaId -> Set MetaId
    forall a. a -> Set a
    Set.singleton MetaId
    x
        -- WRONG:
        -- let partialSubst = List.sort $ zip xs $ map var $ downFrom n
        -- assignMeta' n x t (length xs) partialSubst u
        -- WRONG: assign DirEq x (map (defaultArg . var) xs) u

      -- Possibly set remaining size metas to ∞ (issue 1862)
      -- unless we have an interaction meta in the cluster (issue 2095).

      Set MetaId
    ims <- [MetaId] -> Set MetaId
    forall a. Ord a => [a] -> Set a
    Set.fromList ([MetaId] -> Set MetaId)
    -> TCMT IO [MetaId] -> TCMT IO (Set MetaId)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO [MetaId]
    forall (m :: * -> *). ReadTCState m => m [MetaId]
    getInteractionMetas

      --  ms = unsolved size metas from cluster
      let ms :: Set MetaId
    ms = [MetaId] -> Set MetaId
    forall a. Ord a => [a] -> Set a
    Set.fromList ((SizeMeta -> MetaId) -> [SizeMeta] -> [MetaId]
    forall a b. (a -> b) -> [a] -> [b]
    map SizeMeta -> MetaId
    sizeMetaId [SizeMeta]
    metas) Set MetaId -> Set MetaId -> Set MetaId
    forall a. Ord a => Set a -> Set a -> Set a
    Set.\\ Set MetaId
    solved
      --  Make sure they do not contain an interaction point
      let noIP :: Bool
    noIP = Set MetaId -> Set MetaId -> Bool
    forall a. Ord a => Set a -> Set a -> Bool
    Set.disjoint Set MetaId
    ims Set MetaId
    ms

      Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Set MetaId -> Bool
    forall a. Null a => a -> Bool
    null Set MetaId
    ms) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.size.solve" Int
    30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    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
    fsep ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $
        TCMT IO Doc
    "cluster did not solve these size metas: " TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a. a -> [a] -> [a]
    : (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 (Set MetaId -> [MetaId]
    forall a. Set a -> [a]
    Set.toList Set MetaId
    ms)

      Bool
    solvedAll <- do
        -- If no metas are left, we have solved this cluster completely.
        if Set MetaId -> Bool
    forall a. Set a -> Bool
    Set.null Set MetaId
    ms                then Bool -> TCMT IO Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True  else do
        -- Otherwise, we can solve it completely if we are allowed to set to ∞.
        if DefaultToInfty
    flag DefaultToInfty -> DefaultToInfty -> Bool
    forall a. Eq a => a -> a -> Bool
    == DefaultToInfty
    DontDefaultToInfty then Bool -> TCMT IO Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False else do
        -- Which is only the case when we have no interaction points in the cluster.
        if Bool -> Bool
    not Bool
    noIP                   then Bool -> TCMT IO Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False else do
        -- Try to set all unconstrained size metas to ∞.
        Term
    inf <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primSizeInf
        [Bool] -> Bool
    forall (t :: * -> *). Foldable t => t Bool -> Bool
    and ([Bool] -> Bool) -> TCMT IO [Bool] -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
          [MetaId] -> (MetaId -> TCMT IO Bool) -> TCMT IO [Bool]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM (Set MetaId -> [MetaId]
    forall a. Set a -> [a]
    Set.toList Set MetaId
    ms) ((MetaId -> TCMT IO Bool) -> TCMT IO [Bool])
    -> (MetaId -> TCMT IO Bool) -> TCMT IO [Bool]
    forall a b. (a -> b) -> a -> b
    $ \ MetaId
    m -> do
            -- If one variable is frozen, we cannot set it (and hence not all) to ∞
            let no :: TCMT IO Bool
    no = do
                  [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.size.solve" Int
    30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    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
    m []) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "is frozen, cannot set it to ∞"
                  Bool -> TCMT IO Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
            TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (MetaId -> TCMT IO Bool
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m Bool
    isFrozen MetaId
    m TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `or2M` do Bool -> Bool
    not (Bool -> Bool) -> TCMT IO Bool -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (TCEnv -> Bool) -> TCMT IO Bool
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Bool
    envAssignMetas) TCMT IO Bool
    no (TCMT IO Bool -> TCMT IO Bool) -> TCMT IO Bool -> TCMT IO Bool
    forall a b. (a -> b) -> a -> b
    $ {-else-} do
              [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.size.solve" Int
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
                TCMT IO Doc
    "solution " 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 (MetaId -> Elims -> Term
    MetaV 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 Term
    inf
              Type
    t <- MetaId -> TCMT IO Type
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m Type
    metaType MetaId
    m
              TelV Tele (Dom Type)
    tel Type
    core <- Type -> TCMT IO (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Type -> m (TelV Type)
    telView Type
    t
              TCMT IO Bool -> TCM () -> TCM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    unlessM (Maybe BoundedSize -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe BoundedSize -> Bool)
    -> TCMT IO (Maybe BoundedSize) -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> TCMT IO (Maybe BoundedSize)
    forall a (m :: * -> *).
    (IsSizeType a, HasOptions m, HasBuiltins m) =>
    a -> m (Maybe BoundedSize)
    isSizeType Type
    core) TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
              Int -> MetaId -> Type -> [Int] -> Term -> TCM ()
    assignMeta Int
    0 MetaId
    m Type
    t (Int -> [Int]
    forall a. Integral a => a -> [a]
    List.downFrom (Int -> [Int]) -> Int -> [Int]
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    tel) Term
    inf
              Bool -> TCMT IO Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True

      -- Double check.
      Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when Bool
    solvedAll (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
        let cs0 :: NonEmpty ProblemConstraint
    cs0 = ((ProblemConstraint, HypSizeConstraint) -> ProblemConstraint)
    -> List1 (ProblemConstraint, HypSizeConstraint)
    -> NonEmpty ProblemConstraint
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (ProblemConstraint, HypSizeConstraint) -> ProblemConstraint
    forall a b. (a, b) -> a
    fst List1 (ProblemConstraint, HypSizeConstraint)
    ccs
            -- Error for giving up
            cannotSolve :: TCM ()
    cannotSolve = TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM ()) -> (Doc -> TypeError) -> Doc -> TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> TypeError
    GenericDocError (Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<<
              NonEmpty (TCMT IO Doc) -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat (TCMT IO Doc
    "Cannot solve size constraints" TCMT IO Doc -> NonEmpty (TCMT IO Doc) -> NonEmpty (TCMT IO Doc)
    forall a. a -> NonEmpty a -> NonEmpty a
    <| (ProblemConstraint -> TCMT IO Doc)
    -> NonEmpty ProblemConstraint -> NonEmpty (TCMT IO Doc)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ProblemConstraint -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM NonEmpty ProblemConstraint
    cs0)
        (TCM () -> (TCErr -> TCM ()) -> TCM ())
    -> (TCErr -> TCM ()) -> TCM () -> TCM ()
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip TCM () -> (TCErr -> TCM ()) -> TCM ()
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    catchError (TCM () -> TCErr -> TCM ()
    forall a b. a -> b -> a
    const TCM ()
    cannotSolve) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
          TCM () -> TCM ()
    forall (m :: * -> *) a.
    (MonadConstraint m, MonadWarning m, MonadError TCErr m,
     MonadFresh ProblemId m) =>
    m a -> m a
    noConstraints (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
            NonEmpty ProblemConstraint
    -> (ProblemConstraint -> TCM ()) -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ NonEmpty ProblemConstraint
    cs0 ((ProblemConstraint -> TCM ()) -> TCM ())
    -> (ProblemConstraint -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ (Constraint -> TCM ()) -> ProblemConstraint -> TCM ()
    forall (m :: * -> *) a.
    MonadConstraint m =>
    (Constraint -> m a) -> ProblemConstraint -> m a
    withConstraint Constraint -> TCM ()
    forall (m :: * -> *). MonadConstraint m => Constraint -> m ()
    solveConstraint

    -- | Collect constraints from a typing context, looking for SIZELT hypotheses.
    getSizeHypotheses :: Context -> TCM [(Nat, SizeConstraint)]
    getSizeHypotheses :: Context -> TCM [(Int, SizeConstraint)]
    getSizeHypotheses Context
    gamma = (Context -> Context)
    -> TCM [(Int, SizeConstraint)] -> TCM [(Int, SizeConstraint)]
    forall (tcm :: * -> *) a.
    MonadTCEnv tcm =>
    (Context -> Context) -> tcm a -> tcm a
    unsafeModifyContext (Context -> Context -> Context
    forall a b. a -> b -> a
    const Context
    gamma) (TCM [(Int, SizeConstraint)] -> TCM [(Int, SizeConstraint)])
    -> TCM [(Int, SizeConstraint)] -> TCM [(Int, SizeConstraint)]
    forall a b. (a -> b) -> a -> b
    $ do
      (Maybe QName
    _, Maybe QName
    msizelt) <- TCMT IO (Maybe QName, Maybe QName)
    forall (m :: * -> *). HasBuiltins m => m (Maybe QName, Maybe QName)
    getBuiltinSize
      Maybe QName
    -> TCM [(Int, SizeConstraint)]
    -> (QName -> TCM [(Int, SizeConstraint)])
    -> TCM [(Int, SizeConstraint)]
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe Maybe QName
    msizelt ([(Int, SizeConstraint)] -> TCM [(Int, SizeConstraint)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []) ((QName -> TCM [(Int, SizeConstraint)])
     -> TCM [(Int, SizeConstraint)])
    -> (QName -> TCM [(Int, SizeConstraint)])
    -> TCM [(Int, SizeConstraint)]
    forall a b. (a -> b) -> a -> b
    $ \ QName
    sizelt -> do
        -- Traverse the context from newest to oldest de Bruijn Index
        [Maybe (Int, SizeConstraint)] -> [(Int, SizeConstraint)]
    forall a. [Maybe a] -> [a]
    catMaybes ([Maybe (Int, SizeConstraint)] -> [(Int, SizeConstraint)])
    -> TCMT IO [Maybe (Int, SizeConstraint)]
    -> TCM [(Int, SizeConstraint)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
          [(Int, Dom' Term (Name, Type))]
    -> ((Int, Dom' Term (Name, Type))
        -> TCMT IO (Maybe (Int, SizeConstraint)))
    -> TCMT IO [Maybe (Int, SizeConstraint)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM ([Int] -> Context -> [(Int, Dom' Term (Name, Type))]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Int
    0..] Context
    gamma) (((Int, Dom' Term (Name, Type))
      -> TCMT IO (Maybe (Int, SizeConstraint)))
     -> TCMT IO [Maybe (Int, SizeConstraint)])
    -> ((Int, Dom' Term (Name, Type))
        -> TCMT IO (Maybe (Int, SizeConstraint)))
    -> TCMT IO [Maybe (Int, SizeConstraint)]
    forall a b. (a -> b) -> a -> b
    $ \ (Int
    i, Dom' Term (Name, Type)
    ce) -> do
            -- Get name and type of variable i.
            let (Name
    x, Type
    t) = Dom' Term (Name, Type) -> (Name, Type)
    forall t e. Dom' t e -> e
    unDom Dom' Term (Name, Type)
    ce
                s :: [Char]
    s      = Name -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Name
    x
            Term
    t <- Term -> TCMT IO Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce (Term -> TCMT IO Term) -> (Type -> Term) -> Type -> TCMT IO Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Term -> Term
    forall a. Subst a => Int -> a -> a
    raise (Int
    1 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    i) (Term -> Term) -> (Type -> Term) -> Type -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type -> Term
    forall t a. Type'' t a -> a
    unEl (Type -> TCMT IO Term) -> Type -> TCMT IO Term
    forall a b. (a -> b) -> a -> b
    $ Type
    t
            case Term
    t of
              Def QName
    d [Apply Arg Term
    u] | QName
    d QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    sizelt -> do
                TCMT IO (Maybe DBSizeExpr)
    -> TCMT IO (Maybe (Int, SizeConstraint))
    -> (DBSizeExpr -> TCMT IO (Maybe (Int, SizeConstraint)))
    -> TCMT IO (Maybe (Int, SizeConstraint))
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (Term -> TCMT IO (Maybe DBSizeExpr)
    sizeExpr (Term -> TCMT IO (Maybe DBSizeExpr))
    -> Term -> TCMT IO (Maybe DBSizeExpr)
    forall a b. (a -> b) -> a -> b
    $ Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    u) (Maybe (Int, SizeConstraint)
    -> TCMT IO (Maybe (Int, SizeConstraint))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (Int, SizeConstraint)
    forall a. Maybe a
    Nothing) ((DBSizeExpr -> TCMT IO (Maybe (Int, SizeConstraint)))
     -> TCMT IO (Maybe (Int, SizeConstraint)))
    -> (DBSizeExpr -> TCMT IO (Maybe (Int, SizeConstraint)))
    -> TCMT IO (Maybe (Int, SizeConstraint))
    forall a b. (a -> b) -> a -> b
    $ \ DBSizeExpr
    a ->
                  Maybe (Int, SizeConstraint)
    -> TCMT IO (Maybe (Int, SizeConstraint))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (Int, SizeConstraint)
     -> TCMT IO (Maybe (Int, SizeConstraint)))
    -> Maybe (Int, SizeConstraint)
    -> TCMT IO (Maybe (Int, SizeConstraint))
    forall a b. (a -> b) -> a -> b
    $ (Int, SizeConstraint) -> Maybe (Int, SizeConstraint)
    forall a. a -> Maybe a
    Just ((Int, SizeConstraint) -> Maybe (Int, SizeConstraint))
    -> (Int, SizeConstraint) -> Maybe (Int, SizeConstraint)
    forall a b. (a -> b) -> a -> b
    $ (Int
    i, DBSizeExpr -> Cmp -> DBSizeExpr -> SizeConstraint
    forall rigid flex.
    SizeExpr' rigid flex
    -> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
    Constraint (NamedRigid -> Offset -> DBSizeExpr
    forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
    Rigid ([Char] -> Int -> NamedRigid
    NamedRigid [Char]
    s Int
    i) Offset
    0) Cmp
    Lt DBSizeExpr
    a)
              Term
    _ -> Maybe (Int, SizeConstraint)
    -> TCMT IO (Maybe (Int, SizeConstraint))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (Int, SizeConstraint)
    forall a. Maybe a
    Nothing

    -- | Convert size constraint into form where each meta is applied
    --   to indices @n-1,...,1,0@ where @n@ is the arity of that meta.
    --
    --   @X[σ] <= t@ becomes @X[id] <= t[σ^-1]@
    --
    --   @X[σ] ≤ Y[τ]@ becomes @X[id] ≤ Y[τ[σ^-1]]@ or @X[σ[τ^1]] ≤ Y[id]@
    --   whichever is defined.  If none is defined, we give up.
    --
    --   Cf. @SizedTypes.oldCanonicalizeSizeConstraint@.
    --
    --   Fixes (the rather artificial) issue 300.
    --   But it is unsound when pruned metas occur and triggers issue 1914.
    --   Thus we deactivate it.
    --   This needs to be properly implemented, possibly using the
    --   metaPermuatation of each meta variable.

    canonicalizeSizeConstraint :: SizeConstraint -> Maybe (SizeConstraint)
    canonicalizeSizeConstraint :: SizeConstraint -> Maybe SizeConstraint
    canonicalizeSizeConstraint c :: SizeConstraint
    c@(Constraint DBSizeExpr
    a Cmp
    cmp DBSizeExpr
    b) = SizeConstraint -> Maybe SizeConstraint
    forall a. a -> Maybe a
    Just SizeConstraint
    c
    {-
      case (a,b) of

        -- Case flex-flex
        (Flex (SizeMeta m xs) n, Flex (SizeMeta l ys) n')
             -- try to invert xs on ys
           | let len = size xs
           , Just ys' <- mapM (\ y -> (len-1 -) <$> findIndex (==y) xs) ys ->
               return $ Constraint (Flex (SizeMeta m $ downFrom len) n)
                               cmp (Flex (SizeMeta l ys') n')
             -- try to invert ys on xs
           | let len = size ys
           , Just xs' <- mapM (\ x -> (len-1 -) <$> findIndex (==x) ys) xs ->
               return $ Constraint (Flex (SizeMeta m xs') n)
                               cmp (Flex (SizeMeta l $ downFrom len) n')
             -- give up
           | otherwise -> Nothing

        -- Case flex-rigid
        (Flex (SizeMeta m xs) n, Rigid (NamedRigid x i) n') -> do
          let len = size xs
          j <- (len-1 -) <$> findIndex (==i) xs
          return $ Constraint (Flex (SizeMeta m $ downFrom len) n)
                          cmp (Rigid (NamedRigid x j) n')

        -- Case rigid-flex
        (Rigid (NamedRigid x i) n, Flex (SizeMeta m xs) n') -> do
          let len = size xs
          j <- (len-1 -) <$> findIndex (==i) xs
          return $ Constraint (Rigid (NamedRigid x j) n)
                          cmp (Flex (SizeMeta m $ downFrom len) n')

        -- Case flex-const
        (Flex (SizeMeta m xs) n, _)      ->
          return $ Constraint (Flex (SizeMeta m $ downFrom $ size xs) n) cmp b

        -- Case const-flex
        (_, Flex (SizeMeta m xs) n') -> do
          return $ Constraint a cmp (Flex (SizeMeta m $ downFrom $ size xs) n')

        -- Case no flex
        _ -> return c
    -}

    -- | Identifiers for rigid variables.
    data NamedRigid = NamedRigid
      { NamedRigid -> [Char]
    rigidName  :: String   -- ^ Name for printing in debug messages.
      , NamedRigid -> Int
    rigidIndex :: Int      -- ^ De Bruijn index.
      } deriving (Int -> NamedRigid -> ShowS
    [NamedRigid] -> ShowS
    NamedRigid -> [Char]
    (Int -> NamedRigid -> ShowS)
    -> (NamedRigid -> [Char])
    -> ([NamedRigid] -> ShowS)
    -> Show NamedRigid
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    showList :: [NamedRigid] -> ShowS
    $cshowList :: [NamedRigid] -> ShowS
    show :: NamedRigid -> [Char]
    $cshow :: NamedRigid -> [Char]
    showsPrec :: Int -> NamedRigid -> ShowS
    $cshowsPrec :: Int -> NamedRigid -> ShowS
    Show)

    instance Eq NamedRigid where == :: NamedRigid -> NamedRigid -> Bool
    (==) = Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) (Int -> Int -> Bool)
    -> (NamedRigid -> Int) -> NamedRigid -> NamedRigid -> Bool
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` NamedRigid -> Int
    rigidIndex
    instance Ord NamedRigid where compare :: NamedRigid -> NamedRigid -> Ordering
    compare = Int -> Int -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (Int -> Int -> Ordering)
    -> (NamedRigid -> Int) -> NamedRigid -> NamedRigid -> Ordering
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` NamedRigid -> Int
    rigidIndex
    instance Pretty NamedRigid where pretty :: NamedRigid -> Doc
    pretty = [Char] -> Doc
    P.text ([Char] -> Doc) -> (NamedRigid -> [Char]) -> NamedRigid -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamedRigid -> [Char]
    rigidName
    instance Plus NamedRigid Int NamedRigid where
      plus :: NamedRigid -> Int -> NamedRigid
    plus (NamedRigid [Char]
    x Int
    i) Int
    j = [Char] -> Int -> NamedRigid
    NamedRigid [Char]
    x (Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    j)

    -- | Size metas in size expressions.
    data SizeMeta = SizeMeta
      { SizeMeta -> MetaId
    sizeMetaId   :: MetaId
      -- TODO to fix issue 300?
      -- , sizeMetaPerm :: Permutation -- ^ Permutation from the current context
      --                               --   to the context of the meta.
      , SizeMeta -> [Int]
    sizeMetaArgs :: [Int]       -- ^ De Bruijn indices.
      } deriving (Int -> SizeMeta -> ShowS
    [SizeMeta] -> ShowS
    SizeMeta -> [Char]
    (Int -> SizeMeta -> ShowS)
    -> (SizeMeta -> [Char]) -> ([SizeMeta] -> ShowS) -> Show SizeMeta
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    showList :: [SizeMeta] -> ShowS
    $cshowList :: [SizeMeta] -> ShowS
    show :: SizeMeta -> [Char]
    $cshow :: SizeMeta -> [Char]
    showsPrec :: Int -> SizeMeta -> ShowS
    $cshowsPrec :: Int -> SizeMeta -> ShowS
    Show)

    -- | An equality which ignores the meta arguments.
    instance Eq  SizeMeta where == :: SizeMeta -> SizeMeta -> Bool
    (==)    = MetaId -> MetaId -> Bool
    forall a. Eq a => a -> a -> Bool
    (==)    (MetaId -> MetaId -> Bool)
    -> (SizeMeta -> MetaId) -> SizeMeta -> SizeMeta -> Bool
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` SizeMeta -> MetaId
    sizeMetaId
    -- | An order which ignores the meta arguments.
    instance Ord SizeMeta where compare :: SizeMeta -> SizeMeta -> Ordering
    compare = MetaId -> MetaId -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (MetaId -> MetaId -> Ordering)
    -> (SizeMeta -> MetaId) -> SizeMeta -> SizeMeta -> Ordering
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` SizeMeta -> MetaId
    sizeMetaId

    instance Pretty SizeMeta where pretty :: SizeMeta -> Doc
    pretty = MetaId -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty (MetaId -> Doc) -> (SizeMeta -> MetaId) -> SizeMeta -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SizeMeta -> MetaId
    sizeMetaId

    instance PrettyTCM SizeMeta where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => SizeMeta -> m Doc
    prettyTCM (SizeMeta MetaId
    x [Int]
    es) = Term -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (MetaId -> Elims -> Term
    MetaV MetaId
    x (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ (Int -> Elim' Term) -> [Int] -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map (Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply (Arg Term -> Elim' Term) -> (Int -> Arg Term) -> Int -> Elim' Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> Arg Term
    forall a. a -> Arg a
    defaultArg (Term -> Arg Term) -> (Int -> Term) -> Int -> Arg Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Term
    var) [Int]
    es)

    instance Subst SizeMeta where
      type SubstArg SizeMeta = Term
      applySubst :: Substitution' (SubstArg SizeMeta) -> SizeMeta -> SizeMeta
    applySubst Substitution' (SubstArg SizeMeta)
    sigma (SizeMeta MetaId
    x [Int]
    es) = MetaId -> [Int] -> SizeMeta
    SizeMeta MetaId
    x ((Int -> Int) -> [Int] -> [Int]
    forall a b. (a -> b) -> [a] -> [b]
    map Int -> Int
    raise [Int]
    es)
        where
          raise :: Int -> Int
    raise Int
    i =
            case Substitution' Term -> Int -> Term
    forall a. EndoSubst a => Substitution' a -> Int -> a
    lookupS Substitution' Term
    Substitution' (SubstArg SizeMeta)
    sigma Int
    i of
              Var Int
    j [] -> Int
    j
              Term
    _        -> Int
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Size expression with de Bruijn indices.
    type DBSizeExpr = SizeExpr' NamedRigid SizeMeta

    -- deriving instance Functor     (SizeExpr' Int)
    -- deriving instance Foldable    (SizeExpr' Int)
    -- deriving instance Traversable (SizeExpr' Int)

    -- | Only for 'raise'.
    instance Subst (SizeExpr' NamedRigid SizeMeta) where
      type SubstArg (SizeExpr' NamedRigid SizeMeta) = Term
      applySubst :: Substitution' (SubstArg DBSizeExpr) -> DBSizeExpr -> DBSizeExpr
    applySubst Substitution' (SubstArg DBSizeExpr)
    sigma DBSizeExpr
    a =
        case DBSizeExpr
    a of
          DBSizeExpr
    Infty   -> DBSizeExpr
    a
          Const{} -> DBSizeExpr
    a
          Flex  SizeMeta
    x Offset
    n -> SizeMeta -> Offset -> DBSizeExpr
    forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
    Flex (Substitution' (SubstArg SizeMeta) -> SizeMeta -> SizeMeta
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg DBSizeExpr)
    Substitution' (SubstArg SizeMeta)
    sigma SizeMeta
    x) Offset
    n
          Rigid NamedRigid
    r Offset
    n ->
            case Substitution' Term -> Int -> Term
    forall a. EndoSubst a => Substitution' a -> Int -> a
    lookupS Substitution' Term
    Substitution' (SubstArg DBSizeExpr)
    sigma (Int -> Term) -> Int -> Term
    forall a b. (a -> b) -> a -> b
    $ NamedRigid -> Int
    rigidIndex NamedRigid
    r of
              Var Int
    j [] -> NamedRigid -> Offset -> DBSizeExpr
    forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
    Rigid NamedRigid
    r{ rigidIndex :: Int
    rigidIndex = Int
    j } Offset
    n
              Term
    _        -> DBSizeExpr
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    type SizeConstraint = Constraint' NamedRigid SizeMeta

    instance Subst SizeConstraint where
      type SubstArg SizeConstraint = Term
      applySubst :: Substitution' (SubstArg SizeConstraint)
    -> SizeConstraint -> SizeConstraint
    applySubst Substitution' (SubstArg SizeConstraint)
    sigma (Constraint DBSizeExpr
    a Cmp
    cmp DBSizeExpr
    b) =
        DBSizeExpr -> Cmp -> DBSizeExpr -> SizeConstraint
    forall rigid flex.
    SizeExpr' rigid flex
    -> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
    Constraint (Substitution' (SubstArg DBSizeExpr) -> DBSizeExpr -> DBSizeExpr
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg SizeConstraint)
    Substitution' (SubstArg DBSizeExpr)
    sigma DBSizeExpr
    a) Cmp
    cmp (Substitution' (SubstArg DBSizeExpr) -> DBSizeExpr -> DBSizeExpr
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg SizeConstraint)
    Substitution' (SubstArg DBSizeExpr)
    sigma DBSizeExpr
    b)

    -- | Assumes we are in the right context.
    instance PrettyTCM (SizeConstraint) where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => SizeConstraint -> m Doc
    prettyTCM (Constraint DBSizeExpr
    a Cmp
    cmp DBSizeExpr
    b) = do
        Term
    u <- DBSizeExpr -> m Term
    forall (m :: * -> *). HasBuiltins m => DBSizeExpr -> m Term
    unSizeExpr DBSizeExpr
    a
        Term
    v <- DBSizeExpr -> m Term
    forall (m :: * -> *). HasBuiltins m => DBSizeExpr -> m Term
    unSizeExpr DBSizeExpr
    b
        Term -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    u m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Cmp -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Cmp
    cmp m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    v

    -- | Size constraint with de Bruijn indices.
    data HypSizeConstraint = HypSizeConstraint
      { HypSizeConstraint -> Context
    sizeContext    :: Context
      , HypSizeConstraint -> [Int]
    sizeHypIds     :: [Nat] -- ^ DeBruijn indices
      , HypSizeConstraint -> [SizeConstraint]
    sizeHypotheses :: [SizeConstraint]  -- ^ Living in @Context@.
      , HypSizeConstraint -> SizeConstraint
    sizeConstraint :: SizeConstraint    -- ^ Living in @Context@.
      }

    instance Flexs HypSizeConstraint where
      type FlexOf HypSizeConstraint = SizeMeta
      flexs :: HypSizeConstraint -> Set (FlexOf HypSizeConstraint)
    flexs (HypSizeConstraint Context
    _ [Int]
    _ [SizeConstraint]
    hs SizeConstraint
    c) = [SizeConstraint] -> Set (FlexOf [SizeConstraint])
    forall a. Flexs a => a -> Set (FlexOf a)
    flexs [SizeConstraint]
    hs Set SizeMeta -> Set SizeMeta -> Set SizeMeta
    forall a. Monoid a => a -> a -> a
    `mappend` SizeConstraint -> Set (FlexOf SizeConstraint)
    forall a. Flexs a => a -> Set (FlexOf a)
    flexs SizeConstraint
    c

    instance PrettyTCM HypSizeConstraint where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => HypSizeConstraint -> m Doc
    prettyTCM (HypSizeConstraint Context
    cxt [Int]
    _ [SizeConstraint]
    hs SizeConstraint
    c) =
        (Context -> Context) -> m Doc -> m Doc
    forall (tcm :: * -> *) a.
    MonadTCEnv tcm =>
    (Context -> Context) -> tcm a -> tcm a
    unsafeModifyContext (Context -> Context -> Context
    forall a b. a -> b -> a
    const Context
    cxt) (m Doc -> m Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $ do
          let cxtNames :: [Name]
    cxtNames = [Name] -> [Name]
    forall a. [a] -> [a]
    reverse ([Name] -> [Name]) -> [Name] -> [Name]
    forall a b. (a -> b) -> a -> b
    $ (Dom' Term (Name, Type) -> Name) -> Context -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Name, Type) -> Name
    forall a b. (a, b) -> a
    fst ((Name, Type) -> Name)
    -> (Dom' Term (Name, Type) -> (Name, Type))
    -> Dom' Term (Name, Type)
    -> Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom' Term (Name, Type) -> (Name, Type)
    forall t e. Dom' t e -> e
    unDom) Context
    cxt
          -- text ("[#cxt=" ++ show (size cxt) ++ "]") <+> do
          [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList ((Name -> m Doc) -> [Name] -> [m Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM [Name]
    cxtNames) m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> do
          Bool -> (m Doc -> m Doc) -> m Doc -> m Doc
    forall a. Bool -> (a -> a) -> a -> a
    applyUnless ([SizeConstraint] -> Bool
    forall a. Null a => a -> Bool
    null [SizeConstraint]
    hs)
           (([m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    hcat (m Doc -> [m Doc] -> [m Doc]
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    m Doc -> t (m Doc) -> [m Doc]
    punctuate m Doc
    ", " ([m Doc] -> [m Doc]) -> [m Doc] -> [m Doc]
    forall a b. (a -> b) -> a -> b
    $ (SizeConstraint -> m Doc) -> [SizeConstraint] -> [m Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map SizeConstraint -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM [SizeConstraint]
    hs) m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> m Doc
    "|-") m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+>)
           (SizeConstraint -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM SizeConstraint
    c)

    -- | Turn a constraint over de Bruijn indices into a size constraint.
    computeSizeConstraint :: ProblemConstraint -> TCM (Maybe HypSizeConstraint)
    computeSizeConstraint :: ProblemConstraint -> TCMT IO (Maybe HypSizeConstraint)
    computeSizeConstraint ProblemConstraint
    c = do
      let cxt :: Context
    cxt = TCEnv -> Context
    envContext (TCEnv -> Context) -> TCEnv -> Context
    forall a b. (a -> b) -> a -> b
    $ Closure Constraint -> TCEnv
    forall a. Closure a -> TCEnv
    clEnv (Closure Constraint -> TCEnv) -> Closure Constraint -> TCEnv
    forall a b. (a -> b) -> a -> b
    $ ProblemConstraint -> Closure Constraint
    theConstraint ProblemConstraint
    c
      (Context -> Context)
    -> TCMT IO (Maybe HypSizeConstraint)
    -> TCMT IO (Maybe HypSizeConstraint)
    forall (tcm :: * -> *) a.
    MonadTCEnv tcm =>
    (Context -> Context) -> tcm a -> tcm a
    unsafeModifyContext (Context -> Context -> Context
    forall a b. a -> b -> a
    const Context
    cxt) (TCMT IO (Maybe HypSizeConstraint)
     -> TCMT IO (Maybe HypSizeConstraint))
    -> TCMT IO (Maybe HypSizeConstraint)
    -> TCMT IO (Maybe HypSizeConstraint)
    forall a b. (a -> b) -> a -> b
    $ do
        case Closure Constraint -> Constraint
    forall a. Closure a -> a
    clValue (Closure Constraint -> Constraint)
    -> Closure Constraint -> Constraint
    forall a b. (a -> b) -> a -> b
    $ ProblemConstraint -> Closure Constraint
    theConstraint ProblemConstraint
    c of
          ValueCmp Comparison
    CmpLeq CompareAs
    _ Term
    u Term
    v -> do
            [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.size.solve" Int
    50 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    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
    "converting size constraint"
              , ProblemConstraint -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM ProblemConstraint
    c
              ]
            Maybe DBSizeExpr
    ma <- Term -> TCMT IO (Maybe DBSizeExpr)
    sizeExpr Term
    u
            Maybe DBSizeExpr
    mb <- Term -> TCMT IO (Maybe DBSizeExpr)
    sizeExpr Term
    v
            ([Int]
    hids, [SizeConstraint]
    hs) <- [(Int, SizeConstraint)] -> ([Int], [SizeConstraint])
    forall a b. [(a, b)] -> ([a], [b])
    unzip ([(Int, SizeConstraint)] -> ([Int], [SizeConstraint]))
    -> TCM [(Int, SizeConstraint)] -> TCMT IO ([Int], [SizeConstraint])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Context -> TCM [(Int, SizeConstraint)]
    getSizeHypotheses Context
    cxt
            let mk :: DBSizeExpr -> DBSizeExpr -> HypSizeConstraint
    mk DBSizeExpr
    a DBSizeExpr
    b = Context
    -> [Int] -> [SizeConstraint] -> SizeConstraint -> HypSizeConstraint
    HypSizeConstraint Context
    cxt [Int]
    hids [SizeConstraint]
    hs (SizeConstraint -> HypSizeConstraint)
    -> SizeConstraint -> HypSizeConstraint
    forall a b. (a -> b) -> a -> b
    $ DBSizeExpr -> Cmp -> DBSizeExpr -> SizeConstraint
    forall rigid flex.
    SizeExpr' rigid flex
    -> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
    Size.Constraint DBSizeExpr
    a Cmp
    Le DBSizeExpr
    b
            -- We only create a size constraint if both terms can be
            -- parsed to our format of size expressions.
            Maybe HypSizeConstraint -> TCMT IO (Maybe HypSizeConstraint)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe HypSizeConstraint -> TCMT IO (Maybe HypSizeConstraint))
    -> Maybe HypSizeConstraint -> TCMT IO (Maybe HypSizeConstraint)
    forall a b. (a -> b) -> a -> b
    $ DBSizeExpr -> DBSizeExpr -> HypSizeConstraint
    mk (DBSizeExpr -> DBSizeExpr -> HypSizeConstraint)
    -> Maybe DBSizeExpr -> Maybe (DBSizeExpr -> HypSizeConstraint)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe DBSizeExpr
    ma Maybe (DBSizeExpr -> HypSizeConstraint)
    -> Maybe DBSizeExpr -> Maybe HypSizeConstraint
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Maybe DBSizeExpr
    mb
          Constraint
    _ -> TCMT IO (Maybe HypSizeConstraint)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Turn a term into a size expression.
    --
    --   Returns 'Nothing' if the term isn't a proper size expression.

    sizeExpr :: Term -> TCM (Maybe DBSizeExpr)
    sizeExpr :: Term -> TCMT IO (Maybe DBSizeExpr)
    sizeExpr Term
    u = do
      Term
    u <- Term -> TCMT IO Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Term
    u -- Andreas, 2009-02-09.
                    -- This is necessary to surface the solutions of metavariables.
      [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.conv.size" Int
    60 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "sizeExpr:" 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
    u
      SizeView
    s <- Term -> TCMT IO SizeView
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
    Term -> m SizeView
    sizeView Term
    u
      case SizeView
    s of
        SizeView
    SizeInf     -> Maybe DBSizeExpr -> TCMT IO (Maybe DBSizeExpr)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe DBSizeExpr -> TCMT IO (Maybe DBSizeExpr))
    -> Maybe DBSizeExpr -> TCMT IO (Maybe DBSizeExpr)
    forall a b. (a -> b) -> a -> b
    $ DBSizeExpr -> Maybe DBSizeExpr
    forall a. a -> Maybe a
    Just DBSizeExpr
    forall rigid flex. SizeExpr' rigid flex
    Infty
        SizeSuc Term
    u   -> (DBSizeExpr -> DBSizeExpr) -> Maybe DBSizeExpr -> Maybe DBSizeExpr
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (DBSizeExpr -> Offset -> DBSizeExpr
    forall a b c. Plus a b c => a -> b -> c
    `plus` (Offset
    1 :: Offset)) (Maybe DBSizeExpr -> Maybe DBSizeExpr)
    -> TCMT IO (Maybe DBSizeExpr) -> TCMT IO (Maybe DBSizeExpr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> TCMT IO (Maybe DBSizeExpr)
    sizeExpr Term
    u
        OtherSize Term
    u -> case Term
    u of
          Var Int
    i []    -> (\ [Char]
    x -> DBSizeExpr -> Maybe DBSizeExpr
    forall a. a -> Maybe a
    Just (DBSizeExpr -> Maybe DBSizeExpr) -> DBSizeExpr -> Maybe DBSizeExpr
    forall a b. (a -> b) -> a -> b
    $ NamedRigid -> Offset -> DBSizeExpr
    forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
    Rigid ([Char] -> Int -> NamedRigid
    NamedRigid [Char]
    x Int
    i) Offset
    0) ([Char] -> Maybe DBSizeExpr)
    -> (Name -> [Char]) -> Name -> Maybe DBSizeExpr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow (Name -> Maybe DBSizeExpr)
    -> TCMT IO Name -> TCMT IO (Maybe DBSizeExpr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Int -> TCMT IO Name
    forall (m :: * -> *).
    (Applicative m, MonadFail m, MonadTCEnv m) =>
    Int -> m Name
    nameOfBV Int
    i
    --      MetaV m es  -> return $ Just $ Flex (SizeMeta m es) 0
          MetaV MetaId
    m Elims
    es | Just [Int]
    xs <- (Elim' Term -> Maybe Int) -> Elims -> Maybe [Int]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM Elim' Term -> Maybe Int
    isVar Elims
    es, [Int] -> Bool
    forall a. Ord a => [a] -> Bool
    List.fastDistinct [Int]
    xs
                      -> Maybe DBSizeExpr -> TCMT IO (Maybe DBSizeExpr)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe DBSizeExpr -> TCMT IO (Maybe DBSizeExpr))
    -> Maybe DBSizeExpr -> TCMT IO (Maybe DBSizeExpr)
    forall a b. (a -> b) -> a -> b
    $ DBSizeExpr -> Maybe DBSizeExpr
    forall a. a -> Maybe a
    Just (DBSizeExpr -> Maybe DBSizeExpr) -> DBSizeExpr -> Maybe DBSizeExpr
    forall a b. (a -> b) -> a -> b
    $ SizeMeta -> Offset -> DBSizeExpr
    forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
    Flex (MetaId -> [Int] -> SizeMeta
    SizeMeta MetaId
    m [Int]
    xs) Offset
    0
          Term
    _           -> Maybe DBSizeExpr -> TCMT IO (Maybe DBSizeExpr)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe DBSizeExpr
    forall a. Maybe a
    Nothing
      where
        isVar :: Elim' Term -> Maybe Int
    isVar (Proj{})  = Maybe Int
    forall a. Maybe a
    Nothing
        isVar (IApply Term
    _ Term
    _ Term
    v) = Elim' Term -> Maybe Int
    isVar (Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply (Term -> Arg Term
    forall a. a -> Arg a
    defaultArg Term
    v))
        isVar (Apply Arg Term
    v) = case Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    v of
          Var Int
    i [] -> Int -> Maybe Int
    forall a. a -> Maybe a
    Just Int
    i
          Term
    _        -> Maybe Int
    forall a. Maybe a
    Nothing

    -- | Turn a de size expression into a term.
    unSizeExpr :: HasBuiltins m => DBSizeExpr -> m Term
    unSizeExpr :: forall (m :: * -> *). HasBuiltins m => DBSizeExpr -> m Term
    unSizeExpr DBSizeExpr
    a =
      case DBSizeExpr
    a of
        DBSizeExpr
    Infty         -> Term -> Maybe Term -> Term
    forall a. a -> Maybe a -> a
    fromMaybe Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Char] -> m (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe Term)
    getBuiltin' [Char]
    builtinSizeInf
        Rigid NamedRigid
    r (O Int
    n) -> do
          Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    0) m ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Int -> Term -> m Term
    forall (m :: * -> *). HasBuiltins m => Int -> Term -> m Term
    sizeSuc Int
    n (Term -> m Term) -> Term -> m Term
    forall a b. (a -> b) -> a -> b
    $ Int -> Term
    var (Int -> Term) -> Int -> Term
    forall a b. (a -> b) -> a -> b
    $ NamedRigid -> Int
    rigidIndex NamedRigid
    r
        Flex (SizeMeta MetaId
    x [Int]
    es) (O Int
    n) -> do
          Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    0) m ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Int -> Term -> m Term
    forall (m :: * -> *). HasBuiltins m => Int -> Term -> m Term
    sizeSuc Int
    n (Term -> m Term) -> Term -> m Term
    forall a b. (a -> b) -> a -> b
    $ MetaId -> Elims -> Term
    MetaV MetaId
    x (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ (Int -> Elim' Term) -> [Int] -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map (Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply (Arg Term -> Elim' Term) -> (Int -> Arg Term) -> Int -> Elim' Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> Arg Term
    forall a. a -> Arg a
    defaultArg (Term -> Arg Term) -> (Int -> Term) -> Int -> Arg Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Term
    var) [Int]
    es
        Const{} -> m Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__