type classes debugging

Stream: general

[Sebastien Gouezel]

A t2 space is a topological space with some separation property. Every metric space is a t2 space. If you try

lemma success {α : Type u} [metric_space α] (s : set α) : true :=
begin
  letI : t2_space s := by apply_instance,
  trivial
end

it works fine: the subset s of α inherits a metric space structure, and is therefore t2. Now, try

lemma fail (s : set ℝ) : true :=
begin
  letI : t2_space s := by apply_instance,
  trivial
end

This should be a special case of the previous one, but it loops forever. I have no idea how to debug this kind of behavior.

[Kenny Lau]

subtype.metric_space :
  Π {α : Type u_1} [_inst_1 : metric_space α] {p : α → Prop} [t : metric_space α], metric_space (subtype p)

problematic instance

[Kenny Lau]

orderable_topology.t2_space :
  ∀ {α : Type u_1} [_inst_1 : topological_space α] [_inst_2 : linear_order α] [t : orderable_topology α],
    t2_space α

ordered_topology.to_t2_space :
  ∀ {α : Type u_1} [_inst_1 : topological_space α] [_inst_2 : partial_order α] [t : ordered_topology α],
    t2_space α

Lean got stuck trying these two

[Kenny Lau]

because R has like 10000 properties

[Kenny Lau]

and the typeclass instance system is not clever enough

[Kenny Lau]

local attribute [instance, priority 0] orderable_topology.t2_space
local attribute [instance, priority 0] ordered_topology.to_t2_space

putting these two lines before the lemma is one solution @Sebastien Gouezel

[Sebastien Gouezel]

This works perfectly (and also in my use case, which involves subtypes of something more complicated than R). Thanks a lot! Could you tell us how you located the problematic instances?

[Kenny Lau]

I just... read through the instance trace

[Sebastien Gouezel]

Just to be sure: before the statement of the lemma, I insert

set_option trace.class_instances true
set_option class.instance_max_depth 15

(the second line to ensure that the process terminates in a reasonable amount of time, the first one to get access to the trace). Then if I put the cursor on apply_instance, I get access to the trace. There, I can see indeed a lot of @orderable_topology ↥s. And I can see at depth (0) that it tries @orderable_topology.t2_space, and gets stuck there. OK, thanks again, I think I will be able to do this by myself next time.

[Mario Carneiro]

Not sure I get what the problem is. Is the orderable_topology.t2_space a wrong turn for the typeclass inference? I guess R is an orderable topology so I don't see the problem

[Mario Carneiro]

Although I guess ordered_topology.to_t2_space implies orderable_topology.t2_space

[Reid Barton]

I think I had the same issue at https://leanprover.zulipchat.com/#narrow/stream/116395-maths/subject/t2_space/near/147451283

[Sebastien Gouezel]

I don't understand what is going on. The trace output is filled with entries like

[class_instances] (1) ?x_4 : @orderable_topology ↥s
  (@uniform_space.to_topological_space ↥s
     (@metric_space.to_uniform_space' ↥s
        (@subtype.metric_space ℝ real.metric_space (λ (x : ℝ), x ∈ s)
           (@normed_group.to_metric_space ℝ
              (@normed_space.to_normed_group ℝ ℝ real.normed_field
                 (@normed_field.to_normed_space ℝ real.normed_field))))))
  (@linear_order.to_partial_order ↥s
     (@subtype.linear_order ℝ
        (@linear_ordered_semiring.to_linear_order ℝ
           (@decidable_linear_ordered_semiring.to_linear_ordered_semiring ℝ real.decidable_linear_ordered_semiring))
        (λ (x : ℝ), x ∈ s))) := ennreal.orderable_topology
failed is_def_eq

or

[class_instances] (1) ?x_4 : @orderable_topology ↥s
  (@uniform_space.to_topological_space ↥s
     (@metric_space.to_uniform_space' ↥s
        (@subtype.metric_space ℝ real.metric_space (λ (x : ℝ), x ∈ s)
           (@normed_group.to_metric_space ℝ
              (@normed_space.to_normed_group ℝ ℝ real.normed_field
                 (@normed_field.to_normed_space ℝ real.normed_field))))))
  (@linear_order.to_partial_order ↥s
     (@subtype.linear_order ℝ
        (@decidable_linear_order.to_linear_order ℝ
           (@conditionally_complete_linear_order.to_decidable_linear_order ℝ
              real.lattice.conditionally_complete_linear_order))
        (λ (x : ℝ), x ∈ s))) := ennreal.orderable_topology
failed is_def_eq

or

[class_instances] (1) ?x_4 : @orderable_topology ↥s
  (@uniform_space.to_topological_space ↥s
     (@metric_space.to_uniform_space' ↥s
        (@subtype.metric_space ℝ real.metric_space (λ (x : ℝ), x ∈ s)
           (@normed_group.to_metric_space ℝ
              (@normed_ring.to_normed_group ℝ (@normed_field.to_normed_ring ℝ real.normed_field))))))
  (@linear_order.to_partial_order ↥s
     (@subtype.linear_order ℝ
        (@linear_ordered_semiring.to_linear_order ℝ
           (@linear_ordered_ring.to_linear_ordered_semiring ℝ
              (@linear_ordered_field.to_linear_ordered_ring ℝ
                 (@discrete_linear_ordered_field.to_linear_ordered_field ℝ real.discrete_linear_ordered_field))))
        (λ (x : ℝ), x ∈ s))) := ennreal.orderable_topology
failed is_def_eq

All of them are subtly different. There are so many ways to use the different structures on ℝ that it gives rise to an exponential blowup. And, while lean has not checked that all the possibilities fail, it will not go and try a more successful path.

[Kenny Lau]

surely depth-first search is troublesome... but that doesn't mean breadth-first search would have no problems

[Mario Carneiro]

aha, even though R is an orderable topology its subspaces aren't necessarily

[Mario Carneiro]

I think the top_space and linear_order arguments should be implicit in the two t2_space instances