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:
-
IO
, for reading and writing metavariables (obviously), - access to a logger for
traceTc
messages, - 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".