When pattern matching instantiates a pattern variable, that variable is (basically) converted to a let-binding. However, if the variable was an instance argument, this is not preserved for the let-binding. Minimal example:
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality
it : {{Nat}} → Nat
it {{x}} = x
fails : {{x : Nat}} (y : Nat) → x ≡ suc y → Nat
fails y refl = it
Error message:
No instance of type Nat was found in scope.
when checking that the expression it has type Nat
A workaround is to manually let-bind the variable as an instance, but this is annoying to do:
workaround : {{x : Nat}} (y : Nat) → x ≡ suc y → Nat
workaround {{x}} y refl =
let instance _ = x
in it
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