Zulip Chat Archive

Stream: general

Topic: Type class caching failure


Rob Lewis (Jan 12 2022 at 14:58):

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 (Jan 12 2022 at 15:07):

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 (Jan 12 2022 at 15:11):

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 (Jan 12 2022 at 15:14):

If you ask for more diagnostics, it looks less repetitive

Gabriel Ebner (Jan 12 2022 at 15:50):

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

Rob Lewis (Jan 12 2022 at 15:51):

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 (Jan 12 2022 at 15:51):

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

Gabriel Ebner (Jan 12 2022 at 16:03):

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 (Jan 12 2022 at 16:07):

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.


Last updated: Dec 20 2023 at 11:08 UTC