[Git][ghc/ghc][wip/T23070-unify] Fix another error: missing kick-out

[Simon Peyton Jones (@simonpj)]

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


Commits:
aec52b60 by Simon Peyton Jones at 2023-04-02T22:51:05+01:00
Fix another error: missing kick-out

- - - - -


2 changed files:

- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Utils/Unify.hs


Changes:

=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -1955,15 +1955,26 @@ unifyWanted :: RewriterSet -> CtLoc
 -- The returned coercion's role matches the input parameter
 
 unifyWanted _rewriters loc role ty1 ty2
-  = do { (co,cts) <- wrapTcS $
-             do { ref <- TcM.newTcRef []
+  = do { (co, unified, cts) <- wrapTcS $
+             do { defer_ref   <- TcM.newTcRef []
+                ; unified_ref <- TcM.newTcRef []
                 ; let env = UE { u_role  = role
                                , u_loc   = loc
-                               , u_defer = ref }
+                               , u_defer = defer_ref
+                               , u_unified = Just unified_ref}
                 ; co <- uType env ty1 ty2
-                ; cts <- TcM.readTcRef ref
-                ; return (co, cts) }
+                ; cts <- TcM.readTcRef defer_ref
+                ; unified <- TcM.readTcRef unified_ref
+                ; return (co, unified, cts) }
+
+       -- Emit the deferred constraints
        ; updWorkListTcS (extendWorkListEqs cts)
+
+       -- And kick out any inert constraint that we have unified
+       -- ToDo: treating the tyvars together might
+       --       be more efficient than one by one
+       ; mapM_ kickOutAfterUnification unified
+
        ; return co }
 
 {-


=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -1745,7 +1745,8 @@ uTypeAndEmit :: TypeOrKind -> CtOrigin -> TcType -> TcType -> TcM CoercionN
 uTypeAndEmit t_or_k orig ty1 ty2
   = do { ref <- newTcRef []
        ; loc <- getCtLocM orig (Just t_or_k)
-       ; let env = UE { u_loc = loc, u_role = Nominal, u_defer = ref }
+       ; let env = UE { u_loc = loc, u_role = Nominal
+                      , u_defer = ref, u_unified = Nothing }
 
        -- The hard work happens here
        ; co <- uType env ty1 ty2
@@ -1765,9 +1766,15 @@ uType is the heart of the unifier.
 -}
 
 data UnifyEnv
-  = UE { u_role  :: Role
-       , u_loc   :: CtLoc
-       , u_defer :: TcRef [Ct] }
+  = UE { u_role   :: Role
+       , u_loc    :: CtLoc
+
+       , u_defer  :: TcRef [Ct]
+         -- Deferred constraints
+
+       , u_unified :: Maybe (TcRef [TcTyVar])
+         -- If Just, track unified type variables
+    }
 
 mkKindEnv :: UnifyEnv -> TcType -> TcType -> UnifyEnv
 -- Modify the UnifyEnv to be right for unifing
@@ -2137,7 +2144,10 @@ uUnfilledVar2 env swapped tv1 ty2
            -- NB: tv1 should still be unfilled, despite the kind unification
            --     because tv1 is not free in ty2' (or, hence, in its kind)
          then do { writeMetaTyVar tv1 ty2
-                 ; return (mkNomReflCo ty2) }
+                 ; case u_unified env of
+                     Nothing -> return ()
+                     Just uref -> updTcRef uref (tv1 :)
+                 ; return (mkNomReflCo ty2) }  -- Unification is always Nominal
 
          else defer  -- This cannot be solved now.  See GHC.Tc.Solver.Canonical
                      -- Note [Equalities with incompatible kinds] for how



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

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/aec52b60ff62c9faf71f46f1a17d36f7a0f72e9d
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/20230402/04d30fe9/attachment-0001.html>