# Zulip Chat Archive

## 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: Dec 20 2023 at 11:08 UTC