Type patterns are used in instance heads: class instances, type instances, and data/newtype instances. These type patterns differ from ordinary types in several ways:

• They must never mention a forall.
• They must never mention a context. (The context in a class instance head is a different part of the instance construct.)
• They must never mention a type family.

Types that appear as arguments on the LHS of a RULE should also be type patterns.

Type patterns are used in GHC differently than types as well: we should match only against patterns, never ordinary types.

I thus propose that a new datatype within GHC to store type patterns. I'll call it TyPat here, but perhaps a longer name is better. The matcher (in the Unify module) would then take a TyPat parameter, making clear which type is the template and which is the concrete instantiation.

We could have a new algorithm to typecheck/desugar source syntax into patterns. This new algorithm could accommodate issues like those mentioned in ticket:14038#comment:140786. It could also avoid ever putting a type family in a kind parameter, which would fix #12564. Separating out checking type patterns from proper types could also improve GADT pattern matching in types, which is currently more like "wobbly types" than OutsideIn.