type class trace dump

Stream: general

[Johan Commelin]

Is this expected behaviour?

import linear_algebra.multivariate_polynomial

set_option trace.class_instances true

instance foobar : comm_ring (mv_polynomial ℕ ℚ) := by apply_instance

I won't copy-paste the trace here, it is pretty long.