The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Le 10 mars 2011 à 15:22, Alexandre Pilkiewicz a écrit :

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

Hi Alexandre,

  This is a bug in the unification code indeed, a constraint of the form
[option ?649 <= ?645 ?647] was ignored and suddenly we allowed ?645 to be 
instantiated with [box] making the constraints unsolvable... It is now
fixed in the 8.3 and trunk branches.
-- Matthieu