[Git][ghc/ghc][wip/issue-23821] Improvements to the documentation of defaulting plugins

Gergő Érdi (@cactus) gitlab at gitlab.haskell.org
Tue Aug 29 06:15:31 UTC 2023



Gergő Érdi pushed to branch wip/issue-23821 at Glasgow Haskell Compiler / GHC


Commits:
f00c6882 by Gergő Érdi at 2023-08-29T07:15:21+01:00
Improvements to the documentation of defaulting plugins

Based on @simonpj's draft and comments in !11117

- - - - -


4 changed files:

- compiler/GHC/Tc/Solver.hs
- compiler/GHC/Tc/Types.hs
- docs/users_guide/extending_ghc.rst
- testsuite/tests/plugins/defaulting-plugin/DefaultLifted.hs


Changes:

=====================================
compiler/GHC/Tc/Solver.hs
=====================================
@@ -3574,6 +3574,49 @@ beta! Concrete example is in indexed_types/should_fail/ExtraTcsUntch.hs:
 *                          Defaulting and disambiguation                        *
 *                                                                               *
 *********************************************************************************
+
+Note [Defaulting plugins]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Defaulting plugins enable extending or overriding the defaulting
+behaviour. In `applyDefaulting`, before the built-in defaulting
+mechanism runs, the loaded defaulting plugins are passed the
+`WantedConstraints` and get a chance to propose defaulting assignments
+based on them.
+
+Proposals are represented as `[DefaultingProposal]` with each proposal
+consisting of a type varible to solve, the list of defaulting types to
+try in order, and a set of constraints to check at each try. This is
+the same representation (albeit in a nicely packaged-up data type) as
+the candidates generated by the built-in defaulting mechanism, so the
+actual trying of proposals is done by the same `disambigGroup` function.
+
+Wrinkle (DP1): The role of `WantedConstraints`
+
+  Plugins are passed `WantedConstraints` that can perhaps be
+  progressed on by defaulting. But a defaulting plugin is not a solver
+  plugin, its job is to provide defaulting proposals, i.e. mappings of
+  type variable to types. How do plugins know which type variables
+  they are supposed to default?
+
+  The `WantedConstraints` passed to the defaulting plugin are zonked
+  beforehand to ensure all remaining metavariables are unfilled. Thus,
+  the `WantedConstraints` serve a dual purpose: they are both the
+  constraints of the given context that can act as hints to the
+  defaulting, as well as the containers of the type variables under
+  consideration for defaulting.
+
+Wrinkle (DP2): Interactions between defaulting mechanisms
+
+  In the general case, we have multiple defaulting plugins loaded and
+  there is also the built-in defaulting mechanism. In this case, we
+  have to be careful to keep the `WantedConstraints` passed to the
+  plugins up-to-date by zonking between successful defaulting
+  rounds. Otherwise, two plugins might come up with a defaulting
+  proposal for the same metavariable; if the first one is accepted by
+  `disambigGroup` (thus the meta gets filled), the second proposal
+  becomes invalid (see #23821 for an example).
+
 -}
 
 applyDefaultingRules :: WantedConstraints -> TcS Bool
@@ -3590,6 +3633,8 @@ applyDefaultingRules wanteds
        ; tcg_env <- TcS.getGblEnv
        ; let plugins = tcg_defaulting_plugins tcg_env
 
