[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:
       Component:  Compiler          |              Version:  8.6.2
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Description changed by simonpj:

Old description:

> 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.
>
> '''Work in progress on `wip/T15952`'''

New description:

 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.

 '''Work in progress on `wip/T15952`'''

 '''Merge request at
 [https://gitlab.haskell.org/ghc/ghc/merge_requests/74]'''

--

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