Typeclasses (again)?

Stream: general

[Sebastien Gouezel]

I may be encountering a diamond problem, but this is way out of my league. I want to apply a result using the fact that ℝ is a topological space, and that its topology is generated by intervals (this is called orderable_topology). All these properties should be known to the system, but when I try to apply a theorem using these properties I get invalid apply tactic, failed to synthesize type class instance. So, I tried to fill in all the instances by hand, as in

haveI foo : orderable_topology ℝ := by apply_instance,
haveI bar : topological_space ℝ := by apply_instance,
apply @my_thm bar foo

but then I get the following complaint:

term
  foo
has type
  @orderable_topology ℝ
    (@uniform_space.to_topological_space ℝ
       (@metric_space.to_uniform_space' ℝ (@normed_field.to_metric_space ℝ real.normed_field)))
    real.partial_order
but is expected to have type
  @orderable_topology ℝ bar
    (@semilattice_inf.to_partial_order ℝ
       (@lattice.to_semilattice_inf ℝ
          (@conditionally_complete_lattice.to_lattice ℝ
             (@conditionally_complete_linear_order.to_conditionally_complete_lattice ℝ
                real.lattice.conditionally_complete_linear_order))))

Strangely, if I reverse the order of the instances

haveI bar : topological_space ℝ := by apply_instance,
haveI foo : orderable_topology ℝ := by apply_instance,

then the second instance is not accepted, with tactic.mk_instance failed to generate instance for orderable_topology ℝ.

Any idea of what is going on?

[Reid Barton]

haveI is like have, it doesn't make the definition visible. So I'm not surprised neither of these work.

[Chris Hughes]

try letI instead.

[Sebastien Gouezel]

Thanks. letI helped me to detect that my problem was not coming from the instances, contrary to what the error message says. Problem solved!