[GHC] #9980: TcS monad is too heavy

#9980: TcS monad is too heavy -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Blocked By: Test Case: | Related Tickets: Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- The typehcecker'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 [wiki:PatternMatchCheck 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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9980 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9980: TcS monad is too heavy -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Description changed by simonpj: Old description:
The typehcecker'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 [wiki:PatternMatchCheck 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?
New description: 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 [wiki:PatternMatchCheck 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? -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9980#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9980: TcS monad is too heavy -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by simonpj): Iavor: any comments about the `unsafeTcPluginTcM` thing? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9980#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9980: TcS monad is too heavy -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 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: | -------------------------------------+------------------------------------- Changes (by gkaracha): * cc: gkarachalias (removed) * cc: gkaracha (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9980#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9980: TcS monad is too heavy -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Resolution: | Keywords: | TypeCheckerPlugins Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by adamgundry): * cc: adamgundry (added) * keywords: => TypeCheckerPlugins -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9980#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9980: TcS monad is too heavy -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Resolution: | Keywords: | TypeCheckerPlugins Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9980#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9980: TcS monad is too heavy -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Resolution: | Keywords: | TypeCheckerPlugins Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9980#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9980: TcS monad is too heavy -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Resolution: | Keywords: | TypeCheckerPlugins Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by adamgundry): * cc: darchon, nfrisby (added) Comment: 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`? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9980#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9980: TcS monad is too heavy -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Resolution: | Keywords: | TypeCheckerPlugins Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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 `unsafeTcPluginTcM`s existence in the first place? To have an escape hatch for situations that weren't easily foreseeable. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9980#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC