In emacs with the Agda mode, pressing C-u C-c C-; in the hole (in the definition of baz) gives the error
An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE_VERBOSE__, called at src/full/Agda/TypeChecking/Reduce.hs:224:18 in Agda-2.7.0.1-6273180bd9b53a251e88a8912e7909d128fe0195585b527f0efc07f60cb86e79:Agda.TypeChecking.Reduce
Agda file below, no flags.
data _≡_ {ℓ} {X : Set ℓ} (x : X) : X → Set ℓ where
refl : x ≡ x
record Foo {ℓ} (X : Set ℓ) : Set ℓ where
field
foo : X
open Foo {{...}}
instance
bar : ∀ {ℓ} {X : Set ℓ} {x : X} → Foo (x ≡ x)
bar .foo = refl
baz : ∀ {X : Set} → X ≡ X
baz = {! foo {{bar}} !}
Agda version 2.7.0.1, recently installed with cabal.
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