doc(elabissues): tc triggers nested tc, potentially with tmp-mvar leak

src/library/type_context.cpp

@@ -2411,9 +2411,14 @@ expr type_context_old::complete_instance(expr const & e) {
                 expr const & m = new_arg;
                 expr m_type    = instantiate_mvars(infer(m));
                 if (!has_expr_metavar(m_type) && is_class(m_type)) {
+                    lean_trace(name({"type_context", "complete_instance"}), tout() << "about to synth: " << m_type << "\n";);
                     if (mk_nested_instance(m, m_type)) {
                         new_arg = instantiate_mvars(new_arg);
                     }
+                } else if (is_class(m_type)) {
+                    if (is_class(m_type)) {
+                        lean_trace(name({"type_context", "complete_instance"}), tout() << "would have synthed: " << m_type << "\n";);
+                    }
                 }
             } else {
                 new_arg = complete_instance(new_arg);
@@ -3943,6 +3948,7 @@ mk_pp_ctx(type_context_old const & ctx) {
 
 void initialize_type_context() {
     register_trace_class("class_instances");
+    register_trace_class(name({"type_context", "complete_instance"}));
     register_trace_class(name({"type_context", "is_def_eq"}));
     register_trace_class(name({"type_context", "mvar_deps"}));
     register_trace_class(name({"type_context", "is_def_eq_detail"}));

tests/elabissues/leaky_tmp_metavars.lean

@@ -0,0 +1,44 @@
+/-
+Here is an artificial example where temporary metavariables created by typeclass resolution
+would otherwise leak into nested typeclass resolution unless we catch it.
+-/
+
+class Foo  (α : Type) : Type := (x : Unit)
+class Bar  (α : Type) : Type := (x : Unit)
+class HasParam (α : Type) [Bar α] : Type := (x : Unit)
+
+instance FooToBar (α : Type) [Foo α] : Bar α := {x:=()}
+
+-- Note: there is an implicit `FooToBar` inside the second argument of the return type.
+instance HasParamInst (α : Type) [h : Foo α] : HasParam α := {x:=()}
+
+class Top : Type := (x : Unit)
+
+-- Note: `AllFoo` is a weird, universal instance.
+instance AllFoo (α : Type) : Foo α := {x:=()}
+
+/-
+When the subgoal `[@HasParam α (@FooToBar α (AllFoo α))]` is triggerred, `α` is not known.
+
+This happens for two reasons:
+
+1. The return type `Top` does not include `α`.
+2. The universal `AllFoo α` instance obviates the need to take a building-block class as argument.
+
+Thus we would be tempted to call nested typeclass resolution on `Foo <tmp-mvar>`.
+-/
+instance Bad (α : Type) [HasParam α] : Top := Top.mk ()
+def foo [Top] : Unit := ()
+
+set_option pp.all true
+set_option trace.class_instances true
+set_option trace.type_context.complete_instance true
+
+#check @foo _
+
+/-
+[class_instances]  class-instance resolution trace
+[class_instances] (0) ?x_0 : Top := @Bad ?x_1 ?x_2
+[class_instances] (1) ?x_2 : @HasParam ?x_1 (@FooToBar ?x_1 (AllFoo ?x_1)) := @HasParamInst ?x_3 ?x_4
+[type_context.complete_instance] would have synthed: Foo ?x_3
+-/

tests/elabissues/leaky_tmp_metavars2.lean

@@ -0,0 +1,66 @@
+/-
+Here is an example where temporary metavariables from typeclass resolution
+could spill into nested typeclass resolution, for which the outer TC succeeds
+iff:
+
+1. the inner TC is still called, even with the leaked tmp mvars
+2. the inner TC is allowed to assign the leaked tmp mvars
+
+This example will *NOT* work in Lean4.
+
+Although it would be easy to allow inner TC to set the outer TC tmp mvars,
+the issue is that the solution to the inner TC problem may not be unique,
+and it would be extremely difficult to allow backtracking from the outer TC
+through to the inner TC.
+
+In Lean4, inner TC can be called with leaked temporary mvars from the outer TC,
+but they are treated as opaque, just as regular mvars are treated in the outer TC.
+So, this example will fail.
+-/
+
+class Foo  (α : Type) : Type := (x : Unit)
+class Zoo  (α : Type) : Type := (x : Unit)
+class Bar  (α : Type) : Type := (x : Unit)
+class HasParam (α : Type) [Bar α] : Type := (x : Unit)
+
+instance FooToBar (α : Type) [f : Foo α] : Bar α :=
+match f.x with
+| () => {x:=()}
+
+instance ZooToBar (α : Type) [z : Zoo α] : Bar α :=
+match z.x with
+| () => {x:=()}
+
+instance HasParamInst (α : Type) [h : Foo α] : HasParam α := {x:=()}
+
+class Top : Type := (x : Unit)
+
+instance FooInt : Foo Int := {x:=()}
+instance AllZoo (α : Type) : Zoo α := {x:=()}
+
+instance Bad (α : Type) [HasParam α] : Top := Top.mk ()
+
+set_option pp.all true
+set_option trace.class_instances true
+set_option trace.type_context.complete_instance true
+
+def foo [Top] : Unit := ()
+#check @foo _
+
+/-
+[class_instances]  class-instance resolution trace
+[class_instances] (0) ?x_0 : Top := @Bad ?x_1 ?x_2
+[class_instances] (1) ?x_2 : @HasParam ?x_1 (@ZooToBar ?x_1 (AllZoo ?x_1)) := @HasParamInst ?x_3 ?x_4
+[type_context.complete_instance] would have synthed: Foo ?x_3
+[type_context.complete_instance] would have synthed: Foo ?x_3
+failed is_def_eq
+-/
+
+def couldWork : Top :=
+@Bad Int (@HasParamInst Int FooInt)
+
+#print couldWork
+/-
+def couldWork : Top :=
+@Bad Int (@HasParamInst Int FooInt)
+-/

tests/elabissues/typeclass_triggers_typeclass.lean

@@ -0,0 +1,33 @@
+/-
+Here is an example where typeclass resolution triggers nested typeclass resolution.
+-/
+
+class Ring   (α : Type) : Type := (x : Unit)
+class Double (α : Type) : Type := (x : Unit)
+class Foo    (α : Type) [Double α] : Type := (x : Unit)
+
+instance RingToDouble (α : Type) [Ring α] : Double α := Double.mk α ()
+
+-- Note: The return type is really `@Foo α (@RingToDouble α s)`.
+instance RingFoo (α : Type) [s : Ring α] : Foo α := Foo.mk α ()
+
+instance RingInt : Ring Int := Ring.mk Int ()
+instance DoubleInt : Double Int := Double.mk Int ()
+
+def foo [@Foo Int DoubleInt] : Unit := ()
+
+set_option pp.all true
+set_option trace.class_instances true
+set_option trace.type_context.complete_instance true
+
+#check @foo _
+
+/-
+[class_instances]  class-instance resolution trace
+[class_instances] (0) ?x_0 : @Foo Int DoubleInt := @RingFoo ?x_1 ?x_2
+[type_context.complete_instance] about to synth: Ring Int
+[class_instances]  class-instance resolution trace
+[class_instances] (0) ?x_3 : Ring Int := RingInt
+[class_instances] (1) ?x_2 : Ring Int := RingInt
+@foo (@RingFoo Int RingInt) : Unit
+-/