Manifold-related typeclass resolution issue

Stream: lean4

[Geoffrey Irving]

Does anyone know the source of this typeclass resolution issue? MWE generated from some ComplexManifold code:

-- Typeclass resolution issue

def uncurry {α β φ : Type} : (α → β → φ) → α × β → φ := fun f a => f a.1 a.2

structure Model (H : Type) where

def Model.prod {A B : Type} (_ : Model A) (_ : Model B) : Model (A × B) where

class Manifold {H : Type} (I : Model H) (M : Type)

instance Manifold.prod {A B M N : Type} {I : Model A} {J : Model B} [Manifold I M] [Manifold J N] :
    Manifold (I.prod J) (M × N) where

def NiceAt {A B M N : Type} (I : Model A) (J : Model B) [Manifold I M] [Manifold J N]
    (_ : M → N) (_ : M) := True

theorem NiceAt.comp {A B C M N O : Type}
    {I : Model A} [Manifold I M]
    {J : Model B} [Manifold J N]
    {K : Model C} [Manifold K O]
    {f : N → O} {g : M → N} {x : M}
    (_ : NiceAt J K f (g x)) (_ : NiceAt I J g x) :
    NiceAt I K (fun x => f (g x)) x := True.intro

theorem NiceAt.prod {A B C M N O : Type}
    {I : Model A} [Manifold I M]
    {J : Model B} [Manifold J N]
    {K : Model C} [Manifold K O]
    {f : M → N} {g : M → O} {x : M}
    (_ : NiceAt I J f x) (_ : NiceAt I K g x) :
    NiceAt I (J.prod K) (fun x => (f x, g x)) x := True.intro

theorem Good {A M : Type} {I : Model A} [cm : Manifold I M]
    {h : M → M → M} {f : M → M} {g : M → M} {x : M}
    (ha : NiceAt (I.prod I) I (uncurry h) (f x, g x)) (fa : NiceAt I I f x) (ga : NiceAt I I g x) :
    NiceAt I I (fun x => h (f x) (g x)) x :=
  @NiceAt.comp A (A × A) A M (M × M) M I cm (I.prod I) _ I cm _ _ _ ha (fa.prod ga)

theorem Bad {A M : Type} {I : Model A} [cm : Manifold I M]
    {h : M → M → M} {f : M → M} {g : M → M} {x : M}
    (ha : NiceAt (I.prod I) I (uncurry h) (f x, g x)) (fa : NiceAt I I f x) (ga : NiceAt I I g x) :
    NiceAt I I (fun x => h (f x) (g x)) x :=
  ha.comp (fa.prod ga)

[Geoffrey Irving]

The Bad theorem produces

typeclass instance problem is stuck, it is often due to metavariables
  Manifold (?m.1279 ha fa ga) M

Good works, and is Bad with lots of implicit arguments filled in.

[Eric Wieser]

A shorter version of Good that works is ha.comp (I := I) (fa.prod ga)

[Geoffrey Irving]

I should be fixed by either ha or fa.prod ga, though, right? Probably I have a poor mental model for how inference works.

[Eric Wieser]

ha.comp (g := fun _ => (_, _)) (fa.prod ga) also works

[Eric Wieser]

I think Lean can't do the higher-order unification needed to work out g

[Geoffrey Irving]

Well, Lean 4 can't. Lean 3 could. :)

(I think. This was minimized from a porting issue.)

[Eric Wieser]

There's a tactic which means "create side goals for typeclass issues rather than failing", but I forget its name

[Floris van Doorn]

Lean 3 definitely also had similar issues with these kinds of issues - composing maps where the intermediate type is a product (though perhaps not this exact issue):
https://leanprover-community.github.io/mathlib_docs/notes.html#continuity%20lemma%20statement