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

Comment (by simonpj):

 I have made some progress here, all on `wip/T15952`.

 A big goal is to sweep away two tricky invariants:

 * `Note [The well-kinded type invariant]` in `TcType`, which asked that
 `tcTypeKind` would work even before zonking.  But that led to the horrible
 need to maintain even Refl casts, because we might have `((a::kappa)
 (b::Type))` where `kappa` is a unification variable that has already been
 unified `kappa := Type -> Type`.  This is only well-kinded if we can see
 through that unification variable.  So previously we used `mkNakedCastTy`
 to add a stupid Refl cast.  `((a::kappa) |> (Refl (Type->Type))
 (b::Type)`.  Not only is this unsavory, but it's also very fragile: many
 functions (e.g. substitution) eliminate that Refl cast.

 * `Note [The tcType invariant]` in `TcHsType`.   This was closely related,
 and was a delicate invariant about the result kind of `tc_hs_type`.  It
 forced a bunch of invariants on related functions.

 The good news is that I was able to completely dispense with both
 invariants.
 I've introduced
 * `Type.tcTypeKind :: TcType -> TcKind`.  This is non-monadic, but
 respects the distinction between `Type` and `Constraint`.
 * `TcMType.tcTypeKindM :: TcType -> TcM TcKind`.  This one is monadic, and
 looks through unification variables.
 You can call the former on any zonked `TcType`; but if the type may be
 well-kinded only after zonking, you must use the latter.

 It's always safe to use `tcTypeKindM`, but there are some times when it is
 clearly safe to call `tcTypeKind`, and very convenient do to so without
 resorting to the monad, such as in `TcErrors`.  Sadly, it's not clear at
 every call site which is the right one.

 A number of other functions had to become monadic too
 * `tcEqTypeM` (because it calls `tcTypeKindM`)
 * `piResultTysM` (needed by `tcTypeKindM`)
 * `splitPiTyInvisibleM`
 * `invisibleTyBndrCountM`
 * `tcTupKindSortM`
 * `tcIsConstraintKindM`
 * `isPredTyM`
 All these functions appear together in `TcMType`.

 All the mkNakedX functions go away, which is great.

 This is all good, but I'm still unhappy.

 * There are many calls to `isPredTy`, just to distinguish `->` from `=>`.
 And we need `isPredTyM` now.  I think we should just add an `ArgFlag` to
 `FunTy`.

 * These changes did not solve #15918 as we thought it would.  The cause of
 #15918 is that `mkCastTy` calls `isReflexiveCo`, which does not respect
 the distinction between `Type` and `Constraint`.  The reason `mkCastTy`
 calls the blunderbuss `isReflexiveCo` is described in `Note [Respecting
 definitional equality]` in `TyCoRep`.

   So do we need a `mkTcCastTy`, wich ''does'' respect the
 `Type`/`Constraint` distinction?  And thence `mkTcAppTy` (since `mkAppTy`
 calls `mkCastTy`), and `tcSubstTy` as well?  This smells like bringing all
 the `mkNakedX` functions back!

   I rather wonder if, rather than having the complicated invariants
 described in `Note [Respecting definitional equality]` we might instead
 just make the `splitX` functions able to deal with casts?

 Oddly, #15799 works in HEAD, and in this new branch; so the new stuff
 can't claim to have fixed it.

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