Turn lemma into instance: error `cannot find synthesization

Stream: new members

[Michael Rothgang]

I'm trying to turn a lemma into an instance, but am getting errors I don't understand. MWE:

import Mathlib
variable {E : Type u} {𝕜 : Type u} [NontriviallyNormedField 𝕜]
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u} [TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H) {M : Type u} [TopologicalSpace M] [ChartedSpace H M]
  [HasGroupoid M (contDiffGroupoid 0 I)]

open Topology
lemma aux [FiniteDimensional 𝕜 E] [LocallyCompactSpace 𝕜] (hI : ModelWithCorners.Boundaryless I)
    {x : M} {n : Set M} (hn : n ∈ 𝓝 x) : ∃ s : Set M, s∈ 𝓝 x ∧ s ⊆ n ∧ IsCompact s  := by
  sorry -- proof omitted for brevity

-- This works. Question: how to turn this into an instance.
lemma Manifold.locallyCompact_of_finiteDimensional_of_boundaryless
    [FiniteDimensional 𝕜 E] [LocallyCompactSpace 𝕜] (hI : ModelWithCorners.Boundaryless I) : LocallyCompactSpace M := by
  exact { local_compact_nhds := fun x n hn ↦ aux I hI hn }

-- This fails with an error mentioning `cannot find synthesization order for instance ...` and
-- `all remaining arguments have metavariables:` with E and 𝕜 being metavariables.
instance [FiniteDimensional 𝕜 E] [LocallyCompactSpace 𝕜] [hI : ModelWithCorners.Boundaryless I] : LocallyCompactSpace M := by
  exact { local_compact_nhds := fun x n hn ↦ aux I hI hn }

-- Next attempt, mention E and 𝕜 explicitly: also fails -- with unchanged error?!
instance {E : Type u} {𝕜 : Type u} [NontriviallyNormedField 𝕜]
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u} [TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H) {M : Type u} [TopologicalSpace M] [ChartedSpace H M]
  [HasGroupoid M (contDiffGroupoid 0 I)]
  [FiniteDimensional 𝕜 E] [LocallyCompactSpace 𝕜] [hI : ModelWithCorners.Boundaryless I] : LocallyCompactSpace M := by
  exact { local_compact_nhds := fun x n hn ↦ aux I hI hn }

I've heard about classes, but not understood them in depth yet (obviously...). I'm cargo-culting here - perhaps somebody can tell me a fix before I've found the time to digest chapter 7 in MIL, including all the exercises...

[Michael Rothgang]

Code on the web editor

[Kevin Buzzard]

The typeclass inference system (the "square bracket system") is a big list of instances. An instance is either a term of a type which is a class (eg "the integers are a commutative ring") or a theorem or construction of the form "if you can find these instances then you can make this instance too" (eg "every commutative ring is an additive abelian group"). So if you try and apply a theorem about additive abelian groups to the integers, the system looks through this big list looking for either a proof that the integers are an additive abelian group, or a theorem which says that every field or whatever is an additive abelian group (and if it tried applying this, which it could well do, then it would start looking for a proof that the integers are a field). I think the computer scientists call this a prolog-like search. So basically the typeclass inference system is solving a big logic game, but one of the rules of the game is that it's only allowed to look at all the instances in the list it has.

Whenever you write variable [NormedSpace k E] the system makes a term inst_37 : NormedSpace k E and adds it to the list. And whenever a theorem has an input in square brackets, the typeclass inference system attempts to make this input using the algorithm and the things currently on the list. Note that instances have to be terms of classes. A class is simply a structure with an internal box ticked saying "I am a class and so the typeclass inference system should pay attention to me when performing its search". For example CommRing and AddCommGroup are classes, not just structures, they're structures with the box ticked.

That's the basics of how it works. I don't know my way around the manifold part of the library at all but now let me try to answer your question unless someone else gets there first

[Kevin Buzzard]

I think your error means "I'm not putting this on my list because I can see that my algorithm will never be able to use this instance" by the way

[Kevin Buzzard]

docs#ModelWithCorners.Boundaryless

[Kevin Buzzard]

Ok so that's a class so your lemma aux which works should definitely have this input in square brackets.

[Kevin Buzzard]

The error, I believe (on mobile and not in familiar territory) is that the typeclass inference system will never be able to find I (because it's not on the list) and hence will never be able to work out what k and E you're talking about. Edit: no that's not right because it can see the HasGroupoid instance. But it's complaining that the logic game it plays can't ever be won for some reason. If you hover over the working lemma, I'm assuming it must be using the HasGroupoid instance? I think I'll stop talking now and defer to a manifold expert.

[Michael Rothgang]

Thank you for the detailed response!

[Michael Rothgang]

Making aux take hI in square brackets doesn't suffice yet.
Hovering over the lemma, I can see the HasGroupoid instance is not shown either. Adding it in square brackets also doesn't suffice, though. Overall, the errors in the second example change slightly, but I still cannot figure them out...

[Michael Rothgang]

Updated code

[Kevin Buzzard]

I would set_option autoImplicit false during this phase to get more accurate error messages (otherwise lean just makes stuff up without you knowing)

[Michael Rothgang]

Good catch. Updated again. Now the error is definitely the same as in the beginning.