Fix #7304: ignore abstract mode when building the instance discrimination tree

agda / agda

Agda is a dependently typed programming language / interactive theorem prover.

https://wiki.portal.chalmers.se/agda/pmwiki.php

Other

2.41k stars 339 forks source link

Fix #7304: ignore abstract mode when building the instance discrimination tree #7306

Closed UlfNorell closed 3 weeks ago

UlfNorell commented 3 weeks ago

fixes #7304

Fix by @plt-amy

UlfNorell commented 3 weeks ago

Cubical fails with

/home/runner/work/agda/agda/cubical/Cubical/Algebra/CommAlgebra/FPAlgebra/Instances.agda:169,41-43
No instance of type
CommAlgebraStr _R_851 (fst (initialCAlg R / ⟨xs⟩)) was found in
scope.
when checking that the expression 0a has type
fst (initialCAlg R / ⟨xs⟩)

UlfNorell commented 3 weeks ago

The fix breaks this example:

module _ where

open import Agda.Builtin.Nat
open import Agda.Builtin.List

it : {A : Set} → ⦃ A ⦄ → A
it ⦃ x ⦄ = x

opaque
  X : Set
  X = Nat

Number = Nat
record Count (A : Set) : Set where
  field count : A → Number

open Count ⦃...⦄ public

instance
  postulate Count-X : Count X

works : X → Nat
works s = count ⦃ it ⦄ s

opaque
  unfolding X
  works₂ : X → Nat
  works₂ s = count s

fails : X → Nat
fails s = count s

plt-amy commented 3 weeks ago

Both succeed and fail pass locally for my fix (incl. both 7304s and the related 6941) but I'll let CI do the cubical library. I also added some comments around the code outlining why AbstractDefns need special handling.