From 8a939b404e26bcaa07caa8b5e83bdf79307d2807 Mon Sep 17 00:00:00 2001 From: sheaf Date: Mon, 23 Aug 2021 17:09:19 +0200 Subject: TcPlugins: solve and report contras simultaneously This changes the TcPlugin datatype to allow type-checking plugins to report insoluble constraints while at the same time solve some other constraints. This allows better error messages, as the plugin can still simplify constraints, even when it wishes to report a contradiction. Pattern synonyms TcPluginContradiction and TcPluginOk are provided for backwards compatibility: existing type-checking plugins should continue to work without modification. --- docs/users_guide/extending_ghc.rst | 24 +++++++++++++----------- 1 file changed, 13 insertions(+), 11 deletions(-) (limited to 'docs') diff --git a/docs/users_guide/extending_ghc.rst b/docs/users_guide/extending_ghc.rst index 0020c0213f..7b3f7f0a78 100644 --- a/docs/users_guide/extending_ghc.rst +++ b/docs/users_guide/extending_ghc.rst @@ -555,11 +555,12 @@ is defined thus: type TcPluginRewriter = RewriteEnv -> [Ct] -> [Type] -> TcPluginM TcPluginRewriteResult - data TcPluginResult - = TcPluginContradiction [Ct] - | TcPluginOk - { tcPluginSolvedCts :: [(EvTerm,Ct)] - , tcPluginNewCts :: [Ct] } + data TcPluginSolveResult + = TcPluginSolveResult + { tcPluginInsolubleCts :: [Ct] + , tcPluginSolvedCts :: [(EvTerm, Ct)] + , tcPluginNewCts :: [Ct] + } data TcPluginRewriteResult = TcPluginNoRewrite @@ -634,19 +635,20 @@ The two ways can be distinguished by checking the Wanted constraints: in the first case (and the first case only), the plugin will be passed an empty list of Wanted constraints. -The plugin is then expected to respond in either of the following ways: +The plugin can then respond with: -* return ``TcPluginOk`` with lists of solved and new constraints, or +* solved constraints, which will be removed from the inert set, -* return ``TcPluginContradiction`` with a list of impossible - constraints, so they can be turned into errors. +* new constraints, which will be added to the work list, -In both cases, the plugin must respond with constraints of the same flavour, +* insoluble constraints, which will be reported as errors. + +The plugin must respond with constraints of the same flavour, i.e. in (1) it should return only Givens, and for (2) it should return only Wanteds (or Deriveds); all other constraints will be ignored. If the plugin cannot make any progress, it should return -``TcPluginOk [] []``. Otherwise, if there were any new constraints, the +``TcPluginSolveResult [] [] []``. Otherwise, if there were any new constraints, the main constraint solver will be re-invoked to simplify them, then the plugin will be invoked again. The plugin is responsible for making sure that this process eventually terminates. -- cgit v1.2.1