subsingleton instance makes a structure timeout

Stream: general

[Junyan Xu]

Adding a subsingleton instance for an alg_hom type causes a structure definition in another file to (deterministically) timeout. One field of the structure is an alg_hom, which probably isn't a coincidence. Replacing the instance with lemma fixed the problem. Could anyone please diagnose the problem, and is it a known problem?

[Yaël Dillies]

#6025

[Eric Rodriguez]

this isn't in simp or anything, Yaël, it's a structure declaration

[Yaël Dillies]

I believe it's at least related.

[Junyan Xu]

This issue actually occurred after the simp issue was fixed in lean#665. I've confirmed that subsingleton instances make little difference on latest master (where they make a large difference before the fix to warrant a hack). However, the subsingleton instance introduced in #12455 still makes the subfield_with_hom structure timeout (after I merged latest master).

I'm not sure how to diagnose this, since set_option profiler true doesn't print anything for structure declaration. The following might offer some clues:

1. adding local attribute [-instance] is_localization.alg_hom_subsingleton before the structure declaration avoids the timeout.
2. replacing structure with class or @[class] structure avoids the timeout.
3. noncomputable and noncomputable! have no effect.

So now I'm curious how subsingleton instances are used in structure declarations and how they're not used in class declarations ...

[Junyan Xu]

So I searched structure among all options printed by #help options., and discovered the trace option trace.compiler.erase_trivial_structures. Once I enable it, I see the trace message

[compiler.erase_trivial_structures]
>> _interaction
tactic.mk_inj_eq

from the declaration structure subfield_with_hom :=, and it looks like it's the culprit, because src#tactic.mk_inj_eq uses congr, which is known to invoke subsingleton lemmas.

[Junyan Xu]

(sorry, wrong trace option above, now corrected.)

Looking at the docstring for erase_trivial_structures:

Remove constructor/projection/cases_on applications of trivial structures.
   We say a structure is trivial if it has only constructor and
   the constructor has only one relevant field.
   In this case, we use a simple optimization where we represent elements of this inductive
   datatype as the only relevant element.

it's plausible that Lean would try to show the field emb is irrelevant in structure subfield_with_hom in the presence of a subsingleton instance for alg_hom, and times out in the process:

structure subfield_with_hom :=
(carrier : subalgebra K L)
(emb : carrier →ₐ[K] M)

[Junyan Xu]

By the way I'm confused by We say a structure is trivial if it has only constructor: does it mean if "it has only one constructor? But doesn't all structures have only one constructor? Does it apply to inductive types other than structures?

[Mario Carneiro]

Yes, the logic is actually running on inductives so the "only one constructor" check is needed

[Junyan Xu]

I'll go with the local attribute [-instance] solution for now and see if it builds. I hope it's not a loop in typeclass inference that caused the timeout ...

[Junyan Xu]

The mathlib build succeeded, but the "dangerous_instance" linter isn't happy with the instance after all, probably because the submonoid M in the typeclass argument [is_localization M P] doesn't appear in the conclusion and hence become a "metavariable". I'd probably revert the instance to a lemma, but it's still puzzling why tactic.mk_inj_eq has issue with the instance while the rest of mathlib is OK with it ...

/- The `dangerous_instance` linter reports: -/
/- DANGEROUS INSTANCES FOUND.
These instances are recursive, and create a new type-class problem which will have metavariables.
Possible solution: remove the instance attribute or make it a local instance instead.

Currently this linter does not check whether the metavariables only occur in arguments marked with `out_param`, in which case this linter gives a false positive. -/
-- ring_theory/localization/basic.lean
#check @is_localization.alg_hom_subsingleton /- The following arguments become metavariables. argument 3: (M : submonoid R) -/