Skip to content

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 TcTypes. 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 TcTypes differently from Types.

Work in progress on wip/T15952

Merge request at !74 (closed)

Edited by Simon Peyton Jones
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information