[Git][ghc/ghc][wip/T24978] More WIP
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Wed Jun 19 22:49:01 UTC 2024
Simon Peyton Jones pushed to branch wip/T24978 at Glasgow Haskell Compiler / GHC
Commits:
e39fd1ef by Simon Peyton Jones at 2024-06-19T23:48:32+01:00
More WIP
does not compile
- - - - -
2 changed files:
- compiler/GHC/Tc/Instance/FunDeps.hs
- compiler/GHC/Tc/Solver/Equality.hs
Changes:
=====================================
compiler/GHC/Tc/Instance/FunDeps.hs
=====================================
@@ -68,8 +68,6 @@ The constraints ([Wanted] C Int Bool) and [Wanted] C Int alpha
will generate the following FunDepEqn
FDEqn { fd_qtvs = []
, fd_eqs = [Pair Bool alpha]
- , fd_pred1 = C Int Bool
- , fd_pred2 = C Int alpha
, fd_loc = ... }
However notice that a functional dependency may have more than one variable
in the RHS which will create more than one pair of types in fd_eqs. Example:
@@ -79,8 +77,6 @@ in the RHS which will create more than one pair of types in fd_eqs. Example:
Will generate:
FDEqn { fd_qtvs = []
, fd_eqs = [Pair Bool alpha, Pair alpha beta]
- , fd_pred1 = C Int Bool
- , fd_pred2 = C Int alpha
, fd_loc = ... }
INVARIANT: Corresponding types aren't already equal
@@ -148,8 +144,6 @@ data FunDepEqn loc
-- free in ty1 but not in ty2. See Wrinkle (1) of
-- Note [Improving against instances]
- , fd_pred1 :: PredType -- The FunDepEqn arose from
- , fd_pred2 :: PredType -- combining these two constraints
, fd_loc :: loc }
deriving Functor
@@ -221,7 +215,7 @@ improveFromAnother loc pred1 pred2
| Just (cls1, tys1) <- getClassPredTys_maybe pred1
, Just (cls2, tys2) <- getClassPredTys_maybe pred2
, cls1 == cls2
- = [ FDEqn { fd_qtvs = [], fd_eqs = eqs, fd_pred1 = pred1, fd_pred2 = pred2, fd_loc = loc }
+ = [ FDEqn { fd_qtvs = [], fd_eqs = eqs, fd_loc = loc }
| let (cls_tvs, cls_fds) = classTvsFds cls1
, fd <- cls_fds
, let (ltys1, rs1) = instFD fd cls_tvs tys1
@@ -245,7 +239,6 @@ improveFromInstEnv :: InstEnvs
-- Post: Equations oriented from the template (matching instance) to the workitem!
improveFromInstEnv inst_env mk_loc cls tys
= [ FDEqn { fd_qtvs = meta_tvs, fd_eqs = eqs
- , fd_pred1 = p_inst, fd_pred2 = pred
, fd_loc = mk_loc p_inst (getSrcSpan (is_dfun ispec)) }
| fd <- cls_fds -- Iterate through the fundeps first,
-- because there often are none!
@@ -257,13 +250,11 @@ improveFromInstEnv inst_env mk_loc cls tys
, ispec <- instances
, (meta_tvs, eqs) <- improveClsFD cls_tvs fd ispec
tys trimmed_tcs -- NB: orientation
- , let p_inst = mkClassPred cls (is_tys ispec)
]
where
(cls_tvs, cls_fds) = classTvsFds cls
instances = classInstances inst_env cls
rough_tcs = RM_KnownTc (className cls) : roughMatchTcs tys
- pred = mkClassPred cls tys
improveClsFD :: [TyVar] -> FunDep TyVar -- One functional dependency from the class
-> ClsInst -- An instance template
=====================================
compiler/GHC/Tc/Solver/Equality.hs
=====================================
@@ -2993,10 +2993,8 @@ tryFunDeps eq_rel work_item@(EqCt { eq_lhs = lhs, eq_ev = ev })
improveTopFunEqs :: TyCon -> [TcType] -> EqCt -> TcS Bool
-- See Note [FunDep and implicit parameter reactions]
improveTopFunEqs fam_tc args (EqCt { eq_ev = ev, eq_rhs = rhs_ty })
- | isGiven ev
- = improveGivenTopFunEqs fam_tc args ev rhs_ty
- | otherwise
- = improveWantedTopFunEqs fam_tc args ev rhs_ty
+ | isGiven ev = 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
@@ -3104,12 +3102,52 @@ improve_top_fun_eqs fam_envs fam_tc args rhs_ty
improveLocalFunEqs :: InertCans -> TyCon -> [TcType] -> EqCt -> TcS Bool
--- Generate improvement equalities, by comparing
+improveLocalFunEqs inerts fam_tc args (EqCt { eq_ev = work_ev, eq_rhs = rhs })
+ | isGiven work_ev = improveGivenLocalFunEqs funeqs_for_tc fam_tc args work_ev rhs
+ | otherwise = improveWantedLocalFunEqs funeqs_for_tc fam_tc args work_ev rhs
+ where
+ funeqs = inert_funeqs inerts
+ funeqs_for_tc :: [EqCt]
+ funeqs_for_tc = [ funeq_ct | equal_ct_list <- findFunEqsByTyCon funeqs fam_tc
+ , funeq_ct <- equal_ct_list
+ , NomEq == eq_eq_rel funeq_ct ]
+ -- Representational equalities don't interact
+ -- with type family dependencies
+
+
+improveGivenLocalFunEqs :: TyCon -> [TcType] -> CtEvidence -> Xi -- Work item
+ -> [EqCt] -- Inert items
+ -> TcS Bool -- True <=> Something was emitted
+improveGivenLocalFunEqs funeqs_for_tc fam_tc work_args work_ev work_rhs
+ | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc
+ = foldlM (do_one ops) False fun_eqs_for_tc
+ | otherwise
+ = return False
+ where
+ do_one ops so_far (EqCt { eq_ev = inert_ev
+ , eq_lhs = TyFamLHS _ inert_args
+ , eq_rhs = inert_rhs })
+ | isGiven inert_ev, not (null quads)
+ = do { emitNewGivens (ctEvLoc ev) quads; return True }
+
+ | otherwise
+ = return so_far
+ where
+ given_co :: Coercion = ctEvCoercion work_ev
+
+ quads = [ (Nominal, s, t, new_co)
+ | (ax, Pair s t) <- tryInteractInertFam ops fam_tc
+ work_args work_rhs inert_args inert_rhs
+ , let new_co = mkAxiomRuleCo ax [given_co] ]
+
+improveWantedLocalFunEqs :: [EqCt] -> TyCon -> [TcType]
+ -> CtEvidence -> Xi -> TcS Bool
+-- Generate improvement equalities for a Watend constraint, by comparing
-- the current work item with inert CFunEqs
-- E.g. x + y ~ z, x + y' ~ z => [W] y ~ y'
--
-- See Note [FunDep and implicit parameter reactions]
-improveLocalFunEqs inerts fam_tc args (EqCt { eq_ev = work_ev, eq_rhs = rhs })
+improveWantedLocalFunEqs fun_eqs_for_tc fam_tc args work_ev rhs
| null improvement_eqns
= return False
| otherwise
@@ -3119,13 +3157,6 @@ improveLocalFunEqs inerts fam_tc args (EqCt { eq_ev = work_ev, eq_rhs = rhs })
, text "Inert eqs:" <+> ppr (inert_eqs inerts) ]
; emitFunDepWanteds work_ev improvement_eqns }
where
- funeqs = inert_funeqs inerts
- funeqs_for_tc :: [EqCt]
- funeqs_for_tc = [ funeq_ct | equal_ct_list <- findFunEqsByTyCon funeqs fam_tc
- , funeq_ct <- equal_ct_list
- , NomEq == eq_eq_rel funeq_ct ]
- -- representational equalities don't interact
- -- with type family dependencies
work_loc = ctEvLoc work_ev
work_pred = ctEvPred work_ev
fam_inj_info = tyConInjectivityInfo fam_tc
@@ -3146,11 +3177,7 @@ improveLocalFunEqs inerts fam_tc args (EqCt { eq_ev = work_ev, eq_rhs = rhs })
--------------------
do_one_built_in ops rhs (EqCt { eq_lhs = TyFamLHS _ iargs, eq_rhs = irhs, eq_ev = inert_ev })
- | isGiven inert_ev && isGiven work_ev
- = [] -- ToDo: fill in
- | otherwise
= mk_fd_eqns inert_ev (map snd $ tryInteractInertFam ops fam_tc args rhs iargs irhs)
-
do_one_built_in _ _ _ = pprPanic "interactFunEq 1" (ppr fam_tc) -- TyVarLHS
--------------------
@@ -3171,14 +3198,12 @@ improveLocalFunEqs inerts fam_tc args (EqCt { eq_ev = work_ev, eq_rhs = rhs })
mk_fd_eqns inert_ev eqns
| null eqns = []
| otherwise = [ FDEqn { fd_qtvs = [], fd_eqs = eqns
- , fd_pred1 = work_pred
- , fd_pred2 = inert_pred
, fd_loc = (loc, inert_rewriters) } ]
where
initial_loc -- start with the location of the Wanted involved
| isGiven work_ev = inert_loc
| otherwise = work_loc
- eqn_orig = InjTFOrigin1 work_pred (ctLocOrigin work_loc) (ctLocSpan work_loc)
+ eqn_orig = InjTFOrigin1 work_pred (ctLocOrigin work_loc) (ctLocSpan work_loc)
inert_pred (ctLocOrigin inert_loc) (ctLocSpan inert_loc)
eqn_loc = setCtLocOrigin initial_loc eqn_orig
inert_pred = ctEvPred inert_ev
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/e39fd1ef1d32c256bf124b496940399c29bd8d34
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/e39fd1ef1d32c256bf124b496940399c29bd8d34
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/20240619/e304cf2c/attachment-0001.html>
More information about the ghc-commits
mailing list