Agda rejects some code that didn't use to be rejected:
{-# OPTIONS --erasure --cubical #-}
module M where
data ⊥ : Set where
record R : Set where
field
f : ⊥
{-# OPTIONS --erasure --erased-cubical #-}
open import M
f : R → ⊥
f ()
$ agda --no-libraries Bug.agda
Checking Bug ([…]/Bug.agda).
Checking M ([…]/M.agda).
[…]/Bug.agda:6,1-5: error: [ShouldBeEmpty]
R should be empty, but that's not obvious to me
when checking the clause left hand side
f ()
Bisection points towards 27ec477 ("[ refactor ] Add two helper functions `isEtaRecordDef` and `isEtaRecordConstructor` to clean up code dealing with eta-equality"). @jespercockx, can you take a look at this?
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