The Coq mailing list

[Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>]

Dear list!

I'm currently playing with type classes in Coq. My goal is to write
some "do notations", but I will present a smaller example (see the
attached file)

I have a class Pointed

>>>>>
Class Pointed (M:Type -> Type) := {
  creturn: forall {A: Type}, A -> M A
}.
<<<<<

with a creturn function (just "return" is sadly not valid).

I often have function that returns a "pair", with the first element of
the pair being the interesting result of the function, and with a
second element that could most of the time be calculated
"automatically" (what I really want here is a monad with bind a
return, but for the simplicity of my question, I'll just present
return).

But I don't want to define a new Instance for each second type (and
sometimes I want a different default element). That's why I defined a
special pair type, with the default element in it:

<<<<<
Unset Implicit Arguments.

Inductive FPair (A B:Type) (neutral: B) : Type:=
 fpair : forall (a:A) (b:B), FPair A B neutral.

Implicit Arguments fpair [[A] [B] [neutral]].

Set Implicit Arguments.

Notation "( x ,> y )" := (fpair x y) (at level 0).
>>>>>

This type is easily Pointed (with a Parameterized instance):

<<<<<
Instance Pointed_FPair B neutral:
 Pointed (fun A => FPair A B neutral) :=
 { creturn := fun A (a:A) => (a,> neutral) }.
>>>>>

But when I try to use it:

<<<<<
Definition blah_fail (x:bool) : FPair bool nat O :=
  creturn x.
>>>>>

the instance search fails:

<<<<<
Toplevel input, characters 75-82:
Error: Cannot infer the implicit parameter Pointed of
creturn.
Could not find an instance for "Pointed ?33" in environment:

x : bool

With the following constraints:
?34 == (Pointed ?33)
?33 == (Type -> Type)

>>>>>


If I help by giving the instance, it works:
<<<<<
Definition blah_explicit (x:bool) : FPair bool nat O :=
  @creturn _ (Pointed_FPair _ ) _ x.
>>>>>

or when I give a simple instance:

<<<<<
Instance Pointed_FPair_mono:
 Pointed (fun A => FPair A nat 0) :=
 { creturn := fun A (a:A) => (a,> 0) }.


Definition blah (x:bool) : FPair bool nat O :=
  creturn x.
>>>>>

Did I do anything wrong with the implicit arguments? Is it possible to
make the "natural" version work?

Thanks!

Alexandre Pilkiewicz

Attachment: TestClass.v
Description: Binary data