Type class caching failure

Stream: general

[Rob Lewis]

This code is producing a type class resolution trace I don't remember ever seeing: it repeats the same "cached failure for ..." message without doing any work in between.

import ring_theory.witt_vector.frobenius

noncomputable theory
variables (k : Type*) [comm_ring k] (p : ℕ) [fact p.prime]

local notation `𝕎` := witt_vector p
local notation `K` := fraction_ring (𝕎 k)

set_option trace.class_instances true

-- example : module K K := by try_for 10000 {apply_instance }-- times out
-- example : module K K := semiring.to_module -- works

At some point, it ends up in a loop of printing

[class_instances] cached failure for @algebra (@fraction_ring (witt_vector p k) (@witt_vector.comm_ring p k _inst_2 _inst_1)) (witt_vector p k)
  (@comm_ring.to_comm_semiring (@fraction_ring (witt_vector p k) (@witt_vector.comm_ring p k _inst_2 _inst_1))
     (@localization.comm_ring (witt_vector p k) (@witt_vector.comm_ring p k _inst_2 _inst_1)
        (@non_zero_divisors (witt_vector p k)
           (@semiring.to_monoid_with_zero (witt_vector p k)
              (@ring.to_semiring (witt_vector p k)
                 (@comm_ring.to_ring (witt_vector p k) (@witt_vector.comm_ring p k _inst_2 _inst_1)))))))
  (@comm_semiring.to_semiring (witt_vector p k)
     (@comm_ring.to_comm_semiring (witt_vector p k) (@witt_vector.comm_ring p k _inst_2 _inst_1)))

with nothing in between.

I'll try to minimize the example, but in the meantime, has anyone seen this before? @Gabriel Ebner any guesses?

[Eric Rodriguez]

I feel like this reminds me of what I ran into on flt_regular: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/TC.20hell.20in.20FLT-regular

[Eric Wieser]

Yes, I saw this recently in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/infinite.20cached.20failure.20for.20comm_semiring.20S/near/267181466

[Eric Wieser]

If you ask for more diagnostics, it looks less repetitive

[Gabriel Ebner]

The standard answer is that this is probably due to nested type-class resolution problems.

[Rob Lewis]

Eric Wieser said:

If you ask for more diagnostics, it looks less repetitive

Ah, yep. This seems to be the same idea as https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Why.20is.20.60int.2Ecast_abs.60.20so.20slow.3F (although I hvaen't figured out what defeq check kicks it off)

[Rob Lewis]

We don't have a good workaround for this yet, besides "wait for Lean 4," is that right?

[Gabriel Ebner]

wait for Lean 4

It's rather "check if it's got any better". Lean 4 still has nested TC problems, and (particularly failing) TC queries can still time out. It might be worth trying out the example in mathlib3port.

[Gabriel Ebner]

Sometimes I wonder if it would be better to assign type class meta variables like ?m_1 := { add := ?m_2, add_comm := ?m_3, ... } instead of doing nested TC synthesis.