Strange typeclass resolution with extends

Stream: lean4

[Eric Conlon]

I defined a Traversable typeclass that extends Functor, but Lean doesn't like it. Am I doing something wrong?

class Traversable (f : Type u -> Type u) extends Functor f where
  traverse : {m : Type u -> Type u} -> [Applicative m] -> {a b : Type u} -> (a -> m b) -> f a -> m (f b)

inductive ProdF (f : Type u -> Type u) (g : Type u -> Type u) (a : Type u) where
  | mk : f a -> g a -> ProdF f g a

instance {a : Type u} [Functor f] [Functor g] : Functor (ProdF f g) where
  map f
    | .mk fa ga => .mk (Functor.map f fa) (Functor.map f ga)

-- Error: fields missing: 'map'
instance {a : Type} [Traversable f] [Traversable g] : Traversable (ProdF f g) where
  traverse f
    | .mk fa ga => .mk <$> Traversable.traverse f fa <*> Traversable.traverse f ga

-- Adding map := Functor.map yields error: failed to synthesize instance Functor (ProdF f g)

Specifically, if I have Traversable extend Functor, then Lean demands an implementation of map. If I try to default it to Functor.map then it can't figure out that I already have a Functor f instance in scope because I have a Traversable f.

If instead I depends on a Functor superclass like class Traversable (f : Type -> Type) [Functor f] where then Lean fails to synthesize a Functor instance for f when I define Traversable (ProdF f g). If I then add [Functor f] to that instance context, it fails to synthesize Functor (ProdF f g), even though the appropriate instances are in scope! This has to be a bug.

[Eric Wieser]

set_option pp.universes true should make the problem clear

[Eric Wieser]

Your Functor instance has a useless argument that causes it not to fire

[Eric Conlon]

OMG you are so right.

[Eric Wieser]

If you add import Std.Tactic.Lint then #lint will tell you this

[Eric Conlon]

Thank you Eric! I added require std from git "https://github.com/leanprover/std4" @ "main" to pick up std and lint is showing me quite a few issues.