Tactic `apply` hangs on a goal

[loutr]

In the following code, application of the apply tactic hangs without any notification to the user, and keeps filling memory. I believe this should never happen for a base tactic like apply.

lemma Ep_bool_gen (d : bool distr) (f : bool -> xreal) :
  Ep d f = mu1 d false ** f false + mu1 d true ** f true.
proof.
have -> := Ep_fin [false; true] d f //; 1: by move => [] //.
rewrite /big.
by have -> : map (d ** f) (filter predT [false; true]) =
  [(d ** f) false; (d ** f) true].
qed.

lemma Ep_dbool (f : bool -> xreal) :
  Ep {0,1} f = of_reald 0.5 ** f true + of_reald 0.5 ** f false.
proof.
  apply Ep_bool_gen. (* here *)

This likely happens because of the unification mu1 d false ≡ of_reald 0.5 (RHS is known to be eq. to 1%r / 2%r); but I did not investigate further.

[fdupress]

Can you please add enough context to reproduce the failure? (In particular, which require statements are necessary to cause the misbehaviour.)
Does simplify also loop at that line?

Smells like a cycle in custom reduction rules.