Type search problem

Stream: general

[Heather Macbeth]

The following error was observed by @Nicolò Cavalleri in #6981 while trying to define a docs#smooth_manifold_with_corners object. By definition smooth_manifold_with_corners is a special case of docs#has_groupoid:

class smooth_manifold_with_corners [*** a bunch of variables ***] extends
  has_groupoid M (times_cont_diff_groupoid ∞ I) : Prop

In this situation we have an existing has_groupoid and are trying to exhibit a smooth_manifold_with_corners. Lean cannot find one of the instances it requires; on the other hand, if you try to provide it, Lean complains that it conflicts with the expected instance. Is there a workaround?

import geometry.manifold.smooth_manifold_with_corners

open_locale manifold

variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
  {E : Type*} [normed_group E] [normed_space 𝕜 E]
  {H : Type*} [topological_space H] (I : model_with_corners 𝕜 E H)
  {M : Type*} [topological_space M]
  (e : local_homeomorph M H) (h : e.source = set.univ)

/-
failed to synthesize type class instance for
....
⊢ charted_space H M
-/
example : @smooth_manifold_with_corners 𝕜 _ E _ _ H _ I M _ (singleton_charted_space e h) :=
{ .. singleton_has_groupoid e h (times_cont_diff_groupoid ∞ I) }

/-
synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  ⁇
inferred
  singleton_charted_space e h
-/
example : @smooth_manifold_with_corners 𝕜 _ E _ _ H _ I M _ (singleton_charted_space e h) :=
{ .. (singleton_has_groupoid e h (times_cont_diff_groupoid ∞ I) :
  @has_groupoid H _ M _ (singleton_charted_space e h) (times_cont_diff_groupoid ∞ I)) }

[Mario Carneiro]

One way to suppress type class inference for an argument is to use (id _) instead of _

[Heather Macbeth]

Thanks for the hint. Do you have time to play with the example a little? I tried some ids in various places but couldn't get it working.

[Mario Carneiro]

The closest equivalent I found was

example : @smooth_manifold_with_corners 𝕜 _ E _ _ H _ I M _ (singleton_charted_space e h) :=
@smooth_manifold_with_corners.mk _ _ _ _ _ _ _ _ _ _ (id _) $
@has_groupoid.compatible _ _ _ _ (id _) _ $
singleton_has_groupoid e h (times_cont_diff_groupoid ∞ I)

[Mario Carneiro]

those typeclass args don't seem like a very good idea if you have to stub them out like this a lot

[Mario Carneiro]

You can make that a bit simpler with an alternate constructor for smooth_manifold_with_corners:

theorem smooth_manifold_with_corners.mk' {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
  {E : Type*} [normed_group E] [normed_space 𝕜 E]
  {H : Type*} [topological_space H] (I : model_with_corners 𝕜 E H)
  (M : Type*) [topological_space M] [charted_space H M]
  [gr : has_groupoid M (times_cont_diff_groupoid ∞ I)] :
  smooth_manifold_with_corners I M := {..gr}

example : @smooth_manifold_with_corners 𝕜 _ E _ _ H _ I M _ (singleton_charted_space e h) :=
@smooth_manifold_with_corners.mk' _ _ _ _ _ _ _ _ _ _ (id _) $
singleton_has_groupoid e h (times_cont_diff_groupoid ∞ I)

[Heather Macbeth]

Thank you!