Unifier can use erased variables in non-erased data parameters

[andy-morris]

In the following code, I would expect there to be an unsolved meta for x in 0-to-ω's rhs, but it is accepted in 2.6.1.2 and in current master.

data _≡⁰_ {A : Set} (@0 x : A) : @0 A → Set where refl : x ≡⁰ x
data _≡ʷ_ {A : Set} (@ω x : A) : @ω A → Set where refl : x ≡ʷ x

0-to-ω : ∀ {A} {@0 x y : A} → x ≡⁰ y → x ≡ʷ y
0-to-ω refl = refl
  -- rejected if hidden args are given explicitly,
  -- which is what I was expecting
-- 0-to-ω {x = x} refl = refl {x = {!x!}}

If I remember correctly, constructors don't actually contain the datatype's parameters, which I suppose is probably why this happens? (Changing the x parameters to indices results in the unsolved meta in 0-to-ω that I was expecting.) But either way it seems strange that one clause is accepted and the other isn't.

Sorry if this is a duplicate of 4727, or if I am misunderstanding something and it's not a bug at all.

[nad]

But either way it seems strange that one clause is accepted and the other isn't.

I agree. If we decide to make the parameters erased in the types of constructors (#4786), then this problem would presumably go away.

[nad]

It does.