[Git][ghc/ghc][wip/cfuneqcan-refactor] Comments, etc., from Friday

[Richard Eisenberg]

Richard Eisenberg pushed to branch wip/cfuneqcan-refactor at Glasgow Haskell Compiler / GHC


Commits:
f2bbcc40 by Richard Eisenberg at 2020-11-17T10:46:37-05:00
Comments, etc., from Friday

- - - - -


4 changed files:

- compiler/GHC/Core/Unify.hs
- compiler/GHC/Tc/Solver/Canonical.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Types/Constraint.hs


Changes:

=====================================
compiler/GHC/Core/Unify.hs
=====================================
@@ -1244,6 +1244,7 @@ data BindFlag
 
   | Skolem      -- This type variable is a skolem constant
                 -- Don't bind it; it only matches itself
+                -- These variables are SurelyApart from other types
   deriving Eq
 
 {-


=====================================
compiler/GHC/Tc/Solver/Canonical.hs
=====================================
@@ -2520,26 +2520,27 @@ Wrinkles:
      must be sure to kick out any such CIrredCan constraints that mention coercion holes
      when those holes get filled in, so that the unification step can now proceed.
 
-     (2a) We must now absolutely make sure to kick out any constraints that
-          mention a newly-filled-in coercion hole -- if there are no more
-          remaining coercion holes. This is done in
-          kickOutAfterFillingCoercionHole. The extra check that there are no
-          more remaining holes avoids needless work when rewriting evidence
-          (which fills coercion holes) and aids efficiency. It also can avoid
-          a loop in the solver that would otherwise arise in this case:
+     (2a) We must now kick out any constraints that mention a newly-filled-in
+          coercion hole, but only if there are no more remaining coercion
+          holes. This is done in kickOutAfterFillingCoercionHole. The extra
+          check that there are no more remaining holes avoids needless work
+          when rewriting evidence (which fills coercion holes) and aids
+          efficiency.
+
+          Moreover, kicking out when there are remaining unfilled holes can
+          cause a loop in the solver in this case:
                [W] w1 :: (ty1 :: F a) ~ (ty2 :: s)
           After canonicalisation, we discover that this equality is heterogeneous.
           So we emit
                [W] co_abc :: F a ~ s
           and preserve the original as
-               [W] w2 :: (ty1 |> co_abc) ~ ty2
-          Then, co_abc comes becomes the work item. It gets swapped back
-          and forth, as it goes through canEqTyVarFunEq. We thus get
+               [W] w2 :: (ty1 |> co_abc) ~ ty2    (blocked on co_abc)
+          Then, co_abc comes becomes the work item. It gets swapped in
+          canEqCanLHS2 and then back again in canEqTyVarFunEq. We thus get
           co_abc := sym co_abd, and then co_abd := sym co_abe, with
                [W] co_abe :: F a ~ s
-          right back where we started. (At this point, we're in canEqCanLHSFinish,
-          so we're not looping.) But all this filling in would,
-          naively, cause w2 to be kicked out. Which, when it got processed,
+          This process has filled in co_abc. Suppose w2 were kicked out.
+          When it gets processed,
           would get this whole chain going again. The solution is to
           kick out a blocked constraint only when the result of filling
           in the blocking coercion involves no further blocking coercions.


=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -1780,9 +1780,9 @@ kick_out_rewritable new_fr new_lhs
 
         kick_out_for_completeness  -- (K3) and Note [K3: completeness of solving]
           = case (eq_rel, new_lhs) of
-              (NomEq, _)  -> rhs_ty `eqType` canEqLHSType new_lhs
-              (ReprEq, TyVarLHS new_tv) -> isTyVarHead new_tv rhs_ty
-              (ReprEq, TyFamLHS new_tf new_tf_args)
+              (NomEq, _)  -> rhs_ty `eqType` canEqLHSType new_lhs     -- (K3a)
+              (ReprEq, TyVarLHS new_tv) -> isTyVarHead new_tv rhs_ty  -- (K3b)
+              (ReprEq, TyFamLHS new_tf new_tf_args)                   -- (K3b)
                 | Just (rhs_tc, rhs_tc_args) <- tcSplitTyConApp_maybe rhs_ty
                 , tcEqTyConApps new_tf new_tf_args rhs_tc rhs_tc_args
                   -> True


=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -1176,6 +1176,12 @@ data ImplicStatus
 -- See Note [When does an implication have given equalities?] in GHC.Tc.Solver.Monad,
 -- which also explains why we need three options here. Also, see
 -- Note [Suppress redundant givens during error reporting] in GHC.Tc.Errors
+--
+--                  Stops floating  |   Suppresses Givens in errors
+--                  -----------------------------------------------
+--  NoGivenEqs         NO           |         YES
+--  LocalGivenEqs      NO           |         NO
+--  MaybeGivenEqs      YES          |         NO
 data HasGivenEqs
   = NoGivenEqs      -- definitely no given equalities
   | LocalGivenEqs   -- might have Given equalities that affect only local skolems



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

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/f2bbcc402adb211c78cf185e0cda194e6f8d87b1
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/20201117/ba7bff16/attachment-0001.html>