If the goal is to write higher-order type families, we can do that already -- and were able to do for a long time. For example, please see http://okmij.org/ftp/Haskell/TTypeable/TTypeable.hs that was written in 2012 for http://okmij.org/ftp/Haskell/typeEQ.html It shows the type-level function that checks for a membership in a type-level using the equality function supplied by a user as the first argument. Incidentally, here is the definition type instance Member f x NIL = HFalse type instance Member f x (h :/ t) = ORELSE (Apply f (x,h)) (CLOS AC_Member (f,x,t)) It was written before the modern syntax for type-level lists and booleans. This is an example of the general technique of defunctionalization.