When doing type level programming you often need a way to report errors. I suggest a closed type family called Error with special semantics. It is kinded like this Error :: Symbol -\> k1 -\> k2 If this function has to be reduced during constraint solving it will simply generate a type error with the given string and printing the type as extra information (this kind can be generalized a lot if we want to). I've found that having this function gives more accurate and earlier error messages. Wiki design page: [Proposal/CustomTypeErrors](proposal/custom-type-errors)