Typeclass instance resolution stuck - is my fix sound?

Stream: new members

[Daniel Levin]

I've been working on a library independent of mathlib https://github.com/daniel-levin/Minimathlib/ to teach myself Lean.

Consider this diff: https://github.com/daniel-levin/Minimathlib/compare/mainline...tci

I find it very annoying to have to constantly ensure that subsets of X are open. I want to define a subtype of Set X that is open wrt to the topology. Why do round bracket binders and explicit parameters work and implicit ones don't?

Broken (typeclass instance problem is stuck, it is often due to metavariables TopologicalSpace ?m.366)

variable {X : Type u} [TopologicalSpace X]

open TopologicalSpace

def open_sets := { S : Set X // isOpen S}

theorem abc (S : open_sets) : True := by sorry

Happy:

variable {X : Type u} [TopologicalSpace X]

open TopologicalSpace

def open_sets (TS: Type u) [TopologicalSpace TS] := { S : Set TS // isOpen S}

theorem abc (S : open_sets X) : True := by sorry

[Etienne Marion]

In the first example, when you write theorem abc (S : open_sets) : True, you do not specify X and lean has no way of guessing it so it is stuck.