Instanceness is lost when expanding absurd pattern in pattern synonym expression

[andreasabel]

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): https://github.com/agda/agda/blob/fc866f9e0264a98e58a3d6034f727c4131844752/src/full/Agda/Syntax/Abstract.hs#L997-L1006

There are two problems:

1. The meta info has no scope info, thus the constraint is printed in the top-level scope (full qualification).

   • 7177

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.