Goal doesn't show variable names that are not used after forall ...,

[jfehrle]

The goal should show forall ... in the goal after each of the first two lines. Perhaps this is corner case because x and y are not used after the comma. Alternatively, should Coq return a warning or error when a forall variable is unused?

Goal forall x y : nat, True.
intros x.
intros.

[TheoWinterhalter]

I don't think it's a bug. The x and y are information on what the variables should be named, so if you do intros you will get indeed x and y so long as they are fresh in the environment.
And non-dependent functions are written as arrows.

[ppedrot]

This is by design indeed. Arrows are just a notation for dependent products. It would be very annoying to force users to replace dependent produces with arrows when the variable does not appear in the body. And as mentioned by @TheoWinterhalter it's important to give a name to the underlying binder.

[Zimmi48]

This is indeed not a bug, but there is a related discussion here: #14912. I guess this particular instance can be closed.

[jfehrle]

Goal nat -> nat -> True. shows the same result as the original example. How is it useful to have a goal like nat -> nat -> True? What can you do with it other than an intro? If it's not simply a curio or a corner case, what would we say in the documentation?

From a usability perspective, it's strange to have "hidden variables" that affect the behavior of tactics.

[Zimmi48]

How is it useful to have a goal like nat -> nat -> True?

This is not a realistic example. In practice, you should not have quantified variables that are not used in the goal.

From a usability perspective, it's strange to have "hidden variables" that affect the behavior of tactics.

I agree, and I think this is kind of the point of #14912.

[jfehrle]

If it's not useful and has the potential to cause confuse, I call that a bug. How do you define "bug"? Should we tag this as "kind: usability"?

[TheoWinterhalter]

I find it pretty useful when coq tells me something is an implication and not a universally quantified thing. After reduction, forall (x : A). P x might become some A -> Q and that's good.

[ppedrot]

Personally I fail to see the problem with the behaviour described here. Arrows are just a notation, and notations can be famously non-injective (and so are coercions, implicit arguments and all the inference paraphernalia that Coq provides). This is not a bug, it's a feature. If you start complaining about arrows, then you could as well ask for the removal of all the other stuff.

The issue described at #14912 is of another nature, it's that the printer works against you to hide the name of the variable when it's unbound in the body of the product. (I think you can actually deactivate that with the Fast Name Printing flag or whatever it's called.) But it's orthogonal to the problem at hand. If you don't want to see the arrow, deactivate the notation.

Also, #14912 mentions some other related issues namely that tactics can observe the bound name in a relevant way, which is bad insofar as this name depends on the context.