## Stream: general

### Topic: Instance resolution failures

#### Sebastian Ullrich (Sep 08 2019 at 17:46):

@Chris Hughes

I made a repository of examples of type class failures in Lean 3. Most of them depend on using some old commit of mathlib. The respository is here

Thanks, this is a good first step. If we want to get serious about analyzing and fixing these issues in Lean 4 (I hope nobody expects a solution for Lean 3), it would help tremendously to reduce them to minimized examples in stand-alone files (we want to port mathlib to Lean 4 after fixing these issues after all). If they are already valid Lean 4, even better. We may even want to port them to other systems to analyze their behavior.

#### Mario Carneiro (Sep 08 2019 at 17:57):

It's not hard to cook up artificial examples, but I thought you wanted real examples

#### Mario Carneiro (Sep 08 2019 at 17:58):

In short it checks the same typeclass problem many times. This causes issues with looping instances, and exponential worst case behavior on dags

#### Sebastian Ullrich (Sep 08 2019 at 20:55):

We'd like to have realistic examples, but we'll still need to extract them if we want to test them in Lean 4

#### Floris van Doorn (Sep 09 2019 at 00:23):

Here is an unrealistic example which shows that diamonds cause an exponential blow-up in the type class inference search:

-- Lean 3 code
set_option old_structure_cmd true
class bottom (α : Type) (n : ℕ) := (x : bool)
class left (α : Type) (n : ℕ) extends bottom α n
class right (α : Type) (n : ℕ) extends bottom α n
class top (α : Type) (n : ℕ) extends left α n, right α n

instance unrealistic_loop (α n) [bottom α n] : top α n.succ := { .._inst_1 }

set_option trace.class_instances true
example : top unit 10 := by apply_instance -- fails, but slowly


Even though this example is unrealistic, diamonds occur all over the algebraic hierarchy, and I don't think there is a way avoiding diamonds from the algebraic hierarchy. And this is not a large amount of diamonds, there is already a significant slowdown with 11 diamonds on top of each other. I think mathlib has more diamonds (more parallel instead of serial).

#### Floris van Doorn (Sep 09 2019 at 00:24):

There should really be a different algorithm for these "forgetful instances". Make a graph of all instances that change the class but not the type (like add_comm_group \a -> add_group \a) and when you have searched through all structural instances (or all instances with priority >= default priority), then use a graph reachability algorithm to quickly search for a path to any instance in the local context.

#### Floris van Doorn (Sep 09 2019 at 00:41):

I don't know if that is the best way to deal with diamonds, but it should avoid the exponential blowup.

#### Sebastian Ullrich (Sep 09 2019 at 08:11):

Thanks Floris. So are repeated (metavariable-free) instance problems the only big issue? Are out_params more or less well behaved or were there fundamental issues as well?

#### Keeley Hoek (Sep 09 2019 at 09:20):

@Scott Morrison do you think the category theory morphism problems deserve a mention here?

#### Scott Morrison (Sep 09 2019 at 09:36):

@Keeley Hoek which did you have in mind?

#### Keeley Hoek (Sep 09 2019 at 09:37):

I meant the whole business with having to specify the morphism universe everywhere because the resolver can't be coerced into being more aggressive.

#### Scott Morrison (Sep 09 2019 at 09:39):

Oh, I see. Yes, it would be lovely if instance resolution would specialise universes in preference to failing.

#### Keeley Hoek (Sep 09 2019 at 09:43):

I'm not so familiar with out_param, but maybe an annotation like that saying to aggressively unify could be a fix.

#### Floris van Doorn (Sep 10 2019 at 05:25):

@Sebastian Ullrich I don't feel confident to judge whether this is the only issue. My gut feeling is that there are more issues, but it's not always easy to say which problem is causing a type class search to time out.
I have not worked with out_params myself, so I cannot judge judge them.

#### Rob Lewis (Sep 10 2019 at 05:39):

What's your timeline for collecting examples here? I'm limiting my Zulip time right now because I have too much else going on. But there are some bad instance searches I half-remember, and probably have saved on my office computer, I can try to write up once I get back there.

#### Sebastian Ullrich (Sep 10 2019 at 08:02):

@Rob Lewis There are always other things to work on for us, so I'd say take your time

#### Mario Carneiro (Sep 10 2019 at 08:15):

out_param is finicky to use correctly, but AFAIK it doesn't cause any performance problems other than the preexisting ones

#### Mario Carneiro (Sep 10 2019 at 08:16):

I would say as long as you can make it not asymptotically exponential everything else will be minor

#### Mario Carneiro (Sep 10 2019 at 08:18):

TBH it's surprisingly fast considering how much work it is currently doing

#### Scott Morrison (Sep 10 2019 at 08:39):

I wonder if just looking through the 53 current instances of set_option class.instance_max_depth ... in mathlib would provide some interesting examples.

#### Sebastien Gouezel (Sep 10 2019 at 11:17):

Orthogonal to instance failures, but the following has been painful for me in manifolds.

class my_source (α : Type) := (source : set α)
lemma foo (α : Type) (A : set (my_source α)) : ∀e ∈ A, e.source = e.source


is not understood by Lean, as it is not able to infer the type of e in the statement of foo (even though e ∈ A should tell everything). So I have to give explicitly the type of e, which is not bad here but can be bad in more complicated instances. I know unification is complicated, but still...

#### Kenny Lau (Sep 10 2019 at 11:21):

I think the issue is that you shouldn't use projection with class.

#### Sebastien Gouezel (Sep 10 2019 at 11:27):

Sorry, I shouldn't have used class. Same outcome with structure instead.

