[Git][ghc/ghc][wip/T25657] Wibbles

[Simon Peyton Jones (@simonpj)]

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


Commits:
6e0326d8 by Simon Peyton Jones at 2025-03-03T17:38:42+00:00
Wibbles

- - - - -


2 changed files:

- compiler/GHC/Core/Unify.hs
- compiler/GHC/Tc/Types/Constraint.hs


Changes:

=====================================
compiler/GHC/Core/Unify.hs
=====================================
@@ -147,7 +147,7 @@ alwaysBindTv _tv _ty = BindMe
 alwaysBindFam :: BindFamFun
 alwaysBindFam _tc _args _rhs = BindMe
 
-dontCareBindFam :: HasDebugCallStack => BindFamFun
+dontCareBindFam :: HasCallStack => BindFamFun
 dontCareBindFam tc args rhs
   = pprPanic "dontCareBindFam" $
     vcat [ ppr tc <+> ppr args, text "rhs" <+> ppr rhs ]
@@ -1374,10 +1374,11 @@ unify_ty env ty1 ty2 kco
 unify_ty env (CastTy ty1 co1) ty2 kco
   | mentionsForAllBoundTyVarsL env (tyCoVarsOfCo co1)
   = surelyApart
+    -- xxx todo ... MaybeApart perhaps?   F a b, where b is forall-bound, but a is not
+    --                                  and F Int b = Int
 
   | um_unif env
   = unify_ty env ty1 ty2 (co1 `mkTransCo` kco)
-    -- ToDo: what if co2 mentions forall-bound variables?
 
   | otherwise -- We are matching, not unifying
   = do { subst <- getSubst env
@@ -1596,9 +1597,8 @@ isSatFamApp _ = Nothing
 
 ---------------------------------
 uVarOrFam :: UMEnv -> CanEqLHS -> InType -> OutCoercion -> UM ()
--- Invariants: (a) ty1 is a TyVarTy or a saturated type-family application
---             (b) If ty1 is a ty-fam-app, then ty2 is NOT a TyVarTy
---             (c) both args have had coreView already applied
+-- Invariants: (a) If ty1 is a TyFamLHS, then ty2 is NOT a TyVarTy
+--             (b) both args have had coreView already applied
 -- Why saturated?  See (ATF4) in Note [Apartness and type families]
 uVarOrFam env ty1 ty2 kco
   = do { substs <- getSubstEnvs
@@ -1646,12 +1646,12 @@ uVarOrFam env ty1 ty2 kco
       , let tv2' = umRnOccR env tv2
       , tv1' == tv2'
       = if | um_unif env     -> return ()
-           | tv1_is_bindable -> extendTvEnv tv1 ty2
+           | tv1_is_bindable -> extendTvEnv tv1' ty2
            | otherwise       -> return ()
 
       | tv1_is_bindable
-      , not (mentionsForAllBoundTyVarsR env rhs_fvs)
-            -- kco does not mention forall-bound vars
+      , not (mentionsForAllBoundTyVarsR env ty2_fvs)
+            -- ty2_fvs: kco does not mention forall-bound vars
       , not occurs_check
       = -- No occurs check, nor skolem-escape; just bind the tv
         -- We don't need to rename `rhs` because it mentions no forall-bound vars
@@ -1671,21 +1671,23 @@ uVarOrFam env ty1 ty2 kco
 
       where
         tv1'            = umRnOccL env tv1
-        rhs_fvs         = tyCoVarsOfType ty2
-        all_rhs_fvs     = rhs_fvs `unionVarSet` tyCoVarsOfCo kco
+        ty2_fvs         = tyCoVarsOfType ty2
+        rhs_fvs         = ty2_fvs `unionVarSet` tyCoVarsOfCo kco
         rhs             = ty2 `mkCastTy` mkSymCo kco
         tv1_is_bindable | not (tv1' `elemVarSet` um_foralls env)
-                          -- tv1' is not forall-bound, so tv1==tv1'
-                        , BindMe <- um_bind_tv_fun env tv1 rhs
+                          -- tv1' is not forall-bound, but tv1 can still differ
+                          -- from tv1; see Note [Cloning the template binders]
+                          -- in GHC.Core.Rules.  So give tv1' to um_bind_tv_fun.
+                        , BindMe <- um_bind_tv_fun env tv1' rhs
                         = True
                         | otherwise
                         = False
 
         occurs_check = um_unif env &&
-                       occursCheck (um_tv_env substs) tv1 all_rhs_fvs
+                       occursCheck (um_tv_env substs) tv1 rhs_fvs
           -- Occurs check, only when unifying
           -- see Note [Fine-grained unification]
-          -- Make sure you include `kco` in all_rhs_tvs #14846
+          -- Make sure you include `kco` in rhs_tvs #14846
 
     -----------------------------
     -- go_fam: LHS is a saturated type-family application


=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -46,7 +46,11 @@ module GHC.Tc.Types.Constraint (
         cterHasNoProblem, cterHasProblem, cterHasOnlyProblem, cterHasOnlyProblems,
         cterRemoveProblem, cterHasOccursCheck, cterFromKind,
 
+        -- Equality left-hand sides, re-exported from GHC.Core.Predicate
+        CanEqLHS(..), canEqLHS_maybe, canTyFamEqLHS_maybe,
+        canEqLHSKind, canEqLHSType, eqCanEqLHS,
 
+        -- Holes
         Hole(..), HoleSort(..), isOutOfScopeHole,
         DelayedError(..), NotConcreteError(..),
 



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

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/6e0326d8af2dbcad227b55db2c234c213f2c70b5
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/20250303/11bfc25d/attachment-0001.html>