Yves Pare`s wrote:

So I'm trying to make a type level function to test if a type list contains a type. Unless I'm wrong, that calls to the use of a type family.

More crucially, list membership also calls for an equality predicate. Recall, List.elem has the Eq constraint; so the type-level membership test should have something similar, a similar equality predicate. As you have discovered, type equality is quite non-trivial. All is not lost however. If we `register' all the types or type constructors, we can indeed write a type-level membership function. In fact, http://okmij.org/ftp/Haskell/TTypeable/ShowListNO.hs does exactly that. It uses the type-level (and higher-order) function Member to test if a given type is a one of the chosen types. If it is, a special instance is selected. Please see http://okmij.org/ftp/Haskell/typeEQ.html#TTypeable http://okmij.org/ftp/Haskell/typeEQ.html#without-over for explanations.