[Git][ghc/ghc][wip/T24978] Add Given builtin deductions
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Wed Jun 12 22:54:16 UTC 2024
Simon Peyton Jones pushed to branch wip/T24978 at Glasgow Haskell Compiler / GHC
Commits:
0d1908ce by Simon Peyton Jones at 2024-06-12T23:53:13+01:00
Add Given builtin deductions
Addresses #24845.
Needs documentation
- - - - -
6 changed files:
- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/TyCo/Rep.hs
- compiler/GHC/Tc/Solver/Dict.hs
- compiler/GHC/Tc/Solver/Equality.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Types/Constraint.hs
Changes:
=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -1459,6 +1459,7 @@ setNominalRole_maybe r co
setNominalRole_maybe_helper co@(UnivCo { uco_prov = prov })
| case prov of PhantomProv {} -> False -- should always be phantom
ProofIrrelProv {} -> True -- it's always safe
+ BuiltinProv {} -> True -- always nominal
PluginProv {} -> False -- who knows? This choice is conservative.
= Just $ co { uco_role = Nominal }
setNominalRole_maybe_helper _ = Nothing
=====================================
compiler/GHC/Core/TyCo/Rep.hs
=====================================
@@ -912,13 +912,14 @@ data Coercion
-- The number coercions should match exactly the expectations
-- of the CoAxiomRule (i.e., the rule is fully saturated).
- | UnivCo { uco_prov :: UnivCoProvenance
- , uco_role :: Role
- , uco_lty, uco_rty :: Type
- , uco_deps :: [Coercion] -- Coercions on which it depends
- -- See Note [The importance of tracking free coercion variables].
- }
- -- Of kind (lty ~role rty)
+ | UnivCo -- See Note [UnivCo]
+ -- Of kind (lty ~role rty)
+ { uco_prov :: UnivCoProvenance
+ , uco_role :: Role
+ , uco_lty, uco_rty :: Type
+ , uco_deps :: [Coercion] -- Coercions on which it depends
+ -- See Note [The importance of tracking UnivCo dependencies]
+ }
| SymCo Coercion -- :: e -> e
| TransCo Coercion Coercion -- :: e -> e -> e
@@ -988,22 +989,6 @@ instance Outputable FunSel where
ppr SelArg = text "arg"
ppr SelRes = text "res"
-instance Binary UnivCoProvenance where
- put_ bh PhantomProv = putByte bh 1
- put_ bh ProofIrrelProv = putByte bh 2
- put_ bh (PluginProv a) = do { putByte bh 3
- ; put_ bh a }
-
- get bh = do
- tag <- getByte bh
- case tag of
- 1 -> return PhantomProv
- 2 -> return ProofIrrelProv
- 3 -> do a <- get bh
- return $ PluginProv a
- _ -> panic ("get UnivCoProvenance " ++ show tag)
-
-
instance Binary CoSel where
put_ bh (SelTyCon n r) = do { putByte bh 0; put_ bh n; put_ bh r }
put_ bh SelForAll = putByte bh 1
@@ -1539,16 +1524,29 @@ in nominal ways. If not, having w be representational is OK.
%************************************************************************
%* *
- UnivCoProvenance
+ UnivCo
%* *
%************************************************************************
+Note [UnivCo]
+~~~~~~~~~~~~~
A UnivCo is a coercion whose proof does not directly express its role
and kind (indeed for some UnivCos, like PluginProv, there /is/ no proof).
-The different kinds of UnivCo are described by UnivCoProvenance. Really
-each is entirely separate, but they all share the need to represent their
-role and kind, which is done in the UnivCo constructor.
+The different kinds of UnivCo are described by UnivCoProvenance. Really each
+is entirely separate, but they all share the need to represent these fields:
+
+ UnivCo
+ { uco_prov :: UnivCoProvenance
+ , uco_role :: Role
+ , uco_lty, uco_rty :: Type
+ , uco_deps :: [Coercion] -- Coercions on which it depends
+
+Here,
+ * uco_role, uco_lty, uco_rty express the type of the coercoin
+ * uco_prov says where it came from
+ * uco_deps specifies the coercions on which this proof (which is not
+ explicity given) depends. See
-}
@@ -1572,17 +1570,124 @@ data UnivCoProvenance
-- ^ From a plugin, which asserts that this coercion is sound.
-- The string and the variable set are for the use by the plugin.
+ | BuiltinProv -- The proof comes form GHC's knowledge of arithmetic
+ -- or strings; e.g. from (co : a+b ~ 0) we can deduce that
+ -- (a ~ 0) and (b ~ 0), with a BuiltinProv proof.
+
deriving (Eq, Ord, Data.Data)
-- Why Ord? See Note [Ord instance of IfaceType] in GHC.Iface.Type
instance Outputable UnivCoProvenance where
+ ppr BuiltinProv = text "(builtin)"
ppr PhantomProv = text "(phantom)"
- ppr ProofIrrelProv = text "(proof irrel.)"
+ ppr ProofIrrelProv = text "(proof irrel)"
ppr (PluginProv str) = parens (text "plugin" <+> brackets (text str))
instance NFData UnivCoProvenance where
rnf p = p `seq` ()
+instance Binary UnivCoProvenance where
+ put_ bh BuiltinProv = putByte bh 1
+ put_ bh PhantomProv = putByte bh 2
+ put_ bh ProofIrrelProv = putByte bh 3
+ put_ bh (PluginProv a) = putByte bh 4 >> put_ bh a
+ get bh = do
+ tag <- getByte bh
+ case tag of
+ 1 -> return BuiltinProv
+ 2 -> return PhantomProv
+ 3 -> return ProofIrrelProv
+ 4 -> do a <- get bh
+ return $ PluginProv a
+ _ -> panic ("get UnivCoProvenance " ++ show tag)
+
+
+{- Note [Phantom coercions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+ data T a = T1 | T2
+Then we have
+ T s ~R T t
+for any old s,t. The witness for this is (TyConAppCo T Rep co),
+where (co :: s ~P t) is a phantom coercion built with PhantomProv.
+The role of the UnivCo is always Phantom. The Coercion stored is the
+(nominal) kind coercion between the types
+ kind(s) ~N kind (t)
+
+Note [ProofIrrelProv]
+~~~~~~~~~~~~~~~~~~~~~
+A ProofIrrelProv is a coercion between coercions. For example:
+
+ data G a where
+ MkG :: G Bool
+
+In core, we get
+
+ G :: * -> *
+ MkG :: forall (a :: *). (a ~ Bool) -> G a
+
+Now, consider 'MkG -- that is, MkG used in a type -- and suppose we want
+a proof that ('MkG a1 co1) ~ ('MkG a2 co2). This will have to be
+
+ TyConAppCo Nominal MkG [co3, co4]
+ where
+ co3 :: co1 ~ co2
+ co4 :: a1 ~ a2
+
+Note that
+ co1 :: a1 ~ Bool
+ co2 :: a2 ~ Bool
+
+Here,
+ co3 = UnivCo ProofIrrelProv Nominal (CoercionTy co1) (CoercionTy co2) [co5]
+ where
+ co5 :: (a1 ~ Bool) ~ (a2 ~ Bool)
+ co5 = TyConAppCo Nominal (~#) [<*>, <*>, co4, <Bool>]
+
+
+Note [The importance of tracking UnivCo dependencies]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+It is vital that `UnivCo` (a coercion that lacks a proper proof)
+tracks the coercions on which it depends. To see why, consider this program:
+
+ type S :: Nat -> Nat
+
+ data T (a::Nat) where
+ T1 :: T 0
+ T2 :: ...
+
+ f :: T a -> S (a+1) -> S 1
+ f = /\a (x:T a) (y:a).
+ case x of
+ 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") (a+1) 1 [gco]`.
+
+ But the `uco_deps` 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 `UnivCo` to mention, in `uco_deps`, the coercion
+variables used by the plugin to justify the `UnivCo` that it builds. You
+should think of it like `TyConAppCo`: the `UnivCo` proof contstructor is
+applied to a list of coercions, just as `TyConAppCo` is
+
+It's very convenient to record a full coercion, not just a set of free coercion
+variables, because during typechecking those coercions might contain coercion
+holes `HoleCo`, which get filled in later.
+-}
+
+{- **********************************************************************
+%* *
+ Coercion holes
+%* *
+%********************************************************************* -}
+
-- | A coercion to be filled in by the type-checker. See Note [Coercion holes]
data CoercionHole
= CoercionHole { ch_co_var :: CoVar
@@ -1618,19 +1723,7 @@ instance Outputable CoercionHole where
instance Uniquable CoercionHole where
getUnique (CoercionHole { ch_co_var = cv }) = getUnique cv
-{- Note [Phantom coercions]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider
- data T a = T1 | T2
-Then we have
- T s ~R T t
-for any old s,t. The witness for this is (TyConAppCo T Rep co),
-where (co :: s ~P t) is a phantom coercion built with PhantomProv.
-The role of the UnivCo is always Phantom. The Coercion stored is the
-(nominal) kind coercion between the types
- kind(s) ~N kind (t)
-
-Note [Coercion holes]
+{- Note [Coercion holes]
~~~~~~~~~~~~~~~~~~~~~~~~
During typechecking, constraint solving for type classes works by
- Generate an evidence Id, d7 :: Num a
@@ -1705,84 +1798,10 @@ constraint from floating] in GHC.Tc.Solver, item (4):
Here co2 is a CoercionHole. But we /must/ know that it is free in
co1, because that's all that stops it floating outside the
implication.
-
-
-Note [ProofIrrelProv]
-~~~~~~~~~~~~~~~~~~~~~
-A ProofIrrelProv is a coercion between coercions. For example:
-
- data G a where
- MkG :: G Bool
-
-In core, we get
-
- G :: * -> *
- MkG :: forall (a :: *). (a ~ Bool) -> G a
-
-Now, consider 'MkG -- that is, MkG used in a type -- and suppose we want
-a proof that ('MkG a1 co1) ~ ('MkG a2 co2). This will have to be
-
- TyConAppCo Nominal MkG [co3, co4]
- where
- co3 :: co1 ~ co2
- co4 :: a1 ~ a2
-
-Note that
- co1 :: a1 ~ Bool
- co2 :: a2 ~ Bool
-
-Here,
- co3 = UnivCo (ProofIrrelProv co5) Nominal (CoercionTy co1) (CoercionTy co2)
- where
- co5 :: (a1 ~ Bool) ~ (a2 ~ Bool)
- co5 = TyConAppCo Nominal (~#) [<*>, <*>, co4, <Bool>]
-
-
-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:
-
- type S :: Nat -> Nat
-
- data T (a::Nat) where
- T1 :: T 0
- T2 :: ...
-
- f :: T a -> S (a+1) -> S 1
- f = /\a (x:T a) (y:a).
- case x of
- 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
-* coercion variables free in kinds (we only need the "shallow" free covars)
-
-This means that we may float past type variables which the original
-proof had as free variables. While surprising, this doesn't jeopardise
-the validity of the coercion, which only depends upon the scoping
-relative to the free coercion variables.
-
-(The free coercion variables are kept as a DCoVarSet in UnivCo,
-since these sets are included in interface files.)
-
-}
+
{- *********************************************************************
* *
foldType and foldCoercion
=====================================
compiler/GHC/Tc/Solver/Dict.hs
=====================================
@@ -1396,16 +1396,16 @@ parameters, is that we simply produce new Wanted equalities. So for example
class D a b | a -> b where ...
Inert:
- d1 :g D Int Bool
+ [G] d1 : D Int Bool
WorkItem:
- d2 :w D Int alpha
+ [W] d2 : D Int alpha
We generate the extra work item
- cv :w alpha ~ Bool
+ [W] cv : alpha ~ Bool
where 'cv' is currently unused. However, this new item can perhaps be
spontaneously solved to become given and react with d2,
discharging it in favour of a new constraint d2' thus:
- d2' :w D Int Bool
+ [W[ d2' : D Int Bool
d2 := d2' |> D Int cv
Now d2' can be discharged from d1
@@ -1415,20 +1415,20 @@ using those extra equalities.
If that were the case with the same inert set and work item we might discard
d2 directly:
- cv :w alpha ~ Bool
+ [W] cv : alpha ~ Bool
d2 := d1 |> D Int cv
But in general it's a bit painful to figure out the necessary coercion,
so we just take the first approach. Here is a better example. Consider:
class C a b c | a -> b
And:
- [Given] d1 : C T Int Char
- [Wanted] d2 : C T beta Int
+ [G] d1 : C T Int Char
+ [W] d2 : C T beta Int
In this case, it's *not even possible* to solve the wanted immediately.
So we should simply output the functional dependency and add this guy
[but NOT its superclasses] back in the worklist. Even worse:
- [Given] d1 : C T Int beta
- [Wanted] d2: C T beta Int
+ [G] d1 : C T Int beta
+ [W] d2: C T beta Int
Then it is solvable, but its very hard to detect this on the spot.
It's exactly the same with implicit parameters, except that the
=====================================
compiler/GHC/Tc/Solver/Equality.hs
=====================================
@@ -115,7 +115,7 @@ solveEquality ev eq_rel ty1 ty2
; solveIrred irred_ct } ;
Right eq_ct -> do { tryInertEqs eq_ct
- ; tryFunDeps eq_ct
+ ; tryFunDeps eq_rel eq_ct
; tryQCsEqCt eq_ct
; simpleStage (updInertEqs eq_ct)
; stopWithStage (eqCtEvidence eq_ct) "Kept inert EqCt" } } }
@@ -2973,29 +2973,47 @@ tryFamFamInjectivity ev eq_rel fun_tc1 fun_args1 fun_tc2 fun_args2 mco
= return False
--------------------
-tryFunDeps :: EqCt -> SolverStage ()
-tryFunDeps work_item@(EqCt { eq_lhs = lhs, eq_ev = ev })
+tryFunDeps :: EqRel -> EqCt -> SolverStage ()
+tryFunDeps eq_rel work_item@(EqCt { eq_lhs = lhs, eq_ev = ev })
+ | NomEq <- eq_rel
+ , TyFamLHS tc args <- lhs
= Stage $
- case lhs of
- TyFamLHS tc args -> do { inerts <- getInertCans
- ; imp1 <- improveLocalFunEqs inerts tc args work_item
- ; imp2 <- improveTopFunEqs tc args work_item
- ; if (imp1 || imp2)
- then startAgainWith (mkNonCanonical ev)
- else continueWith () }
- TyVarLHS {} -> continueWith ()
+ do { inerts <- getInertCans
+ ; imp1 <- improveLocalFunEqs inerts tc args work_item
+ ; imp2 <- improveTopFunEqs tc args work_item
+ ; if (imp1 || imp2)
+ then startAgainWith (mkNonCanonical ev)
+ else continueWith () }
+ | otherwise
+ = nopStage ()
--------------------
improveTopFunEqs :: TyCon -> [TcType] -> EqCt -> TcS Bool
-- See Note [FunDep and implicit parameter reactions]
-improveTopFunEqs fam_tc args (EqCt { eq_ev = ev, eq_rhs = rhs })
+improveTopFunEqs fam_tc args (EqCt { eq_ev = ev, eq_rhs = rhs_ty })
| isGiven ev
- = return False -- See Note [No Given/Given fundeps]
+ = improveGivenTopFunEqs fam_tc args ev rhs_ty
+ | otherwise
+ = improveWantedTopFunEqs fam_tc args ev rhs_ty
+improveGivenTopFunEqs :: TyCon -> [TcType] -> CtEvidence -> Xi -> TcS Bool
+improveGivenTopFunEqs fam_tc args ev rhs_ty
+ | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc
+ = do { emitNewGivens (ctEvLoc ev) $
+ [ (Nominal, s, t, new_co)
+ | Pair s t <- sfInteractTop ops args rhs_ty
+ , let new_co = mkUnivCo BuiltinProv [given_co] Nominal s t ]
+ ; return False }
| otherwise
+ = return False -- See Note [No Given/Given fundeps]
+ where
+ given_co :: Coercion = ctEvCoercion ev
+
+improveWantedTopFunEqs :: TyCon -> [TcType] -> CtEvidence -> Xi -> TcS Bool
+improveWantedTopFunEqs fam_tc args ev rhs_ty
= do { fam_envs <- getFamInstEnvs
- ; eqns <- improve_top_fun_eqs fam_envs fam_tc args rhs
- ; traceTcS "improveTopFunEqs" (vcat [ ppr fam_tc <+> ppr args <+> ppr rhs
+ ; eqns <- improve_top_fun_eqs fam_envs fam_tc args rhs_ty
+ ; traceTcS "improveTopFunEqs" (vcat [ ppr fam_tc <+> ppr args <+> ppr rhs_ty
, ppr eqns ])
; unifyFunDeps ev Nominal $ \uenv ->
uPairsTcM (bump_depth uenv) (reverse eqns) }
@@ -3008,7 +3026,7 @@ improveTopFunEqs fam_tc args (EqCt { eq_ev = ev, eq_rhs = rhs })
-- See #14778
improve_top_fun_eqs :: FamInstEnvs
- -> TyCon -> [TcType] -> TcType
+ -> TyCon -> [TcType] -> Xi
-> TcS [TypeEqn]
improve_top_fun_eqs fam_envs fam_tc args rhs_ty
| Just ops <- isBuiltInSynFamTyCon_maybe fam_tc
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -34,7 +34,7 @@ module GHC.Tc.Solver.Monad (
-- The pipeline
StopOrContinue(..), continueWith, stopWith,
startAgainWith, SolverStage(Stage, runSolverStage), simpleStage,
- stopWithStage,
+ stopWithStage, nopStage,
-- Tracing etc
panicTcS, traceTcS, tryEarlyAbortTcS,
@@ -284,6 +284,9 @@ instance Monad SolverStage where
Stop ev d -> return (Stop ev d)
ContinueWith x -> runSolverStage (k x) }
+nopStage :: a -> SolverStage a
+nopStage res = Stage (continueWith res)
+
simpleStage :: TcS a -> SolverStage a
-- Always does a ContinueWith; no Stop or StartAgain
simpleStage thing = Stage (do { res <- thing; continueWith res })
=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -2022,7 +2022,7 @@ ctEvTerm ev = EvExpr (ctEvExpr ev)
-- return an empty set.
ctEvRewriters :: CtEvidence -> RewriterSet
ctEvRewriters (CtWanted { ctev_rewriters = rewriters }) = rewriters
-ctEvRewriters _other = emptyRewriterSet
+ctEvRewriters (CtGiven {}) = emptyRewriterSet
ctEvExpr :: HasDebugCallStack => CtEvidence -> EvExpr
ctEvExpr ev@(CtWanted { ctev_dest = HoleDest _ })
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/0d1908cefe56a6743e295c42d6e9fa3f41119bac
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/0d1908cefe56a6743e295c42d6e9fa3f41119bac
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/20240612/5c7638b3/attachment-0001.html>
More information about the ghc-commits
mailing list