Typeclasses with multiple fields vs. single field in Coq / Unexpected behaviour of Compute command

Question

I'm studying typeclasses in Coq with the book Software Foundations.

Running the following:

Class Eq A :=
  {
  eqb: A -> A -> bool;
  }.

Notation "x =? y" := (eqb x y) (at level 70).

Instance eqBool : Eq bool :=
  {
  eqb := fun (b c : bool) =>
           match b, c with
           | true, true => true
           | true, false => false
           | false, true => false
           | false, false => true
           end
  }.

Compute (true =? false).
= false
: bool

I get the message as expected. But if I do the following instead,

Class Eq A :=
  {
  eqb: A -> A -> bool;
  eqb_refl: forall (x : A), eqb x x = true;
  }.

Notation "x =? y" := (eqb x y) (at level 70).

#[refine] Instance eqBool : Eq bool :=
  {
  eqb := fun (b c : bool) =>
           match b, c with
           | true, true => true
           | true, false => false
           | false, true => false
           | false, false => true
           end
  }.
forall x : bool,
(if x
 then if x then true else false
 else if x then false else true) = true
Proof.
forall x : bool,
(if x
 then if x then true else false
 else if x then false else true) = true
  intros []; reflexivity.
Qed.

Compute (true =? false).
= match eqBool with
  | {| eqb := eqb |} => eqb
  end true false
: bool

I don't seem to be able to simplify this expression and not sure what went wrong and where. How can I define the typeclass above with the extra hypothesis, and still be able to use the instance i've defined (i.e get the same message as before)?

Thanks a lot!

Answer

The Qed command creates opaque definitions, which are never unfolded by commands like Compute. You can tell Coq to make only the proof obligation opaque by using the Program Instance command:

Require Import Coq.Program.Tactics.

Class Eq A :=
  {
  eqb: A -> A -> bool;
  eqb_refl: forall (x : A), eqb x x = true;
  }.

Notation "x =? y" := (eqb x y) (at level 70).

Program Instance eqBool : Eq bool :=
  {
  eqb := fun (b c : bool) =>
           match b, c with
           | true, true => true
           | true, false => false
           | false, true => false
           | false, false => true
           end
  }.
Next Obligation.
x: bool
(if x as c' return (c' = x -> x = x -> bool)
 then
  if x as b' return (true = x -> b' = x -> bool)
  then fun _ _ : true = x => true
  else fun (_ : true = x) (_ : false = x) => false
 else
  if x as b' return (false = x -> b' = x -> bool)
  then fun (_ : false = x) (_ : true = x) => false
  else fun _ _ : false = x => true) eq_refl eq_refl =
true now destruct x. Qed.

Compute (true =? false).
= false
: bool