Closed UlfNorell closed 3 weeks ago
Bisection blames 403ee4263 (#7183).
(Not at home today, I'll only be able to look into this tomorrow.)
Well, I can't look into it properly, but I think removing this check, so it always does ignoreAbstractMode, should fix this issue.
Thanks! It makes the example go through. I'll make a PR and see if anything breaks.
(Cross-post to the PR). The attempted 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
Thanks for the minimised example (and for trying the fix), @UlfNorell! That makes sense, since by ignoring abstract
when adding the instance we in effect add it for Count Nat
instead. I think a more correct fix will be to treat opaque
symbols as FlexK
s (ie treat them as if they were blocked & could reduce, since they can, and leave it for instance selection to discard them, using the conversion checker), but that's not something I can implement on my phone; tomorrow, then.
Instances defined outside the opaque block sometimes fail to resolve when inside. Possibly some issue with the discrimination trees (ping @plt-amy). Works on 2.6.4.3.