elaboration regression

Stream: general

[Patrick Massot]

I'm trying to recycle an old demo file but it seems Lean became worse at elaborating.

import topology.metric_space.basic

lemma foo {α : Type*} [metric_space α] {β : Type*} [metric_space β] {f : α → β} (h : continuous f) :
  continuous (λ p : α × α, dist (f p.1) (f p.2)) :=
continuous_dist.comp (h.prod_map h)
/-
  failed to synthesize type class instance for
  α : Type u_1,
  _inst_1 : metric_space α,
  β : Type u_2,
  _inst_2 : metric_space β,
  f : α → β,
  h : continuous f
  ⊢ topological_space (β × β)
-/

This is using Lean 3.34. 0. It works perfectly on Lean 3.18.4. Replacing lemma foo by example makes it work.
Also, using continuous_dist.comp (h.prod_map h : _) works. @Gabriel Ebner any idea?

[Gabriel Ebner]

I think this might be related to the recent changes with the universe levels and Floris' linter.

[Gabriel Ebner]

This is how the goal looks like:

⊢ @continuous.{(max u_2 ?l_1) 0} (prod.{(max u_2 ?l_1) (max u_2 ?l_1)} β β) real
    (@prod.topological_space.{(max u_2 ?l_1) (max u_2 ?l_1)} β β
       (@uniform_space.to_topological_space.{(max u_2 ?l_1)} β
          (@metric_space.to_uniform_space'.{(max u_2 ?l_1)} β (@metric_space.to_pseudo_metric_space.{u_2} β _inst_2)))
       (@uniform_space.to_topological_space.{(max u_2 ?l_1)} β
          (@metric_space.to_uniform_space'.{(max u_2 ?l_1)} β
             (@metric_space.to_pseudo_metric_space.{u_2} β _inst_2))))
    (@uniform_space.to_topological_space.{0} real (@metric_space.to_uniform_space'.{0} real real.pseudo_metric_space))
    (λ (p : prod.{(max u_2 ?l_1) (max u_2 ?l_1)} β β),
       @has_dist.dist.{(max u_2 ?l_1)} β
         (@pseudo_metric_space.to_has_dist.{(max u_2 ?l_1)} β (@metric_space.to_pseudo_metric_space.{u_2} β _inst_2))
         (@prod.fst.{(max u_2 ?l_1) (max u_2 ?l_1)} β β p)
         (@prod.snd.{(max u_2 ?l_1) (max u_2 ?l_1)} β β p))

[Gabriel Ebner]

The max u_2 ?l_1 is highly suspicious.

[Patrick Massot]

(deleted)

[Patrick Massot]

(deleted)

[Patrick Massot]

(deleted)

[Patrick Massot]

(deleted)

[Gabriel Ebner]

This part is weird, where the ?l_1 appears the first time in the trace:

[class_instances] (0) ?x_0 : topological_space.{?u_0} β := @uniform_space.to_topological_space.{?u_22} ?x_43 ?x_44
[type_context.is_def_eq_detail] [1]: topological_space.{?u_0} β =?= topological_space.{?u_22} ?x_43
[type_context.is_def_eq_detail] [2]: topological_space.{?u_0} =?= topological_space.{?u_22}
[type_context.is_def_eq_detail] process_assignment ?x_43 := β
[type_context.is_def_eq_detail] assign: ?x_43 := β
[class_instances] (1) ?x_44 : uniform_space.{?l__fresh.10.172} β := @Pi.uniform_space.{?u_23 ?u_24} ?x_45 ?x_46 ?x_47

[Patrick Massot]

There shouldn't be any Pi.uniform_space appearing

[Patrick Massot]

and indeed it doesn't appear in the goal you quoted

[Patrick Massot]

It seems the only difference is there is now a pseudo_metric_space class between metric_space and uniform_space

[Floris van Doorn]

Hmm... This is weird.
When replacing lemma by example (or equivalently, def), it works, but it makes β have type Type (max u_2 u_3), which is definitely undesired.

[Gabriel Ebner]

Patrick, the Pi.uniform_space is not what I wanted to show (and of course that type class instance doesn't apply here). The weird part is that applying the uniform_space.to_topological_space instance creates the ?l__fresh.10.172 universe metavariable, for no good reason.

[Gabriel Ebner]

An easy workaround for the lemma: continuous_dist.comp (h.prod_map h : _)

[Floris van Doorn]

As far as workarounds go, following the advice in #9954 we can replace the proof by (h.comp continuous_fst).dist (h.comp continuous_snd)

[Patrick Massot]

It's nice to see this workaround but it's clearly less natural than the original proof