Another irrelevant instance search bug

[ncfavier]

While fixing #405, I found another seemingly unrelated bug with irrelevant instance metas: with the current Agda master, the module

open import 1Lab.Type
open import 1Lab.HLevel
open import 1Lab.HLevel.Closure

postulate
  foo : .(is-prop ⊥) → ⊤

bar : ⊤
bar = foo (hlevel 1)

results in the error

/home/n/git/1lab/src/wip/bug.agda:13,12-20
⊥ !=< (x : _T_14) → _S_17 x
when checking that the expression hlevel 1 has type is-prop ⊥

Log with -vtactic:100 -vtc.instance:30

Checking wip.bug (/home/n/git/1lab/src/wip/bug.agda).
The type of the FindInstance constraint isn't known, trying to find it again.
Found instance type head:  Number
no instance field candidates
instance candidates from signature for goal:
  (Number _A_7)
  {Number-Nat} length: 1
blocker:
  _A_7
mutual block:
  {bar}
Postponing possibly recursive instance search.
The type of the FindInstance constraint isn't known, trying to find it again.
Instance type is not yet known. 
Can't figure out target of instance goal. Postponing constraint.
The type of the FindInstance constraint isn't known, trying to find it again.
Found instance type head:  H-Level
no instance field candidates
instance candidates from signature for goal:
  H-Level _T_5 1
  {H-Level-pi, H-Level-⊤, H-Level-⊥, H-Level-pi', H-Level-sigma,
   H-Level-PathP, H-Level-Lift, H-Level-is-contr,
   H-Level-is-equiv} length: 9
blocker:
  any(_T_5, _r_8)
mutual block:
  {bar}
Postponing possibly recursive instance search.
findInstance 2: constraint: _10@13977009405847656758; candidates left: 9
findInstance 3: t = H-Level _T_5 1
{ checkCandidates _10@13977009405847656758
  target: H-Level _T_5 1
  candidates
  - H-Level-pi : {T.ℓ : Level} {T : Type T.ℓ} {ℓ : Level} {n : Nat}
                 {S : T → Type ℓ} ⦃ _ : {x : T} → H-Level (S x) n ⦄ →
                 H-Level ((x : T) → S x) n
  - H-Level-⊤ : {n : Nat} → H-Level ⊤ n
  - H-Level-⊥ : {n : Nat} → H-Level ⊥ (suc n)
  - H-Level-pi' : {T.ℓ : Level} {T : Type T.ℓ} {ℓ : Level} {n : Nat}
                  {S : T → Type ℓ} ⦃ _ : {x : T} → H-Level (S x) n ⦄ →
                  H-Level ({x : T} → S x) n
  - H-Level-sigma : {T.ℓ : Level} {T : Type T.ℓ} {ℓ : Level}
                    {n : Nat} {S : T → Type ℓ} ⦃ _ : H-Level T n ⦄
                    ⦃ _ : {x : T} → H-Level (S x) n ⦄ →
                    H-Level (Σ T S) n
  - H-Level-PathP : {ℓ : Level} {n : Nat}
                    {S : Prim.Interval.I → Type ℓ}
                    ⦃ s : H-Level (S Prim.Interval.i1) (suc n) ⦄
                    {x : S Prim.Interval.i0} {y : S Prim.Interval.i1} →
                    H-Level (Prim.Kan.PathP S x y) n
  - H-Level-Lift : {T.ℓ : Level} {T : Type T.ℓ} {ℓ : Level} {n : Nat}
                   ⦃ s : H-Level T n ⦄ →
                   H-Level (Lift ℓ T) n
  - H-Level-is-contr : {n : Nat} {ℓ : Level} {T : Type ℓ} →
                       H-Level (is-contr T) (suc n)
  - H-Level-is-equiv : {ℓ ℓ' : Level} {A : Type ℓ} {B : Type ℓ'}
                       {f : A → B} {n : Nat} →
                       H-Level (1Lab.Equiv.is-equiv f) (suc n)
{ checkCandidateForMeta _10@13977009405847656758
checkCandidateForMeta
  t    = H-Level _T_5 1
  t'   = {T.ℓ : Level} {T : Type T.ℓ} {ℓ : Level} {n : Nat}
         {S : T → Type ℓ} ⦃ _ : {x : T} → H-Level (S x) n ⦄ →
         H-Level ((x : T) → S x) n
  term = H-Level-pi
instance search: checking H-Level ((x : _T_14) → _S_17 x)
                          _n_16 <= H-Level _T_5 1
instance search: found solution for _x_10: H-Level-pi
candidate H-Level-pi okay for overlap? True
}
{ checkCandidateForMeta _10@13977009405847656758
checkCandidateForMeta
  t    = H-Level _T_5 1
  t'   = {n : Nat} → H-Level ⊤ n
  term = H-Level-⊤
instance search: checking H-Level ⊤ _n_13 <= H-Level _T_5 1
instance search: found solution for _x_10: H-Level-⊤
candidate H-Level-⊤ okay for overlap? True
}
{ checkCandidateForMeta _10@13977009405847656758
checkCandidateForMeta
  t    = H-Level _T_5 1
  t'   = {n : Nat} → H-Level ⊥ (suc n)
  term = H-Level-⊥
instance search: checking H-Level ⊥ (suc _n_13) <= H-Level _T_5 1
instance search: found solution for _x_10: H-Level-⊥
candidate H-Level-⊥ okay for overlap? False
suc _n_13 = 1 : Nat (blocked on _r_8, belongs to problems 9, 12)
}
{ checkCandidateForMeta _10@13977009405847656758
checkCandidateForMeta
  t    = H-Level _T_5 1
  t'   = {T.ℓ : Level} {T : Type T.ℓ} {ℓ : Level} {n : Nat}
         {S : T → Type ℓ} ⦃ _ : {x : T} → H-Level (S x) n ⦄ →
         H-Level ({x : T} → S x) n
  term = H-Level-pi'
instance search: checking H-Level ({x : _T_14} → _S_17 x)
                          _n_16 <= H-Level _T_5 1
instance search: found solution for _x_10: H-Level-pi'
candidate H-Level-pi' okay for overlap? True
}
{ checkCandidateForMeta _10@13977009405847656758
checkCandidateForMeta
  t    = H-Level _T_5 1
  t'   = {T.ℓ : Level} {T : Type T.ℓ} {ℓ : Level} {n : Nat}
         {S : T → Type ℓ} ⦃ _ : H-Level T n ⦄
         ⦃ _ : {x : T} → H-Level (S x) n ⦄ →
         H-Level (Σ T S) n
  term = H-Level-sigma
instance search: checking H-Level (Σ _T_14 _S_17) _n_16 <= H-Level
                                                           _T_5 1
instance search: found solution for _x_10: H-Level-sigma
candidate H-Level-sigma okay for overlap? True
}
{ checkCandidateForMeta _10@13977009405847656758
checkCandidateForMeta
  t    = H-Level _T_5 1
  t'   = {ℓ : Level} {n : Nat} {S : Prim.Interval.I → Type ℓ}
         ⦃ s : H-Level (S Prim.Interval.i1) (suc n) ⦄
         {x : S Prim.Interval.i0} {y : S Prim.Interval.i1} →
         H-Level (Prim.Kan.PathP S x y) n
  term = H-Level-PathP
instance search: checking H-Level
                          (Prim.Kan.PathP _S_15 _x_17 _y_18) _n_14 <= H-Level _T_5 1
instance search: found solution for _x_10: H-Level-PathP
candidate H-Level-PathP okay for overlap? True
}
{ checkCandidateForMeta _10@13977009405847656758
checkCandidateForMeta
  t    = H-Level _T_5 1
  t'   = {T.ℓ : Level} {T : Type T.ℓ} {ℓ : Level} {n : Nat}
         ⦃ s : H-Level T n ⦄ →
         H-Level (Lift ℓ T) n
  term = H-Level-Lift
instance search: checking H-Level (Lift _ℓ_15 _T_14)
                          _n_16 <= H-Level _T_5 1
instance search: found solution for _x_10: H-Level-Lift
candidate H-Level-Lift okay for overlap? True
}
{ checkCandidateForMeta _10@13977009405847656758
checkCandidateForMeta
  t    = H-Level _T_5 1
  t'   = {n : Nat} {ℓ : Level} {T : Type ℓ} →
         H-Level (is-contr T) (suc n)
  term = H-Level-is-contr
instance search: checking H-Level (is-contr _T_15)
                          (suc _n_13) <= H-Level _T_5 1
instance search: found solution for _x_10: H-Level-is-contr
candidate H-Level-is-contr okay for overlap? False
suc _n_13 = 1 : Nat (blocked on _r_8, belongs to problems 9, 12)
}
{ checkCandidateForMeta _10@13977009405847656758
checkCandidateForMeta
  t    = H-Level _T_5 1
  t'   = {ℓ ℓ' : Level} {A : Type ℓ} {B : Type ℓ'} {f : A → B}
         {n : Nat} →
         H-Level (1Lab.Equiv.is-equiv f) (suc n)
  term = H-Level-is-equiv
instance search: checking H-Level (1Lab.Equiv.is-equiv _f_17)
                          (suc _n_18) <= H-Level _T_5 1
instance search: found solution for _x_10: H-Level-is-equiv
candidate H-Level-is-equiv okay for overlap? False
suc _n_18 = 1 : Nat (blocked on _r_8, belongs to problems 9, 12)
}
{ dropSameCandidates
instances after resolving overlap:
- H-Level-pi : {T.ℓ : Level} {T : Type T.ℓ} {ℓ : Level} {n : Nat}
               {S : T → Type ℓ} ⦃ _ : {x : T} → H-Level (S x) n ⦄ →
               H-Level ((x : T) → S x) n
- H-Level-⊤ : {n : Nat} → H-Level ⊤ n
- H-Level-⊥ : {n : Nat} → H-Level ⊥ (suc n)
- H-Level-pi' : {T.ℓ : Level} {T : Type T.ℓ} {ℓ : Level} {n : Nat}
                {S : T → Type ℓ} ⦃ _ : {x : T} → H-Level (S x) n ⦄ →
                H-Level ({x : T} → S x) n
- H-Level-sigma : {T.ℓ : Level} {T : Type T.ℓ} {ℓ : Level}
                  {n : Nat} {S : T → Type ℓ} ⦃ _ : H-Level T n ⦄
                  ⦃ _ : {x : T} → H-Level (S x) n ⦄ →
                  H-Level (Σ T S) n
- H-Level-PathP : {ℓ : Level} {n : Nat}
                  {S : Prim.Interval.I → Type ℓ}
                  ⦃ s : H-Level (S Prim.Interval.i1) (suc n) ⦄
                  {x : S Prim.Interval.i0} {y : S Prim.Interval.i1} →
                  H-Level (Prim.Kan.PathP S x y) n
- H-Level-Lift : {T.ℓ : Level} {T : Type T.ℓ} {ℓ : Level} {n : Nat}
                 ⦃ s : H-Level T n ⦄ →
                 H-Level (Lift ℓ T) n
- H-Level-is-contr : {n : Nat} {ℓ : Level} {T : Type ℓ} →
                     H-Level (is-contr T) (suc n)
- H-Level-is-equiv : {ℓ ℓ' : Level} {A : Type ℓ} {B : Type ℓ'}
                     {f : A → B} {n : Nat} →
                     H-Level (1Lab.Equiv.is-equiv f) (suc n)
dropSameCandidates: Meta is irrelevant so any candidate will do.
}
  valid candidates
  - H-Level-pi : {T.ℓ : Level} {T : Type T.ℓ} {ℓ : Level} {n : Nat}
                 {S : T → Type ℓ} ⦃ _ : {x : T} → H-Level (S x) n ⦄ →
                 H-Level ((x : T) → S x) n
}
instance search: attempting
  _x_10 := H-Level-pi
