[Git][ghc/ghc][master] Prioritise nominal equalities
Marge Bot (@marge-bot)
gitlab at gitlab.haskell.org
Wed Jun 12 16:54:43 UTC 2024
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
b0b64177 by Simon Peyton Jones at 2024-06-12T12:53:31-04:00
Prioritise nominal equalities
The main payload of this patch is
* Prioritise nominal equalities in the constraint solver. This
ameliorates the incompleteness of solving for representational
constraints over newtypes: see #24887.
See (EX2) in Note [Decomposing newtype equalities] in
GHC.Tc.Solver.Equality
In doing this patch I tripped over some other things that I refactored:
* Move `isCoVarType` from `GHC.Core.Type` to `GHC.Core.Predicate`
where it seems more at home.
* Clarify the "rewrite role" of a constraint. I was very puzzled
about what the role of, say `(Eq a)` might be, but see the new
Note [The rewrite-role of a constraint].
In doing so I made predTypeEqRel crash when given a non-equality.
Usually it expects an equality; but it was being mis-used for
the above rewrite-role stuff.
- - - - -
16 changed files:
- compiler/GHC/Core/Lint.hs
- compiler/GHC/Core/Make.hs
- compiler/GHC/Core/Predicate.hs
- compiler/GHC/Core/SimpleOpt.hs
- compiler/GHC/Core/Type.hs
- compiler/GHC/Core/Utils.hs
- compiler/GHC/Tc/Solver/Dict.hs
- compiler/GHC/Tc/Solver/Equality.hs
- compiler/GHC/Tc/Solver/InertSet.hs
- compiler/GHC/Tc/Solver/Rewrite.hs
- compiler/GHC/Tc/Solver/Solve.hs
- compiler/GHC/Tc/Types.hs
- compiler/GHC/Tc/Types/Constraint.hs
- compiler/GHC/Types/Id.hs
- + testsuite/tests/typecheck/should_compile/T24887.hs
- testsuite/tests/typecheck/should_compile/all.T
Changes:
=====================================
compiler/GHC/Core/Lint.hs
=====================================
@@ -49,6 +49,7 @@ import GHC.Core.DataCon
import GHC.Core.Ppr
import GHC.Core.Coercion
import GHC.Core.Type as Type
+import GHC.Core.Predicate( isCoVarType )
import GHC.Core.Multiplicity
import GHC.Core.UsageEnv
import GHC.Core.TyCo.Rep -- checks validity of types/coercions
=====================================
compiler/GHC/Core/Make.hs
=====================================
@@ -67,9 +67,10 @@ import GHC.Types.Unique.Supply
import GHC.Core
import GHC.Core.Utils ( exprType, mkSingleAltCase, bindNonRec )
import GHC.Core.Type
-import GHC.Core.TyCo.Compare( eqType )
-import GHC.Core.Coercion ( isCoVar )
-import GHC.Core.DataCon ( DataCon, dataConWorkId )
+import GHC.Core.Predicate ( isCoVarType )
+import GHC.Core.TyCo.Compare ( eqType )
+import GHC.Core.Coercion ( isCoVar )
+import GHC.Core.DataCon ( DataCon, dataConWorkId )
import GHC.Core.Multiplicity
import GHC.Builtin.Types
=====================================
compiler/GHC/Core/Predicate.hs
=====================================
@@ -12,7 +12,7 @@ module GHC.Core.Predicate (
-- Equality predicates
EqRel(..), eqRelRole,
- isEqPrimPred, isEqPred,
+ isEqPrimPred, isNomEqPred, isReprEqPrimPred, isEqPred, isCoVarType,
getEqPredTys, getEqPredTys_maybe, getEqPredRole,
predTypeEqRel,
mkPrimEqPred, mkReprPrimEqPred, mkPrimEqPredRole,
@@ -60,7 +60,7 @@ data Pred
-- | A typeclass predicate.
= ClassPred Class [Type]
- -- | A type equality predicate.
+ -- | A type equality predicate, (t1 ~#N t2) or (t1 ~#R t2)
| EqPred EqRel Type Type
-- | An irreducible predicate.
@@ -80,7 +80,7 @@ classifyPredType :: PredType -> Pred
classifyPredType ev_ty = case splitTyConApp_maybe ev_ty of
Just (tc, [_, _, ty1, ty2])
| tc `hasKey` eqReprPrimTyConKey -> EqPred ReprEq ty1 ty2
- | tc `hasKey` eqPrimTyConKey -> EqPred NomEq ty1 ty2
+ | tc `hasKey` eqPrimTyConKey -> EqPred NomEq ty1 ty2
Just (tc, tys)
| Just clas <- tyConClass_maybe tc
@@ -189,16 +189,21 @@ getEqPredTys_maybe ty
_ -> Nothing
getEqPredRole :: PredType -> Role
+-- Precondition: the PredType is (s ~#N t) or (s ~#R t)
getEqPredRole ty = eqRelRole (predTypeEqRel ty)
-- | Get the equality relation relevant for a pred type.
-predTypeEqRel :: PredType -> EqRel
+-- Precondition: the PredType is (s ~#N t) or (s ~#R t)
+predTypeEqRel :: HasDebugCallStack => PredType -> EqRel
predTypeEqRel ty
- | Just (tc, _) <- splitTyConApp_maybe ty
- , tc `hasKey` eqReprPrimTyConKey
- = ReprEq
- | otherwise
- = NomEq
+ = case splitTyConApp_maybe ty of
+ Just (tc, _) | tc `hasKey` eqReprPrimTyConKey
+ -> ReprEq
+ | otherwise
+ -> assertPpr (tc `hasKey` eqPrimTyConKey) (ppr ty)
+ NomEq
+ _ -> pprPanic "predTypeEqRel" (ppr ty)
+
{-------------------------------------------
Predicates on PredType
@@ -219,20 +224,51 @@ see Note [Equality superclasses in quantified constraints]
in GHC.Tc.Solver.Dict.
-}
+-- | Does this type classify a core (unlifted) Coercion?
+-- At either role nominal or representational
+-- (t1 ~# t2) or (t1 ~R# t2)
+-- See Note [Types for coercions, predicates, and evidence] in "GHC.Core.TyCo.Rep"
+isCoVarType :: Type -> Bool
+ -- ToDo: should we check saturation?
+isCoVarType ty = isEqPrimPred ty
+
isEvVarType :: Type -> Bool
--- True of (a) predicates, of kind Constraint, such as (Eq a), and (a ~ b)
--- (b) coercion types, such as (t1 ~# t2) or (t1 ~R# t2)
+-- True of (a) predicates, of kind Constraint, such as (Eq t), and (s ~ t)
+-- (b) coercion types, such as (s ~# t) or (s ~R# t)
-- See Note [Types for coercions, predicates, and evidence] in GHC.Core.TyCo.Rep
-- See Note [Evidence for quantified constraints]
isEvVarType ty = isCoVarType ty || isPredTy ty
+isEqPrimPred :: PredType -> Bool
+-- True of (s ~# t) (s ~R# t)
+isEqPrimPred ty
+ | Just tc <- tyConAppTyCon_maybe ty
+ = tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey
+ | otherwise
+ = False
+
+isReprEqPrimPred :: PredType -> Bool
+isReprEqPrimPred ty
+ | Just tc <- tyConAppTyCon_maybe ty
+ = tc `hasKey` eqReprPrimTyConKey
+ | otherwise
+ = False
+
+isNomEqPred :: PredType -> Bool
+-- A nominal equality, primitive or not (s ~# t), (s ~ t), or (s ~~ t)
+isNomEqPred ty
+ | Just tc <- tyConAppTyCon_maybe ty
+ = tc `hasKey` eqPrimTyConKey || tc `hasKey` heqTyConKey || tc `hasKey` eqTyConKey
+ | otherwise
+ = False
+
isClassPred :: PredType -> Bool
isClassPred ty = case tyConAppTyCon_maybe ty of
Just tc -> isClassTyCon tc
_ -> False
isEqPred :: PredType -> Bool
-isEqPred ty -- True of (a ~ b) and (a ~~ b)
+isEqPred ty -- True of (s ~ t) and (s ~~ t)
-- ToDo: should we check saturation?
| Just tc <- tyConAppTyCon_maybe ty
, Just cls <- tyConClass_maybe tc
@@ -240,10 +276,6 @@ isEqPred ty -- True of (a ~ b) and (a ~~ b)
| otherwise
= False
-isEqPrimPred :: PredType -> Bool
-isEqPrimPred ty = isCoVarType ty
- -- True of (a ~# b) (a ~R# b)
-
isEqualityClass :: Class -> Bool
-- True of (~), (~~), and Coercible
-- These all have a single primitive-equality superclass, either (~N# or ~R#)
=====================================
compiler/GHC/Core/SimpleOpt.hs
=====================================
@@ -29,27 +29,32 @@ import GHC.Core.Unfold
import GHC.Core.Unfold.Make
import GHC.Core.Make ( FloatBind(..), mkWildValBinder )
import GHC.Core.Opt.OccurAnal( occurAnalyseExpr, occurAnalysePgm, zapLambdaBndrs )
+import GHC.Core.DataCon
+import GHC.Core.Coercion.Opt ( optCoercion, OptCoercionOpts (..) )
+import GHC.Core.Type hiding ( substTy, extendTvSubst, extendCvSubst, extendTvSubstList
+ , isInScope, substTyVarBndr, cloneTyVarBndr )
+import GHC.Core.Predicate( isCoVarType )
+import GHC.Core.Coercion hiding ( substCo, substCoVarBndr )
+
import GHC.Types.Literal
import GHC.Types.Id
import GHC.Types.Id.Info ( realUnfoldingInfo, setUnfoldingInfo, setRuleInfo, IdInfo (..) )
import GHC.Types.Var ( isNonCoVarId )
import GHC.Types.Var.Set
import GHC.Types.Var.Env
-import GHC.Core.DataCon
import GHC.Types.Demand( etaConvertDmdSig, topSubDmd )
import GHC.Types.Tickish
-import GHC.Core.Coercion.Opt ( optCoercion, OptCoercionOpts (..) )
-import GHC.Core.Type hiding ( substTy, extendTvSubst, extendCvSubst, extendTvSubstList
- , isInScope, substTyVarBndr, cloneTyVarBndr )
-import GHC.Core.Coercion hiding ( substCo, substCoVarBndr )
+import GHC.Types.Basic
+
import GHC.Builtin.Types
import GHC.Builtin.Names
-import GHC.Types.Basic
+
import GHC.Unit.Module ( Module )
import GHC.Utils.Encoding
import GHC.Utils.Outputable
import GHC.Utils.Panic
import GHC.Utils.Misc
+
import GHC.Data.Maybe ( orElse )
import GHC.Data.Graph.UnVar
import Data.List (mapAccumL)
=====================================
compiler/GHC/Core/Type.hs
=====================================
@@ -113,7 +113,7 @@ module GHC.Core.Type (
isForAllTy_ty, isForAllTy_co,
isForAllTy_invis_ty,
isPiTy, isTauTy, isFamFreeTy,
- isCoVarType, isAtomicTy,
+ isAtomicTy,
isValidJoinPointType,
tyConAppNeedsKindSig,
@@ -2493,18 +2493,6 @@ isTerminatingType ty = case tyConAppTyCon_maybe ty of
Just tc -> isClassTyCon tc && not (isNewTyCon tc)
_ -> False
--- | Does this type classify a core (unlifted) Coercion?
--- At either role nominal or representational
--- (t1 ~# t2) or (t1 ~R# t2)
--- See Note [Types for coercions, predicates, and evidence] in "GHC.Core.TyCo.Rep"
-isCoVarType :: Type -> Bool
- -- ToDo: should we check saturation?
-isCoVarType ty
- | Just tc <- tyConAppTyCon_maybe ty
- = tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey
- | otherwise
- = False
-
isPrimitiveType :: Type -> Bool
-- ^ Returns true of types that are opaque to Haskell.
isPrimitiveType ty = case splitTyConApp_maybe ty of
=====================================
compiler/GHC/Core/Utils.hs
=====================================
@@ -74,6 +74,7 @@ import GHC.Core.Ppr
import GHC.Core.FVs( bindFreeVars )
import GHC.Core.DataCon
import GHC.Core.Type as Type
+import GHC.Core.Predicate( isCoVarType )
import GHC.Core.FamInstEnv
import GHC.Core.TyCo.Compare( eqType, eqTypeX )
import GHC.Core.Coercion
=====================================
compiler/GHC/Tc/Solver/Dict.hs
=====================================
@@ -84,7 +84,7 @@ solveDict dict_ct@(DictCt { di_ev = ev, di_cls = cls, di_tys = tys })
= solveEqualityDict ev cls tys
| otherwise
- = assertPpr (ctEvRole ev == Nominal) (ppr ev $$ ppr cls $$ ppr tys) $
+ = assertPpr (ctEvRewriteRole ev == Nominal) (ppr ev $$ ppr cls $$ ppr tys) $
do { simpleStage $ traceTcS "solveDict" (ppr dict_ct)
; tryInertDicts dict_ct
=====================================
compiler/GHC/Tc/Solver/Equality.hs
=====================================
@@ -1092,11 +1092,29 @@ There are two ways in which decomposing (N ty1) ~r (N ty2) could be incomplete:
have a nominal role. Thus, decomposing the wanted will yield [W] Int ~N Age,
which is unsatisfiable. Unwrapping, though, leads to a solution.
- Conclusion: always unwrap newtypes before attempting to decompose
+ CONCLUSION: always unwrap newtypes before attempting to decompose
them. This is done in can_eq_nc. Of course, we can't unwrap if the data
constructor isn't in scope. See Note [Unwrap newtypes first].
-* Incompleteness example (EX2): available Givens
+* Incompleteness example (EX2): see #24887
+ data family D a
+ data instance D Int = MkD1 (D Char)
+ data instance D Bool = MkD2 (D Char)
+ Now suppose we have
+ [W] g1: D Int ~R# D a
+ [W] g2: a ~# Bool
+ If we solve g2 first, giving a:=Bool, then we can solve g1 easily:
+ D Int ~R# D Char ~R# D Bool
+ by newtype unwrapping.
+
+ BUT: if we instead attempt to solve g1 first, we can unwrap the LHS (only)
+ leaving [W] D Char ~#R D Bool
+ If we decompose now, we'll get (Char ~R# Bool), which is insoluble.
+
+ CONCLUSION: prioritise nominal equalites in the work list.
+ See Note [Prioritise equalities] in GHC.Tc.Solver.InertSet.
+
+* Incompleteness example (EX3): available Givens
newtype Nt a = Mk Bool -- NB: a is not used in the RHS,
type role Nt representational -- but the user gives it an R role anyway
@@ -1110,7 +1128,7 @@ There are two ways in which decomposing (N ty1) ~r (N ty2) could be incomplete:
Givens for class constraints: see Note [Instance and Given overlap] in
GHC.Tc.Solver.Dict.
- Conclusion: don't decompose [W] N s ~R N t, if there are any Given
+ CONCLUSION: don't decompose [W] N s ~R N t, if there are any Given
equalities that could later solve it.
But what precisely does it mean to say "any Given equalities that could
@@ -2536,7 +2554,7 @@ rewriteEqEvidence new_rewriters old_ev swapped (Reduction lhs_co nlhs) (Reductio
| CtWanted { ctev_dest = dest
, ctev_rewriters = rewriters } <- old_ev
, let rewriters' = rewriters S.<> new_rewriters
- = do { (new_ev, hole_co) <- newWantedEq loc rewriters' (ctEvRole old_ev) nlhs nrhs
+ = do { (new_ev, hole_co) <- newWantedEq loc rewriters' (ctEvRewriteRole old_ev) nlhs nrhs
; let co = maybeSymCo swapped $
lhs_co `mkTransCo` hole_co `mkTransCo` mkSymCo rhs_co
; setWantedEq dest co
@@ -2602,7 +2620,7 @@ tryInertEqs work_item@(EqCt { eq_ev = ev, eq_eq_rel = eq_rel })
-> do { setEvBindIfWanted ev True $
evCoercion (maybeSymCo swapped $
downgradeRole (eqRelRole eq_rel)
- (ctEvRole ev_i)
+ (ctEvRewriteRole ev_i)
(ctEvCoercion ev_i))
; stopWith ev "Solved from inert" }
=====================================
compiler/GHC/Tc/Solver/InertSet.hs
=====================================
@@ -133,9 +133,16 @@ It's very important to process equalities over class constraints:
E.g. a CIrredCan can be a hetero-kinded (t1 ~ t2), which may become
homo-kinded when kicked out, and hence we want to prioritise it.
-Among the equalities we prioritise ones with an empty rewriter set;
-see Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint, wrinkle (W1).
+Further refinements:
+* Among the equalities we prioritise ones with an empty rewriter set;
+ see Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint, wrinkle (W1).
+
+* Among equalities with an empty rewriter set, we prioritise nominal equalities.
+ * They have more rewriting power, so doing them first is better.
+ * Prioritising them ameliorates the incompleteness of newtype
+ solving: see (Ex2) in Note [Decomposing newtype equalities] in
+ GHC.Tc.Solver.Equality.
Note [Prioritise class equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -168,12 +175,14 @@ See GHC.Tc.Solver.Monad.deferTcSForAllEq
-- See Note [WorkList priorities]
data WorkList
- = WL { wl_eqs :: [Ct] -- CEqCan, CDictCan, CIrredCan
- -- Given and Wanted
- -- Contains both equality constraints and their
- -- class-level variants (a~b) and (a~~b);
- -- See Note [Prioritise equalities]
- -- See Note [Prioritise class equalities]
+ = WL { wl_eqs_N :: [Ct] -- /Nominal/ equalities (s ~#N t), (s ~ t), (s ~~ t)
+ -- with empty rewriter set
+ , wl_eqs_X :: [Ct] -- CEqCan, CDictCan, CIrredCan
+ -- with empty rewriter set
+ -- All other equalities: contains both equality constraints and
+ -- their class-level variants (a~b) and (a~~b);
+ -- See Note [Prioritise equalities]
+ -- See Note [Prioritise class equalities]
, wl_rw_eqs :: [Ct] -- Like wl_eqs, but ones that have a non-empty
-- rewriter set; or, more precisely, did when
@@ -182,48 +191,69 @@ data WorkList
-- see Note [Prioritise Wanteds with empty RewriterSet]
-- in GHC.Tc.Types.Constraint for more details.
- , wl_rest :: [Ct]
+ , wl_rest :: [Ct]
, wl_implics :: Bag Implication -- See Note [Residual implications]
}
appendWorkList :: WorkList -> WorkList -> WorkList
appendWorkList
- (WL { wl_eqs = eqs1, wl_rw_eqs = rw_eqs1
+ (WL { wl_eqs_N = eqs1_N, wl_eqs_X = eqs1_X, wl_rw_eqs = rw_eqs1
, wl_rest = rest1, wl_implics = implics1 })
- (WL { wl_eqs = eqs2, wl_rw_eqs = rw_eqs2
+ (WL { wl_eqs_N = eqs2_N, wl_eqs_X = eqs2_X, wl_rw_eqs = rw_eqs2
, wl_rest = rest2, wl_implics = implics2 })
- = WL { wl_eqs = eqs1 ++ eqs2
+ = WL { wl_eqs_N = eqs1_N ++ eqs2_N
+ , wl_eqs_X = eqs1_X ++ eqs2_X
, wl_rw_eqs = rw_eqs1 ++ rw_eqs2
, wl_rest = rest1 ++ rest2
, wl_implics = implics1 `unionBags` implics2 }
workListSize :: WorkList -> Int
-workListSize (WL { wl_eqs = eqs, wl_rw_eqs = rw_eqs, wl_rest = rest })
- = length eqs + length rw_eqs + length rest
+workListSize (WL { wl_eqs_N = eqs_N, wl_eqs_X = eqs_X, wl_rw_eqs = rw_eqs, wl_rest = rest })
+ = length eqs_N + length eqs_X + length rw_eqs + length rest
extendWorkListEq :: RewriterSet -> Ct -> WorkList -> WorkList
-extendWorkListEq rewriters ct wl
+extendWorkListEq rewriters ct
+ wl@(WL { wl_eqs_N = eqs_N, wl_eqs_X = eqs_X, wl_rw_eqs = rw_eqs })
| isEmptyRewriterSet rewriters -- A wanted that has not been rewritten
-- isEmptyRewriterSet: see Note [Prioritise Wanteds with empty RewriterSet]
-- in GHC.Tc.Types.Constraint
- = wl { wl_eqs = ct : wl_eqs wl }
+ = if isNomEqPred (ctPred ct)
+ then wl { wl_eqs_N = ct : eqs_N }
+ else wl { wl_eqs_X = ct : eqs_X }
+
| otherwise
- = wl { wl_rw_eqs = ct : wl_rw_eqs wl }
+ = wl { wl_rw_eqs = ct : rw_eqs }
extendWorkListEqs :: RewriterSet -> Bag Ct -> WorkList -> WorkList
-- Add [eq1,...,eqn] to the work-list
-- They all have the same rewriter set
-- The constraints will be solved in left-to-right order:
--- see Note [Work-list ordering] in GHC.Tc.Solved.Equality
-extendWorkListEqs rewriters eqs wl
+-- see Note [Work-list ordering] in GHC.Tc.Solver.Equality
+--
+-- Precondition: new_eqs is non-empty
+extendWorkListEqs rewriters new_eqs
+ wl@(WL { wl_eqs_N = eqs_N, wl_eqs_X = eqs_X, wl_rw_eqs = rw_eqs })
| isEmptyRewriterSet rewriters
-- isEmptyRewriterSet: see Note [Prioritise Wanteds with empty RewriterSet]
-- in GHC.Tc.Types.Constraint
- = wl { wl_eqs = foldr (:) (wl_eqs wl) eqs }
- -- The foldr just appends wl_eqs to the bag of eqs
+ = case partitionBag is_nominal new_eqs of
+ (new_eqs_N, new_eqs_X)
+ | isEmptyBag new_eqs_N -> wl { wl_eqs_X = new_eqs_X `push_on_front` eqs_X }
+ | isEmptyBag new_eqs_X -> wl { wl_eqs_N = new_eqs_N `push_on_front` eqs_N }
+ | otherwise -> wl { wl_eqs_N = new_eqs_N `push_on_front` eqs_N
+ , wl_eqs_X = new_eqs_X `push_on_front` eqs_X }
+ -- These isEmptyBag tests are just trying
+ -- to avoid creating unnecessary thunks
+
| otherwise
- = wl { wl_rw_eqs = foldr (:) (wl_rw_eqs wl) eqs }
+ = wl { wl_rw_eqs = new_eqs `push_on_front` rw_eqs }
+ where
+ push_on_front :: Bag Ct -> [Ct] -> [Ct]
+ -- push_on_front puts the new equlities on the front of the queue
+ push_on_front new_eqs eqs = foldr (:) eqs new_eqs
+
+ is_nominal ct = isNomEqPred (ctPred ct)
extendWorkListNonEq :: Ct -> WorkList -> WorkList
-- Extension by non equality
@@ -255,26 +285,33 @@ extendWorkListCts :: Cts -> WorkList -> WorkList
extendWorkListCts cts wl = foldr extendWorkListCt wl cts
isEmptyWorkList :: WorkList -> Bool
-isEmptyWorkList (WL { wl_eqs = eqs, wl_rest = rest, wl_implics = implics })
- = null eqs && null rest && isEmptyBag implics
+isEmptyWorkList (WL { wl_eqs_N = eqs_N, wl_eqs_X = eqs_X
+ , wl_rest = rest, wl_implics = implics })
+ = null eqs_N && null eqs_X && null rest && isEmptyBag implics
emptyWorkList :: WorkList
-emptyWorkList = WL { wl_eqs = [], wl_rw_eqs = [], wl_rest = [], wl_implics = emptyBag }
+emptyWorkList = WL { wl_eqs_N = [], wl_eqs_X = []
+ , wl_rw_eqs = [], wl_rest = [], wl_implics = emptyBag }
selectWorkItem :: WorkList -> Maybe (Ct, WorkList)
-- See Note [Prioritise equalities]
-selectWorkItem wl@(WL { wl_eqs = eqs, wl_rw_eqs = rw_eqs, wl_rest = rest })
- | ct:cts <- eqs = Just (ct, wl { wl_eqs = cts })
+selectWorkItem wl@(WL { wl_eqs_N = eqs_N, wl_eqs_X = eqs_X
+ , wl_rw_eqs = rw_eqs, wl_rest = rest })
+ | ct:cts <- eqs_N = Just (ct, wl { wl_eqs_N = cts })
+ | ct:cts <- eqs_X = Just (ct, wl { wl_eqs_X = cts })
| ct:cts <- rw_eqs = Just (ct, wl { wl_rw_eqs = cts })
| ct:cts <- rest = Just (ct, wl { wl_rest = cts })
| otherwise = Nothing
-- Pretty printing
instance Outputable WorkList where
- ppr (WL { wl_eqs = eqs, wl_rw_eqs = rw_eqs, wl_rest = rest, wl_implics = implics })
+ ppr (WL { wl_eqs_N = eqs_N, wl_eqs_X = eqs_X, wl_rw_eqs = rw_eqs
+ , wl_rest = rest, wl_implics = implics })
= text "WL" <+> (braces $
- vcat [ ppUnless (null eqs) $
- text "Eqs =" <+> vcat (map ppr eqs)
+ vcat [ ppUnless (null eqs_N) $
+ text "Eqs_N =" <+> vcat (map ppr eqs_N)
+ , ppUnless (null eqs_X) $
+ text "Eqs_X =" <+> vcat (map ppr eqs_X)
, ppUnless (null rw_eqs) $
text "RwEqs =" <+> vcat (map ppr rw_eqs)
, ppUnless (null rest) $
=====================================
compiler/GHC/Tc/Solver/Rewrite.hs
=====================================
@@ -81,7 +81,7 @@ liftTcS thing_inside
-- the rewriting operation
runRewriteCtEv :: CtEvidence -> RewriteM a -> TcS (a, RewriterSet)
runRewriteCtEv ev
- = runRewrite (ctEvLoc ev) (ctEvFlavour ev) (ctEvEqRel ev)
+ = runRewrite (ctEvLoc ev) (ctEvFlavour ev) (ctEvRewriteEqRel ev)
-- Run thing_inside (which does the rewriting)
-- Also returns the set of Wanteds which rewrote a Wanted;
@@ -160,10 +160,18 @@ recordRewriter other = pprPanic "recordRewriter" (ppr other)
Note [Rewriter EqRels]
~~~~~~~~~~~~~~~~~~~~~~~
When rewriting, we need to know which equality relation -- nominal
-or representation -- we should be respecting. The only difference is
-that we rewrite variables by representational equalities when re_eq_rel
-is ReprEq, and that we unwrap newtypes when rewriting w.r.t.
-representational equality.
+or representational -- we should be respecting. This is controlled
+by the `re_eq_rel` field of RewriteEnv.
+
+* When rewriting primitive /representational/ equalities, (t1 ~# t2),
+ we set re_eq_rel=ReprEq.
+* For all other constraints, we set re_eq_rel=NomEq
+
+See Note [The rewrite-role of a constraint] in GHC.Tc.Types.Constraint.
+
+The only difference is that when re_eq_rel=ReprEq
+* we rewrite variables by representational equalities
+* we unwrap newtypes
Note [Rewriter CtLoc]
~~~~~~~~~~~~~~~~~~~~~~
@@ -233,7 +241,7 @@ rewriteForErrors ev ty
; result@(redn, rewriters) <-
runRewrite (ctEvLoc ev) (ctEvFlavour ev) NomEq (rewrite_one ty)
; traceTcS "rewriteForErrors }" (ppr $ reductionReducedType redn)
- ; return $ case ctEvEqRel ev of
+ ; return $ case ctEvRewriteEqRel ev of
NomEq -> result
ReprEq -> (mkSubRedn redn, rewriters) }
=====================================
compiler/GHC/Tc/Solver/Solve.hs
=====================================
@@ -545,18 +545,21 @@ finish_rewrite ev@(CtGiven { ctev_evar = old_evar, ctev_loc = loc })
; continueWith new_ev }
where
-- mkEvCast optimises ReflCo
- new_tm = mkEvCast (evId old_evar)
- (downgradeRole Representational (ctEvRole ev) co)
+ ev_rw_role = ctEvRewriteRole ev
+ new_tm = assert (coercionRole co == ev_rw_role)
+ mkEvCast (evId old_evar)
+ (downgradeRole Representational ev_rw_role co)
finish_rewrite ev@(CtWanted { ctev_dest = dest
, ctev_loc = loc
, ctev_rewriters = rewriters })
(Reduction co new_pred) new_rewriters
= do { mb_new_ev <- newWanted loc rewriters' new_pred
- ; massert (coercionRole co == ctEvRole ev)
+ ; let ev_rw_role = ctEvRewriteRole ev
+ ; massert (coercionRole co == ev_rw_role)
; setWantedEvTerm dest True $
mkEvCast (getEvExpr mb_new_ev)
- (downgradeRole Representational (ctEvRole ev) (mkSymCo co))
+ (downgradeRole Representational ev_rw_role (mkSymCo co))
; case mb_new_ev of
Fresh new_ev -> continueWith new_ev
Cached _ -> stopWith ev "Cached wanted" }
=====================================
compiler/GHC/Tc/Types.hs
=====================================
@@ -319,9 +319,8 @@ data RewriteEnv
-- See Note [Rewriter CtLoc] in GHC.Tc.Solver.Rewrite.
, re_flavour :: !CtFlavour
, re_eq_rel :: !EqRel
- -- ^ At what role are we rewriting?
- --
- -- See Note [Rewriter EqRels] in GHC.Tc.Solver.Rewrite
+ -- ^ At what role are we rewriting?
+ -- See Note [Rewriter EqRels] in GHC.Tc.Solver.Rewrite
, re_rewriters :: !(TcRef RewriterSet) -- ^ See Note [Wanteds rewrite Wanteds]
}
=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -83,7 +83,7 @@ module GHC.Tc.Types.Constraint (
ctEvExpr, ctEvTerm, ctEvCoercion, ctEvEvId,
ctEvRewriters, ctEvUnique, tcEvDestUnique,
mkKindEqLoc, toKindLoc, toInvisibleLoc, mkGivenLoc,
- ctEvRole, setCtEvPredType, setCtEvLoc, arisesFromGivens,
+ ctEvRewriteRole, ctEvRewriteEqRel, setCtEvPredType, setCtEvLoc, arisesFromGivens,
tyCoVarsOfCtEvList, tyCoVarsOfCtEv, tyCoVarsOfCtEvsList,
-- RewriterSet
@@ -1967,6 +1967,18 @@ For Givens we make new EvVars and bind them immediately. Two main reasons:
So a Given has EvVar inside it rather than (as previously) an EvTerm.
+Note [The rewrite-role of a constraint]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The rewrite-role of a constraint says what can rewrite that constraint:
+
+* If the rewrite-role = Nominal, only a nominal equality can rewrite it
+
+* If the rewrite-rule = Representational, either a nominal or
+ representational equality can rewrit it.
+
+Notice that the constraint may itself not be an equality at all.
+For example, the rewrite-role of (Eq [a]) is Nominal; only nominal
+equalities can rewrite it.
-}
-- | A place for type-checking evidence to go after it is generated.
@@ -2006,12 +2018,21 @@ ctEvOrigin :: CtEvidence -> CtOrigin
ctEvOrigin = ctLocOrigin . ctEvLoc
-- | Get the equality relation relevant for a 'CtEvidence'
-ctEvEqRel :: CtEvidence -> EqRel
+ctEvEqRel :: HasDebugCallStack => CtEvidence -> EqRel
ctEvEqRel = predTypeEqRel . ctEvPred
--- | Get the role relevant for a 'CtEvidence'
-ctEvRole :: CtEvidence -> Role
-ctEvRole = eqRelRole . ctEvEqRel
+-- | Get the rewrite-role relevant for a 'CtEvidence'
+-- See Note [The rewrite-role of a constraint]
+ctEvRewriteRole :: HasDebugCallStack => CtEvidence -> Role
+ctEvRewriteRole = eqRelRole . ctEvRewriteEqRel
+
+ctEvRewriteEqRel :: CtEvidence -> EqRel
+-- ^ Return the rewrite-role of an abitrary CtEvidence
+-- See Note [The rewrite-role of a constraint]
+-- We return ReprEq for (a ~R# b) and NomEq for all other preds
+ctEvRewriteEqRel ev
+ | isReprEqPrimPred (ctEvPred ev) = ReprEq
+ | otherwise = NomEq
ctEvTerm :: CtEvidence -> EvTerm
ctEvTerm ev = EvExpr (ctEvExpr ev)
@@ -2167,8 +2188,8 @@ ctEvFlavour (CtGiven {}) = Given
type CtFlavourRole = (CtFlavour, EqRel)
-- | Extract the flavour, role, and boxity from a 'CtEvidence'
-ctEvFlavourRole :: CtEvidence -> CtFlavourRole
-ctEvFlavourRole ev = (ctEvFlavour ev, ctEvEqRel ev)
+ctEvFlavourRole :: HasDebugCallStack => CtEvidence -> CtFlavourRole
+ctEvFlavourRole ev = (ctEvFlavour ev, ctEvRewriteEqRel ev)
-- | Extract the flavour and role from a 'Ct'
eqCtFlavourRole :: EqCt -> CtFlavourRole
@@ -2180,7 +2201,7 @@ dictCtFlavourRole (DictCt { di_ev = ev })
= (ctEvFlavour ev, NomEq)
-- | Extract the flavour and role from a 'Ct'
-ctFlavourRole :: Ct -> CtFlavourRole
+ctFlavourRole :: HasDebugCallStack => Ct -> CtFlavourRole
-- Uses short-cuts to role for special cases
ctFlavourRole (CDictCan di_ct) = dictCtFlavourRole di_ct
ctFlavourRole (CEqCan eq_ct) = eqCtFlavourRole eq_ct
=====================================
compiler/GHC/Types/Id.hs
=====================================
@@ -146,27 +146,32 @@ import GHC.Types.Var( Id, CoVar, JoinId,
import qualified GHC.Types.Var as Var
import GHC.Core.Type
-import GHC.Types.RepType
+import GHC.Core.Predicate( isCoVarType )
import GHC.Core.DataCon
+import GHC.Core.Class
+import GHC.Core.Multiplicity
+
+import GHC.Types.RepType
import GHC.Types.Demand
import GHC.Types.Cpr
import GHC.Types.Name
-import GHC.Unit.Module
-import GHC.Core.Class
-import {-# SOURCE #-} GHC.Builtin.PrimOps (PrimOp)
import GHC.Types.ForeignCall
-import GHC.Data.Maybe
import GHC.Types.SrcLoc
import GHC.Types.Unique
+
+import GHC.Stg.InferTags.TagSig
+
+import GHC.Unit.Module
+import {-# SOURCE #-} GHC.Builtin.PrimOps (PrimOp)
import GHC.Builtin.Uniques (mkBuiltinUnique)
import GHC.Types.Unique.Supply
+
+import GHC.Data.Maybe
import GHC.Data.FastString
-import GHC.Core.Multiplicity
import GHC.Utils.Misc
import GHC.Utils.Outputable
import GHC.Utils.Panic
-import GHC.Stg.InferTags.TagSig
-- infixl so you can say (id `set` a `set` b)
infixl 1 `setIdUnfolding`,
=====================================
testsuite/tests/typecheck/should_compile/T24887.hs
=====================================
@@ -0,0 +1,62 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE ScopedTypeVariables, TypeAbstractions #-}
+
+module Data.Array.Nested.Internal where
+
+import Data.Coerce (coerce)
+
+
+type family Id (b :: Bool) where
+ Id b = b
+
+newtype Ranked b a = MkRanked (Mixed b a)
+
+
+data family Mixed (b :: Bool) a
+
+newtype instance Mixed b1 (Mixed b2 a) = M_Nest (Mixed False a)
+
+newtype instance Mixed b (Ranked c a) = M_Ranked (Mixed b (Mixed (Id c) a))
+--
+-- newtype MixedNT b c a = M_Ranked (Mixed b (Mixed (Id c) a))
+-- And we Mixed b (Ranked c a) ~N MixedNT b c a
+
+idMixed :: Mixed b a -> Mixed b a
+idMixed = undefined
+
+bar :: forall a b c. Mixed b (Ranked c a) -> Mixed b (Ranked c a)
+bar (M_Ranked @_ @c @a arr)
+ = coerce (idMixed arr) -- fails
+ -- = coerce (idMixed @_ @(Mixed (Id c) a) arr) -- ok
+ -- = coerce (id arr) -- ok
+ -- = let r = idMixed arr in coerce r -- ok
+
+{-
+
+arr :: Mixed b (Mixed (Id c) a)
+
+idMixed arr :: Mixed b (Mixed (Id c) a)
+
+coerce does
+ [W] (Mixed b (Mixed (Id c) a)) ~R (Mixed b (Ranked c a))
+--> Unwrap lHS
+ [W] Mixed False a ~R (Mixed b (Ranked c a))
+--> Unwrap RHS
+ [W] Mixed False a ~R Mixed b (Mixed (Id c) a)
+--> Unwrap RHS again
+ [W] Mixed False a ~R Mixed False a
+
+
+That is true if
+ Mixed (Id c) a ~N Ranked c a
+
+Also
+ Mixed b (Ranked c a) ~N MixedNT b c a
+
+ [W] (Mixed b (Mixed (Id c) a)) ~R (Mixed b (Ranked c a))
+-->
+ [W] (Mixed b (Mixed (Id c) a)) ~R (MixedNT b c a)
+--> unwrap NT
+ [W] (Mixed b (Mixed (Id c) a)) ~R (Mixed b (Mixed (Id c) a))
+-}
=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -917,3 +917,4 @@ test('T24566', [], makefile_test, [])
test('T23764', normal, compile, [''])
test('T23739a', normal, compile, [''])
test('T24810', normal, compile, [''])
+test('T24887', normal, compile, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/b0b641771ef22d6259cc093d1fcb380f602cf370
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/b0b641771ef22d6259cc093d1fcb380f602cf370
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/e42ec770/attachment-0001.html>
More information about the ghc-commits
mailing list