No scope info for underscores inserted by pattern synonym expansion

[andreasabel]

When an underscore is created during expansion of pattern synonyms, it lacks the scope info. The symptom is that constraints are printed in top-level scope (with lots of qualification).

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

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

pattern ff {i} = c {i}

works : D
works = c

-- yellow:
-- _i_6 : true ≡ false

test : D
test = ff

-- yellow:
-- _i_8
--   : Agda.Builtin.Bool.Bool.true Agda.Builtin.Equality.≡
--     Agda.Builtin.Bool.Bool.false