On Agda 2.6.4 the following self-contained code
module Test {A : Set} where
open import Agda.Primitive using (Level; _⊔_; lsuc)
private
variable
ℓ₃ : Level
record Rec ℓ₃ : Set₁ where
field
IsS : A → Set
extract : ∀ {a : A} → IsS a → Set
module Test (r : Rec ℓ₃) (open Rec r) where
postulate f : A → ?
begin-contradiction_ : Set
begin-contradiction_ = ?
where
x<x : ?
x<x = extract (f ?)
throws the error:
An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full/Agda/TypeChecking/Sort.hs:224:21 in Agda-2.6.4-e6510447f87a1a26375f0a932139120d3050d11d5f869249fbd6acc3a8abb596:Agda.TypeChecking.Sort
Maybe someone else will have better luck minimising it further!
Andreas, 2023-10-23: The crash is here:
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