    -- | Imperfect discrimination trees for indexing data by internal
    -- syntax.
    module Agda.TypeChecking.DiscrimTree
      ( insertDT
      , lookupDT, lookupUnifyDT, QueryResult(..)
      , deleteFromDT
      )
      where

    import qualified Data.Map.Strict as Map
    import qualified Data.Set as Set
    import Data.Foldable
    import Data.Maybe

    import Control.Monad.Trans.Maybe
    import Control.Monad.Trans
    import Control.Monad

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

    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Telescope
    import Agda.TypeChecking.Records
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Free

    import Agda.TypeChecking.DiscrimTree.Types

    import qualified Agda.Utils.ProfileOptions as Profile

    import Agda.Utils.Impossible
    import Agda.Utils.Trie (Trie(..))

    -- | Dummy term to use as a stand-in for expanded eta-records while
    -- building instance trees.
    etaExpansionDummy :: Term
    etaExpansionDummy :: Term
    etaExpansionDummy = String -> Elims -> Term
    Dummy String
    "eta-record argument in instance head" []

    -- | Extract a list of arguments from the list of eliminations; If
    -- called while *adding* an instance, additionally replace any arguments
    -- that might belong to an eta-record by dummy terms.
    termKeyElims
      :: Bool      -- ^ Are we adding or looking up an instance?
      -> TCM Type  -- ^ Continuation to compute the type of the arguments in the spine.
      -> [Arg Term] -- ^ The spine.
      -> TCM (Int, [Term])

    -- Since the case tree was generated with wildcards everywhere an eta
    -- record appeared, if we're *looking up* an instance, we don't have to
    -- do the censorship again.
    termKeyElims :: Bool -> TCM Type -> [Arg Term] -> TCM (Int, [Term])
    termKeyElims Bool
    False TCM Type
    _ [Arg Term]
    es = (Int, [Term]) -> TCM (Int, [Term])
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ([Arg Term] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Arg Term]
    es, (Arg Term -> Term) -> [Arg Term] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Term
    forall e. Arg e -> e
    unArg [Arg Term]
    es)

    termKeyElims Bool
    precise TCM Type
    ty [Arg Term]
    args = do
      let
        go :: Type -> [Arg Term] -> m (a, [Term])
    go Type
    ty (Arg ArgInfo
    _ Term
    a:[Arg Term]
    as) = ((Dom Type -> Abs Type -> m (a, [Term]))
     -> (Blocked Type -> m (a, [Term])) -> m (a, [Term]))
    -> (Blocked Type -> m (a, [Term]))
    -> (Dom Type -> Abs Type -> m (a, [Term]))
    -> m (a, [Term])
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (Type
    -> (Dom Type -> Abs Type -> m (a, [Term]))
    -> (Blocked Type -> m (a, [Term]))
    -> m (a, [Term])
    forall (m :: * -> *) a.
    MonadReduce m =>
    Type
    -> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a
    ifPiTypeB Type
    ty) (Blocker -> m (a, [Term])
    forall a. Blocker -> m a
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation (Blocker -> m (a, [Term]))
    -> (Blocked Type -> Blocker) -> Blocked Type -> m (a, [Term])
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Blocked Type -> Blocker
    forall t a. Blocked' t a -> Blocker
    getBlocker) \Dom Type
    dom Abs Type
    ty' -> do

          -- Is this argument an eta record type --- or a blocked value? In
          -- either case, we replace this position by a dummy, to make sure
          -- that eta-equality is respected.
          maybeEta <- Type
    -> (Blocker -> Type -> m Bool)
    -> (NotBlocked -> Type -> m Bool)
    -> m Bool
    forall t (m :: * -> *) a.
    (Reduce t, IsMeta t, MonadReduce m) =>
    t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
    ifBlocked (Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    dom) (\Blocker
    _ Type
    _ -> Bool -> m Bool
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Bool
    True) \NotBlocked
    _ Type
    tm ->
            Maybe (QName, [Arg Term]) -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe (QName, [Arg Term]) -> Bool)
    -> m (Maybe (QName, [Arg Term])) -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> m (Maybe (QName, [Arg Term]))
    forall (m :: * -> *).
    HasConstInfo m =>
    Type -> m (Maybe (QName, [Arg Term]))
    isEtaRecordType Type
    tm

          let
            here
              | Bool
    maybeEta  = Term
    etaExpansionDummy
              | Bool
    otherwise = Term
    a

          (k, there) <- addContext dom (go (unAbs ty') as)
          pure (k + 1, here:there)

        go Type
    _ [] = (a, [Term]) -> m (a, [Term])
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (a
    0, [])

      TCM Type
    ty TCM Type -> (Type -> TCM (Int, [Term])) -> TCM (Int, [Term])
    forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= (Type -> [Arg Term] -> TCM (Int, [Term]))
    -> [Arg Term] -> Type -> TCM (Int, [Term])
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip Type -> [Arg Term] -> TCM (Int, [Term])
    forall {m :: * -> *} {a}.
    (MonadReduce m, MonadBlock m, HasConstInfo m, MonadAddContext m,
     Num a) =>
    Type -> [Arg Term] -> m (a, [Term])
    go [Arg Term]
    args

    -- | Ticky profiling for the reason behind "inexactness" in instance
    -- search. If at some point while narrowing the set of candidates we had
    -- to go through all the possibilities, one of these counters is
    -- incremented.
    tickExplore :: Term -> TCM ()
    tickExplore :: Term -> TCM ()
    tickExplore Term
    tm = ProfileOption -> TCM () -> TCM ()
    forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
    whenProfile ProfileOption
    Profile.Instances do
      String -> TCM ()
    forall (m :: * -> *). MonadStatistics m => String -> m ()
    tick String
    "flex term blocking instance"

      case Term
    tm of
        Def{}      -> String -> TCM ()
    forall (m :: * -> *). MonadStatistics m => String -> m ()
    tick String
    "explore: Def"
        Var{}      -> String -> TCM ()
    forall (m :: * -> *). MonadStatistics m => String -> m ()
    tick String
    "explore: Var"
        Lam ArgInfo
    _ Abs Term
    v
          -- These two are a hunch: just like FunK, it might be worth
          -- optimising for the case where a lambda is constant (which is
          -- easy to handle, by just pretending the term is something else).
          -- These would come up in e.g. Dec (PathP (λ i → Nat) x y)
          | NoAbs{} <- Abs Term
    v -> String -> TCM ()
    forall (m :: * -> *). MonadStatistics m => String -> m ()
    tick String
    "explore: constant function"
          | Abs String
    _ Term
    b <- Abs Term
    v, Bool -> Bool
    not (Int
    0 Int -> Term -> Bool
    forall a. Free a => Int -> a -> Bool
    `freeIn` Term
    b) -> String -> TCM ()
    forall (m :: * -> *). MonadStatistics m => String -> m ()
    tick String
    "explore: constant function"

          | Bool
    otherwise    -> String -> TCM ()
    forall (m :: * -> *). MonadStatistics m => String -> m ()
    tick String
    "explore: Lam"
        Lit{}      -> String -> TCM ()
    forall (m :: * -> *). MonadStatistics m => String -> m ()
    tick String
    "explore: Lit"
        Sort{}     -> String -> TCM ()
    forall (m :: * -> *). MonadStatistics m => String -> m ()
    tick String
    "explore: Sort"
        Level{}    -> String -> TCM ()
    forall (m :: * -> *). MonadStatistics m => String -> m ()
    tick String
    "explore: Level"
        MetaV{}    -> String -> TCM ()
    forall (m :: * -> *). MonadStatistics m => String -> m ()
    tick String
    "explore: Meta"
        DontCare{} -> String -> TCM ()
    forall (m :: * -> *). MonadStatistics m => String -> m ()
    tick String
    "explore: DontCare"
        Term
    _ -> () -> TCM ()
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()

    -- | Split a term into a 'Key' and some arguments. The 'Key' indicates
    -- whether or not the 'Term' is in head-normal form, and provides a
    -- quick way to match on the head.
    --
    -- The 'Int' argument indicates how free a variable must be to be
    -- considered a 'LocalK'.
    --
    -- Presently, non-head-normal terms end up with an empty argument list.
    splitTermKey :: Bool -> Int -> Term -> TCM (Key, [Term], Blocker)
    splitTermKey :: Bool -> Int -> Term -> TCM (Key, [Term], Blocker)
    splitTermKey Bool
    precise Int
    local Term
    tm = (Blocker -> TCM (Key, [Term], Blocker))
    -> TCM (Key, [Term], Blocker) -> TCM (Key, [Term], Blocker)
    forall a. (Blocker -> TCMT IO a) -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a.
    MonadBlock m =>
    (Blocker -> m a) -> m a -> m a
    catchPatternErr (\Blocker
    b -> (Key, [Term], Blocker) -> TCM (Key, [Term], Blocker)
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Key
    FlexK, [], Blocker
    b)) do
      (b, tm') <- Term
    -> (Blocker -> Term -> TCMT IO (NotBlocked, Term))
    -> (NotBlocked -> Term -> TCMT IO (NotBlocked, Term))
    -> TCMT IO (NotBlocked, Term)
    forall t (m :: * -> *) a.
    (Reduce t, IsMeta t, MonadReduce m) =>
    t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
    ifBlocked Term
    tm (\Blocker
    b Term
    _ -> Blocker -> TCMT IO (NotBlocked, Term)
    forall a. Blocker -> TCMT IO a
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation Blocker
    b) (\NotBlocked
    b -> (Term -> (NotBlocked, Term))
    -> TCMT IO Term -> TCMT IO (NotBlocked, Term)
    forall a b. (a -> b) -> TCMT IO a -> TCMT IO b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (NotBlocked
    b,) (TCMT IO Term -> TCMT IO (NotBlocked, Term))
    -> (Term -> TCMT IO Term) -> Term -> TCMT IO (NotBlocked, Term)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> TCMT IO Term
    forall (m :: * -> *). HasBuiltins m => Term -> m Term
    constructorForm)

      case tm' of
        -- Adding a 'Def' to the key poses a few problems when opacity (or
        -- abstractness) are involved (see issue #7304). Suppose we have an
        -- opaque binding `X = Y`, and an opaque instance `C X`. The problem
        -- is as follows:
        --
        --   if we unfold X → Y when adding the instance, then it will not
        --   get recorded as an instance for C X, only C Y; this is 7304b.
        --
        --   if we *don't* unfold X → Y, then it only gets added as an
        --   instance of C X; in opaque blocks where X is allowed to unfold,
        --   we *won't* find it, because we're looking for C Y.
        --
        -- The solution is to throw our hands up and say "not our problem".
        -- The discrimination tree is allowed to return more results than
        -- strictly necessary, after all, so the solution is to add an
        -- instance for *neither* of C X or C Y, but instead, to treat all
        -- 'Def's headed by 'AbstractDefn' as though they were flexible
        -- (think "as though they were metas").
        Def QName
    q Elims
    as | NotBlocked
    ReallyNotBlocked <- NotBlocked
    b, ([Arg Term]
    as, Elims
    _) <- Elims -> ([Arg Term], Elims)
    forall a. [Elim' a] -> ([Arg a], [Elim' a])
    splitApplyElims Elims
    as -> do
          info <- QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q
          case theDef info of
            AbstractDefn{} | Bool
    precise -> (Key, [Term], Blocker) -> TCM (Key, [Term], Blocker)
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Key
    FlexK, [], Blocker
    neverUnblock)
            Defn
    _ -> do
              (arity, as) <- Bool -> TCM Type -> [Arg Term] -> TCM (Int, [Term])
    termKeyElims Bool
    precise (Type -> TCM Type
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Definition -> Type
    defType Definition
    info)) [Arg Term]
    as
              pure (RigidK q arity, as, neverUnblock)

        -- When adding a quantified instance, we record how many 'Pi's we went
        -- under, and only variables beyond those are considered LocalK. The
        -- others are considered FlexK since they're "pattern variables" of
        -- the instance.
        Var Int
    i Elims
    as | Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    local, Just [Arg Term]
    as <- Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    as -> do
          let ty :: TCM Type
    ty = Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom (Dom Type -> Type) -> TCMT IO (Dom Type) -> TCM Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Int -> TCMT IO (Dom Type)
    forall (m :: * -> *).
    (MonadDebug m, MonadTCEnv m) =>
    Int -> m (Dom Type)
    domOfBV Int
    i
          (arity, as) <- Bool -> TCM Type -> [Arg Term] -> TCM (Int, [Term])
    termKeyElims Bool
    precise TCM Type
    ty [Arg Term]
    as
          pure (LocalK (i - local) arity, as, neverUnblock)

        -- When looking up an instance, it's better to treat variables and
        -- neutral definitions as rigid things regardless of their spines
        -- (especially if they have projections), than it is to try to
        -- represent them accurately.
        Def QName
    q Elims
    as | Bool -> Bool
    not Bool
    precise             -> (Key, [Term], Blocker) -> TCM (Key, [Term], Blocker)
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (QName -> Int -> Key
    RigidK QName
    q Int
    0, [], Blocker
    neverUnblock)
        Var Int
    i Elims
    as | Bool -> Bool
    not Bool
    precise, Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    local -> (Key, [Term], Blocker) -> TCM (Key, [Term], Blocker)
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Int -> Int -> Key
    LocalK (Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    local) Int
    0, [], Blocker
    neverUnblock)

        Con ConHead
    ch ConInfo
    _ Elims
    as | Just [Arg Term]
    as <- Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    as -> do
          let
            q :: QName
    q  = ConHead -> QName
    conName ConHead
    ch
            ty :: TCM Type
    ty = Definition -> Type
    defType (Definition -> Type) -> TCMT IO Definition -> TCM Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q
          (arity, as) <- Bool -> TCM Type -> [Arg Term] -> TCM (Int, [Term])
    termKeyElims Bool
    precise TCM Type
    ty [Arg Term]
    as
          pure (RigidK q arity, as, neverUnblock)

        Pi Dom Type
    dom Abs Type
    ret ->
          let
            -- If we're looking at a non-dependent function type, then we
            -- might as well represent the codomain accurately; Otherwise,
            -- turn the codomain into a wildcard.
            --
            -- The use of a dummy term *shouldn't* leak to the user, because
            -- when we call splitTermKey again, it'll be handled by the last
            -- case, and become a FlexK.
            ret' :: Term
    ret' = case Abs Term -> Maybe Term
    forall a. (Free a, Subst a) => Abs a -> Maybe a
    isNoAbs (Type -> Term
    forall t a. Type'' t a -> a
    unEl (Type -> Term) -> Abs Type -> Abs Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Abs Type
    ret) of
              Just Term
    b  -> Term
    b
              Maybe Term
    Nothing -> Term
    HasCallStack => Term
    __DUMMY_TERM__
          in (Key, [Term], Blocker) -> TCM (Key, [Term], Blocker)
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Hiding -> Key
    PiK (Dom Type -> Hiding
    forall a. LensHiding a => a -> Hiding
    getHiding Dom Type
    dom), [Type -> Term
    forall t a. Type'' t a -> a
    unEl (Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    dom), Term
    ret'], Blocker
    neverUnblock)

        Lam ArgInfo
    _ Abs Term
    body
          -- Constant lambdas come up quite a bit, particularly (in cubical
          -- mode) as the domain of a PathP. Having this trick improves the
          -- indexing of 'Dec' instances in the 1Lab significantly.
          | Just Term
    b <- Abs Term -> Maybe Term
    forall a. (Free a, Subst a) => Abs a -> Maybe a
    isNoAbs Abs Term
    body -> (Key, [Term], Blocker) -> TCM (Key, [Term], Blocker)
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Key
    ConstK, [Term
    b], Blocker
    neverUnblock)

        -- Probably not a good idea for accurate indexing if universes
        -- overlap literally everything else.
        Sort Sort
    _ -> (Key, [Term], Blocker) -> TCM (Key, [Term], Blocker)
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Key
    SortK, [], Blocker
    neverUnblock)

        Term
    _ -> do
          String -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.instance.split" Int
    30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Term -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Term
    tm
          (Key, [Term], Blocker) -> TCM (Key, [Term], Blocker)
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Key
    FlexK, [], Blocker
    neverUnblock)

    termPath :: Int -> Bool -> Int -> [Key] -> [Term] -> TCM [Key]
    termPath :: Int -> Bool -> Int -> [Key] -> [Term] -> TCM [Key]
    termPath Int
    0 Bool
    _ Int
    _ [Key]
    acc [Term]
    _                        = [Key] -> TCM [Key]
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ([Key] -> TCM [Key]) -> [Key] -> TCM [Key]
    forall a b. (a -> b) -> a -> b
    $! [Key] -> [Key]
    forall a. [a] -> [a]
    reverse [Key]
    acc
    termPath Int
    limit Bool
    toplevel Int
    local [Key]
    acc []        = [Key] -> TCM [Key]
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ([Key] -> TCM [Key]) -> [Key] -> TCM [Key]
    forall a b. (a -> b) -> a -> b
    $! [Key] -> [Key]
    forall a. [a] -> [a]
    reverse [Key]
    acc
    termPath Int
    limit Bool
    toplevel Int
    local [Key]
    acc (Term
    tm:[Term]
    todo) = do

      -- We still want to ignore abstractness at the very top-level of
      -- instance heads, for issue #6941, to ensure that each instance ends
      -- up in the right 'class'. See the comment in `splitTermKey` about
      -- abstract definitions.
      (k, as, blk) <-
        if Bool
    toplevel
          then TCM (Key, [Term], Blocker) -> TCM (Key, [Term], Blocker)
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    ignoreAbstractMode (Bool -> Int -> Term -> TCM (Key, [Term], Blocker)
    splitTermKey Bool
    True Int
    local Term
    tm)
          else Bool -> Int -> Term -> TCM (Key, [Term], Blocker)
    splitTermKey Bool
    True Int
    local Term
    tm

      reportSDoc "tc.instance.discrim.add" 666 $ vcat
        [ "k:  " <+> prettyTCM k
        , "as: " <+> prettyTCM as
        , "blk:" <+> prettyTCM blk
        , "lim:" <+> prettyTCM limit
        ]
      termPath (limit - 1) False local (k:acc) (as <> todo)

    -- | Maximum length for the keys (thus, depth for the discrimination
    -- tree) that should be used.
    --
    -- Adding an instance still causes reduction of everything 'rigid' in
    -- the type of the instance (so if normalisation is slow, so will be
    -- adding the instance) but this limit prevents us from building a
    -- discrimination tree with 2^32 intermediate @case 0 of suc → ...@
    -- nodes.
    discrimTreeDepthLimit :: Int
    discrimTreeDepthLimit :: Int
    discrimTreeDepthLimit = Int
    16

    -- | Insert a value into the discrimination tree, turning variables into
    -- rigid locals or wildcards depending on the given scope.
    insertDT
      :: (Ord a, PrettyTCM a)
      => Int   -- ^ Number of variables to consider wildcards, e.g. the number of leading invisible pis in an instance type.
      -> Term  -- ^ The term to use as a key
      -> a
      -> DiscrimTree a
      -> TCM (DiscrimTree a)
    insertDT :: forall a.
    (Ord a, PrettyTCM a) =>
    Int -> Term -> a -> DiscrimTree a -> TCM (DiscrimTree a)
    insertDT Int
    local Term
    key a
    val DiscrimTree a
    tree = do
      path <- Int -> Bool -> Int -> [Key] -> [Term] -> TCM [Key]
    termPath Int
    discrimTreeDepthLimit Bool
    True Int
    local [] [Term
    key]
      let it = [Key] -> a -> DiscrimTree a
    forall a. [Key] -> a -> DiscrimTree a
    singletonDT [Key]
    path a
    val
      reportSDoc "tc.instance.discrim.add" 20 $ vcat
        [ "added value" <+> prettyTCM val <+> "to discrimination tree with case"
        , nest 2 (prettyTCM it)
        , "its type:"
        , nest 2 (prettyTCM key)
        , "its path:"
        , nest 2 (prettyTCM path)
        ]
      pure $ mergeDT it tree

    -- | If a term matches this key, how many arguments does it place on the
    -- spine?
    keyArity :: Key -> Int
    keyArity :: Key -> Int
    keyArity = \case
      RigidK QName
    _ Int
    a -> Int
    a
      LocalK Int
    _ Int
    a -> Int
    a
      PiK Hiding
    _      -> Int
    2
      Key
    ConstK     -> Int
    1
      Key
    SortK      -> Int
    0
      Key
    FlexK      -> Int
    0

    data QueryResult a = QueryResult
      { forall a. QueryResult a -> Set a
    resultValues  :: Set.Set a
      , forall a. QueryResult a -> Blocker
    resultBlocker :: Blocker
      }

    instance Ord a => Semigroup (QueryResult a) where
      QueryResult Set a
    s Blocker
    b <> :: QueryResult a -> QueryResult a -> QueryResult a
    <> QueryResult Set a
    s' Blocker
    b' = Set a -> Blocker -> QueryResult a
    forall a. Set a -> Blocker -> QueryResult a
    QueryResult (Set a
    s Set a -> Set a -> Set a
    forall a. Semigroup a => a -> a -> a
    <> Set a
    s') (Blocker
    b Blocker -> Blocker -> Blocker
    `unblockOnEither` Blocker
    b')

    instance Ord a => Monoid (QueryResult a) where
      mempty :: QueryResult a
    mempty = Set a -> Blocker -> QueryResult a
    forall a. Set a -> Blocker -> QueryResult a
    QueryResult Set a
    forall a. Monoid a => a
    mempty Blocker
    neverUnblock

    setResult :: Set.Set a -> QueryResult a
    setResult :: forall a. Set a -> QueryResult a
    setResult = (Set a -> Blocker -> QueryResult a)
    -> Blocker -> Set a -> QueryResult a
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip Set a -> Blocker -> QueryResult a
    forall a. Set a -> Blocker -> QueryResult a
    QueryResult Blocker
    neverUnblock

    blockerResult :: Blocker -> QueryResult a
    blockerResult :: forall a. Blocker -> QueryResult a
    blockerResult = Set a -> Blocker -> QueryResult a
    forall a. Set a -> Blocker -> QueryResult a
    QueryResult Set a
    forall a. Set a
    Set.empty

    -- | Look up a 'Term' in the given discrimination tree, treating local
    -- variables as rigid symbols. The returned set is guaranteed to contain
    -- everything that could overlap the given key.
    lookupDT :: forall a. (Ord a, PrettyTCM a) => Term -> DiscrimTree a -> TCM (QueryResult a)
    lookupDT :: forall a.
    (Ord a, PrettyTCM a) =>
    Term -> DiscrimTree a -> TCM (QueryResult a)
    lookupDT = Bool -> Term -> DiscrimTree a -> TCM (QueryResult a)
    forall a.
    (Ord a, PrettyTCM a) =>
    Bool -> Term -> DiscrimTree a -> TCM (QueryResult a)
    lookupDT' Bool
    True

    -- | Look up a 'Term' in the given discrimination tree, treating local
    -- variables as wildcards.
    lookupUnifyDT :: forall a. (Ord a, PrettyTCM a) => Term -> DiscrimTree a -> TCM (QueryResult a)
    lookupUnifyDT :: forall a.
    (Ord a, PrettyTCM a) =>
    Term -> DiscrimTree a -> TCM (QueryResult a)
    lookupUnifyDT = Bool -> Term -> DiscrimTree a -> TCM (QueryResult a)
    forall a.
    (Ord a, PrettyTCM a) =>
    Bool -> Term -> DiscrimTree a -> TCM (QueryResult a)
    lookupDT' Bool
    False

    lookupDT'
      :: forall a. (Ord a, PrettyTCM a)
      => Bool -- ^ Should local variables be treated as rigid?
      -> Term -- ^ The term to use as key
      -> DiscrimTree a
      -> TCM (QueryResult a)
    lookupDT' :: forall a.
    (Ord a, PrettyTCM a) =>
    Bool -> Term -> DiscrimTree a -> TCM (QueryResult a)
    lookupDT' Bool
    localsRigid Term
    term DiscrimTree a
    tree = Bool -> [Term] -> DiscrimTree a -> TCM (QueryResult a)
    match Bool
    True [Term
    term] DiscrimTree a
    tree where

      split :: Term -> TCM (Key, [Term], Blocker)
      split :: Term -> TCM (Key, [Term], Blocker)
    split Term
    tm | Bool
    localsRigid = Bool -> Int -> Term -> TCM (Key, [Term], Blocker)
    splitTermKey Bool
    False Int
    0 Term
    tm
      split Term
    tm = do
        ctx <- TCMT IO Int
    forall (m :: * -> *). MonadTCEnv m => m Int
    getContextSize
        splitTermKey False ctx tm

      ignoreAbstractMaybe :: forall a. Bool -> TCM a -> TCM a
      ignoreAbstractMaybe :: forall a. Bool -> TCM a -> TCM a
    ignoreAbstractMaybe Bool
    True  = TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    ignoreAbstractMode
      ignoreAbstractMaybe Bool
    False = TCMT IO a -> TCMT IO a
    forall a. a -> a
    id

      -- Match a spine against *all* clauses.
      explore :: [Term] -> [Term] -> [Term] -> [(Key, DiscrimTree a)] -> TCM (QueryResult a)
      explore :: [Term]
    -> [Term]
    -> [Term]
    -> [(Key, DiscrimTree a)]
    -> TCM (QueryResult a)
    explore [Term]
    sp0 [Term]
    sp1 [Term]
    args [(Key, DiscrimTree a)]
    bs = do
        let
          cont :: (Key, DiscrimTree a) -> QueryResult a -> TCM (QueryResult a)
    cont (Key
    key, DiscrimTree a
    trie) QueryResult a
    res = do
            -- At the moment, explore will always be called with empty args.
            -- But even if this restriction is lifted in the future, we have
            -- to be careful about exploring. Consider:
            --
            --   instance
            --     _ : Foo (con x)
            --
            --   ⊢ Foo ?0
            --
            -- Since ?0 might be applied to more or less arguments than the
            -- one argument that is expected to be between sp0 and sp1 after
            -- matching con, we need to make sure that the spine has the
            -- right number of arguments, otherwise the (sp0, t:sp1) pattern
            -- for a Case will fail.
            let
              dummy :: a -> Term
    dummy a
    n = String -> Elims -> Term
    Dummy (String
    "_pad" String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> a -> String
    forall a. Show a => a -> String
    show a
    n) []
              args' :: [Term]
    args' = Int -> [Term] -> [Term]
    forall a. Int -> [a] -> [a]
    take (Key -> Int
    keyArity Key
    key) ([Term]
    args [Term] -> [Term] -> [Term]
    forall a. [a] -> [a] -> [a]
    ++ [ Integer -> Term
    forall {a}. Show a => a -> Term
    dummy Integer
    n | Integer
    n <- [Integer
    0..] ])

            String -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.instance.discrim.lookup" Int
    99 (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
    "explore" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Key -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Key -> m Doc
    prettyTCM Key
    key TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Int -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty (Key -> Int
    keyArity Key
    key) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Int -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty ([Term] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Term]
    args)
              , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (DiscrimTree a -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => DiscrimTree a -> m Doc
    prettyTCM DiscrimTree a
    trie)
              , TCMT IO Doc
    "sp0:  " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Term] -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => [Term] -> m Doc
    prettyTCM [Term]
    sp0
              , TCMT IO Doc
    "sp1:  " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Term] -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => [Term] -> m Doc
    prettyTCM [Term]
    sp1
              , TCMT IO Doc
    "args: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Term] -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => [Term] -> m Doc
    prettyTCM [Term]
    args
              , TCMT IO Doc
    "args':" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Term] -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => [Term] -> m Doc
    prettyTCM [Term]
    args'
              ]
            (QueryResult a -> QueryResult a -> QueryResult a
    forall a. Semigroup a => a -> a -> a
    <> QueryResult a
    res) (QueryResult a -> QueryResult a)
    -> TCM (QueryResult a) -> TCM (QueryResult a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Bool -> [Term] -> DiscrimTree a -> TCM (QueryResult a)
    match Bool
    False ([Term]
    sp0 [Term] -> [Term] -> [Term]
    forall a. [a] -> [a] -> [a]
    ++ [Term]
    args' [Term] -> [Term] -> [Term]
    forall a. [a] -> [a] -> [a]
    ++ [Term]
    sp1) DiscrimTree a
    trie

        ((Key, DiscrimTree a) -> QueryResult a -> TCM (QueryResult a))
    -> QueryResult a -> [(Key, DiscrimTree a)] -> TCM (QueryResult a)
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> b -> m b) -> b -> t a -> m b
    foldrM (Key, DiscrimTree a) -> QueryResult a -> TCM (QueryResult a)
    cont QueryResult a
    forall a. Monoid a => a
    mempty [(Key, DiscrimTree a)]
    bs

      match :: Bool -> [Term] -> DiscrimTree a -> TCM (QueryResult a)
      match :: Bool -> [Term] -> DiscrimTree a -> TCM (QueryResult a)
    match Bool
    toplevel [Term]
    ts DiscrimTree a
    EmptyDT    = QueryResult a -> TCM (QueryResult a)
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure QueryResult a
    forall a. Monoid a => a
    mempty
      match Bool
    toplevel [Term]
    ts (DoneDT Set a
    t) = Set a -> QueryResult a
    forall a. Set a -> QueryResult a
    setResult Set a
    t QueryResult a -> TCM () -> TCM (QueryResult a)
    forall a b. a -> TCMT IO b -> TCMT IO a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ do
        String -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.instance.discrim.lookup" Int
    99 (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
    "done" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Term] -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => [Term] -> m Doc
    prettyTCM [Term]
    ts
          , TCMT IO Doc
    "  →" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Set a -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Set a -> m Doc
    prettyTCM Set a
    t
          ]

      match Bool
    toplevel [Term]
    ts tree :: DiscrimTree a
    tree@(CaseDT Int
    i Map Key (DiscrimTree a)
    branches DiscrimTree a
    rest) | ([Term]
    sp0, Term
    t:[Term]
    sp1) <- Int -> [Term] -> ([Term], [Term])
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    i [Term]
    ts = do
        let
          ([Term]
    sp0, Term
    t:[Term]
    sp1) = Int -> [Term] -> ([Term], [Term])
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    i [Term]
    ts
          visit :: Key -> [Term] -> TCM (QueryResult a)
    visit Key
    k [Term]
    sp' = case Key -> Map Key (DiscrimTree a) -> Maybe (DiscrimTree a)
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Key
    k Map Key (DiscrimTree a)
    branches of
            Just DiscrimTree a
    m  -> Bool -> [Term] -> DiscrimTree a -> TCM (QueryResult a)
    match Bool
    False [Term]
    sp' DiscrimTree a
    m
            Maybe (DiscrimTree a)
    Nothing -> QueryResult a -> TCM (QueryResult a)
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure QueryResult a
    forall a. Monoid a => a
    mempty

        Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless Bool
    toplevel (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ String -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.instance.discrim.lookup" Int
    99 (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
    "match" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Term] -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => [Term] -> m Doc
    prettyTCM [Term]
    sp0 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 a. Semigroup a => a -> a -> a
    <> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    t TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall a. Semigroup a => a -> a -> a
    <> TCMT IO Doc
    "»") TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Term] -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => [Term] -> m Doc
    prettyTCM [Term]
    sp1
          , DiscrimTree a -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => DiscrimTree a -> m Doc
    prettyTCM DiscrimTree a
    tree
          ]

        -- TODO (Amy, 2024-02-12): Could use reduceB in splitTermKey, and
        -- the blocker here, to suspend instances more precisely when there
        -- is an ambiguity.
        Bool -> TCM (Key, [Term], Blocker) -> TCM (Key, [Term], Blocker)
    forall a. Bool -> TCM a -> TCM a
    ignoreAbstractMaybe Bool
    toplevel (Term -> TCM (Key, [Term], Blocker)
    split Term
    t) TCM (Key, [Term], Blocker)
    -> ((Key, [Term], Blocker) -> TCM (QueryResult a))
    -> TCM (QueryResult a)
    forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
          (Key
    FlexK, [Term]
    args, Blocker
    blocker) -> do

            String -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.instance.discrim.lookup" Int
    99 (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
    "flexible term was forced"
              , TCMT IO Doc
    "t:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (Term -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty (Term -> TCMT IO Doc) -> TCMT IO Term -> TCMT IO Doc
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Term -> TCMT IO Term
    forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
    instantiate Term
    t)
              , TCMT IO Doc
    "will explore" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Int -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty (Map Key (DiscrimTree a) -> Int
    forall a. Map Key a -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length Map Key (DiscrimTree a)
    branches Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "branches"
              ]
            Term -> TCM ()
    tickExplore Term
    t

            -- If we have a "flexible head" at this position then instance
            -- search *at this point* degenerates to looking for all
            -- possible matches.
            --
            -- In any nested CaseDTs, however, it's possible for us to
            -- recover and go back to productively matching. Consider:
            --
            --    instance
            --      xa : X T1 A
            --      xb : X T2 B
            --
            --    ⊢ X ?0 A
            --
            -- Since ?0 is way too flabby to narrow which of T1 or T2 should
            -- be taken, we take both. But then we match A against A and B:
            -- this query will only return {xa}.

            branches <- [Term]
    -> [Term]
    -> [Term]
    -> [(Key, DiscrimTree a)]
    -> TCM (QueryResult a)
    explore [Term]
    sp0 [Term]
    sp1 [Term]
    args ([(Key, DiscrimTree a)] -> TCM (QueryResult a))
    -> [(Key, DiscrimTree a)] -> TCM (QueryResult a)
    forall a b. (a -> b) -> a -> b
    $ Map Key (DiscrimTree a) -> [(Key, DiscrimTree a)]
    forall k a. Map k a -> [(k, a)]
    Map.toList Map Key (DiscrimTree a)
    branches
            rest <- match False ts rest

            pure $! rest <> branches <> blockerResult blocker

          (Key
    k, [Term]
    args, Blocker
    blocker) -> do
            let sp' :: [Term]
    sp' = [Term]
    sp0 [Term] -> [Term] -> [Term]
    forall a. [a] -> [a] -> [a]
    ++ [Term]
    args [Term] -> [Term] -> [Term]
    forall a. [a] -> [a] -> [a]
    ++ [Term]
    sp1

            -- Actually take the branch corresponding to our rigid head.
            branch <- Key -> [Term] -> TCM (QueryResult a)
    visit Key
    k [Term]
    sp'

            -- When exploring the rest of the tree, the value we cased on
            -- has to be put back in the tree. mergeDT does not perform
            -- commuting conversions to ensure that variables aren't
            -- repeatedly cased on.
            rest <- match False ts rest

            pure $! rest <> branch

      match Bool
    _ [Term]
    ts tree :: DiscrimTree a
    tree@(CaseDT Int
    i Map Key (DiscrimTree a)
    _ DiscrimTree a
    rest) = do
        String -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.instance.discrim.lookup" Int
    99 (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
    "IMPOSSIBLE match" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Term] -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => [Term] -> m Doc
    prettyTCM [Term]
    ts
          , DiscrimTree a -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => DiscrimTree a -> m Doc
    prettyTCM DiscrimTree a
    tree
          ]
        -- This really is impossible: since each branch is annotated with
        -- its arity, we only take branches corresponding to neutrals which
        -- exploded into enough arguments.
        TCM (QueryResult a)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Smart constructor for a leaf node.
    doneDT :: Set.Set a -> DiscrimTree a
    doneDT :: forall a. Set a -> DiscrimTree a
    doneDT Set a
    s | Set a -> Bool
    forall a. Set a -> Bool
    Set.null Set a
    s = DiscrimTree a
    forall a. DiscrimTree a
    EmptyDT
    doneDT Set a
    s = Set a -> DiscrimTree a
    forall a. Set a -> DiscrimTree a
    DoneDT Set a
    s

    -- | Remove a set of values from the discrimination tree. The tree is
    -- rebuilt so that cases with no leaves are removed.
    deleteFromDT :: Ord a => Set.Set a -> DiscrimTree a -> DiscrimTree a
    deleteFromDT :: forall a. Ord a => Set a -> DiscrimTree a -> DiscrimTree a
    deleteFromDT Set a
    gone = \case
      DiscrimTree a
    EmptyDT -> DiscrimTree a
    forall a. DiscrimTree a
    EmptyDT
      DoneDT Set a
    s -> Set a -> DiscrimTree a
    forall a. Set a -> DiscrimTree a
    doneDT (Set a -> DiscrimTree a) -> Set a -> DiscrimTree a
    forall a b. (a -> b) -> a -> b
    $! Set a -> Set a -> Set a
    forall a. Ord a => Set a -> Set a -> Set a
    Set.difference Set a
    s Set a
    gone
      CaseDT Int
    i Map Key (DiscrimTree a)
    s DiscrimTree a
    k ->
        let
          del :: DiscrimTree a -> Maybe (DiscrimTree a)
    del DiscrimTree a
    x = case Set a -> DiscrimTree a -> DiscrimTree a
    forall a. Ord a => Set a -> DiscrimTree a -> DiscrimTree a
    deleteFromDT Set a
    gone DiscrimTree a
    x of
            DiscrimTree a
    EmptyDT -> Maybe (DiscrimTree a)
    forall a. Maybe a
    Nothing
            DiscrimTree a
    dt'     -> DiscrimTree a -> Maybe (DiscrimTree a)
    forall a. a -> Maybe a
    Just DiscrimTree a
    dt'

          s' :: Map Key (DiscrimTree a)
    s' = (DiscrimTree a -> Maybe (DiscrimTree a))
    -> Map Key (DiscrimTree a) -> Map Key (DiscrimTree a)
    forall a b k. (a -> Maybe b) -> Map k a -> Map k b
    Map.mapMaybe DiscrimTree a -> Maybe (DiscrimTree a)
    del Map Key (DiscrimTree a)
    s
          k' :: DiscrimTree a
    k' = Set a -> DiscrimTree a -> DiscrimTree a
    forall a. Ord a => Set a -> DiscrimTree a -> DiscrimTree a
    deleteFromDT Set a
    gone DiscrimTree a
    k
        in if | Map Key (DiscrimTree a) -> Bool
    forall k a. Map k a -> Bool
    Map.null Map Key (DiscrimTree a)
    s' -> DiscrimTree a
    k'
              | Bool
    otherwise   -> Int -> Map Key (DiscrimTree a) -> DiscrimTree a -> DiscrimTree a
    forall a.
    Int -> Map Key (DiscrimTree a) -> DiscrimTree a -> DiscrimTree a
    CaseDT Int
    i Map Key (DiscrimTree a)
    s' DiscrimTree a
    k'