[Git][ghc/ghc][wip/T24887] Put all nominal equalities in eqs_N

[Simon Peyton Jones (@simonpj)]

Simon Peyton Jones pushed to branch wip/T24887 at Glasgow Haskell Compiler / GHC


Commits:
bcb05c05 by Simon Peyton Jones at 2024-06-03T11:20:01+01:00
Put all nominal equalities in eqs_N

- - - - -


2 changed files:

- compiler/GHC/Core/Predicate.hs
- compiler/GHC/Tc/Solver/InertSet.hs


Changes:

=====================================
compiler/GHC/Core/Predicate.hs
=====================================
@@ -12,7 +12,7 @@ module GHC.Core.Predicate (
 
   -- Equality predicates
   EqRel(..), eqRelRole,
-  isEqPrimPred, isNomEqPrimPred, isReprEqPrimPred, isEqPred, isCoVarType,
+  isEqPrimPred, isNomEqPred, isReprEqPrimPred, isEqPred, isCoVarType,
   getEqPredTys, getEqPredTys_maybe, getEqPredRole,
   predTypeEqRel,
   mkPrimEqPred, mkReprPrimEqPred, mkPrimEqPredRole,
@@ -189,11 +189,11 @@ getEqPredTys_maybe ty
       _ -> Nothing
 
 getEqPredRole :: PredType -> Role
--- Precondition: the PredType is (a ~#N b) or (a ~#R b)
+-- 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.
--- Precondition: the PredType is (a ~#N b) or (a ~#R b)
+-- Precondition: the PredType is (s ~#N t) or (s ~#R t)
 predTypeEqRel :: HasDebugCallStack => PredType -> EqRel
 predTypeEqRel ty
   = case splitTyConApp_maybe ty of
@@ -232,21 +232,21 @@ 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 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 (a ~# b) (a ~R# b)
+-- True of (s ~# t) (s ~R# t)
 isEqPrimPred ty
   | Just tc <- tyConAppTyCon_maybe ty
   = tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey
   | otherwise
   = False
 
-isNomEqPrimPred :: PredType -> Bool
-isNomEqPrimPred ty
-  | Just tc <- tyConAppTyCon_maybe ty
-  = tc `hasKey` eqPrimTyConKey
-  | otherwise
-  = False
-
 isReprEqPrimPred :: PredType -> Bool
 isReprEqPrimPred ty
   | Just tc <- tyConAppTyCon_maybe ty
@@ -254,12 +254,13 @@ isReprEqPrimPred ty
   | otherwise
   = False
 
-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)
--- 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
+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
@@ -267,7 +268,7 @@ isClassPred ty = case tyConAppTyCon_maybe ty of
     _       -> 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


=====================================
compiler/GHC/Tc/Solver/InertSet.hs
=====================================
@@ -175,7 +175,7 @@ See GHC.Tc.Solver.Monad.deferTcSForAllEq
 
 -- See Note [WorkList priorities]
 data WorkList
-  = WL { wl_eqs_N :: [Ct]  -- Primitive /nominal/ equalities (a ~#N b)
+  = 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
@@ -218,7 +218,7 @@ extendWorkListEq rewriters ct
   | isEmptyRewriterSet rewriters      -- A wanted that has not been rewritten
     -- isEmptyRewriterSet: see Note [Prioritise Wanteds with empty RewriterSet]
     --                         in GHC.Tc.Types.Constraint
-  = if isNomEqPrimPred (ctPred ct)
+  = if isNomEqPred (ctPred ct)
     then wl { wl_eqs_N = ct : eqs_N }
     else wl { wl_eqs_X = ct : eqs_X }
 
@@ -253,7 +253,7 @@ extendWorkListEqs rewriters new_eqs
     -- 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 = isNomEqPrimPred (ctPred ct)
+    is_nominal ct = isNomEqPred (ctPred ct)
 
 extendWorkListNonEq :: Ct -> WorkList -> WorkList
 -- Extension by non equality



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/bcb05c055cc594b1f9d739700e3b2474b8a019dd

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/bcb05c055cc594b1f9d739700e3b2474b8a019dd
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/20240603/49b8c393/attachment-0001.html>