Reduce zonking-related invariants in the type checker
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 (closed) and #15918 (closed), which is about treating TcType
s differently from Type
s.
Work in progress on wip/T15952
Merge request at !74 (closed)