[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
      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:                    |
-------------------------------------+-------------------------------------

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.

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`'''

--

Comment (by simonpj):

 Commits on `wip/T15952`:
 {{{
 commit b169960c5ed45a7b6fa35d2dbcb66f44128f6a38
 Author: Simon Peyton Jones <simonpj at microsoft.com>
 Date:   Wed Dec 5 08:43:59 2018 +0000

     Start on Trac #15952

     Actually it's working pretty well.  Just one error message regression
     in typecheck/should_fail/T15629.
 }}}
 and
 {{{
 commit 79d031326d614f6ca637b67a11949dab64afe728
 Author: Simon Peyton Jones <simonpj at microsoft.com>
 Date:   Wed Dec 5 12:25:14 2018 +0000

     Remove TcKind result for tc_infer_hs_type

     More cleaning up

     All works except a couple or piResultTys crashes in
        polykinds/T11399
        polykinds/T14174a

     due to using substTy (rather than nakedSubstTy) in
     piResultTys
 }}}
 and
 {{{
 commit a99a43bbb7a8a506f31307591b3ee8e9ba3c4c6f
 Author: Simon Peyton Jones <simonpj at microsoft.com>
 Date:   Thu Dec 6 09:24:44 2018 +0000

     Make tcTypeKind monadic

     This patch is work in progress on Trac #15952.

     IT DOES NOT COMPILE.

     The main payload is progress towards making tcTypeKind monadic.
     However I have not yet made a monadic version of tcEqType, nor
     changed all those tcEqType calls to a monadic context.  Hence,
     it won't compile as-is.

     I'm just parking the work I've done, on a branch,
     until I've had a chance to agree the path with Richard.

     (The previous patches on this branch /do/ compile and
     almost-completely validate.)
 }}}

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