Case where a generalised instance variable is changed to implicit

When using generalised instance variables, the hiding is not preserved in the following case:

Currently (the level becomes implicit):

variable ⦃ ℓ ⦄ : Level
variable ⦃ X ⦄ : Set ℓ
variable ⦃ x ⦄ : X

test : x → Set₁
test {_} ⦃ _ ⦄ _ = Set

The type of test is: {x.X.1 : Level} ⦃ x : Set x.X.1 ⦄ → x → Set₁

Expected (the level should still be an instance):

variable ⦃ ℓ ⦄ : Level
variable ⦃ X ⦄ : Set ℓ
variable ⦃ x ⦄ : X

test : x → Set₁
test ⦃ _ ⦄ ⦃ _ ⦄ _ = Set

The type of test should be: ⦃ x.X.1 : Level ⦄ ⦃ x : Set x.X.1 ⦄ → x → Set₁

Of course, one can just use X instead of x in test and it would work as expected. Just thought this behaviour was a bit odd.

Tested versions: 2.6.2-caeadac, 2.6.5-ea16c4c

Provide feedback