# Zulip Chat Archive

## 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):

In the stream https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/more.20type.20class.20inference.20issues I suggested:

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_param`

s 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_param`

s 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] (M : Type*) [topological_space M] [out_param $ manifold H M] extends has_groupoid H M (times_cont_diff_groupoid ⊤ 𝕜 E H) : Prop

#### Sebastian Ullrich (Sep 13 2019 at 12:55):

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 Is this still true with overlapping/incoherent instances?

#### Sebastian Ullrich (Sep 13 2019 at 12:58):

@Sebastien Gouezel Why are your `out_param`

s instance implicit? That looks very suspicious to me.

#### Sebastien Gouezel (Sep 13 2019 at 16:50):

Sebastien Gouezel Why are your

`out_param`

s instance implicit? That looks very suspicious to me.

Probably because I am not using them properly. I did not find any doc, and hardly any example, so I tried some things until it worked. With my current setup, it works very well: with the definition

variables (𝕜 : Type*) [nondiscrete_normed_field 𝕜] {E : Type*} [normed_group E] [normed_space 𝕜 E] {H : Type*} [topological_space H] [I : model_with_corners 𝕜 E H] {M : Type*} [topological_space M] [manifold H M] [smooth_manifold_with_corners 𝕜 E H M] {E' : Type*} [normed_group E'] [normed_space 𝕜 E'] {H' : Type*} [topological_space H'] [I' : model_with_corners 𝕜 E' H'] {M' : Type*} [topological_space M'] [manifold H' M'] [smooth_manifold_with_corners 𝕜 E' H' M'] include I I' def mdifferentiable_at (f : M → M') (x : M) := continuous_at f x ∧ differentiable_within_at 𝕜 (written_in_ext_chart_at 𝕜 x f) (range I.to_fun) ((ext_chart_at 𝕜 x).to_fun x)

I can write `mdifferentiable_at 𝕜 f x`

(where `𝕜`

is a normed field and `f : M → M'`

and `x : M`

), and Lean will infer by itself that it needs a manifold with corners structure on `M`

and `M'`

, and it will find all by itself about `E`

and `H`

and `I`

and `E'`

and `H'`

and `I'`

. Which is what I want to do differential geometry: when I want to talk about the derivative of a function, I just want to specify the field, and I am happy to let Lean fill in the gaps by itself.

As far as I understand, this is the goal of `out_param`

s, and with my current setup it works well. But maybe there is a better syntax, or outparams are not designed for this. I would be super happy to hear your thoughts about this! And I guess it could be useful to other people on this forum (I remember @Patrick Massot asking naive questions on outparams too).

#### Reid Barton (Sep 13 2019 at 17:02):

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 Is this still true with overlapping/incoherent instances?

Well, what is true in general is that instance search in GHC never backtracks

#### Sebastian Ullrich (Sep 14 2019 at 14:36):

Well, what is true in general is that instance search in GHC never backtracks

Sure. But that is not compatible with Lean's current model of instances from child to parent classes.

#### Sebastian Ullrich (Sep 14 2019 at 14:40):

As far as I understand, this is the goal of

`out_param`

s, and with my current setup it works well.

@Sebastien Gouezel Yes, `out_param`

s are made for situations like this, at least for parameters like `E`

. Does it still work if you remove the `out_param`

s from the instance parameters like `normed_group E`

? Is there any difference?

#### Sebastien Gouezel (Sep 14 2019 at 16:11):

If I remove the `out_param`

from the instance parameter, replacing `[out_param $ normed_group E]`

with `[normed_group E]`

, then it doesn't work any more: I get errors `don't know how to synthesize placeholder`

whenever I mention a `smooth_manifold_with_corners`

.

#### 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] instance forget_right : is_right_adjoint (monad.forget T) := { left := monad.free T , adj := monad.adj T } /- algebras.lean:12:42: error failed to synthesize type class instance for C : Type u₁, 𝒞 : category C, T : C ⥤ C ⊢ monad T -/

while this works

variables (T : C ⥤ C) --[monad.{v₁} T] instance forget_right [𝕋 : monad.{v₁} T] : is_right_adjoint (monad.forget T) := { left := monad.free T , adj := monad.adj T }

as does this

variables (T : C ⥤ C) [monad.{v₁} T] instance forget_right : is_right_adjoint (monad.forget T) := { left := monad.free T , adj := monad.adj 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.

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

Is it already an issue?

#### Bryan Gin-ge Chen (Mar 25 2020 at 16:12):

#### 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: Dec 20 2023 at 11:08 UTC