## Stream: general

### Topic: Typeclasses (again)?

#### Sebastien Gouezel (Nov 16 2018 at 21:49):

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 (Nov 16 2018 at 21:54):

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

#### Chris Hughes (Nov 16 2018 at 21:55):

try letI instead.

#### Sebastien Gouezel (Nov 16 2018 at 22:04):

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

Last updated: May 09 2021 at 20:11 UTC