Zulip Chat Archive

Stream: general

Topic: Instance resolution failures


view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Sep 08 2019 at 17:57):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Keeley Hoek (Sep 09 2019 at 09:20):

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

view this post on Zulip Scott Morrison (Sep 09 2019 at 09:36):

@Keeley Hoek which did you have in mind?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Sep 10 2019 at 08:18):

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

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip Kenny Lau (Sep 10 2019 at 11:21):

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

view this post on Zulip Sebastien Gouezel (Sep 10 2019 at 11:27):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Sebastian Ullrich (Sep 13 2019 at 12:58):

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

view this post on Zulip Sebastien Gouezel (Sep 13 2019 at 16:50):

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).

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Sebastian Ullrich (Sep 14 2019 at 14:40):

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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Wojciech Nawrocki (Mar 25 2020 at 15:53):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 25 2020 at 16:11):

Can this bug be fixed in community lean?

view this post on Zulip Reid Barton (Mar 25 2020 at 16:12):

I think it should be easy.

view this post on Zulip Kevin Buzzard (Mar 25 2020 at 16:12):

Is it already an issue?

view this post on Zulip Bryan Gin-ge Chen (Mar 25 2020 at 16:12):

lean#146

view this post on Zulip Kevin Buzzard (Mar 25 2020 at 16:14):

Oh nice, will hopefully be fixed in 3.8

view this post on Zulip 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