Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Showing content from https://github.com/agda/agda/issues/7533 below:

`DISPLAY` pragmas should treat any defined name as matchable · Issue #7533 · agda/agda · GitHub

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 private variables, then interaction is as expected.
• similarly, if the import of Data.Empty is 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?

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