Skip to content

Introduce a zonking monad to reduce inter-module dependencies

Currently, zonking is done in the TcM monad, but it seems that only a very limited amount of functionality is needed:

  1. IO, for reading and writing metavariables (obviously),
  2. access to a logger for traceTc messages,
  3. ability to add error messages, e.g. as added by @monoidal's commit adding an error when encountering a concrete metavariable in zonkTcTypeToType

So I think it would be good to introduce a slimmer version of the TcM monad which has just enough to be able to do zonking. I would like to ask @simonpj if that seems possible, or if there's something I'm missing which means that zonking indirectly needs access to full TcM functionality.

I would also like to remove the ability for zonking to add errors, as this zonking monad is (I believe) the monad we end up needing in the ErrCtxt type (defined currently in GHC.Tc.Types); it seems worthwhile to rule out any erroring operations and guarantee that the monad only supports reading/writing of metavariables (and logging).

My main motivation for this is to remove inter-module dependencies. This would make the module graph more parallelisable, increase modularity, and help avoid having so many hs-boot files.
Such a refactor would also facilitate the insertion of assertions that are only true "up to zonking".

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