[GHC] #14119: Refactor type patterns

[GHC]

#14119: Refactor type patterns
-------------------------------------+-------------------------------------
           Reporter:  goldfire       |             Owner:  (none)
               Type:  task           |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.1
           Keywords:  TypeInType     |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:  12564, 14038   |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 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 comment:6:ticket:14038. 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.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14119>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler