[GHC] #15952: Reduce zonking-related invariants in the type checker

[GHC]

#15952: Reduce zonking-related invariants in the type checker
-------------------------------------+-------------------------------------
           Reporter:  goldfire       |             Owner:  (none)
               Type:  task           |            Status:  new
           Priority:  normal         |         Milestone:  8.6.3
          Component:  Compiler       |           Version:  8.6.2
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 The type checker currently maintains two invariants, documented in `Note
 [The well-kinded type invariant]` in TcType and `Note [The tcType
 invariant]` in TcHsType. These are a pain to maintain, and Simon and I
 cooked up a plan not to.

 Step 1. The tcType invariant is all about `tcInferApps`, at least
 according to the Note. Previously, we couldn't zonk in `tcInferApps`,
 because types were knot-tied. But now we can! So, `tcInferApps` could take
 the type only (not its kind), zonk it, then get the type's (zonked) kind.
 This might also mean that `tc_infer_hs_type` no longer needs to return a
 type/kind pair, but could just return a type.

 After this is done, we can likely remove all the zonks that are in service
 to the tcType invariant, findable by a search.

 Step 2. The well-kinded type invariant is also about the need to zonk
 sometimes. But, instead, we could just always zonk on-the-fly. That is, we
 introduce new functions like `tcTypeKind` and `tcSubstTy` that zonk as
 they go. To make sure we're calling the right function at the right time,
 we introduce `newtype TcType = TcType { unTcType :: Type }`. Then, we're
 forced to call monadic functions on `TcType`s. This will likely lead to
 code duplication between `Type` and `TcType`, but we might be able to
 banish `zonkTcType` (and its many friends) entirely. Also gone would be
 the `naked` functions, which are all about maintaining the well-kinded
 type invariant. This step would, as a side effect, fix #15799 and #15918,
 which is about treating `TcType`s differently from `Type`s.

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