The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi Alexandre,

  it seems you managed to trigger two problems with unification in a
single example, congrats! Basically you want higher-order unification 
to work here, unifying the return type [?M bool] with [FPair bool nat 0]
but this unification fails (using [apply (creturn x)] in proof mode). If you 
try 
[exact (creturn x)] then typeclass resolution is launched and unification
fails on the problem [Pointed (fun A : Type => FPair A ?1 ?2) = Pointed ?59]
(but ?1 and ?2 are existentials of a different kind than [?59 : Type -> Type] 
here, as you cannot see). It seems to me there is no workaround. Hopefully we 
will be able to fix this in the next 8.3 version though. Could you please 
report
this as a bug?

Cheers,
-- Matthieu

Le 20 juil. 2010 à 14:58, Alexandre Pilkiewicz a écrit :

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