[Git][ghc/ghc][master] 2 commits: If we have multiple defaulting plugins, then we should zonk in between them
Marge Bot (@marge-bot)
gitlab at gitlab.haskell.org
Fri Sep 8 08:04:59 UTC 2023
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
1d92f2df by Gergő Érdi at 2023-09-08T04:04:30-04:00
If we have multiple defaulting plugins, then we should zonk in between them
after any defaulting has taken place, to avoid a defaulting plugin seeing
a metavariable that has already been filled.
Fixes #23821.
- - - - -
eaee4d29 by Gergő Érdi at 2023-09-08T04:04:30-04:00
Improvements to the documentation of defaulting plugins
Based on @simonpj's draft and comments in !11117
- - - - -
3 changed files:
- compiler/GHC/Tc/Solver.hs
- compiler/GHC/Tc/Types.hs
- docs/users_guide/extending_ghc.rst
Changes:
=====================================
compiler/GHC/Tc/Solver.hs
=====================================
@@ -3577,6 +3577,48 @@ 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 variable to fill-in, 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
@@ -3593,20 +3635,16 @@ applyDefaultingRules wanteds
; tcg_env <- TcS.getGblEnv
; let plugins = tcg_defaulting_plugins tcg_env
- ; plugin_defaulted <- if null plugins then return [] else
+ -- 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)
- ; defaultedGroups <- mapM (run_defaulting_plugin wanteds) plugins
+ ; (wanteds, defaultedGroups) <- mapAccumLM run_defaulting_plugin wanteds plugins
; traceTcS "defaultingPlugins }" (ppr defaultedGroups)
- ; return defaultedGroups
+ ; return (wanteds, defaultedGroups)
}
- -- If a defaulting plugin solves a tyvar, some of the wanteds
- -- will have filled-in metavars by now (see #23281). So we
- -- re-zonk to make sure the built-in defaulting rules don't try
- -- to solve the same metavars.
- ; wanteds <- if or plugin_defaulted then TcS.zonkWC wanteds else pure wanteds
-
; let groups = findDefaultableGroups info wanteds
; traceTcS "applyDefaultingRules {" $
@@ -3629,8 +3667,14 @@ applyDefaultingRules wanteds
groups
; traceTcS "defaultingPlugin " $ ppr defaultedGroups
; case defaultedGroups of
- [] -> return False
- _ -> return True
+ [] -> return (wanteds, False)
+ _ -> do
+ -- If a defaulting plugin solves any tyvars, some of the wanteds
+ -- 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
=====================================
@@ -1066,7 +1066,12 @@ instance Outputable DefaultingProposal where
<+> ppr (deProposals p)
<+> ppr (deProposalCts p)
-type FillDefaulting = WantedConstraints -> TcPluginM [DefaultingProposal]
+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
=====================================
@@ -1378,18 +1378,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 ``[DefaultingProposal]``: a list of types that
-should be attempted for the given type variables that are 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 return in ``deProposalCts``
-is the list of all wanted constraints that mention the variables 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:
+ * ``deProposals``: specifies a list,
+ in priority order, of sets of type variable assignments
+ * ``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 ``deProposals`` in turn:
+
+* It assigns the proposed types to the type variables, 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 ``DefaultingProposal``
+* If not, GHC tries the next assignment in ``deProposals``.
+
+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
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/e0aa8c6e3a8b6004eca9349e5b705b8a767050aa...eaee4d296a0782c1acfde610ed3f0a7c7668c06c
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/e0aa8c6e3a8b6004eca9349e5b705b8a767050aa...eaee4d296a0782c1acfde610ed3f0a7c7668c06c
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/20230908/b3efc115/attachment-0001.html>
More information about the ghc-commits
mailing list