findInstance 5: solved by instance search using the only candidate
  H-Level-pi = H-Level-pi
of type  {T.ℓ : Level} {T : Type T.ℓ} {ℓ : Level} {n : Nat}
         {S : T → Type ℓ} ⦃ _ : {x : T} → H-Level (S x) n ⦄ →
         H-Level ((x : T) → S x) n
for type H-Level ((x : _T_14) → _S_17 x) 1
The type of the FindInstance constraint isn't known, trying to find it again.
Instance type is not yet known. 
Can't figure out target of instance goal. Postponing constraint.
findInstance 2: constraint: _8@13977009405847656758; candidates left: 1
findInstance 3: t = (Number Nat)
{ checkCandidates _8@13977009405847656758
  target: (Number Nat)
  candidates
  - Number-Nat : (Number Nat)
{ checkCandidateForMeta _8@13977009405847656758
checkCandidateForMeta
  t    = (Number Nat)
  t'   = (Number Nat)
  term = Number-Nat
instance search: checking (Number Nat) <= (Number Nat)
instance search: found solution for _r_8: Number-Nat
candidate Number-Nat okay for overlap? True
}
{ dropSameCandidates
instances after resolving overlap:
- Number-Nat : (Number Nat)
dropSameCandidates: Meta is irrelevant so any candidate will do.
}
  valid candidates
  - Number-Nat : (Number Nat)
}
instance search: attempting
  _r_8 := Number-Nat
findInstance 5: solved by instance search using the only candidate
  Number-Nat = Number-Nat
of type  (Number Nat)
for type (Number Nat)
The type of the FindInstance constraint isn't known, trying to find it again.
Found instance type head:  H-Level
Can't figure out target of instance goal. Postponing constraint.
The type of the FindInstance constraint isn't known, trying to find it again.
Found instance type head:  ⊤
no instance field candidates
instance candidates from signature for goal:
  ⊤
  {tt} length: 1
blocker:
  any()
mutual block:
  {bar}
findInstance 2: constraint: _9@13977009405847656758; candidates left: 1
findInstance 3: t = (Number-Nat .Number.Constraint 1)
{ checkCandidates _9@13977009405847656758
  target: (Number-Nat .Number.Constraint 1)
  candidates
  - tt : ⊤
{ checkCandidateForMeta _9@13977009405847656758
checkCandidateForMeta
  t    = (Number-Nat .Number.Constraint 1)
  t'   = ⊤
  term = tt
instance search: checking ⊤ <= (Number-Nat .Number.Constraint 1)
}
{ dropSameCandidates
instances after resolving overlap:
}
  valid candidates
}
findInstance 5: the only viable candidate failed...
/home/n/git/1lab/src/wip/bug.agda:11,12-20
⊥ !=< (x : _T_14) → _S_17 x
when checking that the expression hlevel 1 has type is-prop ⊥

Bisection shows agda/agda#7298 as the first bad change.

Using suc zero instead of 1 fixes the error, as does making the argument to foo relevant.

[plt-amy]

Bisection shows 7298 as the first bad change.

that's pretty funny.