+       -- Run any defaulting plugins
+       -- See Note [Defaulting plugins] for an overview
        ; (wanteds, plugin_defaulted) <- if null plugins then return (wanteds, []) else
            do {
              ; traceTcS "defaultingPlugins {" (ppr wanteds)
@@ -3622,9 +3667,9 @@ applyDefaultingRules wanteds
                  [] -> return (wanteds, False)
                  _  -> do
                      -- If a defaulting plugin solves any tyvars, some of the wanteds
-                     -- will have filled-in metavars by now (see #23281). So we
-                     -- re-zonk to make sure later defaulting doesn't try to solve
-                     -- the same metavars.
+                     -- will have filled-in metavars by now (see wrinkle DP2 of
+                     -- Note [Defaulting plugins]). So we re-zonk to make sure later
+                     -- defaulting doesn't try to solve the same metavars.
                      wanteds' <- TcS.zonkWC wanteds
                      return (wanteds', True)
                }


=====================================
compiler/GHC/Tc/Types.hs
=====================================
@@ -86,7 +86,7 @@ module GHC.Tc.Types(
 
         -- Defaulting plugin
         DefaultingPlugin(..), DefaultingProposal(..),
-        FillDefaulting, DefaultingPluginResult,
+        FillDefaulting,
 
         -- Role annotations
         RoleAnnotEnv, emptyRoleAnnotEnv, mkRoleAnnotEnv,
@@ -1069,8 +1069,12 @@ instance Outputable DefaultingProposal where
           <+> ppr (deProposalCandidates p)
           <+> ppr (deProposalCts p)
 
-type DefaultingPluginResult = [DefaultingProposal]
-type FillDefaulting = WantedConstraints -> TcPluginM DefaultingPluginResult
+type FillDefaulting
+  = WantedConstraints
+      -- Zonked constraints containing the unfilled metavariables that
+      -- can be defaulted. See wrinkle (DP1) of Note [Defaulting plugins]
+      -- in GHC.Tc.Solver
+  -> TcPluginM [DefaultingProposal]
 
 -- | A plugin for controlling defaulting.
 data DefaultingPlugin = forall s. DefaultingPlugin


=====================================
docs/users_guide/extending_ghc.rst
=====================================
@@ -1368,8 +1368,7 @@ Defaulting plugins have a single access point in the `GHC.Tc.Types` module
           -- ^ The constraints against which defaults are checked.
         }
 
-    type DefaultingPluginResult = [DefaultingProposal]
-    type FillDefaulting = WantedConstraints -> TcPluginM DefaultingPluginResult
+    type FillDefaulting = WantedConstraints -> TcPluginM [DefaultingProposal]
 
     -- | A plugin for controlling defaulting.
     data DefaultingPlugin = forall s. DefaultingPlugin
@@ -1381,18 +1380,36 @@ Defaulting plugins have a single access point in the `GHC.Tc.Types` module
        -- ^ Clean up after the plugin, when exiting the type-checker.
       }
 
-
-The plugin gets a combination of wanted constraints which can be most easily
-broken down into simple wanted constraints with ``approximateWC``. The result of
-running the plugin should be a ``DefaultingPluginResult``, a list of types that
-should be attempted for a given type variable that is ambiguous in a given
-context. GHC will check if one of the proposals is acceptable in the given
-context and then default to it. The most robust context to provide is the list
-of all wanted constraints that mention the variable you are defaulting. If you
-leave out a constraint, the default will be accepted, and then potentially
-result in a type checker error if it is incompatible with one of the constraints
-you left out. This can be a useful way of forcing a default and reporting errors
-to the user.
+The plugin has type ``WantedConstraints -> [DefaultingProposal]``.
+
+* It is given the currently unsolved constraints.
+* It returns a list of independent "defaulting proposals".
+* Each proposal of type ``DefaultingProposal`` specifies:
+  * ``deProposalTyVar``, ``deProposalCandidates``: specifies a list,
+    in priority order, of type to assign to that type variable
+  * ``deProposalCts :: [Ct]`` gives a set of constraints (always a
+    subset of the incoming ``WantedConstraints``) to use as a
+    criterion for acceptance
+
+After calling the plugin, GHC executes each ``DefaultingProposal`` in
+turn.  To "execute" a proposal, GHC tries each of the proposed type
+assignments in ``deProposalCandidates`` in turn:
+
+* It assigns the proposed type to the type variable, and then tries to
+  solve ``deProposalCts``
+* If those constraints are completely solved by the assignment, GHC
+  accepts the assignment and moves on to the next ``DefaultingPropsal``
+* If not, GHC tries the next assignment in ``deProposalCandidates``.
+
+The plugin can assume that the incoming constraints are fully
+"zonked" (see :ghc-wiki:`the Wiki page on zonking <zonking>`).
+
+The most robust ``deProposalCts`` to provide is the list of all wanted
+constraints that mention the variable you are defaulting. If you leave
+out a constraint, the default may be accepted, and then potentially
+result in a type checker error if it is incompatible with one of the
+constraints you left out. This can be a useful way of forcing a
+default and reporting errors to the user.
 
 There is an example of defaulting lifted types in the GHC test suite. In the
 `testsuite/tests/plugins/` directory see `defaulting-plugin/` for the


=====================================
testsuite/tests/plugins/defaulting-plugin/DefaultLifted.hs
=====================================
@@ -68,7 +68,7 @@ data PluginState = PluginState { defaultClassName :: Name }
 lookupName :: Module -> OccName -> TcPluginM Name
 lookupName md occ = lookupOrig md occ
 
-solveDefaultType :: PluginState -> [Ct] -> TcPluginM DefaultingPluginResult
+solveDefaultType :: PluginState -> [Ct] -> TcPluginM [DefaultingProposal]
 solveDefaultType _     []      = return []
 solveDefaultType state wanteds = do
   envs <- getInstEnvs
@@ -103,7 +103,7 @@ initialize :: TcPluginM PluginState
 initialize = do
   lookupDefaultTypes
 
-run :: PluginState -> WantedConstraints -> TcPluginM DefaultingPluginResult
+run :: PluginState -> WantedConstraints -> TcPluginM [DefaultingProposal]
 run s ws = do
   solveDefaultType s (ctsElts $ approximateWC False ws)
 



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/f00c6882132782480ee128d587ce7e8ca0eeff4f

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/f00c6882132782480ee128d587ce7e8ca0eeff4f
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20230829/f8cf8b06/attachment-0001.html>


More information about the ghc-commits mailing list