The following code does not work:
{-# OPTIONS --cubical --level-universe #-}
open import Agda.Primitive
data _≡_ {l : Level} {X : Set l} : X → X → Set l where
refl : {x : X} → x ≡ x
Jbased : {l : Level} {X : Set l} (x : X) (A : (y : X) → x ≡ y → Set l)
→ A x refl → (y : X) (r : x ≡ y) → A y r
Jbased x A b _ refl = b
and the error message is:
Panic: Pattern match failure in 'do' block at
src/full/Agda/TypeChecking/Rules/LHS/Unify/LeftInverse.hs:203:3-15
when checking that the pattern refl has type x ≡ y
If I remove either --level-universe or --cubical it works. Interestingly, changing the equality type to the builtin equality type makes it work:
{-# OPTIONS --cubical --level-universe #-}
open import Agda.Primitive
open import Agda.Builtin.Equality
Jbased : {l : Level} {X : Set l} (x : X) (A : (y : X) → x ≡ y → Set l)
→ A x refl → (y : X) (r : x ≡ y) → A y r
Jbased x A b _ refl = b
Me and @martinescardo came across this when trying to combine the TypeTopology and agda/cubical libraries.
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