infer_instance succeeds, exact infer_instance fails

Stream: general

[Eric Wieser]

What's going on here?

import data.mv_polynomial.basic
import algebra.algebra.tower

variables {R : Type*} [comm_semiring R]

-- fails quickly
example (m n : ℕ) : is_scalar_tower R (mv_polynomial (fin m) R) (mv_polynomial (fin n) (mv_polynomial (fin m) R)) :=
  by show_term { exact infer_instance }

-- succeeds, very slowly
example (m n : ℕ) : is_scalar_tower R (mv_polynomial (fin m) R) (mv_polynomial (fin n) (mv_polynomial (fin m) R)) :=
  infer_instance

(the instance it finds is docs#mv_polynomial.is_scalar_tower via docs#is_scalar_tower.right)