[Git][ghc/ghc][wip/T23070-dicts] Further improvements to insolubles and ambiguity checking

[Simon Peyton Jones (@simonpj)]

Simon Peyton Jones pushed to branch wip/T23070-dicts at Glasgow Haskell Compiler / GHC


Commits:
b53bd72d by Simon Peyton Jones at 2023-05-16T17:50:23+01:00
Further improvements to insolubles and ambiguity checking

- - - - -


6 changed files:

- compiler/GHC/Core/Predicate.hs
- compiler/GHC/Tc/Solver/Dict.hs
- compiler/GHC/Tc/Solver/InertSet.hs
- compiler/GHC/Tc/Types/Constraint.hs
- compiler/GHC/Tc/Utils/TcType.hs
- compiler/GHC/Tc/Validity.hs


Changes:

=====================================
compiler/GHC/Core/Predicate.hs
=====================================
@@ -20,7 +20,7 @@ module GHC.Core.Predicate (
 
   -- Class predicates
   mkClassPred, isDictTy, typeDeterminesValue,
-  isClassPred, isEqPredClass, isCTupleClass,
+  isClassPred, isEqualityClass, isCTupleClass,
   getClassPredTys, getClassPredTys_maybe,
   classMethodTy, classMethodInstTy,
 
@@ -217,11 +217,6 @@ isEvVarType :: Type -> Bool
 -- See Note [Evidence for quantified constraints]
 isEvVarType ty = isCoVarType ty || isPredTy ty
 
-isEqPredClass :: Class -> Bool
--- True of (~) and (~~)
-isEqPredClass cls =  cls `hasKey` eqTyConKey
-                  || cls `hasKey` heqTyConKey
-
 isClassPred :: PredType -> Bool
 isClassPred ty = case tyConAppTyCon_maybe ty of
     Just tc -> isClassTyCon tc
@@ -232,7 +227,7 @@ isEqPred ty  -- True of (a ~ b) and (a ~~ b)
              -- ToDo: should we check saturation?
   | Just tc <- tyConAppTyCon_maybe ty
   , Just cls <- tyConClass_maybe tc
-  = isEqPredClass cls
+  = isEqualityClass cls
   | otherwise
   = False
 
@@ -240,9 +235,18 @@ 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#)
+isEqualityClass cls
+  = cls `hasKey` heqTyConKey
+    || cls `hasKey` eqTyConKey
+    || cls `hasKey` coercibleTyConKey
+
 isCTupleClass :: Class -> Bool
 isCTupleClass cls = isTupleTyCon (classTyCon cls)
 
+
 {- *********************************************************************
 *                                                                      *
               Implicit parameters


=====================================
compiler/GHC/Tc/Solver/Dict.hs
=====================================
@@ -848,15 +848,6 @@ naturallyCoherentClass cls
   = isCTupleClass cls || isEqualityClass cls
 -}
 
-isEqualityClass :: Class -> Bool
--- True of (~), (~~), and Coercible
--- These all have a single primitive-equality superclass, either (~N# or ~R#)
-isEqualityClass cls
-  = cls `hasKey` heqTyConKey
-    || cls `hasKey` eqTyConKey
-    || cls `hasKey` coercibleTyConKey
-
-
 {- Note [Instance and Given overlap]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Example, from the OutsideIn(X) paper:


=====================================
compiler/GHC/Tc/Solver/InertSet.hs
=====================================
@@ -241,7 +241,7 @@ extendWorkListCt ct wl
        -> extendWorkListEq rewriters ct wl
 
      ClassPred cls _  -- See Note [Prioritise class equalities]
-       |  isEqPredClass cls
+       |  isEqualityClass cls
        -> extendWorkListEq rewriters ct wl
 
      _ -> extendWorkListNonEq ct wl


=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -543,7 +543,7 @@ cteSolubleOccurs   = CTEP (bit 3)   -- Occurs-check under a type function, or in
                                     -- or in a representational equality; see
    -- See Note [Occurs check and representational equality]
    -- cteSolubleOccurs must be one bit to the left of cteInsolubleOccurs
-   -- See also Note [Insoluble occurs check] in GHC.Tc.Errors
+   -- See also Note [Insoluble mis-match] in GHC.Tc.Errors
 
 cteCoercionHole    = CTEP (bit 4)   -- Coercion hole encountered
 cteConcrete        = CTEP (bit 5)   -- Type variable that can't be made concrete


=====================================
compiler/GHC/Tc/Utils/TcType.hs
=====================================
@@ -161,8 +161,8 @@ module GHC.Tc.Utils.TcType (
   mkTyConTy, mkTyVarTy, mkTyVarTys,
   mkTyCoVarTy, mkTyCoVarTys,
 
-  isClassPred, isEqPrimPred, isIPLikePred, isEqPred, isEqPredClass,
-  mkClassPred,
+  isClassPred, isEqPrimPred, isIPLikePred, isEqPred,
+  isEqualityClass, mkClassPred,
   tcSplitQuantPredTy, tcSplitDFunTy, tcSplitDFunHead, tcSplitMethodTy,
   isRuntimeRepVar, isFixedRuntimeRepKind,
   isVisiblePiTyBinder, isInvisiblePiTyBinder,
@@ -2538,11 +2538,10 @@ isTerminatingClass cls
   = isIPClass cls    -- Implicit parameter constraints always terminate because
                      -- there are no instances for them --- they are only solved
                      -- by "local instances" in expressions
-    || isEqPredClass cls
+    || isEqualityClass cls
     || cls `hasKey` typeableClassKey
             -- Typeable constraints are bigger than they appear due
             -- to kind polymorphism, but we can never get instance divergence this way
-    || cls `hasKey` coercibleTyConKey
     || cls `hasKey` unsatisfiableClassNameKey
 
 allDistinctTyVars :: TyVarSet -> [KindOrType] -> Bool


=====================================
compiler/GHC/Tc/Validity.hs
=====================================
@@ -1230,7 +1230,7 @@ e.g.   module A where
 check_class_pred :: TidyEnv -> DynFlags -> UserTypeCtxt
                  -> PredType -> Class -> [TcType] -> TcM ()
 check_class_pred env dflags ctxt pred cls tys
-  | isEqPredClass cls    -- (~) and (~~) are classified as classes,
+  | isEqualityClass cls  -- (~) and (~~) and Coercible are classified as classes,
                          -- but here we want to treat them as equalities
   = -- Equational constraints are valid in all contexts, and
     -- we do not need to check e.g. for FlexibleContexts here, so just do nothing



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

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/b53bd72d5eaf8261551fb1c4bf010ba1e50af36d
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/20230516/0b730db6/attachment-0001.html>