Post-process error messages

[ybertot]

For variables that were not specifically given a type by the user, the rocq system finds a type whose name is an unreadable long name generated by hierarchy builder. This can be avoided by asking for simplification. However, rocq also uses these long unreadable types in error messages, and in these cases, the user has no way to force the simplified type to be used instead.

Here is an example.

From HB Require Import structures.
From mathcomp Require Import all_ssreflect all_algebra.
Require Export Field.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Require Import NArithRing.
Import Order.TTheory GRing.Theory Num.Theory Num.ExtraDef Num.

Open Scope ring_scope.

Section working_environment.

Variable R : realFieldType.

Record pt := { p_x : R; p_y : R }.

Definition pt_eqb (a b : pt) : bool :=
  let: Build_pt a_x a_y := a in
  let: Build_pt b_x b_y := b in
     (a_x == b_x) && (a_y == b_y).

Lemma pt_eqP : Equality.axiom pt_eqb.
Proof.
rewrite /Equality.axiom.
move=> [a_x a_y] [b_x b_y]; rewrite /pt_eqb/=.
have [/eqP <-|/eqP anb] := boolP (a_x == b_x).
  have [/eqP <- | /eqP anb] := boolP (a_y == b_y).
    by apply: ReflectT.
  by apply : ReflectF => [][].
by apply: ReflectF=> [][].
Qed.

HB.instance Definition _ := hasDecEq.Build _ pt_eqP.


Definition dummy_pt := Build_pt 0 0.

Axiom sorted_last : forall (T : eqType) (r : rel T) (x0 x : T) (s : seq T),
  transitive r -> sorted r s -> x \in s -> sorted r s ->
  x \in s -> (x == last x0 s) || r x (last x0 s).

Check fun s : seq _ =>
  sorted_last dummy_pt (rev_trans lt_trans).

The error message looks like this, exposing various type names that were created by Hierarchy Builder, but are awkward to read.

In environment
R : realFieldType
s : seq ?A
The term "rev_trans lt_trans" has type
 "@transitive (@Order.POrder.sort ?disp ?T)
    (fun x y : @Order.POrder.sort ?disp ?T => @Order.lt ?disp ?T y x)"
while it is expected to have type
 "@transitive (Equality.sort order_problem_pt__canonical__eqtype_Equality) ?r".

[CohenCyril]

2 kinds of solutions:

• make sure the naming scheme for structure instances is user-configurable (e.g. #[suffix="eqType"]) so that it can be shorter and predictible (hence it become ok to use it and nicer to look at)
• modify Rocq to have post-processing of statements that includes more than just beta-reduction (TODO: open issue on Rocq to document the feature request)

[ybertot]

I have a hard time understanding whether the first solution is practically feasible. How much of the extra annotations would be required for the full math-comp?

[CohenCyril]

I have a hard time understanding whether the first solution is practically feasible. How much of the extra annotations would be required for the full math-comp?

probably none as we could reuse the #[short(type=X)] construction by default.

[CohenCyril]

(the only problem I foresee is the interaction with deprecation 😬)