The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

> Nobody seems to know about this feature/bug.
> If it is a feature then it is not documented (as far as I understand
> the reference manual).
> If it is a bug then it is a useful one.
> 
> On Mon, Sep 20, 2010, I wrote:
> > Record T : Type := {
> >  carrier : Set ;
> >  op : carrier -> carrier -> carrier
> > }.
> >
> > Check fun (t:T)(x y:carrier t), op _ x y.
> >
> > (*
> > Above, the implicit argument is inferred to be t.
> > But there are other legal choices such as below.
> > On which bases Coq chooses?
> > *)
> >
> > Check fun (t:T)(x y:carrier t), op {| carrier := carrier t ; op := fun
> > x y => x |} x y.

This has nothing to do with a bug. Call it a feature if you want. At
worst, what can be said is that the combination of heuristics used to
infer missing arguments, and hence to interpret user-level terms into
terms of the Calculus of Inductive Constructions, is not fully
specified.

Basically, inference of implicit arguments relies on a combination of
unification, search for type class instances, canonical structures.

In the present case, typing the application of op to x and y yields
the equation "carrier _ = carrier t" and only unification is used.

Unification being over λ-terms, it is undecidable in the general case,
and indeed, as you point it out, the above problem has many solutions
(arbitrarily many if I'm computing correctly).

To shrink the search space, Coq gives the priority to a
first-order-like unification strategy which, in the present situation,
means considering "carrier" as a rigid symbol and to directly
instantiate _ by t. This is a strategy that was implemented long time
ago in Coq (IIRC by Chet Murthy at the time he was contributing to the
development of Coq) and it generally matches the intuitive expectation
of the user.

Hugo Herbelin