[Git][ghc/ghc][wip/T24984] Fix egregious bug in any2

[Simon Peyton Jones (@simonpj)]

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


Commits:
cc6e9cd2 by Simon Peyton Jones at 2024-07-16T14:25:29+01:00
Fix egregious bug in any2

- - - - -


5 changed files:

- compiler/GHC/Core/Predicate.hs
- compiler/GHC/Core/Type.hs
- compiler/GHC/Tc/Solver/InertSet.hs
- compiler/GHC/Tc/Utils/TcType.hs
- compiler/GHC/Utils/Misc.hs


Changes:

=====================================
compiler/GHC/Core/Predicate.hs
=====================================
@@ -194,7 +194,7 @@ getEqPredRole ty = eqRelRole (predTypeEqRel ty)
 
 -- | Get the equality relation relevant for a pred type
 -- Returns NomEq for dictionary predicates, etc
-predTypeEqRel :: HasDebugCallStack => PredType -> EqRel
+predTypeEqRel :: PredType -> EqRel
 predTypeEqRel ty
   | isReprEqPrimPred ty = ReprEq
   | otherwise           = NomEq


=====================================
compiler/GHC/Core/Type.hs
=====================================
@@ -171,7 +171,7 @@ module GHC.Core.Type (
 
         anyFreeVarsOfType, anyFreeVarsOfTypes,
         noFreeVarsOfType,
-        expandTypeSynonyms,
+        expandTypeSynonyms, expandSynTyConApp_maybe,
         typeSize, occCheckExpand,
 
         -- ** Closing over kinds


=====================================
compiler/GHC/Tc/Solver/InertSet.hs
=====================================
@@ -1516,6 +1516,10 @@ data KickOutSpec -- See Note [KickOutSpec]
   | KOAfterAdding CanEqLHS     -- We are adding to the inert set a canonical equality
                                -- constraint with this LHS
 
+instance Outputable KickOutSpec where
+  ppr (KOAfterUnify tvs)  = text "KOAfterUnify" <> ppr tvs
+  ppr (KOAfterAdding lhs) = text "KOAfterAdding" <> parens (ppr lhs)
+
 {- Note [KickOutSpec]
 ~~~~~~~~~~~~~~~~~~~~~~
 KickOutSpec explains why we are kicking out.
@@ -1632,8 +1636,10 @@ kickOutRewritableLHS ko_spec new_fr@(_, new_role)
     kick_out_eq :: EqCt -> Bool
     kick_out_eq (EqCt { eq_lhs = lhs, eq_rhs = rhs_ty
                       , eq_ev = ev, eq_eq_rel = eq_rel })
+
+      -- (KK0) Keep it in the inert set if the new thing can't rewrite it
       | not (fr_may_rewrite fs)
-      = False  -- (KK0) Keep it in the inert set if the new thing can't rewrite it
+      = False
 
       -- Below here (fr_may_rewrite fs) is True
 


=====================================
compiler/GHC/Tc/Utils/TcType.hs
=====================================
@@ -1012,21 +1012,26 @@ any_rewritable :: EqRel   -- Ambient role
 --
 -- See Note [Rewritable] in GHC.Tc.Solver.InertSet for a specification for this function.
 {-# INLINE any_rewritable #-} -- this allows specialization of predicates
-any_rewritable role tv_pred tc_pred
-  = go False emptyVarSet role
+any_rewritable role tv_pred tc_pred ty
+  = go False emptyVarSet role ty
   where
     go_tv uf bvs rl tv | tv `elemVarSet` bvs = False
                        | otherwise           = tv_pred uf rl tv
 
     go :: UnderFam -> VarSet -> EqRel -> TcType -> Bool
-    go under_fam bvs rl ty@(TyConApp tc tys)
-      | isFamFreeTyCon tc    -- Not a type family, not a synonym hiding type families
-      = go_tc under_fam bvs rl tc tys
+    go under_fam bvs rl (TyConApp tc tys)
 
-      | Just ty' <- coreView ty   -- Expand synonyms
+      -- Expand synonyms, unless (a) we are at Nominal role and (b) the synonym
+      -- is type-family-free; then it suffices just to look at the args
+      | isTypeSynonymTyCon tc
+      , case rl of { NomEq -> not (isFamFreeTyCon tc); ReprEq -> True }
+      , Just ty' <- expandSynTyConApp_maybe tc tys
       = go under_fam bvs rl ty'
 
-      | isTypeFamilyTyCon tc
+      -- Check if we are going under a type family application
+      | case rl of
+           NomEq  -> isTypeFamilyTyCon tc
+           ReprEq -> isFamilyTyCon     tc
       = if | tc_pred under_fam rl tc tys -> True
            | otherwise                   -> go_fam under_fam (tyConArity tc) bvs tys
 
@@ -1048,12 +1053,12 @@ any_rewritable role tv_pred tc_pred
     go_tc uf bvs NomEq  _  tys = any (go uf bvs NomEq) tys
     go_tc uf bvs ReprEq tc tys = any2 (go_arg uf bvs) tys (tyConRoleListRepresentational tc)
 
-    go_arg uf bvs ty Nominal          = go uf bvs NomEq  ty
+    go_arg uf bvs ty Nominal          = go uf bvs NomEq ty
     go_arg uf bvs ty Representational = go uf bvs ReprEq ty
     go_arg _   _  _  Phantom          = False  -- We never rewrite with phantoms
 
-    -- For a type-family application (F t1 .. tn), all arguments have Nominal role
-    --   (whether in F's arity or, if over-saturated, beyond it)
+    -- For a type-family or data-family application (F t1 .. tn), all arguments
+    --   have Nominal role (whether in F's arity or, if over-saturated, beyond it)
     -- Switch on under_fam for arguments <= arity
     go_fam uf 0 bvs tys      = any (go uf bvs NomEq) tys   -- Like AppTy
     go_fam _  _ _   []       = False


=====================================
compiler/GHC/Utils/Misc.hs
=====================================
@@ -655,7 +655,7 @@ all2 _ _      _      = False
 any2 :: (a -> b -> Bool) -> [a] -> [b] -> Bool
 -- True if any of the corresponding elements satisfy the predicate
 -- Unlike `all2`, this ignores excess elements of the other list
-any2 p (x:xs) (y:ys) = p x y || all2 p xs ys
+any2 p (x:xs) (y:ys) = p x y || any2 p xs ys
 any2 _ _      _      = False
 
 -- Count the number of times a predicate is true



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

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/cc6e9cd20bcdd06d01b5902c750c785e5c67ef8d
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/20240716/6163c153/attachment-0001.html>