Fixpoints using variables fail to type check
Closed this issue · 1 comments
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
).
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.