Zulip Chat Archive

Stream: general

Topic: Typeclasses (again)?


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Chris Hughes (Nov 16 2018 at 21:55):

try letI instead.

view this post on Zulip 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