The Coq mailing list

[Conor T McBride <c.t.mcbride AT durham.ac.uk>]

Hi all

Pierre Casteran wrote:

This is an interesting problem. I'm fairly sure that Lego
wouldn't solve it either. Epigram just about gets it.

I don't know how Coq handles the equational constraints which
come from typechecking, but let's see which ones show up in
this problem:

> Record Signature : Type := {
>   V : Set; (* variables *)
>   C : Set; (* constants *)
>   P : nat -> Set (* predicates with arity *)
> }.
>
> Section form_def.
> Variable sigma : Signature.
>
> Inductive dForm : Set :=
>   |   dall : V sigma -> dForm -> dForm
>   |   dtrue : dForm.
>
> End form_def.

[..]

> Definition sigma : Signature.
>  split.
>  exact vars.
>  exact consts.
>  exact preds.
> Defined.
>
> Implicit Arguments dtrue [sigma].
>
> Definition f : dForm sigma :=
>     dall x dtrue.

Please forgive my made up syntax, but if we show the implicit
arguments, then we have

   dall_?a x (dtrue_?b) : dForm sigma

and if we follow the typing rules, we'll get these three
constraints

  (type of x is domain of dall_?a)          vars = V ?a
  (type of dtrue_?b is domain of dall_?a x) dForm ?b = dForm ?a
  (type of expression is dForm sigma)       dForm ?a = dForm sigma

Now, the first of these has no obvious solution: it would take a
very clever computer to think up the right term of which vars is
a reduct. If the typechecker insists on solving the first
constraint first, it won't be happy, and will say something like

> Toplevel input, characters 99-100
>  > Definition f : dForm sigma :=     dall x dtrue.
>  >                                        ^
> Error: The term "x" has type "vars" while it is expected to have type "V 
> ?5"

If only it tried the last constraint first, it would correctly
get ?a = sigma, and then the first constraint would hold.

So what does Coq actually do here? Does it try to solve constraints
as soon as they arise? I know that's what Lego does, and it's
very sensitive to the order in which problems are solved. Lego
will unify

   (?x,?x+?y) = (0,z)

but not

   (?x+?y,?x) = (z,0)

because it works left-to-right.

It's quite annoying, having to be aware not only of _how much_
information the typechecker needs, but also the _order_ in which the
typechecker needs it. Any fixed order of constraint solving will lead
to a problem like this.

> Nevertheless, putting explicit type constraint on x will work, but I 
> don't know why I should be so explicit, cause, by constraining the type 
> of f
> I gave enough information, no?

Yes, you did.

> Definition f0 : dForm sigma :=
>    dall (x:V sigma) dtrue.
>
> f0 is defined.

Now, this I find a little odd. Why does this work when the other does
not? Now the first constraint reads

  V sigma = V ?a

from which one cannot conclude that necessarily ?a = sigma, just that ?a
must have a V projection coinciding with sigma's. Is this what's
happening? Of course, ?a = sigma is a very plausible guess under the
circumstances, even if it is not necessarily the case, so perhaps it's
good in practice to make that choice. I'm pretty sure that Lego would
take ?a = sigma here, although I'm not sure that I'd want it to.

So, is there a `guessing strategy' at work here? If so, what is it? Are
there good examples of proofs which would be harder without it? Are
there good examples of non-proofs which would work if the machine was
less keen to jump to the wrong solution?

I haven't got the Coq source code handy, so I'm only speculating, based
on the error message, and having seen how Lego handles these issues. I'd
like to know how Coq handles them: is there anything on paper about it?
(No criticism intended if there isn't: I'm not the best citizen in that
respect myself.)

All the best

Conor