[Git][ghc/ghc][wip/T23923-mikolaj-take-2] Fix according to the third round of Simon's instruction
Mikolaj Konarski (@Mikolaj)
gitlab at gitlab.haskell.org
Thu Feb 29 12:19:54 UTC 2024
Mikolaj Konarski pushed to branch wip/T23923-mikolaj-take-2 at Glasgow Haskell Compiler / GHC
Commits:
4927c11a by Mikolaj Konarski at 2024-02-29T13:17:42+01:00
Fix according to the third round of Simon's instruction
- - - - -
4 changed files:
- compiler/GHC/Core/TyCo/Rep.hs
- compiler/GHC/Core/TyCo/Subst.hs
- docs/users_guide/extending_ghc.rst
- testsuite/tests/tcplugins/CtIdPlugin.hs
Changes:
=====================================
compiler/GHC/Core/TyCo/Rep.hs
=====================================
@@ -1527,9 +1527,10 @@ data UnivCoProvenance
| PluginProv String !DCoVarSet
-- ^ From a plugin, which asserts that this coercion is sound.
- -- The string and the variable set are for the use of the plugin.
+ -- The string and the variable set are for the use by the plugin.
-- E.g., the set may contain the in-scope coercion variables
-- that the the proof represented by the coercion makes use of.
+ -- See Note [The importance of tracking free coercion variables].
deriving Data.Data
@@ -1693,30 +1694,35 @@ Here,
co5 = TyConAppCo Nominal (~#) [<*>, <*>, co4, <Bool>]
-The importance of tracking free coercion variables
---------------------------------------------------
-
--- !!! Rewrite the below, explaining how plugins need the vars:
+Note [The importance of tracking free coercion variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+It is vital that `UnivCo` (a coercion that lacks a proper proof)
+tracks its free coercion variables. To see why, consider this program:
-It is vital that zapped coercions track their free coercion variables.
-To see why, consider this program:
+ type S :: Nat -> Nat
- data T a where
- T1 :: Bool -> T Bool
- T2 :: T Int
+ data T (a::Nat) where
+ T1 :: T 0
+ T2 :: ...
- f :: T a -> a -> Bool
+ f :: T a -> S (a+1) -> S 1
f = /\a (x:T a) (y:a).
case x of
- T1 (c : a~Bool) (z : Bool) -> not (y |> c)
- T2 -> True
-
-Now imagine that we zap the coercion `c`, replacing it with a generic UnivCo
-between `a` and Bool. If we didn't record the fact that this coercion was
-previously free in `c`, we may incorrectly float the expression `not (y |> c)`
-out of the case alternative which brings proof of `c` into scope. If this
-happened then `f T2 (I# 5)` would try to interpret `y` as a Bool, at
-which point we aren't far from a segmentation fault or much worse.
+ T1 (gco : a ~# 0) -> y |> wco
+
+For this to typecheck we need `wco :: S (a+1) ~# S 1`, given that `gco : a ~# 0`.
+To prove that we need to know that `a+1 = 1` if `a=0`, which a plugin might know.
+So it solves `wco` by providing a `UnivCo (PluginProv "my-plugin" gcvs) (a+1) 1`.
+
+ But the `gcvs` in `PluginProv` must mention `gco`.
+
+Why? Otherwise we might float the entire expression (y |> wco) out of the
+the case alternative for `T1` which brings `gco` into scope. If this
+happens then we aren't far from a segmentation fault or much worse.
+See #23923 for a real-world example of this happening.
+
+So it is /crucial/ for the `PluginProv` to mention, in `gcvs`, the coercion
+variables used by the plugin to justify the `UnivCo` that it builds.
Note that we don't need to track
* the coercion's free *type* variables
=====================================
compiler/GHC/Core/TyCo/Subst.hs
=====================================
@@ -916,8 +916,8 @@ subst_co subst co
go_hole h@(CoercionHole { ch_co_var = cv })
= h { ch_co_var = updateVarType go_ty cv }
--- | Perform a substitution within a 'DVarSet' of free variables.
--- returning the shallow free coercion variables
+-- | Perform a substitution within a 'DVarSet' of free variables,
+-- returning the shallow free coercion variables.
substDCoVarSet :: Subst -> DCoVarSet -> DCoVarSet
substDCoVarSet subst cvs = coVarsOfCosDSet $ map (substCoVar subst) $
dVarSetElems cvs
=====================================
docs/users_guide/extending_ghc.rst
=====================================
@@ -760,18 +760,39 @@ This evidence is ignored for Given constraints, which GHC
"solves" simply by discarding them; typically this is used when they are
uninformative (e.g. reflexive equations). For Wanted constraints, the
evidence will form part of the Core term that is generated after
-typechecking, and can be checked by ``-dcore-lint``. It is possible for
-the plugin to create equality axioms for use in evidence terms, but GHC
-does not check their consistency, and inconsistent axiom sets may lead
-to segfaults or other runtime misbehaviour.
+typechecking, and can be checked by ``-dcore-lint``.
+
+When solving a Wanted equality constraint (of type ``t1 ~N# t2``
+or ``t1 ~R# t2`` for nominal and representation equalities respectively),
+the evidence (of type ``EvTerm``) will take the form ``EvExpr (Coercion co)``,
+where the coercion ``co`` has type ``co :: t1 ~N# t2`` or ``co :: t1 ~R# t2``
+respectively.
+
+It is up to the plugin to construct a suitable coercion ``co``.
+However, one possibility is to construct one of form ::
+
+ UnivCo (PluginProv "my-plugin" gcvs) role t1 t2
+
+A ``UnivCo`` of this form says "trust me: my-plugin has solved this Wanted
+using (only) ``gcvs``".
+
+Here
+
+* The ``role`` should be the role of the original equality constraint
+ (nominal or representational).
+* The ``gcvs`` is a set of "given coercion variables"; these are the coercion
+ variable bound by enclosing Given constraints, which the plugin has used
+ to justify solving the Wanted.
+
+For soundness, it is very important to include the ``gcvs``; otherwise
+GHC may transform the program into a form that seg-faults.
+See #23923 for a long dicussion.
Evidence is required also when creating new Given constraints, which are
usually implied by old ones. It is not uncommon that the evidence of a new
Given constraint contains a removed constraint: the new one has replaced the
removed one.
--- !!! Given that "Evidence" and "Given" is mentioned here, is this the right place to "explain when plugin authors need to record coercion variables in their PluginProv"? I think, ideally, we'd explaion this in a subsection about a relevant example plugin, but I can't spot any.
-
.. _type-family-rewriting-with-plugins:
Type family rewriting with plugins
=====================================
testsuite/tests/tcplugins/CtIdPlugin.hs
=====================================
@@ -42,7 +42,7 @@ solver :: [String]
-> PluginDefs -> EvBindsVar -> [Ct] -> [Ct]
-> TcPluginM TcPluginSolveResult
solver _args defs ev givens wanteds = do
- let pluginCo = mkUnivCo (PluginProv "CtIdPlugin" emptyUniqDSet) Representational -- Empty is fine. This plugin does not use "givens". -- !!! is it true for this plugin as well?
+ let pluginCo = mkUnivCo (PluginProv "CtIdPlugin" emptyUniqDSet) Representational -- Empty is fine. This plugin does not use "givens".
let substEvidence ct ct' =
evCast (ctEvExpr $ ctEvidence ct') $ pluginCo (ctPred ct') (ctPred ct)
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/4927c11af40531563e12c21fd667e5c285b50e2f
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/4927c11af40531563e12c21fd667e5c285b50e2f
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/20240229/fa7ddff4/attachment-0001.html>
More information about the ghc-commits
mailing list