#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