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):
Sebastien Gouezel (Nov 16 2018 at 22:04):
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