Description
Agda version v2.7.0 (also v2.6.4.3, it seems)
stdlib version: master branch
Interactive attempt to check the following MWE causes a weird error, which I don't even know how to localise as to cause (failure in the variable generalisation mechanism? in the DISPLAY pragma?):
module IrrelevantBug where
open import Level
open import Data.Empty using (⊥)
open import Data.Irrelevant
open import Relation.Nullary.Recomputable
private
variable
a : Level
A : Set a
recompute-irrelevant : Recomputable (Irrelevant A)
recompute-irrelevant p = {!p!}Emacs interaction, instead of printing ?0 : Irrelevant A prints ?0 : ⊥?
NB
- if quantification is explicit, rather than generalisation via the above
privatevariables, then interaction is as expected. - similarly, if the
importofData.Emptyis excluded, and with it the{-# DISPLAY Irrelevant Empty = ⊥ #-}pragma, then again the example is OK.
Any ideas how to avoid this? Data.Empty has been stable in the stdlib for a while now, so it seems to be only the interaction with the explicit import of Data.Irrelevant/Relation.Nullary.Recomputable (or: irrelevance annotaions?) causing the bug?