[Git][ghc/ghc][wip/T24978] More updates
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Tue Jun 25 16:34:25 UTC 2024
Simon Peyton Jones pushed to branch wip/T24978 at Glasgow Haskell Compiler / GHC
Commits:
2e1a44b1 by Simon Peyton Jones at 2024-06-25T17:34:04+01:00
More updates
- - - - -
7 changed files:
- compiler/GHC/Builtin/Types/Literals.hs
- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/Coercion.hs-boot
- compiler/GHC/Core/TyCo/Rep.hs
- compiler/GHC/Tc/Solver/Equality.hs
- compiler/GHC/Tc/Solver/Monad.hs
- docs/users_guide/9.12.1-notes.rst
Changes:
=====================================
compiler/GHC/Builtin/Types/Literals.hs
=====================================
@@ -273,19 +273,19 @@ axAddTops :: [CoAxiomRule]
axAddTops
= [ -- (s + t ~ 0) => (s ~ 0)
mkTopBinFamDeduction "AddT-0L" typeNatAddTyCon $ \ a _b r ->
- do { known r (== 0); return (Pair a (num 0)) }
+ do { _ <- known r (== 0); return (Pair a (num 0)) }
, -- (s + t ~ 0) => (t ~ 0)
mkTopBinFamDeduction "AddT-0R" typeNatAddTyCon $ \ _a b r ->
- do { known r (== 0); return (Pair b (num 0)) }
+ do { _ <- known r (== 0); return (Pair b (num 0)) }
, -- (5 + t ~ 8) => (t ~ 3)
mkTopBinFamDeduction "AddT-KKL" typeNatAddTyCon $ \ a b r ->
- do { na <- isNumLitTy a; nr <- isNumLitTy r; return (Pair b (num (nr-na))) }
+ do { na <- isNumLitTy a; nr <- known r (>= na); return (Pair b (num (nr-na))) }
, -- (s + 5 ~ 8) => (s ~ 3)
mkTopBinFamDeduction "AddT-KKR" typeNatAddTyCon $ \ a b r ->
- do { nb <- isNumLitTy b; nr <- isNumLitTy r; return (Pair a (num (nr-nb))) } ]
+ do { nb <- isNumLitTy b; nr <- known r (>= nb); return (Pair a (num (nr-nb))) } ]
axAddInteracts :: [CoAxiomRule]
axAddInteracts
@@ -405,11 +405,11 @@ axMulTops :: [CoAxiomRule]
axMulTops
= [ -- (s * t ~ 1) => (s ~ 1)
mkTopBinFamDeduction "MulT1" typeNatMulTyCon $ \ s _t r ->
- do { known r (== 1); return (Pair s r) }
+ do { _ <- known r (== 1); return (Pair s r) }
, -- (s * t ~ 1) => (t ~ 1)
mkTopBinFamDeduction "MulT2" typeNatMulTyCon $ \ _s t r ->
- do { known r (== 1); return (Pair t r) }
+ do { _ <- known r (== 1); return (Pair t r) }
, -- (3 * t ~ 15) => (t ~ 5)
mkTopBinFamDeduction "MulT3" typeNatMulTyCon $ \ s t r ->
@@ -423,11 +423,11 @@ axMulInteracts :: [CoAxiomRule]
axMulInteracts
= [ -- (x*y1 ~ z, x*y2 ~ z) => (y1~y2) if x/=0
mkInteractBinFamDeduction "MulI1" typeNatMulTyCon $ \ x1 y1 z1 x2 y2 z2 ->
- do { known x1 (/= 0); same x1 x2; same z1 z2; return (Pair y1 y2) }
+ do { nx1 <- known x1 (/= 0); _ <- known x2 (== nx1); same z1 z2; return (Pair y1 y2) }
, -- (x1*y ~ z, x2*y ~ z) => (x1~x2) if y/0
mkInteractBinFamDeduction "MulI2" typeNatMulTyCon $ \ x1 y1 z1 x2 y2 z2 ->
- do { known y1 (/= 0); same y1 y2; same z1 z2; return (Pair x1 x2) } ]
+ do { ny1 <- known y1 (/= 0); _ <- known y2 (== ny1); same z1 z2; return (Pair x1 x2) } ]
-------------------------------------------------------------------------------
@@ -480,8 +480,8 @@ typeNatExpTyCon :: TyCon -- Exponentiation
typeNatExpTyCon = mkTypeNatFunTyCon2 name
BuiltInSynFamily
{ sfMatchFam = matchFamExp
- , sfInteractInert = axExpTops
- , sfInteractTop = axExpInteracts
+ , sfInteractTop = axExpTops
+ , sfInteractInert = axExpInteracts
}
where
name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPENATS (fsLit "^")
@@ -516,13 +516,11 @@ axExpInteracts :: [CoAxiomRule]
axExpInteracts
= [ -- (x1^y1 ~ z, x2^y2 ~ z) {x1=x2, x1>1}=> (y1~y2)
mkInteractBinFamDeduction "ExpI1" typeNatExpTyCon $ \ x1 y1 z1 x2 y2 z2 ->
- do { known x1 (> 1); same x1 x2; same z1 z2; return (Pair y1 y2) }
+ do { nx1 <- known x1 (> 1); _ <- known x2 (== nx1); same z1 z2; return (Pair y1 y2) }
, -- (x1^y1 ~ z, x2^y2 ~ z) {y1=y2, y1>0}=> (x1~x2)
mkInteractBinFamDeduction "ExpI2" typeNatExpTyCon $ \ x1 y1 z1 x2 y2 z2 ->
- do { known y1 (> 0); same y1 y2; same z1 z2; return (Pair x1 x2) } ]
-
-
+ do { ny1 <- known y1 (> 0); _ <- known y2 (== ny1); same z1 z2; return (Pair x1 x2) } ]
-------------------------------------------------------------------------------
-- Logarithm: Log2
-------------------------------------------------------------------------------
@@ -1162,8 +1160,8 @@ injCheck x1 x2 y1 y2 z1 z2
same :: Type -> Type -> Maybe ()
same ty1 ty2 = guard (ty1 `tcEqType` ty2)
-known :: Type -> (Integer -> Bool) -> Maybe ()
-known x p = do { nx <- isNumLitTy x; guard (p nx) }
+known :: Type -> (Integer -> Bool) -> Maybe Integer
+known x p = do { nx <- isNumLitTy x; guard (p nx); return nx }
charToInteger :: Char -> Integer
charToInteger c = fromIntegral (Char.ord c)
@@ -1274,7 +1272,7 @@ typeCharCmpTyCon =
typeCharCmpTyFamNameKey typeCharCmpTyCon
ops = BuiltInSynFamily
{ sfMatchFam = matchFamCmpChar
- , sfInteractTop = [axCmpCharTop]
+ , sfInteractTop = axCmpCharTops
, sfInteractInert = []
}
@@ -1296,10 +1294,11 @@ axCmpCharDef = mkBinAxiom "CmpCharDef" typeCharCmpTyCon isCharLitTy isCharLitTy
axCmpCharRefl = mkAxiom1 "CmpCharRefl" $
\(Pair s _) -> (cmpChar s s) === ordering EQ
-axCmpCharTop :: CoAxiomRule
-axCmpCharTop -- (CmpChar s t ~ EQ) => s ~ t
- = mkTopBinFamDeduction "CmpCharT" typeCharCmpTyCon $ \ s t r ->
- do { EQ <- isOrderingLitTy r; return (Pair s t) }
+axCmpCharTops :: [CoAxiomRule]
+axCmpCharTops
+ = [ -- (CmpChar s t ~ EQ) => s ~ t
+ mkTopBinFamDeduction "CmpCharT" typeCharCmpTyCon $ \ s t r ->
+ do { EQ <- isOrderingLitTy r; return (Pair s t) } ]
=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -2446,10 +2446,10 @@ coercionType co = case coercionKindRole co of
--
-- i.e. the kind of @c@ relates @t1@ and @t2@, then @coercionKind c = Pair t1 t2 at .
-coercionKind :: Coercion -> Pair Type
+coercionKind :: HasDebugCallStack => Coercion -> Pair Type
coercionKind co = Pair (coercionLKind co) (coercionRKind co)
-coercionLKind :: Coercion -> Type
+coercionLKind :: HasDebugCallStack => Coercion -> Type
coercionLKind co
= go co
where
@@ -2494,7 +2494,7 @@ coercionLKind co
go_app (InstCo co arg) args = go_app co (go arg:args)
go_app co args = piResultTys (go co) args
-coercionRKind :: Coercion -> Type
+coercionRKind :: HasDebugCallStack => Coercion -> Type
coercionRKind co
= go co
where
=====================================
compiler/GHC/Core/Coercion.hs-boot
=====================================
@@ -49,9 +49,9 @@ mkCoercionType :: Role -> Type -> Type -> Type
seqCo :: Coercion -> ()
-coercionKind :: Coercion -> Pair Type
-coercionLKind :: Coercion -> Type
-coercionRKind :: Coercion -> Type
+coercionKind :: HasDebugCallStack => Coercion -> Pair Type
+coercionLKind :: HasDebugCallStack => Coercion -> Type
+coercionRKind :: HasDebugCallStack => Coercion -> Type
coercionType :: Coercion -> Type
topNormaliseNewType_maybe :: Type -> Maybe (Coercion, Type)
=====================================
compiler/GHC/Core/TyCo/Rep.hs
=====================================
@@ -1546,8 +1546,8 @@ 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
-
+ explicity given) depends. See
+ Note [The importance of tracking UnivCo dependencies]
-}
-- | For simplicity, we have just one UnivCo that represents a coercion from
=====================================
compiler/GHC/Tc/Solver/Equality.hs
=====================================
@@ -2935,13 +2935,10 @@ tryFamFamInjectivity ev eq_rel fun_tc1 fun_args1 fun_tc2 fun_args2 mco
= return False -- Injectivity applies only for Nominal equalities
| fun_tc1 /= fun_tc2
= return False -- If the families don't match, stop.
- | isGiven ev
- = return False -- See Note [No Given/Given fundeps] in GHC.Tc.Solver.Dict
-
- -- So this is a [W] (F tys1 ~N# F tys2)
-- Is F an injective type family
- | Injective inj <- tyConInjectivityInfo fun_tc1
+ | isWanted ev -- Injectivity conditions only work for Wanteds
+ , Injective inj <- tyConInjectivityInfo fun_tc1
= unifyFunDeps ev Nominal $ \uenv ->
uPairsTcM uenv [ Pair ty1 ty2
| (ty1,ty2,True) <- zip3 fun_args1 fun_args2 inj ]
@@ -2952,6 +2949,8 @@ tryFamFamInjectivity ev eq_rel fun_tc1 fun_args1 fun_tc2 fun_args2 mco
-- be a burden to make sure the new entry point and existing ones
-- were internally consistent. This is slightly distasteful, but
-- it works well in practice and localises the problem. Ugh.
+ --
+ -- This path works both Wanteds and Givens
| Just ops <- isBuiltInSynFamTyCon_maybe fun_tc1
= let tc_kind = tyConKind fun_tc1
ki1 = piResultTys tc_kind fun_args1
@@ -2967,8 +2966,12 @@ tryFamFamInjectivity ev eq_rel fun_tc1 fun_args1 fun_tc2 fun_args2 mco
eqs = map snd $ tryInteractInertFam ops fun_tc1
fun_args1 fake_rhs1 fun_args2 fake_rhs2
in
- unifyFunDeps ev Nominal $ \uenv ->
- uPairsTcM uenv eqs
+ do { traceTcS "famfam" (vcat [ppr fun_tc1
+ , text "1side" <+> ppr fun_args1 <+> ppr fake_rhs1
+ , text "2side" <+> ppr fun_args2 <+> ppr fake_rhs2
+ , ppr eqs ])
+ ; unifyFunDeps ev Nominal $ \uenv ->
+ uPairsTcM uenv eqs }
| otherwise -- ordinary, non-injective type family
= return False
@@ -2998,11 +3001,12 @@ improveTopFunEqs fam_tc args (EqCt { eq_ev = ev, eq_rhs = 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) $
+ = do { traceTcS "improveGivenTopFunEqs" (ppr fam_tc <+> ppr args $$ ppr ev $$ ppr rhs_ty)
+ ; emitNewGivens (ctEvLoc ev) $
[ (Nominal, new_co)
| (ax, _) <- tryInteractTopFam ops fam_tc args rhs_ty
, let new_co = mkAxiomRuleCo ax [given_co] ]
- ; return False }
+ ; return False } -- False: no unifications
| otherwise
= return False -- See Note [No Given/Given fundeps]
where
@@ -3122,19 +3126,25 @@ improveGivenLocalFunEqs :: [EqCt] -- Inert items, mixture of Given and Wanted
-- e.g. (x+y1~z, x+y2~z) => (y1 ~ y2)
improveGivenLocalFunEqs funeqs_for_tc fam_tc work_args work_ev work_rhs
| Just ops <- isBuiltInSynFamTyCon_maybe fam_tc
- = foldlM (do_one ops) False funeqs_for_tc
+ = do { mapM_ (do_one ops) funeqs_for_tc
+ ; return False } -- False: no unifications
| otherwise
= return False
where
given_co :: Coercion = ctEvCoercion work_ev
- do_one :: BuiltInSynFamily -> Bool -> EqCt -> TcS Bool
- do_one ops _ (EqCt { eq_ev = inert_ev
- , eq_lhs = TyFamLHS _ inert_args
- , eq_rhs = inert_rhs })
+ do_one :: BuiltInSynFamily -> EqCt -> TcS ()
+ do_one ops (EqCt { eq_ev = inert_ev
+ , eq_lhs = TyFamLHS _ inert_args
+ , eq_rhs = inert_rhs })
| isGiven inert_ev
, not (null pairs)
- = do { emitNewGivens (ctEvLoc inert_ev) pairs; return True }
+ = do { traceTcS "improveGivenLocalFunEqs" (vcat[ ppr fam_tc <+> ppr work_args
+ , text "work_ev" <+> ppr work_ev
+ , text "inert_ev" <+> ppr inert_ev
+ , ppr work_rhs
+ , ppr pairs ])
+ ; emitNewGivens (ctEvLoc inert_ev) pairs }
-- This CtLoc for the new Givens doesn't reflect the
-- fact that it's a combination of Givens, but I don't
-- this that matters.
@@ -3142,9 +3152,9 @@ improveGivenLocalFunEqs funeqs_for_tc fam_tc work_args work_ev work_rhs
pairs = [ (Nominal, new_co)
| (ax, _) <- tryInteractInertFam ops fam_tc
work_args work_rhs inert_args inert_rhs
- , let new_co = mkAxiomRuleCo ax [given_co] ]
+ , let new_co = mkAxiomRuleCo ax [given_co, ctEvCoercion inert_ev] ]
- do_one _ so_far _ = return so_far
+ do_one _ _ = return ()
improveWantedLocalFunEqs
:: [EqCt] -- Inert items (Given and Wanted)
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -1773,7 +1773,8 @@ newBoundEvVarId pred rhs
emitNewGivens :: CtLoc -> [(Role,TcCoercion)] -> TcS ()
emitNewGivens loc pts
- = do { evs <- mapM (newGivenEvVar loc) $
+ = do { traceTcS "emitNewGivens" (ppr pts)
+ ; evs <- mapM (newGivenEvVar loc) $
[ (mkPrimEqPredRole role ty1 ty2, evCoercion co)
| (role, co) <- pts
, let Pair ty1 ty2 = coercionKind co
=====================================
docs/users_guide/9.12.1-notes.rst
=====================================
@@ -44,7 +44,7 @@ Compiler
for typing plugins, gets an extra ``DCoVarSet`` argument.
The argument is intended to 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]``
+ See ``Note [The importance of tracking UnivCo dependencies]``
in ``GHC.Core.TyCo.Rep``, :ref:`constraint-solving-with-plugins`
and the migration guide.
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/2e1a44b178f3968fa4b4c5380f7a30ad30124526
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/2e1a44b178f3968fa4b4c5380f7a30ad30124526
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/20240625/3e11daf6/attachment-0001.html>
More information about the ghc-commits
mailing list