The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Coq users,

one note on this: in case the type t2 is defined directly and not computed by 
the fixpoint on the structure definition, the Type Class mechanism does work. 
Definition t2 := (bool * (bool * unit) * (bool * (bool * unit) * unit))%type.

Example v1 := (true, (false, tt), (true, (false, tt), tt)).
Example v2 : t2 := (true, (false, tt), (true, (true, tt), tt)).
Eval compute in eqb v1 v2. (* => false *)
Eval compute in eqb v1 v1. (* => true *)

Example v3 : t2 := (true, (false, tt), (true, (false, tt), tt)).
Eval compute in eqb v3 v2. (* => false *)

Only if t2 is computed by the fixpoint given in my first post, it doesn't 
work.

Example v3 : t2 := (true, (false, tt), (true, (false, tt), tt)).
Eval compute in eqb v3 v2. (* =>
     = (let (eqb, _) := ?257 in eqb)
         (true, (false, tt), (true, (false, tt), tt))
         (true, (false, tt), (true, (true, tt), tt))
     : bool
*)

Is this a bug in the Type Class mechanism?

Best regards,

Michael