The Coq mailing list

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

Dear list

I'm using coq 8.3-pl1


<<<<<<<<<<<<<<<<<<<<<<<<
(* Suppose I have a type class for almost monad *)

Class Monadish (M:Type -> Type) :=
  bind: forall {A B :Type}, M A -> (A -> M B) -> M B.

(*And a type class for monad, that encapsulate the first (in real
code, it has more, but lets keep it simpl) *)

Class Monad (M:Type -> Type) := {
  Monad_Monadish :> Monadish M
}.


(* I can statethat option is a monad *)

Instance Monad_option: Monad option :=
{
  Monad_Monadish := fun _ _ oa f =>
    match oa with
      | None => None
      | Some a => f a
    end
}.

(* and I can prove lemmas with one bind *)
Goal (bind (Some O) (fun n => Some n) = Some O).
compute. reflexivity. Qed.

(* or two binds *)
Goal (bind (Some O) (fun n => bind (Some n) (fun x => Some x)) = Some O).
compute. reflexivity. Qed.


(* now let us pollute things with a second monadish *)

Inductive box (A:Type) : Type :=
  | BOX: A -> box A.

Instance Monadish_box: Monadish box:=
  { bind := fun A B ba f =>
    match ba with BOX a => f a end}.

(* the first lemma still works fine *)
Goal (bind (Some O) (fun n => Some n) = Some O).
compute. reflexivity. Qed.

(* the second fails ! *)
Goal (bind (Some O) (fun n => bind (Some n) (fun x => Some x)) = Some O).
(* Error: Impossible to unify "option ?649" with "?645 ?647". *)


(* but if I add a specific instance for monadish option, even *before*
defining the one for box, everything works again *)
(*Instance Monadish_option: Monadish option.
eauto with typeclass_instances.
Defined.*)
>>>>>>>>>>>>>>>>>>>>>>

Is this a known problem?

Cheers

Alexandre