let: unexpected generalization of variable

[omelkonian]

Agda 2.6.2.0.20211129

When using generalized variables in a constructor, I expect to get the same behaviour as if I had explicitly introduced it with a ∀ quantifier.
This breaks by the following MWE:

postulate
  X : Set
  ∀≡ : ∀ (x : X) → x ≡ x

variable  x : X

data C : Σ X (λ x → x ≡ x) → Set where
  _ :
    -- works if I remove this comment
    -- ∀ {x} → 
    let
      eq : x ≡ x
      eq = ∀≡ x
    in
    C (x , eq)

x != x of type X
(because one has de Bruijn index 1 and the other 0)
when checking that the expression ∀≡ x has type x ≡ x

It seems that the let-clause does its own generalization (producing x = # 0) and shadows the previous x = # 1.

[UlfNorell]

The fix would be to not generalize types if you are already in scope of a generalization. This makes sense I think.

[omelkonian]

If you mean the fix is to disallow any (nested) generalization, it might be too limiting. What I would expect is to never re-generalise a variable with the same name.

[UlfNorell]

I'm not sure it would be that limiting. It's very close to the principle that says we don't generalize the type of eq in

_ : (eq : x ≡ x) -> C (x , eq)

[omelkonian]

If I understood correctly, the fix would disallow C⁺ because there is a generalized x in scope, but allow C⁻?
(currently both are accepted)

postulate
  X : Set
  ∀≡ : ∀ {x y : X} → x ≡ y

variable x y : X

data C⁻ : (∀ {x : X} → x ≡ x) → Set where
  _ :
    let
      eq : y ≡ y
      eq = ∀≡
    in
    C⁻ eq

data C⁺ : X → (∀ {x : X} → x ≡ x) → Set where
  _ :
    let
      eq : y ≡ y
      eq = ∀≡
    in
    C⁺ x eq

[UlfNorell]

No I was thinking it would disallow both. The generalization point in both examples would be the top-level type.