Fixpoints using variables fail to type check

[ionathanch]

The fixpoint definition g fails to type check, while h does not.

Section Test.
Variable f : nat -> nat.
Fail Fixpoint g (n : nat) := f n.
Definition h (n : nat) := f n.
End Test.

Although g is a fixpoint, it should be fine to use a declaration: The type of f should be inferred to nat^∞ → nat^∞, which leads to g being inferred as nat^s → nat^∞ for some size variable s.
For some reason this does not fail outside of a section (i.e. using Parameter).

[ionathanch]

Found the cause: Var declarations were being treated like Rel declarations (as if they were local with relevant constraints in the current constraint set) instead of Const declarations (as if they were global with constraints solved and types needing size substitution). I don't know why Coq has these two separate notions, Var is just a namespaced Const. Many things in the kernel do not make sense.