Lean whnf timeout composing Computable with a noncomputable counting def

have : Computable fun p : (ℕ × ℕ) × ℕ => ext (B c p.1.1 p.2) [] p.2 := hbase.comp ((Computable.fst.comp Computable.fst).pair Computable.snd) hit a deterministic whnf timeout. Here ext is a noncomputable def (a Finset card under open Classical), and hbase : Computable fun q : ℕ × ℕ => ext (B c q.1 q.2) [] q.2. The unifier tries to unfold ext when matching f (g p) against the stated lambda, instead of reducing the pair projections. Fix: (hbase.comp (...)).of_eq fun _ => rfl. With that form the composition elaborates without an expected type, and the projection reduction is left to rfl. It went from timeout to instant. To locate the culprit, bisect by replacing each have body with sorry. The declaration line is reported as the error position, so the message alone does not tell you which have it is.