Number Notation typechecking shouldn't enable elaboration

[proux01]

Coercion nat_of_option (u : option nat) : nat :=
  match u with Some u => u | None => 0 end.

Number Notation nat Nat.of_num_int Nat.to_num_int : nat_scope.

Check 3.  (* "Some 3 : option nat" instead of "3 : nat" *)

The issue is that Number Notation accept Nat.of_num_int as a complete function (of type _ -> nat) instead of a partial one (of type _ -> option nat) because its typechecking enable to elaborate the parsing function Nat.of_num_int to fun u => nat_of_option (Nat.of_num_int u) which is a complete parsing function, but still uses the unelaborated Nat.of_num_int as parsing function.

I think that Number Notation typechecking should just forbid elaboration (otherwise it elaborates new parsing/printing functions that are completely hidden to the user).

[gares]

One option to fix this is wait for #15845 , then add an option to disable coercions to and finally use it in number notations.

Another option is to rewrite the code of number notation to not work with constr_expr, but rather constr, and hence short-circuit the elaborator (which does not seem to be needed, really).

[SkySkimmer]

Another option is to rewrite the code of number notation to not work with constr_expr, but rather constr

Why not globref? Not sure why constr would work better tbh.

[proux01]

Note that there are examples in the test-suite with holes, so not sure how constr would work here:

coq/test-suite/output/NumberNotations.v

Line 775 in d225e17

Notation eqO := (eq _ O) (only parsing).

[SkySkimmer]

That's only on the type argument, not the functions though.

[gares]

Why not globref? Not sure why constr would work better tbh.

The code does type check the two functions against T1 -> T2 or T1 -> option T2, so you need a data type which supports typing.