Bug in extended binders?

Stream: std4

[Kyle Miller]

The expression ∀ x, ∀ x < x, True currently expands to ∀ (x : ?m) (x_1 : ?m), x_1 < x_1 → True rather than ∀ (x : ?m) (x_1 : ?m), x_1 < x → True. This seems like a bug to me, since you'd expect the < x to be sort of like a type ascription (and that's what a student at the MSRI summer school expected; they had another example using \in that seemed like it ought to work, but I forgot exactly what it was). Alpha renaming lets you work around it easily at least.

I imagine a fix would be to be careful with macro scopes, but it seems like it'd make the | `(∀ $x:ident $pred:binderPred, $p) => `(∀ $x:ident, satisfies_binder_pred% $x $pred → $p) macro rule much more complicated.

[Kevin Buzzard]

I would regard the expression as garbage. Do we really want to work around people using x to mean two different things in the same sentence?

[Kyle Miller]

You're not wrong, but it's good to have a solid interpretation of even unreasonable things. You don't want the meaning to change drastically just because of some shadowing.

[Kyle Miller]

The example I saw was closer to \forall n, ..., \forall n \in f n, ..., which is less nonsensical than seeing x < x, and on first glance whatever it was seemed fine.

[Mario Carneiro]

I don't think it can be done with macro scopes alone. When you write ∀ x, ∀ x < x, True, all occurrences of x there have exactly the same hygiene

[Mario Carneiro]

it is rather the elaborator that does the resolution of names to particular fvars and which is affected by name shadowing

[Mario Carneiro]

If the inner x was being introduced by the macro then we could fix this with hygiene (or rather, it would behave as you would like already), but here both x's are being specified by the user so there is no way to hygiene them separately

[Mario Carneiro]

What might work is

| `(∀ $x:ident $pred:binderPred, $p) => `(∀ $x:ident, satisfies_binder_pred% $x (clear% $x; $pred) → $p)

[Kyle Miller]

Ah right that seems like it could work, or something like letI p := fun x => satisfies_binder_pred% x $pred; ∀ $x:ident, beta% p $x → $p, where beta% would be this