search

the1lab / 1lab

A formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory
https://1lab.dev
GNU Affero General Public License v3.0
348 stars 68 forks source link

Another irrelevant instance search bug #407

Open ncfavier opened 3 months ago

ncfavier commented 3 months ago

While fixing https://github.com/plt-amy/1lab/issues/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 https://github.com/agda/agda/pull/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 commented 3 months ago

Bisection shows 7298 as the first bad change.

that's pretty funny.