Phrasing and formatting of the unsatisfiable constraints error message

[herbelin]

This PR is an attempt to get:

• a more consistent printing (same line breaking and non-quote when printing hypotheses and evars)
• a better space management when reporting about unsatisfiable constraints
• a better message when there are actually no constraints at all

For instance, in an example I'm working on, it gives:

Unable to satisfy the following constraints:
In environment:
arity : HSet
FrameBlock :
  forall n : nat,
  nat -> forall prefix : Type, FrameBlockPrev n prefix -> Type
n, p : nat
prefix : Type
FramePrev : FrameBlockPrev n prefix
frame : p <= n -> prefix -> HSet
restrFrame :
  forall (q : nat) (Hpq : p.+1 <= q.+1) (Hq : q.+1 <= n),
  arity ->
  forall D : prefix, frame (↓ (Hpq ↕ Hq)) D -> FramePrev.(frame') p D
q, r : nat
Hpr : p.+2 <= r.+2
Hrq : r.+2 <= q.+2
Hq : q.+2 <= n
ε, ω : arity
D : prefix
d : frame (↓ (?Hpq0 ↕ ?Hq0)) D
?Hpq : p.+2 <= q.+2
?Hq : q.+2 <= n
?Hpq0 : p.+1 <= r.+1
?Hq0 : r.+1 <= n
?Hpq1 : p.+2 <= r.+2
?Hq1 : r.+2 <= n
?Hpq2 : p.+1 <= q.+2
?Hq2 : q.+2 <= n
[arity] [FrameBlock n p prefix FramePrev frame restrFrame q r Hpr Hrq Hq ε ω
  D d q0 Hqn] |- ?Hq2 q0 (?Hpq2 q0 Hqn) == (↓ (?Hpq1 ↕ ?Hq1)) q0 Hqn
[arity] [FrameBlock n p prefix FramePrev frame restrFrame q r Hpr Hrq Hq ε ω
  D d q0 Hqn] |- ?Hq0 q0 (?Hpq0 q0 Hqn) == (↓ (?Hpq ↕ ?Hq)) q0 Hqn

while it was before:

Unable to satisfy the following constraints:
In environment:
arity : HSet
FrameBlock :
  forall n : nat,
  nat -> forall prefix : Type, FrameBlockPrev n prefix -> Type
n, p : nat
prefix : Type
FramePrev : FrameBlockPrev n prefix
frame : p <= n -> prefix -> HSet
restrFrame :
  forall (q : nat) (Hpq : p.+1 <= q.+1) (Hq : q.+1 <= n),
  arity ->
  forall D : prefix, frame (↓ (Hpq ↕ Hq)) D -> FramePrev.(frame') p D
q, r : nat
Hpr : p.+2 <= r.+2
Hrq : r.+2 <= q.+2
Hq : q.+2 <= n
ε, ω : arity
D : prefix
d : frame (↓ (?Hpq0 ↕ ?Hq0)) D

?Hpq : "p.+2 <= q.+2"

?Hq : "q.+2 <= n"

?Hpq0 : "p.+1 <= r.+1"

?Hq0 : "r.+1 <= n"

?Hpq1 : "p.+2 <= r.+2"

?Hq1 : "r.+2 <= n"

?Hpq2 : "p.+1 <= q.+2"

?Hq2 : "q.+2 <= n"
[arity] [FrameBlock n p prefix FramePrev frame restrFrame q r Hpr Hrq Hq ε ω D d q0 Hqn] |- ?Hq2
                                                 q0 (?Hpq2 q0 Hqn) == (↓ 
                                                 (?Hpq1 ↕ ?Hq1)) q0 Hqn
[arity] [FrameBlock n p prefix FramePrev frame restrFrame q r Hpr Hrq Hq ε ω D d q0 Hqn] |- ?Hq0
                                                 q0 (?Hpq0 q0 Hqn) == (↓ 
                                                 (?Hpq ↕ ?Hq)) q0 Hqn

Maybe the context and list of evars should be more clearly separated?

Also, in a situation without proper constraints like this one:

Class T : SProp.
Parameter t : T.
Parameter c : T -> T -> T.
Parameter P : T -> Type.
Parameter f : forall x, P (c (c x x) t).
Parameter g : forall x, P (c t (c x x)).
Definition h : f _ = g _.

the message is now:

Could not find an instance for the following existential variables:
?x : T
?x0 : T

while it was before:

Unable to satisfy the following constraints:

?x : "T"

?x0 : "T"

This is to be compared to the case of only one remaining existential variable in a class:

Class T : SProp.
Parameter t : T.
Parameter c : T -> T -> T.
Parameter P : T -> Type.
Parameter f : forall x, P (c (c x x) t).
Definition h : f _ = f _.
(* Could not find an instance for "T". *)

Maybe the message for one or more unresolved evars could be merged actually?

• Added / updated test-suite.

[SkySkimmer]

I think I prefer having the empty newline to separate the evars.

[herbelin]

I think I prefer having the empty newline to separate the evars.

We could have something similar to the conversion mismatch error, that is, printing the reason after the environment:

In environment:
...
Unable to satisfy the following constraints:
?x : T
?x0 : T
[...] [...] |- t == u

and:

In environment:
...
Could not find an instance for the following existential variables:
?x : T
?x0 : T

??

(And incidentally adding a colon to In environment in the conversion mismatch error.)

[SkySkimmer]

I mean the newline between evars, ie I prefer

?x : T

?x0 : T

rather than

?x : T
?x0 : T

[herbelin]

@SkySkimmer:

But then why newlines between existential variables and not also between the (universal) variables of an environment?

Actually, and more generally, I wonder whether it would not be worth to always print the type and context of evars occurring in a goal. Say, that the following:

Goal forall x, exists y, forall z, z + y + x = x + z.
intro; eexists; intro.
Show.

gives:

  x : nat
  ?y : nat
  z : nat
  ============================
  z + ?y + x = x + z

(possibly with extra context information when the evar derives by unification from a hole not in the current "spine" of the term)

[proux01]

We could have something similar to the conversion mismatch error, that is, printing the reason after the environment:

That indeed sounds better.

[SkySkimmer]

But then why newlines between existential variables and not also between the (universal) variables of an environment?

Because I want to quickly distinguish the failed constraints (which is harder when they're a wall of text), I don't need to quickly distinguish env variables.

[herbelin]

@proux01, @SkySkimmer: I moved "In environment" before the main explanation and I restored the double newlines (though w/o the last trailing one).

[SkySkimmer]

??

[herbelin]

Apparently a too eager git add output.

[SkySkimmer]

@coqbot merge now