[Git][ghc/ghc][wip/T21623] Wibbles

[Simon Peyton Jones (@simonpj)]

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


Commits:
8646dbaa by Simon Peyton Jones at 2022-08-16T11:13:55+01:00
Wibbles

- - - - -


3 changed files:

- compiler/GHC/Core/TyCo/Rep.hs
- compiler/GHC/Tc/Solver/Canonical.hs
- compiler/GHC/Tc/Types/Constraint.hs


Changes:

=====================================
compiler/GHC/Core/TyCo/Rep.hs
=====================================
@@ -1380,8 +1380,8 @@ It is easy to see that
 A nominal reflexive coercion is quite common, so we keep the special form Refl to
 save allocation.
 
-Note [Coercion selection]
-~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [SelCo]
+~~~~~~~~~~~~
 The Coercion form SelCo allows us to decompose a structural coercion, one
 between ForallTys, or TyConApps, or FunTys.
 


=====================================
compiler/GHC/Tc/Solver/Canonical.hs
=====================================
@@ -52,6 +52,7 @@ import GHC.Data.Pair
 import GHC.Utils.Misc
 import GHC.Data.Bag
 import GHC.Utils.Monad
+import GHC.Utils.Constants( debugIsOn )
 import Control.Monad
 import Data.Maybe ( isJust, isNothing )
 import Data.List  ( zip4 )
@@ -957,8 +958,14 @@ canEqNC :: CtEvidence -> EqRel -> Type -> Type -> TcS (StopOrContinue Ct)
 canEqNC ev eq_rel ty1 ty2
   = do { result <- zonk_eq_types ty1 ty2
        ; case result of
-           Left (Pair ty1' ty2') -> can_eq_nc False ev eq_rel ty1' ty1 ty2' ty2
-           Right ty              -> canEqReflexive ev eq_rel ty }
+           Right ty              -> canEqReflexive ev eq_rel ty
+           Left (Pair ty1' ty2') -> can_eq_nc False ev' eq_rel ty1' ty1' ty2' ty2'
+             where
+               ev' | debugIsOn = setCtEvPredType ev $
+                                 mkPrimEqPredRole (eqRelRole eq_rel) ty1' ty2'
+                   | otherwise = ev
+                   -- ev': satisfy the precondition of can_eq_nc
+       }
 
 can_eq_nc
    :: Bool            -- True => both types are rewritten
@@ -967,6 +974,11 @@ can_eq_nc
    -> Type -> Type    -- LHS, after and before type-synonym expansion, resp
    -> Type -> Type    -- RHS, after and before type-synonym expansion, resp
    -> TcS (StopOrContinue Ct)
+-- Precondition: in DEBUG mode, the `ctev_pred` of `ev` is (ps_ty1 ~# ps_ty2),
+--               without zonking
+-- This precondition is needed (only in DEBUG) to satisfy the assertions
+--   in mkSelCo, called in canDecomposableTyConAppOK and canDecomposableFunTy
+
 can_eq_nc rewritten ev eq_rel ty1 ps_ty1 ty2 ps_ty2
   = do { traceTcS "can_eq_nc" $
          vcat [ ppr rewritten, ppr ev, ppr eq_rel, ppr ty1, ppr ps_ty1, ppr ty2, ppr ps_ty2 ]
@@ -1948,7 +1960,7 @@ canDecomposableFunTy ev eq_rel f1@(m1,a1,r1) f2@(m2,a2,r2)
                                     , evCoercion $ mkSelCo role' (SelFun fs) ev_co )
                                   | (fs, ty1, ty2) <- [(SelMult, m1, m2)
                                                       ,(SelArg,  a1, a2)
-                                                      ,(SelRes,  r2, r2)]
+                                                      ,(SelRes,  r1, r2)]
                                   , let role' = funRole role fs ]
                    ; emitWorkNC given_evs }
 


=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -1926,23 +1926,17 @@ arisesFromGivens ct = isGivenCt ct || isGivenLoc (ctLoc ct)
 -- the evidence and the ctev_pred in sync with each other.
 -- See Note [CtEvidence invariants].
 setCtEvPredType :: HasDebugCallStack => CtEvidence -> Type -> CtEvidence
-setCtEvPredType old_ctev new_pred
-  = case old_ctev of
-    CtGiven { ctev_evar = ev, ctev_loc = loc } ->
-      CtGiven { ctev_pred = new_pred
-              , ctev_evar = setVarType ev new_pred
-              , ctev_loc  = loc
-              }
-    CtWanted { ctev_dest = dest, ctev_loc = loc, ctev_rewriters = rewriters } ->
-      CtWanted { ctev_pred      = new_pred
-               , ctev_dest      = new_dest
-               , ctev_loc       = loc
-               , ctev_rewriters = rewriters
-               }
-        where
-          new_dest = case dest of
-            EvVarDest ev -> EvVarDest (setVarType ev new_pred)
-            HoleDest h   -> HoleDest  (setCoHoleType h new_pred)
+setCtEvPredType old_ctev@(CtGiven { ctev_evar = ev }) new_pred
+  = old_ctev { ctev_pred = new_pred
+             , ctev_evar = setVarType ev new_pred }
+
+setCtEvPredType old_ctev@(CtWanted { ctev_dest = dest }) new_pred
+  = old_ctev { ctev_pred = new_pred
+             , ctev_dest = new_dest }
+  where
+    new_dest = case dest of
+      EvVarDest ev -> EvVarDest (setVarType ev new_pred)
+      HoleDest h   -> HoleDest  (setCoHoleType h new_pred)
 
 instance Outputable TcEvDest where
   ppr (HoleDest h)   = text "hole" <> ppr h



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

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/8646dbaaace379583741ca5bed180981ac78e45d
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/20220816/f0b4c723/attachment-0001.html>