The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

Hi,

On 22 juil. 2013, at 00:44, Michiel Helvensteijn 
<mhelvens AT gmail.com>
 wrote:

> 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.

Declaring Parameters, or section variables, of type a type class 
implicitly declares it as an available instance indeed.

> Is this what is called a "contextual implicit argument"?

No, that notion is just used for computing implicits automatically.

> I've tried to
> use it with plain Records, but I can't figure out how. Is it a
> Class-only thing?

Yes.

> 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 
> *)
> - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 

That's unfortunate, maybe a bug? You could try the [Implict Arguments 
elements []]
command instead. 

> 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?

:> in a Class declaration does not declare a coercion (as documented in the
reference manual) but an instance. You can certainly make elements a coercion 
afterwards using the [Coercion] command.

Hope this helps,
-- Matthieu