Instance resolution failures

Stream: general

[Sebastian Ullrich]

@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]

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

[Mario Carneiro]

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]

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]

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]

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]

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

[Sebastian Ullrich]

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]

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

[Scott Morrison]

@Keeley Hoek which did you have in mind?

[Keeley Hoek]

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]

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

[Keeley Hoek]

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]

@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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Scott Morrison]

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]

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]

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

[Sebastien Gouezel]

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

[Reid Barton]

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]

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]

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

[Sebastien Gouezel]

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]

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]

@Sebastien Gouezel Why are your out_params instance implicit? That looks very suspicious to me.

[Sebastien Gouezel]

Sebastien Gouezel Why are your out_params 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_params, 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]

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]

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]

As far as I understand, this is the goal of out_params, and with my current setup it works well.

@Sebastien Gouezel Yes, out_params are made for situations like this, at least for parameters like E. Does it still work if you remove the out_params from the instance parameters like normed_group E? Is there any difference?

[Sebastien Gouezel]

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]

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]

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

[Wojciech Nawrocki]

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

[Reid Barton]

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

[Reid Barton]

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]

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

[Reid Barton]

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]

Can this bug be fixed in community lean?

[Reid Barton]

I think it should be easy.

[Kevin Buzzard]

Is it already an issue?

[Bryan Gin-ge Chen]

lean#146

[Kevin Buzzard]

Oh nice, will hopefully be fixed in 3.8

[Reid Barton]

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