Meaning that we see the following behaviour:
open import Agda.Builtin.Equality open import Agda.Builtin.Nat data Foo (A : Set) (a : A) : Set where mk : (b : A) → Foo A a Foo′ : (A : Set) → A → Set Foo′ A a = Foo A a -- This doesn't work: Foo has polarity [*, +], so the conversion checker -- does actually look at the second argument -- _ : Foo Nat 0 ≡ Foo Nat 1 -- _ = refl -- But Foo′ has polarity [*, _] for some reason, so, with -- lossy-unification, the following is accepted: _ : Foo′ Nat 0 ≡ Foo′ Nat 1 _ = refl
I do not understand why the positivity/polarity checkers think the second argument to Foo′ is nonvariant, when it doesn't think this of Foo, but this has caused some subtly incorrect code to be accepted in the cubical library:
The context of the proof is a bit hairy, but it is a proof about jᵣ, which mentions HopfInvariantPush n (fst g). But since the module has lossy-unification and HopfInvariantPush is an alias to a datatype, the incorrect code was accepted. That's also what caused the seeming off-by-one error in @nad's #6344.
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4