cached failure

Stream: general

[Kenny Lau]

import algebra.algebra.subalgebra

def foo (R : Type) [ring R] : subring R := ⊥

variables (R : Type) [comm_ring R]
set_option trace.class_instances true
set_option class.instance_max_depth 4
#check (by apply_instance : algebra (foo R) R)

[Kenny Lau]

This code times out (warning)

[Kenny Lau]

with error message being the following repeated a million times:

[class_instances] cached failure for @is_subring R (@comm_ring.to_ring R _inst_1) (@foo R (@comm_ring.to_ring R _inst_1)).carrier

[Kenny Lau]

What does "cached failure" mean?

[Gabriel Ebner]

Cached failure means that the type class code couldn't find an instance for this type before, and now doesn't bother again. (It has "cached the failure".)

[Gabriel Ebner]

This looks like a bug tbh.