Idiomatic type families

Stream: new members

[Eric Conlon]

Hi all, I'm trying to figure out how I would encode type families a la Haskell. (For example, Base in Data.Functor.Foldable from recursion-schemes) The best I can come up with is something approximating fundeps:

class Base (g : Type u) (f : outParam (Type u -> Type u))

instance {a : Type u} : Base (List a) (ListF a) where

class Recursive (g : Type u) (f: outParam (Type u -> Type u)) extends Base g f where
  project : g -> f g

Please teach me how to make this idiomatic Lean! Thanks :)