mysterious error related to outParam

Stream: mathlib4

[Scott Morrison]

I minimised this out of mathlib4#692 (@Riccardo Brasca attempting to remove unnecessary outParams):

class FunLike (F : Sort _) (α : outParam (Sort _)) (β : outParam <| α → Sort _) where
  coe : F → ∀ a : α, β a

instance (priority := 100) {F α β} [FunLike F α β] : CoeFun F fun _ => ∀ a : α, β a where coe := FunLike.coe

structure A (α : Type u) where

class S (F : Type _) (α β : outParam (Type _)) extends FunLike F α fun _ => β where

-- Comment out either this instance or this class, and the error goes away.
instance {α} [Add α] : Add (A α) := sorry
-- Replacing `[Add α]` with `[outParam (Add α)]` also kills the error.
class T (F : Type _) (α β : outParam (Type _)) [Add α] extends FunLike F α fun _ => β where

-- Errors with `function expected at f term has type F`:
example [S F α β] (f : F) (a b : α) : f a = f b := by
  sorry

Does anyone recognise what is going on? If not I'll report a Lean 4 issue.