Opened 5 years ago

Last modified 20 months ago

#9980 new bug

TcS monad is too heavy

Reported by: simonpj Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.8.4
Keywords: TypeCheckerPlugins Cc: diatchki, dimitris, goldfire, gkaracha, adamgundry, darchon, nfrisby
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by simonpj)

The typechecker's constraint-solving monad, TcS, is simply built on top of TcM, but it doesn't use most of TcM's facilities. That was fine while TcS was only called from the typechecker, but now (as part of fixing pattern-match overlap checking) we invoke it from the desugarer.

It seems quite wrong to construct a vast, and unnecessary TcM context just to invoke TcS.

Better: make TcS into its own monad, with its own TcSLclEnv, built on IOEnv like the others.

Main objection: the plugins mechanism exposes unsafeTcPluginTcM, which would become unavailable. But it it used?

Change History (8)

comment:1 Changed 5 years ago by simonpj

Description: modified (diff)

comment:2 Changed 5 years ago by simonpj

Iavor: any comments about the unsafeTcPluginTcM thing?

comment:3 Changed 4 years ago by gkaracha

Cc: gkaracha added; gkarachalias removed

comment:4 Changed 20 months ago by adamgundry

Cc: adamgundry added
Keywords: TypeCheckerPlugins added

comment:5 Changed 20 months ago by diatchki

I hand't seen this ticket until Adam updated it a couple of days ago. Is that still the plan? The main things I can think of that a plugin might want from TcM are:

  1. access to variable "sort" (e.g., isTouchableMetaVar)
  2. a way to lookup things in the environment so that a plugin can recognize the types it supposed to work with (e.g., a plugin might know that it wants to work on type T defined in module X.Y.Z, but it needs to lookup this type's TyCon so that it can recognize the type in a constraint).

On the second point: it is probably better if a plugin looks up this information only once (on startup) and stores the info somewhere, rather than looking it up all the time. So we could probably change the plugin API to add some initialization in TcM, but then keep the actual plugin execution in TcS.

comment:6 Changed 20 months ago by simonpj

I'd be delighted if someone wanted to make progress on this line. I don't have the capacity to drive it myself, but it seems like the right direction.

comment:7 Changed 20 months ago by adamgundry

Cc: darchon nfrisby added

I don't think unsafeTcPluginTcM should block this refactoring, provided we can provide unsafeTcPluginTcS and make sure that TcS is still sufficiently well-equipped. What "sufficiently well-equipped" means is a bit hard to pin down, but it should at least support the existing TcPluginM API.

I think we should preserve the ability to do lookups in TcPluginM. For example, ghc-typelits-knownnat needs mkNaturalExpr, which relies on lookup (via MonadThings). I guess in that case one could copy code and refactor so as to do the lookups once, but in general I can imagine a plugin wanting to look up things that are not known at initialisation time. We should probably just make TcPluginM instantiate MonadThings.

Perhaps Christiaan or Nick can comment on other use cases for unsafeTcPluginTcM?

comment:8 Changed 20 months ago by darchon

I had no need for unsafeTcPluginTcM until GHC 8.5, and only because:

  • The evidence for KnownNat is a Natural, even though Core doesn't have "first-class" support for Natural literals (but if I understand correctly, somebody is working on improving this situation)
  • Evidence is no longer a separate data type, but just a normal core expressions (except for evidence for Typeable).

So the causes for my need unsafeTcPluginTcM can simply be classified as a "series of unfortunate/unforeseen events". However, isn't that exactly the reason for unsafeTcPluginTcMs existence in the first place? To have an escape hatch for situations that weren't easily foreseeable.

Note: See TracTickets for help on using tickets.