A RetroSearch Logo

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

Search Query:

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

Instanceness is lost when expanding absurd pattern in pattern synonym expression · Issue #7176 · agda/agda · GitHub

open import Agda.Builtin.Bool
open import Agda.Builtin.Equality

data D : Set where
  c : {{ i : true ≡ false }} → D

pattern ff = c {{ () }}

works : D → D
works ff

works' : D → D
works' c = c

test : D → D
test c = ff

The test fails with an unsolved constraint:

_i_12
  : Agda.Builtin.Bool.Bool.true Agda.Builtin.Equality.≡
    Agda.Builtin.Bool.Bool.false

The code to translate a pattern synonym with absurd pattern to an expression is this one (last line):

patternToExpr :: Pattern -> Expr patternToExpr = \case VarP x -> Var (unBind x) ConP _ c ps -> Con c `app` map (fmap (fmap patternToExpr)) ps ProjP _ o ds -> Proj o ds DefP _ fs ps -> Def (headAmbQ fs) `app` map (fmap (fmap patternToExpr)) ps WildP _ -> Underscore emptyMetaInfo AsP _ _ p -> patternToExpr p DotP _ e -> e AbsurdP _ -> Underscore emptyMetaInfo -- TODO: could this happen?

There are two problems:

  1. The meta info has no scope info, thus the constraint is printed in the top-level scope (full qualification).
  2. The absurd pattern is in instance position and should turn into an instance meta, but it does not.

The second problem is a consequence of rejecting the semantics of {{_}} suggested in #2172, but after #7173 we have some machinery to fix 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