Projection-likeness and instance arguments

[plt-amy]

The following reproducer was minimized from a macro that generates a big expression containing hlevel 2; We'd like to use this macro with elaborate-and-give, since it fills out a definition skeleton and allows the user to fill in any gaps by themselves.

open import Agda.Primitive renaming (Set to Type)
open import Agda.Builtin.Nat
open import Agda.Builtin.Cubical.Path

is-hlevel : ∀ {ℓ} → Type ℓ → Nat → Type ℓ
is-hlevel A 0 = (x y : A) → x ≡ y
is-hlevel A (suc n) = (x y : A) → is-hlevel (x ≡ y) n

record H-Level {ℓ} (T : Type ℓ) (n : Nat) : Type ℓ where
  constructor hlevel-instance
  field
    has-hlevel : is-hlevel T n

hlevel : ∀ {ℓ} {T : Type ℓ} n ⦃ x : H-Level T n ⦄ → is-hlevel T n
hlevel n ⦃ x ⦄ = H-Level.has-hlevel x

-- vvv need a confounding instance otherwise Agda will eagerly commit to hl
postulate instance H-Level-⊤ : ∀ {n} → H-Level Nat n

private module _ {ℓ} {A : Type ℓ} ⦃ hl : H-Level A 2 ⦄ where
  p : is-hlevel A 2
  p = {! hlevel 2 !}

Try doing elaborate-and-give for hlevel 2. What you get is hlevel _: the hlevel function is projection-like for the x argument, so Agda erases the 2, since it's reconstructible from x. But it's not reconstructible after printing: if you write just p = hlevel _, or reload after doing elaborate-and-give on the interaction point, Agda does not solve the instance constraint.

I'm not too familiar with the projection-likeness analysis, but I'm suspicious of whether an instance argument whose type depends on a visible argument in the same telescope should be considered "principal". Because of that unfamiliarity, the fix I implemented doesn't change the analysis: I reconstruct arguments in elaborate_and_give and I added a NOT_PROJECTION_LIKE pragma.

[jespercockx]

I think the projection-likeness is supposed to be purely an optimization so it should not matter what the visibility of the arguments is (visible or hidden or instance). However I agree it's a good idea to reconstruct these arguments then for interactive commands. In general pretty-printing is not always very good at guessing which arguments can be inferred or not.

[andreasabel]

@plt-amy Is this planned for 2.6.3? (Please assign a milestone: 2.6.3 or 2.6.4.)