Recursive inductive notation and incremental type checking

Using Rocq
1

Hi,

I noticed that it is hard to find a bug caused by a typo in an inductive definition using recursive notation.

So if user types a “.” somewhere in the middle of a long inductive type definition - he, instead of a syntax error, pointing to the issue, might get a misleading type checking error.
I haven’t work before with proof assistants and I guess for a typical programmer such error would probably make him to freeze too for quite awhile. So I would like to share this aha moment.

Declare Custom Entry com.
Reserved Notation "st '[=]' c" (at level 40, st constr, c  custom com).
Inductive com : Type := | CSkip : com | CNop : com.
Notation "'skip'" := CSkip (in custom com at level 0).
Notation "'nop'" := CNop (in custom com at level 0).

Inductive ind : nat -> com -> Prop :=
| E_Skip : forall st, st [=] skip
| E_Nop  : forall st, st [=] nop
where "st [=] c" := (ind st c).

Module M.
  Inductive com : Type := | CSkip : com | CNop : com.
  Notation "'skip'" := CSkip (in custom com at level 0).
  Notation "'nop'" := CNop (in custom com at level 0).

  Inductive ind : nat -> com -> Prop :=
  | E_Skip : forall st, st [=] skip
  | E_Nop  : forall st, st [=] nop. (* this period causing the problem *)
  where "st [=] c" := (ind st c).
End M.

Error:
In environment
ind : nat -> com -> Prop
st : nat
The term "CSkip" has type "com" while it is expected to have type "X.com".

Rocq has long history and changing anything requires lot of efforts, but I would like to have:

  • Basic syntax verification for a single statement after the cursor
  • Alternative syntax for notation binding preceeding data constructors e.g.
Inductive ind : nat -> com -> Prop where "st [=] c" := (ind st c) :=
  | E_Skip : forall st, st [=] skip
  | E_Nop  : forall st, st [=] nop.
2
  • Basic syntax verification for a single statement after the cursor

This would not change your problem: the error message would be the same.

What could be wished for is a visual delimitation of the whole command which triggered a message (together with the delimitation given by the error message which only point to the error itself). That is a good idea I will try someday to implement this in proofgeneral.

  • Alternative syntax for notation binding preceeding data constructors e.g.

Not sure you will have a consensus on this one.

EDIT: done here . Thanks for the idea!