The Coq mailing list

[Michiel Helvensteijn <mhelvens AT gmail.com>]

Hi all,

Type classes have a specific and rather invasive way of making
arguments implicit. An example:

- - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
Class DM := {
    elements :> Ensemble E;
    order : relation E
}.

Notation "x ≺ y" := (@order _ x y)  (at level 70, no associativity).

Parameter dm: DM.

Goal forall x y: E, x ≺ y. (* works fine *)
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

As you see, the ≺ notation automatically grabs `dm` as its implicit
argument, just, it appears, by having it in its context.

Is this what is called a "contextual implicit argument"? I've tried to
use it with plain Records, but I can't figure out how. Is it a
Class-only thing?

Anyway, I actually like it... some of the time.

I'd like to have some better control over it, but it seems to be a
stubborn feature. For example, I'd like to turn it off for some
functions, but I can't seem to manage it:

- - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
Arguments elements _ _.
Print Implicit elements. (* Argument DM is implicit and maximally inserted *)
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

Furthermore, it seems to break other things, like the `elements`
coercion I asked for with `:>`:

- - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
Goal forall x y: E, (In _ elements x) -> x ≺ y. (* works fine *)
Goal forall x y: E, (In _ dm x) -> x ≺ y. (* error *)
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

If I use a Record instead of a Class, the coercion works as expected,
but then the implicit argument inference for ≺ doesn't work. Can I
somehow have my cake and eat it too?

--
www.mhelvens.net