Zulip Chat Archive

Stream: general

Topic: cached failure


view this post on Zulip Kenny Lau (Oct 20 2020 at 10:08):

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)

view this post on Zulip Kenny Lau (Oct 20 2020 at 10:08):

This code times out (warning)

view this post on Zulip Kenny Lau (Oct 20 2020 at 10:08):

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

view this post on Zulip Kenny Lau (Oct 20 2020 at 10:09):

What does "cached failure" mean?

view this post on Zulip Gabriel Ebner (Oct 20 2020 at 10:16):

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".)

view this post on Zulip Gabriel Ebner (Oct 20 2020 at 10:16):

This looks like a bug tbh.


Last updated: May 13 2021 at 18:26 UTC