{-# OPTIONS -vtactic.hlevel:20 -vtc.def:10 #-}
open import 1Lab.Reflection.Record
open import 1Lab.Equiv.Embedding
open import 1Lab.HLevel.Retracts
open import 1Lab.HLevel.Universe
open import 1Lab.Reflection
open import 1Lab.Type.Sigma
open import 1Lab.HLevel
open import 1Lab.Equiv
open import 1Lab.Path
open import 1Lab.Type

open import Data.Bool
open import Data.List

open import Meta.Foldable

open import Prim.Data.Nat

module 1Lab.Reflection.HLevel where

{-
Tactic for generating readable h-level proofs automatically. Contains an
essential reimplementation of the instance search mechanism, with
support for arbitrary level offsets (`level-minus) and searching under
binders (`search-under). Ambiguity is explicitly supported: the first
goal for which we can complete a proof tree is the one we go with.

The tactic works in a naïve way, trying h-level lemmas until one
succeeds. There are three ways of making progress: Using a *projection
hint*, using a *decomposition hint*, or by falling back to instance
selection. The instance selection fallback is self-explanatory.

Projection hints handle the situation is-hlevel (X .p) n, where X
inhabits a record that contains evidence of its hlevel. If there is a
projection hint with `underlying-type == p`, then we use `has-level
(get-argument (X .p))` as the solution. Being a base case, projection
hints also handle raising h-levels: If `get-level (X .p) < n`, we solve
by raising `has-level ...` the appropriate amount.

Decomposition hints are slightly more interesting. Decomposition hints
apply to a type, say P, and instruct the tactic on how to build an
application of type (is-hlevel P n). The way this application is built
is customizable.

Finding rules
-------------

Rules are found using instance search, specifically for the
'hlevel-decomposition' and 'hlevel-projection' types. The
hlevel-projection type is flat, so the runtime of
projection-decomposition is *linear in the number of possible
projections*.

The hlevel-decomposition type is more interesting, since it is indexed
by the type that it can decompose. That way, we can use Agda's own
instance selection mechanism to narrow down to relevant decompositions.

Nondeterminism
--------------

In case more than one projection and/or decomposition hint is possible,
they will all be tried in order. This allows the tactic to generate
sensible-looking code, by trying simpler decompositions first. As an
example, the non-dependent lemmas for → and × will be tried before those
for Π and Σ, just like a human would.
-}

-- | Specifies how an argument should be filled in during elaboration of
-- an h-level lemma.
data Arg-spec : Type where
  `level-minus  : (n : Nat) → Arg-spec
  -- ^ Insert the level we're solving for minus the given offset (note
  -- that this is the wonky subtraction operation, "monus") at this
  -- argument position

  `search-under : (n : Nat) → Arg-spec
  -- ^ Recursively search for an h-level witness, under @n@ visible
  -- lambdas. This is suitable for lemmas of type
  -- (∀ x y z → is-hlevel ...) → is-hlevel ...

  `term         : Term → Arg-spec
  -- ^ Insert a literal term at this argument position. No search will be
  -- performed if this is a meta, so it must be solved from the context in
  -- which the lemma is used.

-- Common patterns: Keep the level, search in the current scope.
pattern `search = `search-under 
pattern `level = `level-minus 
pattern `meta = `term unknown

-- | A specification for how to decompose the type @T@ into
-- sub-components, to establish an h-level result.
data hlevel-decomposition {ℓ} (T : Type ℓ) : Type where
  decomp
    : (h-level-lemma : Name) (arguments : List Arg-spec)
    → hlevel-decomposition T
  -- To prove that T has a given h-level, we can invoke the
  -- @h-level-lemma@ with the specified @arguments@.

-- | How to decompose an application of a record selector into something
-- which might have an h-level.
record hlevel-projection (proj : Name) : Type where
  field
    has-level : Name
    -- ^ The name of the h-level lemma. It must be sufficient to apply
    -- this name to the argument (see get-argument below); arg specs are
    -- not supported.
    get-level : Term → TC Term
    -- ^ Given an application of underlying-type, what h-level does this
    -- type have? Necessary for computing lifts.
    get-argument : List (Arg Term) → TC Term
    -- ^ Extract the argument out from under the application.
{-
Using projections
-----------------

Projection decomposition happens as follows; suppose we have some
neutral

  n = def (quote X) as

in order, every 'hlevel-projection' instance definition will be tried;
Let us call a generic instance I. If I.underlying-type == X, then we'll
use this instance, otherwise, we fail (i.e. backtrack and try another
projection).

To use this instance, the get-level and get-argument functions are
involved; get-argument must take 'as' and return some representative
sub-expression e. get-level will receive e's inferred type and must
return the h-level of the type n. Finally, we return

  I.has-level (get-argument e),

possibly wrapped in (k - get-level (get-argument e)) applications of
is-hlevel-suc.
-}

open hlevel-projection
private
  -- Throw an empty type error to try another alternative, stating the
  -- purpose of backtracking for debugging:
  backtrack : ∀ {ℓ} {A : Type ℓ} → List ErrorPart → TC A
  backtrack note = do
    debugPrint "tactic.hlevel"  $ "Backtracking search... " ∷ note
    typeError $ "Search hit a dead-end: " ∷ note

  -- A list of names which we should not reduce while trying to invert
  -- an application of is-hlevel/is-prop/is-set into an 'underlying
  -- type' and level arguments.
  hlevel-types : List Name
  hlevel-types = quote is-hlevel ∷ quote is-prop ∷ quote is-set ∷ quote is-groupoid ∷ []

  pattern nat-lit n =
    def (quote Number.fromNat) (_ ∷ _ ∷ _ ∷ lit (nat n) v∷ _)

  -- Decompose an application of is-hlevel and/or one of the other
  -- 'hlevel-types' into its constituent parts. Invariant:
  --
  --    decompose-is-hlevel' t = (a , n) ⊢ t = is-hlevel a n
  decompose-is-hlevel' : Term → TC (Term × Term)

  -- Infer the type of the given term, and decompose it according to
  -- decompose-is-hlevel'.
  decompose-is-hlevel : Term → TC (Term × Term)
  decompose-is-hlevel goal = do
    ty ← withReduceDefs (false , hlevel-types) $ infer-type goal >>= reduce
    decompose-is-hlevel' ty

  decompose-is-hlevel' ty = do
    def (quote is-hlevel) (_ ∷ ty v∷ lv v∷ []) ← pure ty
      where
        -- Handle the ones with special names:
        def (quote is-groupoid) (_ ∷ ty v∷ []) → do
          ty ← wait-just-a-bit ty
          pure (ty , lit (nat ))

        def (quote is-set) (_ ∷ ty v∷ []) → do
          ty ← wait-just-a-bit ty
          pure (ty , lit (nat ))

        def (quote is-prop) (_ ∷ ty v∷ []) → do
          ty ← wait-just-a-bit ty
          pure (ty , lit (nat ))

        def (quote is-contr) (_ ∷ ty v∷ []) → do
          ty ← wait-just-a-bit ty
          pure (ty , lit (nat ))

        _ → backtrack "Goal type isn't is-hlevel"

    -- To support having bare hlevel! in the source file, we need to
    -- block decomposition on having a rigid-ish type at the
    -- top-level. Otherwise the first hint that matches will get
    -- matched endlessly until we run out of fuel!
    ty ← wait-just-a-bit ty
    lv ← wait-just-a-bit lv
    pure (ty , lv)

  -- Wait for the "principal argument" of a term, i.e. the (principal
  -- argument of) the first visible argument in the spine of a
  -- definition.
  wait-principal-arg : Term → TC ⊤
  wait-principal-arg topl = go topl where
    go : Term → TC ⊤
    go* : List (Arg Term) → TC ⊤

    go mv@(meta m _) = do
      debugPrint "tactic.hlevel" 
        [ "wait-principal-arg: blocking on meta " , termErr mv , " in principal arguments of\n  "
        , termErr topl
        ]
      block-on-meta m
    go (def d ds) = go* ds
    go t          = pure tt

    go* (arg (arginfo visible _) t ∷ as) = go t
    go* (_ ∷ as)                         = go* as
    go* []                               = pure tt

{-
Lifting n-Types
---------------

The n-types are the leaves of the hlevel solving process, so they're
pretty much our only opportunity to adjust levels in a big way. Suppose
you have

  T = def (quote X) as

with
  get-level (get-argument T) = n
  w : is-hlevel T n

but what you want is a witness of is-hlevel T (k + n), where k is some
numeral? Well, the solution is obvious: we can compute k - n and lift
T's witness (k - n) levels. Right?

No: we're dealing with potential open naturals, so we have to be careful
about performing ‘symbolic’ subtractions. The way we do this is with,
essentially, a loop: If w doesn't work, then try

  is-hlevel-suc n w : is-hlevel T (suc n)

until you reach a sucᵏ n = k + n. Actually, slightly more efficient, we
keep around a counter k' for the number of tries, and transfer successors
from the wanted level (k + n) until is-hlevel-+ n (sucᵏ' n) w works.
-}
  lift-sol : Term → Term → Nat → Term
  lift-sol tm _  = tm
  lift-sol tm l1 l = def (quote is-hlevel-+) (l1 v∷ lit (nat l) v∷ tm v∷ [])

  pred-term : Term → Maybe Term
  pred-term (con (quote suc) (x v∷ [])) = just x
  pred-term (lit (nat n)) with n
  ... | suc k = just (lit (nat k))
  ... | _ = nothing
  pred-term _ = nothing

  {-# TERMINATING #-}
  lifting-loop : Nat → Term → Term → Term → Term → TC ⊤
  lifting-loop it solution goal l1 l2 =
    let's-hope <|> do
      (just l2') ← pred-term <$> normalise l2 where
        nothing → backtrack "Lifting loop reached its end with no success"
      lifting-loop (suc it) solution goal l1 l2'
    where
      let's-hope : TC ⊤
      let's-hope = do
        debugPrint "tactic.hlevel"  $ "Lifting loop: Trying " ∷ termErr (lift-sol solution l1 it) ∷ " for level " ∷ termErr l2 ∷ []
        unify goal (lift-sol solution l1 it)

  -- Projection decomposition.
  treat-as-n-type : ∀ {n} → hlevel-projection n → Term → TC ⊤
  treat-as-n-type projection goal = do
    -- First we must be looking at a goal which is of the type is-hlevel
    -- A n. We'll need both n and A.
    (ty , wanted-level) ← decompose-is-hlevel goal
    debugPrint "tactic.hlevel"  $
      "Attempting to treat as " ∷ termErr wanted-level ∷ "-Type: " ∷ termErr ty ∷ []
    ty ← reduce ty

    -- Reduce the type to whnf and check whether the outermost term
    -- constructor is an application of the projection we're looking
    -- for.
    def namen args ← pure ⦃ Idiom-TC ⦄ ty
      where what → backtrack $ "Thing isn't an application, it is " ∷ termErr what ∷ []

    it ← projection .get-argument args

    -- And compute the level of the projected thing, in addition to a
    -- numeral form of the wanted level.
    actual-level ← infer-type it >>= projection .get-level

    debugPrint "tactic.hlevel"  $
      "... but it's actually a(n) " ∷ termErr actual-level ∷ "-Type" ∷ []

    lv ← normalise wanted-level
    lv' ← normalise actual-level
    lifting-loop  (def (projection .has-level) (it v∷ [])) goal lv' lv

    commitTC

  -- Fall back to Agda's instance search mechanism. This isn't as
  -- straightforward as just using the 'hlevel' function for a couple of
  -- reasons.
  use-instance-search : Bool → Term → TC ⊤
  use-instance-search has-alts goal = run-speculative $ do
    (ty , lv) ← decompose-is-hlevel goal
    (mv , solved) ← new-meta' (def (quote H-Level) (ty v∷ lv v∷ []))
    instances ← get-instances mv

    t ← quoteTC instances
    debugPrint "tactic.hlevel"  $
      "Using instance search for\n" ∷ termErr ty ∷
      "\nFound candidates\n " ∷ termErr t ∷ []

    -- We actually want to manage the instance searching ourselves,
    -- sorta, to avoid getting into situations where the macro has
    -- committed to instance search but Agda will disagree with it.
    let
      go : List Term → TC (⊤ × Bool)
      go = λ where
        -- If there is *exactly* one instance candidate for this goal,
        -- then we can go ahead and solve it. That's because having
        -- exactly one instance means Agda will solve using that
        -- instance!
        (x ∷ []) → do
          -- Note that, since get-instances works by creating a new meta,
          -- we have to commit to the instance ourselves.
          unify solved x
          withReduceDefs (false , quote hlevel ∷ []) $ withReconstructed true $
            unify goal (def (quote hlevel) (lv v∷ []))
          pure (tt , true)

        -- If there are any more alternatives to be tried after this
        -- one, then we fail (backtrack). Otherwise, we discard the TC
        -- state but indicate success: this will cause the meta to be
        -- solved with an interaction point (if using
        -- elaborate-and-give).
        [] → if has-alts
          then backtrack "No possible instances, but have other decompositions to try"
          else pure (tt , false)

        _ → backtrack "Too many possible instances; will not use instance search for this goal"
    go instances

  -- Entry point for calling the tactic.
  search : Bool → Term → Nat → Term → TC ⊤
  -- Give up if we're out of fuel:
  search has-alts _     zero    goal = unify goal unknown

  -- Actual main loop: try using the hints database, try treating the
  -- goal as an n-type, fall back to instance search.
  search has-alts level (suc n) goal =
    use-projections
      <|> use-hints
      <|> use-instance-search has-alts goal
      <|> typeError "Search failed!!"
    where
      open hlevel-projection

      -- Nondeterministically use a projection for establishing the
      -- result. This follows the approach described in [Using
      -- projections].
      use-projections : TC ⊤
      use-projections = do
        def qn _ ← (fst <$> decompose-is-hlevel goal) >>= reduce
          where tm → backtrack $ "Term " ∷ termErr tm ∷ " is not headed by a definition; ignoring projections."

        goalt ← infer-type goal
        debugPrint "tactic.hlevel"  $
          "Will attempt to use projections for goal\n  " ∷ termErr goalt ∷ []

        (solved , instances) ← run-speculative $ do
          (mv , solved) ← new-meta' (def (quote hlevel-projection) (lit (name qn) v∷ []))

          -- If there are some hints, then great, otherwise we discard
          -- the TC state.
          (x ∷ xs) ← get-instances mv
            where [] → pure ((unknown , []) , false)

          pure ((solved , x ∷ xs) , true)

        nondet (eff List) instances λ a → do
          projection ← unquoteTC {A = hlevel-projection qn} a
          ty ← withReduceDefs (false , hlevel-types) (infer-type goal >>= reduce)
          debugPrint "tactic.hlevel"  $
            "Outer type: " ∷ termErr ty ∷ []
          treat-as-n-type projection goal >> unify solved a

      -- Get rid of any invisible binders that lead the term.
      remove-invisible : Term → Term → TC Term
      remove-invisible
        (lam _ (abs _ t))
        (pi (arg (arginfo invisible _) _) (abs _ ret))
        = remove-invisible t ret
      remove-invisible inner _ = pure inner

      -- Search using decompositions involves manipulating the scope,
      -- which is why it's spread over so many functions, and even then,
      -- some are too big.

      -- Wrap the given term in a series of visible lambdas.
      wrap-lams : Nat → Term → Term
      wrap-lams zero r = r
      wrap-lams (suc x) r = lam visible $ abs "a" $ wrap-lams x r

      -- Compute a continuation which extends the context by n visible
      -- variables, all typed 'unknown'.
      extend-n : ∀ {ℓ} → Nat → TC ((A : Type ℓ) → TC A → TC A)
      extend-n zero = pure λ _ x → x
      extend-n (suc n) = do
        rest ← extend-n n
        lift mv ← rest (Lift _ Term) $ lift <$> new-meta unknown
        let domain = arg (arginfo visible (modality relevant quantity-ω)) mv
        pure λ a k → rest a $ extend-context "a" domain $ k

      -- Given a list of argument specs, actually unify the goal with
      -- the solution of decomposition, and call a continuation to
      -- perform any outstanding searches.
      gen-args
        : Bool              -- ^ Are there any alternatives after this one?
        → Term              -- ^ What level are we searching for?

        → Name              -- ^ Name of the lemma,
        → List Arg-spec     -- ^ and the arguments we should invent.

        → List (Arg Term)
        -- ^ Accumulator: computed arguments (criminally, in reverse
        -- order)
        → TC ⊤
          -- ^ Accumulator/continuation: what do we need to do after
          -- unifying the goal with the lemma?. This is both
          -- continuation (it can be used to run something after the
          -- arguments are built) and accumulator (searching recursively
          -- is done last).
        → TC ⊤              -- ^ Returns nada
      gen-args has-alts level defn [] accum cont = do
        -- If we have no arguments to generate, then we can go ahead and
        -- use the accumulator as-is.
        unify goal (def defn (reverse accum))
        debugPrint "tactic.hlevel"  $
          "Committed to solution: " ∷ termErr (def defn (reverse accum)) ∷ []
        cont

      gen-args has-alts level defn (x ∷ args) accum cont with x
      -- If we got asked for the level without an adjustment (i.e. monus
      -- by zero), then we may as well not bother *trying* to adjust it.
      -- Saves a bit of computation.
      ... | `level-minus  = gen-args has-alts level defn args (level v∷ accum) cont
      -- If we have to insert the level minus some offset, then we need
      -- to do the computation:
      ... | `level-minus n@(suc _) =
        do
          level ← normalise level
          debugPrint "tactic.hlevel"  $
            "Hint demands offset, performing symbolic monus, subtracting from\n  " ∷ termErr level ∷ []
          level'' ← monus level n
          -- Reduce otherwise we get Number.fromNat as the term
          gen-args has-alts level defn args (level'' v∷ accum) cont
        where
          -- A 'symbolic' monus function. If we're looking at an actual
          -- number, then we can just do the computation in TC, but
          -- otherwise we have to reimplement the builtin subtraction,
          -- where the minuend is a *term* rather than a number. In
          -- addition to being a bad operation (monus, grr), it's
          -- *partial*. We can end up backtracking while subtracting.
          monus : Term → Nat → TC Term
          monus (lit (nat n)) k = pure $ lit (nat (n - k))
          monus tm zero = pure tm
          monus thezero@(con (quote zero) []) (suc it) = pure thezero
          monus (con (quote suc) (x v∷ [])) (suc it) = do
            x ← reduce x
            monus x it
          monus tm (suc it) = do
            debugPrint "tactic.hlevel"  $ "Dunno how to take 1 from " ∷ termErr tm ∷ []
            typeError []

      ... | `term t = gen-args has-alts level defn args (t v∷ accum) cont

      ... | `search-under under = do
        -- To search under some variables, we work in a scope extended
        -- by 'under'-many variables. The metavariable lives in that
        -- scope, so we have to quantify over the variables we
        -- introduced to use it outside, i.e., in the actual (outer)
        -- search problem.
        debugPrint "tactic.hlevel"  $ "Going under " ∷ termErr (lit (nat under)) ∷ []
        gounder ← extend-n under
        mv ← gounder Term $ do
          debugPrint "tactic.hlevel"  $ "In extended context"
          new-meta unknown
        debugPrint "tactic.hlevel"  $ "Metavariable: " ∷ termErr (wrap-lams under mv) ∷ []
        -- After we've put the mv wrapped under some lambdas in the
        -- argument list,
        gen-args has-alts level defn args (wrap-lams under mv v∷ accum) $ do
          -- On our way back up, we do any more searching that needed to
          -- get done, and..
          cont
          -- go back under the new scope to recursively search for
          -- levels.
          gounder ⊤ $ search has-alts unknown n mv

      -- Try all the candidate hints in order. This is a version of
      -- 'nondet' which additionally threads whether we're looking at
      -- last alternative.
      use-decomp-hints : (Term × Term) → Term → List Term → TC (⊤ × Bool)
      use-decomp-hints (goal-ty , lv) solved (c1 ∷ cs) = do
        ty ← infer-type c1
        c1' ← reduce c1
        (remove-invisible c1' ty >>= λ where

          -- If we have an actual decomp constructor, then we can try
          -- using its argument specification to construct a little
          -- h-level lemma
          (con (quote decomp) (_ ∷ _ ∷ nm v∷ argspec v∷ [])) → do
            debugPrint "tactic.hlevel"  $
              "Using " ∷ termErr nm ∷ " decomposition for:\n  "
              ∷ termErr (def (quote is-hlevel) (goal-ty v∷ lv v∷ [])) ∷ []

            nm' ← unquoteTC nm
            argsp ← unquoteTC argspec
            -- Generate the argument spine, and discard the instance
            -- search meta.
            gen-args (not (length cs == )) lv nm' argsp [] (pure tt)
            unify solved c1

            pure (tt , true)

          -- It's possible that this particular hint was a bust, i.e.
          -- because someone wasn't being careful with what
          -- hlevel-decomposition instances they've defined. That's no
          -- matter: we can just ignore it.
          _ → backtrack "Non-canonical hint")
          -- If we didn't manage to get the hint to work, for any
          -- reason, try again with the rest of the hints.
          <|> use-decomp-hints (goal-ty , lv) solved cs

      use-decomp-hints (goal-ty , _) _ [] =
        backtrack $ "Ran out of decomposition hints for " ∷ termErr goal-ty ∷ []

      -- Using the hints involving querying Agda for potential
      -- instances, then trying each in order.
      use-hints : TC ⊤
      use-hints = run-speculative $ do
        (ty , lv) ← decompose-is-hlevel goal

        -- We have to block on any metavariable here which is blocking
        -- head-normalisation of the goal type. Unfortunately the
        -- reflection interface does not let us reduce with a blocker.
        --
        -- The reason is twofold:
        --
        --    (a) if the type is a bare meta, the tactic may go into a tailspin.
        --
        --    (b) if the type a projection blocked on a meta,
        --        e.g. .Pathᵉ (_123 ...) ...,
        --        then we may commit to an incorrect solution too early,
        --        preventing the extensionality tactic from doing *its*
        --        job.
        wait-principal-arg ty

        -- Create a meta of type hlevel-decomposition to find any possible hints..
        (mv , solved) ← new-meta' (def (quote hlevel-decomposition) (ty v∷ []))
        instances ← get-instances mv

        t ← quoteTC instances
        debugPrint "tactic.hlevel"  $
          "Finding decompositions for\n" ∷
          termErr ty ∷
          "\nFound candidates\n " ∷
          termErr t ∷ []

        -- And try using the hints.
        use-decomp-hints (ty , lv) solved instances

  -- At the top-level, our goal doesn't need to have literally the type
  -- is-hlevel A n. It can be under any number of Πs, both implicit and
  -- explicit. This means that a goal like (∀ x → is-hlevel T n) can be
  -- solved using just hlevel!, rather than λ _ → hlevel!. Of course,
  -- the effect is the same.
  decompose-is-hlevel-top
    : ∀ {ℓ} {A : Type ℓ}
    → Term → TC (Term × Term × (TC A → TC A) × (Term → Term))
  decompose-is-hlevel-top goal =
    do
      ty ← withReduceDefs (false , hlevel-types) $
        infer-type goal >>= reduce >>= wait-just-a-bit
      go ty
    where
      go : Term → TC _
      go (pi (arg as at) (abs vn cd)) = do
        (inner , hlevel , enter , leave) ← go cd
        pure $ inner , hlevel , extend-context vn (arg as at) ∘ enter , λ t → lam (ArgInfo.arg-vis as) (abs vn (leave t))
      go tm = do
        (inner , hlevel) ← decompose-is-hlevel' tm
        pure $ inner , hlevel , (λ x → x) , (λ x → x)

-- This is public so it's usable in tactic attributes. It decomposes the
-- top-level goal type and enters the search loop.
hlevel-tactic-worker : Term → TC ⊤
hlevel-tactic-worker goal = do
  ty ← withReduceDefs (false , hlevel-types) $ infer-type goal >>= reduce
  (ty , lv , enter , leave) ← decompose-is-hlevel-top goal <|>
    typeError
      ( "hlevel tactic: goal type is not of the form ``is-hlevel A n'':\n"
      ∷ termErr ty
      ∷ [])

  -- 10 units of fuel isn't too many but it's enough for any realistic
  -- use-case. Note the scope nonsense: we have to 'enter' to get under
  -- the Πs (extend the scope with their argument types), then 'leave'
  -- (wrap in lambdas) to get back out.
  solved ← enter $ do
    goal' ← new-meta (def (quote is-hlevel) (ty v∷ lv v∷ []))
    search false lv  goal'
    pure goal'
  unify goal (leave solved)

-- Entry points to the macro
----------------------------
macro hlevel! = hlevel-tactic-worker

-- In addition to using the macro as a.. well, macro, it can be used as
-- a tactic argument, to replace instance search by the more powerful
-- decomposition-projection mechanism of the tactic. We provide only
-- some of the most common helpers:
el! : ∀ {ℓ} (A : Type ℓ) {n} {@(tactic hlevel-tactic-worker) hl : is-hlevel A n} → n-Type ℓ n
∣ el! A {hl = hl} ∣ = A
el! A {hl = hl} .is-tr = hl

prop-ext!
  : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}
    {@(tactic hlevel-tactic-worker) aprop : is-hlevel A }
    {@(tactic hlevel-tactic-worker) bprop : is-hlevel B }
  → (A → B) → (B → A)
  → A ≃ B
prop-ext! {aprop = aprop} {bprop = bprop} = prop-ext aprop bprop

Σ-prop-path!
  : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'}
  → {@(tactic hlevel-tactic-worker) bxprop : ∀ x → is-hlevel (B x) }
  → {x y : Σ A B}
  → x .fst ≡ y .fst
  → x ≡ y
Σ-prop-path! {bxprop = bxprop} = Σ-prop-path bxprop

prop!
  : ∀ {ℓ} {A : I → Type ℓ} {@(tactic hlevel-tactic-worker) aip : is-hlevel (A i0) }
  → {x : A i0} {y : A i1}
  → PathP (λ i → A i) x y
prop! {A = A} {aip = aip} {x} {y} =
  is-prop→pathp (λ i → coe0→i (λ j → is-prop (A j)) i aip) x y

injective→is-embedding!
  : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}
      {@(tactic hlevel-tactic-worker) bset : is-set B}
  → ∀ {f : A → B}
  → injective f
  → is-embedding f
injective→is-embedding! {bset = bset} {f} inj = injective→is-embedding bset f inj

open hlevel-projection

-- Hint database bootstrap
--------------------------
-- This instance block contains most of the decompositions we have
-- defined in the dependencies of this module.

instance
  decomp-lift : ∀ {ℓ ℓ'} {T : Type ℓ} → hlevel-decomposition (Lift ℓ' T)
  decomp-lift = decomp (quote Lift-is-hlevel) (`level ∷ `search ∷ [])

  -- h-level types themselves are propositions. These instances should be tried
  -- before Π types.

  decomp-is-prop : ∀ {ℓ} {A : Type ℓ} → hlevel-decomposition (is-prop A)
  decomp-is-prop = decomp (quote is-hlevel-is-hlevel-suc) (`level-minus  ∷ `term (lit (nat )) ∷ [])

  decomp-is-set : ∀ {ℓ} {A : Type ℓ} → hlevel-decomposition (is-set A)
  decomp-is-set = decomp (quote is-hlevel-is-hlevel-suc) (`level-minus  ∷ `term (lit (nat )) ∷ [])

  decomp-is-groupoid : ∀ {ℓ} {A : Type ℓ} → hlevel-decomposition (is-groupoid A)
  decomp-is-groupoid = decomp (quote is-hlevel-is-hlevel-suc) (`level-minus  ∷ `term (lit (nat )) ∷ [])

  {-
  Since `is-prop A` starts with a Π, the decomp-piⁿ instances below could "bite" into
  it and make decomp-is-prop inapplicable. To avoid this, we handle those situations explicitly:
  -}

  decomp-pi²-is-prop : ∀ {ℓa ℓb ℓc} {A : Type ℓa} {B : A → Type ℓb} {C : ∀ a (b : B a) → Type ℓc}
                     → hlevel-decomposition (∀ a b → is-prop (C a b))
  decomp-pi²-is-prop = decomp (quote Π-is-hlevel²) (`level ∷ `search-under  ∷ [])

  decomp-pi-is-prop : ∀ {ℓa ℓb} {A : Type ℓa} {B : A → Type ℓb}
                    → hlevel-decomposition (∀ a → is-prop (B a))
  decomp-pi-is-prop = decomp (quote Π-is-hlevel) (`level ∷ `search-under  ∷ [])

  -- -- Non-dependent Π and Σ for readability first:

  -- decomp-fun = decomp (quote fun-is-hlevel) (`level ∷ `search ∷ [])

  -- decomp-prod : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → hlevel-decomposition (A × B)
  -- decomp-prod = decomp (quote ×-is-hlevel) (`level ∷ `search ∷ `search ∷ [])

  -- Dependent type formers:

  decomp-pi³
    : ∀ {ℓa ℓb ℓc ℓd} {A : Type ℓa} {B : A → Type ℓb} {C : ∀ x (y : B x) → Type ℓc}
    → {D : ∀ x y (z : C x y) → Type ℓd}
    → hlevel-decomposition (∀ a b c → D a b c)
  decomp-pi³ = decomp (quote Π-is-hlevel³) (`level ∷ `search-under  ∷ [])

  decomp-pi²
    : ∀ {ℓa ℓb ℓc} {A : Type ℓa} {B : A → Type ℓb} {C : ∀ x (y : B x) → Type ℓc}
    → hlevel-decomposition (∀ a b → C a b)
  decomp-pi² = decomp (quote Π-is-hlevel²) (`level ∷ `search-under  ∷ [])

  decomp-pi : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} → hlevel-decomposition (∀ a → B a)
  decomp-pi = decomp (quote Π-is-hlevel) (`level ∷ `search-under  ∷ [])

  decomp-impl-pi : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} → hlevel-decomposition (∀ {a} → B a)
  decomp-impl-pi = decomp (quote Π-is-hlevel') (`level ∷ `search-under  ∷ [])

  decomp-sigma : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} → hlevel-decomposition (Σ A B)
  decomp-sigma = decomp (quote Σ-is-hlevel) (`level ∷ `search ∷ `search-under  ∷ [])

  -- Path decomposition rules we have in scope. Note the use of
  -- nondeterminism: the following three instances both compete for
  -- solving the same goals --- but generally only one will be
  -- applicable. That way we don't have to juggle h-levels quite as
  -- much.
  decomp-path' : ∀ {ℓ} {A : Type ℓ} {a b : A} → hlevel-decomposition (a ≡ b)
  decomp-path' = decomp (quote Path-is-hlevel') (`level ∷ `search ∷ `meta ∷ `meta ∷ [])

  decomp-path : ∀ {ℓ} {A : Type ℓ} {a b : A} → hlevel-decomposition (a ≡ b)
  decomp-path = decomp (quote Path-is-hlevel) (`level ∷ `search ∷ [])

  decomp-univalence : ∀ {ℓ} {A B : Type ℓ} → hlevel-decomposition (A ≡ B)
  decomp-univalence = decomp (quote ≡-is-hlevel) (`level ∷ `search ∷ `search ∷ [] )

  -- This one really ought to work with instance selection only, but
  -- Agda has trouble with the (1 + k + n) level in H-Level-n-Type. The
  -- decomposition here is a bit more flexible.
  decomp-ntype : ∀ {ℓ} {n} → hlevel-decomposition (n-Type ℓ n)
  decomp-ntype = decomp (quote n-Type-is-hlevel) (`level-minus  ∷ [])

  decomp-list : ∀ {ℓ} {A : Type ℓ} → hlevel-decomposition (List A)
  decomp-list = decomp (quote ListPath.List-is-hlevel) (`level-minus  ∷ `search ∷ [])

  hlevel-proj-n-type : hlevel-projection (quote n-Type.∣_∣)
  hlevel-proj-n-type .has-level = quote n-Type.is-tr
  hlevel-proj-n-type .get-level ty = do
    def (quote n-Type) (ell v∷ lv't v∷ []) ← reduce ty
      where _ → backtrack $ "Type of thing isn't n-Type, it is " ∷ termErr ty ∷ []
    normalise lv't
  hlevel-proj-n-type .get-argument (_ ∷ _ ∷ it v∷ []) = pure it
  hlevel-proj-n-type .get-argument _ = typeError []

private
  module _ {ℓ} {A : n-Type ℓ } {B : ∣ A ∣ → n-Type ℓ } where
    -- some-def = ∣ A ∣
    -- _ : is-hlevel (∣ A ∣ → ∣ A ∣ → ∣ A ∣ → ∣ A ∣) 2
    -- _ = hlevel!

    -- _ : is-hlevel (Σ some-def λ x → ∣ B x ∣) 3
    -- _ = hlevel!

    _ : ∀ a → is-hlevel (∣ A ∣ × ∣ A ∣ × (Nat → ∣ B a ∣)) 
    _ = hlevel!

    _ : ∀ a → is-hlevel (∣ A ∣ × ∣ A ∣ × (Nat → ∣ B a ∣)) 
    _ = hlevel!

    _ : is-hlevel ∣ A ∣ 
    _ = hlevel!

    _ : ∀ n → is-hlevel (n-Type ℓ n) (suc n)
    _ = hlevel!

    _ : ∀ n (x : n-Type ℓ n) → is-hlevel ∣ x ∣ ( + n)
    _ = hlevel!

    _ : ∀ {ℓ} {A : Type ℓ} → is-prop ((x : A) → is-prop A)
    _ = hlevel!

    _ : ∀ {ℓ} {A : Type ℓ} → is-prop ((x y : A) → is-prop A)
    _ = hlevel!

    _ : ∀ {ℓ} {A : Type ℓ} → is-groupoid (is-hlevel A )
    _ = hlevel!