#### Reid Barton (Sep 11 2019 at 21:22):

Here is a pretty egregious failure:

import algebra.module
set_option trace.class_instances true
example {T : Type} (t : T) : T := (1 : ℚ) • t


Obviously the search has_scalar ℚ T cannot succeed, but this is not obvious to Lean

#### Reid Barton (Sep 11 2019 at 21:23):

I know I keep going on about GHC, but in GHC this kind of thing will fail in constant* time
(* okay, probably logarithmic in something)

#### Reid Barton (Sep 11 2019 at 21:24):

regardless of the number of classes or instances in the system or the depth of the class hierarchy

#### Sebastien Gouezel (Sep 12 2019 at 13:35):

I just stumbled on a behavior I don't understand. Involving out_params, structures and typeclasses, so something a little bit exotic and probably the behavior will be completely different in Lean 4, but still let me record it here. Everything is fine with

def local_homeomorph.is_mdifferentiable (f : local_homeomorph M M') :=
(mdifferentiable_on 𝕜 f.to_fun f.source) ∧ (mdifferentiable_on 𝕜 f.inv_fun f.target)

lemma mdifferentiable_atlas (h : e ∈ atlas M H) : e.is_mdifferentiable 𝕜 :=
⟨mdifferentiable_on_atlas_to_fun 𝕜 h, mdifferentiable_on_atlas_inv_fun 𝕜 h⟩


But if I switch the definition to a structure, with

structure local_homeomorph.is_mdifferentiable (f : local_homeomorph M M') : Prop :=
(diff_to_fun : mdifferentiable_on 𝕜 f.to_fun f.source)
(diff_inv_fun : mdifferentiable_on 𝕜 f.inv_fun f.target)


then the lemma is not accepted any more, failing with 4 messages

don't know how to synthesize placeholder
context:
𝕜 : Type u_1,
_inst_1 : nondiscrete_normed_field 𝕜,
E : Type u_2,
_inst_2 : normed_group E,
_inst_3 : normed_space 𝕜 E,
H : Type u_3,
_inst_4 : topological_space H,
I : model_with_corners 𝕜 E H,
M : Type u_4,
_inst_5 : topological_space M,
_inst_6 : manifold H M,
_inst_7 : smooth_manifold_with_corners 𝕜 E H M,
e : local_homeomorph M H,
h : e ∈ atlas M H
⊢ Type ?


I have several typeclass variables in scope, and I guess the main missing piece of information is the only exotic typeclass definition with outparams, i.e.,

/- Specialization to the case of smooth manifolds with corners, over a field 𝕜 and with infinite
smoothness to simplify.
The set E is a vector space, and H is a model with corners based on E.
When 𝕜 is fixed, the model space with corners (E, H) should always be the same for a
given manifold M. Therefore, we register it as an out_param: it will not be necessary to write
it out explicitely when talking about smooth manifolds. This is the main point of this definition. -/
class smooth_manifold_with_corners (𝕜 : Type*) [nondiscrete_normed_field 𝕜]
(E : out_param $Type*) [out_param$ normed_group E] [out_param $normed_space 𝕜 E] (H : out_param$ Type*) [out_param $topological_space H] [I : out_param$ model_with_corners 𝕜 E H]

#### Wojciech Nawrocki (Mar 25 2020 at 14:52):

Why does Lean fail to synthesize a typeclass after I name it in a variables block? That is, given the prelude

import category_theory.monad
open category_theory
universes v₁ v₂ v₃ u₁ u₂ u₃ -- declare the v's first; see category_theory.category for an explanation
variables {C : Type u₁} [𝒞 : category.{v₁} C]
include 𝒞


the following fails

variables (T : C ⥤ C) [𝕋 : monad.{v₁} T]

/- algebras.lean:12:42: error
failed to synthesize type class instance for
C : Type u₁,
𝒞 : category C,
T : C ⥤ C


while this works

variables (T : C ⥤ C) --[monad.{v₁} T]


as does this

variables (T : C ⥤ C) [monad.{v₁} T]


What does adding the name do that breaks inference?

#### Reid Barton (Mar 25 2020 at 15:01):

The category theory stuff is a distraction! The auto-inclusion of [] variables only occurs for ones that are not named, I think.

#### Wojciech Nawrocki (Mar 25 2020 at 15:08):

Do you know why that is? Is it to make sure I don't refer to the particular instance?

#### Reid Barton (Mar 25 2020 at 15:43):

It is just a design choice I think. I mean, the default is to not include variables.

#### Reid Barton (Mar 25 2020 at 15:44):

For unnamed [] variables the rule is just always include all those that mention an included variable. It doesn't include them only if they are actually needed or anything like that.

#### Wojciech Nawrocki (Mar 25 2020 at 15:53):

Ah right, so that's why we need include 𝒞. Thanks!

#### Reid Barton (Mar 25 2020 at 16:07):

The business with 𝒞 is a specific Lean bug related to the fact that category C has a universe variable which doesn't appear in the type of C. Otherwise we wouldn't name 𝒞 either.

#### Kevin Buzzard (Mar 25 2020 at 16:11):

Can this bug be fixed in community lean?

#### Reid Barton (Mar 25 2020 at 16:12):

I think it should be easy.

lean#146

#### Kevin Buzzard (Mar 25 2020 at 16:14):

Oh nice, will hopefully be fixed in 3.8

#### Reid Barton (Mar 25 2020 at 16:15):

when I looked at this originally (long before the community fork) it seemed that the elaborator basically already had the machinery to do this, it just wasn't being used in this particular case

Last updated: May 13 2021 at 19:20 UTC