[Git][ghc/ghc][wip/T18126] 2 commits: wibbles ql

[Simon Peyton Jones]

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


Commits:
7572a47e by Simon Peyton Jones at 2020-09-14T15:30:36+01:00
wibbles ql

- - - - -
9f5ec175 by Simon Peyton Jones at 2020-09-14T15:31:00+01:00
wibbles generalisation patch

- - - - -


5 changed files:

- compiler/GHC/Tc/Gen/App.hs
- compiler/GHC/Tc/Solver.hs
- compiler/GHC/Tc/Solver/Canonical.hs
- compiler/GHC/Tc/Utils/Unify.hs
- docs/users_guide/ghci.rst


Changes:

=====================================
compiler/GHC/Tc/Gen/App.hs
=====================================
@@ -33,6 +33,7 @@ import GHC.Core.TyCon
 import GHC.Core.TyCo.Rep
 import GHC.Core.TyCo.Ppr
 import GHC.Core.TyCo.Subst (substTyWithInScope)
+import GHC.Core.TyCo.FVs( shallowTyCoVarsOfType )
 import GHC.Core.Type
 import GHC.Tc.Types.Evidence
 import GHC.Types.Var.Set
@@ -852,31 +853,69 @@ qlUnify delta ty1 ty2
                                   ; go_flexi bvs kappa ty2 } }
 
     ----------------
-    -- ToDo: what about other magic in Unify.metaTyVarUpdateOK?
     go_flexi (_,bvs2) kappa ty2  -- ty2 is zonked
-      | ty2_tvs `intersectsVarSet` bvs2   -- We really only need shallow here
-      = return ()   -- Can't instantiate a delta-var
-                    -- to a forall-bound variable
-
-      | kappa `elemVarSet` ty2_tvs
-      = return ()   -- Occurs-check
-
-      | otherwise
-      = do { -- Unify the kinds
-             -- c.f. Note [Equalities with incompatible kinds] in Solver.Canonical
-           ; co <- unifyKind (Just (ppr ty2)) ty2_kind kappa_kind
+      | -- See Note [Actual unification in qlUnify]
+        let ty2_tvs = shallowTyCoVarsOfType ty2
+      , not (ty2_tvs `intersectsVarSet` bvs2)
+          -- Can't instantiate a delta-varto a forall-bound variable
+      , Just ty2' <- occCheckExpand [kappa] ty2
+          -- Passes the occurs check
+      = do { co <- unifyKind (Just (ppr ty2)) ty2_kind kappa_kind
+                   -- unifyKind: see Note [Actual unification in qlUnify]
 
            ; traceTc "qlUnify:update" $
              vcat [ hang (ppr kappa <+> dcolon <+> ppr kappa_kind)
                        2 (text ":=" <+> ppr ty2 <+> dcolon <+> ppr ty2_kind)
                  , text "co:" <+> ppr co ]
            ; writeMetaTyVar kappa (mkCastTy ty2 co) }
+
+      | otherwise
+      = return ()   -- Occurs-check or forall-bound varialbe
       where
-        ty2_tvs    = tyCoVarsOfType ty2
         ty2_kind   = typeKind ty2
         kappa_kind = tyVarKind kappa
 
 
+{- Note [Actual unification in qlUnify]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In qlUnify, if we find (kappa ~ ty), we are going to update kappa := ty.
+That is the entire point of qlUnify!   Wrinkles
+
+* We must not unify with anything bound by an enclosing forall; e.g.
+    (forall a. kappa -> Int) ~ forall a. a -> Int)
+  That's tracked by the 'bvs' arg of 'go'.
+
+* We must not make an occurs-check; we use occCheckExpand for that.
+
+* metaTyVarUpdateOK also checks for various other things, including
+  - foralls, and predicate types, which we want to allow here
+  - blocking coercion holes
+  - type families
+  But after some thought we believe that none of these are relevant
+  here.
+
+* What if kappa and ty have different kinds?  We solve that problem by
+  calling unifyKind, producing a coercion perhaps emitting some deferred
+  equality constraints.  That is /different/ from the approach we use in
+  the main constraint solver for herterogeneous equalities; see Note
+  [Equalities with incompatible kinds] in Solver.Canonical
+
+  Why different? Because:
+  - We can't use qlUnify to solve the kind constraint because qlUnify
+    won't unify ordinary (non-instantiation) unification variables.
+    (It would have to worry about lots of things like untouchability
+    if it did.)
+  - qlUnify can't give up if the kinds look un-equal because that would
+    mean that it might succeed some times (when the eager unifier
+    has already unified those kinds) but not others -- order
+    dependence.
+  - We can't use the ordinary unifier/constraint solver instead,
+    because it doesn't unify polykinds, and has all kinds of other
+    magic.  qlUnify is very focused.
+
+  TL;DR Calling unifyKind seems like the lesser evil.
+  -}
+
 {- *********************************************************************
 *                                                                      *
               Guardedness


=====================================
compiler/GHC/Tc/Solver.hs
=====================================
@@ -161,6 +161,9 @@ pushLevelAndSolveEqualities :: SkolemInfo -> [TcTyVar] -> TcM a -> TcM a
 -- Push level, and solve all resulting equalities
 -- If there are any unsolved equalities, report them
 -- and fail (in the monad)
+--
+-- Panics if we solve any non-equality constraints.  (In runTCSEqualities
+-- we use an error thunk for the evidence bindings.)
 pushLevelAndSolveEqualities skol_info skol_tvs thing_inside
   = do { (tclvl, wanted, res) <- pushLevelAndSolveEqualitiesX
                                       "pushLevelAndSolveEqualities" thing_inside
@@ -172,6 +175,9 @@ pushLevelAndSolveEqualitiesX :: String -> TcM a
 -- Push the level, gather equality constraints, and then solve them.
 -- Returns any remaining unsolved equalities.
 -- Does not report errors.
+--
+-- Panics if we solve any non-equality constraints.  (In runTCSEqualities
+-- we use an error thunk for the evidence bindings.)
 pushLevelAndSolveEqualitiesX callsite thing_inside
   = do { traceTc "pushLevelAndSolveEqualitiesX {" (text "Called from" <+> text callsite)
        ; (tclvl, (wanted, res))
@@ -187,6 +193,9 @@ pushLevelAndSolveEqualitiesX callsite thing_inside
 -- constraints we can and re-emitting constraints that we can't.
 -- Use this variant only when we'll get another crack at it later
 -- See Note [Failure in local type signatures]
+--
+-- Panics if we solve any non-equality constraints.  (In runTCSEqualities
+-- we use an error thunk for the evidence bindings.)
 solveEqualities :: String -> TcM a -> TcM a
 solveEqualities callsite thing_inside
   = do { traceTc "solveEqualities {" (text "Called from" <+> text callsite)


=====================================
compiler/GHC/Tc/Solver/Canonical.hs
=====================================
@@ -2144,7 +2144,7 @@ k2 and use this to cast. To wit, from
 
   [X] (tv :: k1) ~ (rhs :: k2)
 
-we go to
+(where [X] is [G], [W], or [D]), we go to
 
   [noDerived X] co :: k2 ~ k1
   [X]           (tv :: k1) ~ ((rhs |> co) :: k1)
@@ -2154,6 +2154,9 @@ where
   noDerived G = G
   noDerived _ = W
 
+For Wanted/Derived, the [X] constraint is "blocked" (not CTyEqCan, is CIrred)
+until the k1~k2 constraint solved: Wrinkle (2).
+
 Wrinkles:
 
  (1) The noDerived step is because Derived equalities have no evidence.
@@ -2166,7 +2169,7 @@ Wrinkles:
        [W] (tv :: k1) ~ ((rhs |> co) :: k1)
      as canonical in the inert set. In particular, we must not unify tv.
      If we did, the Wanted becomes a Given (effectively), and then can
-     rewrite other Wanteds. But that's bad: See Note [Wanteds to not rewrite Wanteds]
+     rewrite other Wanteds. But that's bad: See Note [Wanteds do not rewrite Wanteds]
      in GHC.Tc.Types.Constraint. The problem is about poor error messages. See #11198 for
      tales of destruction.
 


=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -14,7 +14,7 @@
 module GHC.Tc.Utils.Unify (
   -- Full-blown subsumption
   tcWrapResult, tcWrapResultO, tcWrapResultMono,
-  tcSkolemise, tcSkolemiseScoped, tcSkolemiseAlways, tcSkolemiseET,
+  tcSkolemise, tcSkolemiseScoped, tcSkolemiseET,
   tcSubType, tcSubTypeSigma, tcSubTypePat,
   tcSubMult,
   checkConstraints, checkTvConstraints,
@@ -93,6 +93,9 @@ matchActualFunTySigma
                                    -- Both are used only for error messages)
   -> TcRhoType                     -- Type to analyse: a TcRhoType
   -> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType)
+-- The /argument/ is a RhoType
+-- The /result/   is an (uninstantiated) SigmaType
+--
 -- See Note [matchActualFunTy error handling] for the first three arguments
 
 -- If   (wrap, arg_ty, res_ty) = matchActualFunTySigma ... fun_ty
@@ -826,10 +829,11 @@ to checkConstraints.
 
 tcSkolemiseScoped is very similar, but differs in two ways:
 
-* It deals specially with just the outer forall, bringing those
-  type variables into lexical scope.  To my surprise, I found that
-  doing this regardless (in tcSkolemise) caused a non-trivial (1%-ish)
-  perf hit on the compiler.
+* It deals specially with just the outer forall, bringing those type
+  variables into lexical scope.  To my surprise, I found that doing
+  this unconditionally in tcSkolemise (i.e. doing it even if we don't
+  need to bring the variables into lexical scope, which is harmless)
+  caused a non-trivial (1%-ish) perf hit on the compiler.
 
 * It always calls checkConstraints, even if there are no skolem
   variables at all.  Reason: there might be nested deferred errors
@@ -837,11 +841,13 @@ tcSkolemiseScoped is very similar, but differs in two ways:
   See Note [When to build an implication] below.
 -}
 
-tcSkolemise, tcSkolemiseScoped, tcSkolemiseAlways
+tcSkolemise, tcSkolemiseScoped
     :: UserTypeCtxt -> TcSigmaType
     -> (TcType -> TcM result)
     -> TcM (HsWrapper, result)
         -- ^ The wrapper has type: spec_ty ~> expected_ty
+-- See Note [Skolemisation] for the differences between
+-- tcSkolemiseScoped and tcSkolemise
 
 tcSkolemiseScoped ctxt expected_ty thing_inside
   = do { (wrap, tv_prs, given, rho_ty) <- topSkolemise expected_ty
@@ -860,9 +866,6 @@ tcSkolemise ctxt expected_ty thing_inside
   = do { res <- thing_inside expected_ty
        ; return (idHsWrapper, res) }
   | otherwise
-  = tcSkolemiseAlways ctxt expected_ty thing_inside
-
-tcSkolemiseAlways ctxt expected_ty thing_inside
   = do  { (wrap, tv_prs, given, rho_ty) <- topSkolemise expected_ty
 
         ; let skol_tvs  = map snd tv_prs
@@ -1946,7 +1949,7 @@ occCheckForErrors :: DynFlags -> TcTyVar -> Type -> MetaTyVarUpdateResult ()
 --   a) the given variable occurs in the given type.
 --   b) there is a forall in the type (unless we have -XImpredicativeTypes)
 occCheckForErrors dflags tv ty
-  = case preCheck dflags True tv ty of
+  = case mtvu_check dflags True tv ty of
       MTVU_OK _        -> MTVU_OK ()
       MTVU_Bad         -> MTVU_Bad
       MTVU_HoleBlocker -> MTVU_HoleBlocker
@@ -1960,13 +1963,20 @@ metaTyVarUpdateOK :: DynFlags
                   -> TcType              -- ty :: k2
                   -> MetaTyVarUpdateResult TcType        -- possibly-expanded ty
 -- (metaTyVarUpdateOK tv ty)
--- We are about to update the meta-tyvar tv with ty
--- Check (a) that tv doesn't occur in ty (occurs check)
+-- Checks that the equality tv~ty is OK to be used to rewrite
+-- other equalities.  Equivalently, checks the conditions for CTyEqCan
+--       (a) that tv doesn't occur in ty (occurs check)
 --       (b) that ty does not have any foralls
 --           (in the impredicative case), or type functions
 --       (c) that ty does not have any blocking coercion holes
 --           See Note [Equalities with incompatible kinds] in "GHC.Tc.Solver.Canonical"
 --
+-- Used in two places:
+--   - In the eager unifier: uUnfilledVar2
+--   - In the canonicaliser: GHC.Tc.Solver.Canonical.canEqTyVar2
+-- Note that in the latter case tv is not necessarily a meta-tyvar,
+-- despite the name of this function.
+
 -- We have two possible outcomes:
 -- (1) Return the type to update the type variable with,
 --        [we know the update is ok]
@@ -1985,7 +1995,7 @@ metaTyVarUpdateOK :: DynFlags
 -- See Note [Refactoring hazard: checkTauTvUpdate]
 
 metaTyVarUpdateOK dflags tv ty
-  = case preCheck dflags False tv ty of
+  = case mtvu_check dflags False tv ty of
          -- False <=> type families not ok
          -- See Note [Prevent unification with type families]
       MTVU_OK _        -> MTVU_OK ty
@@ -1995,8 +2005,8 @@ metaTyVarUpdateOK dflags tv ty
                             Just expanded_ty -> MTVU_OK expanded_ty
                             Nothing          -> MTVU_Occurs
 
-preCheck :: DynFlags -> Bool -> TcTyVar -> TcType -> MetaTyVarUpdateResult ()
--- A quick check for
+mtvu_check :: DynFlags -> Bool -> TcTyVar -> TcType -> MetaTyVarUpdateResult ()
+-- Checks the invariants for CTyEqCan.   In particular:
 --   (a) a forall type (forall a. blah)
 --   (b) a predicate type (c => ty)
 --   (c) a type family; see Note [Prevent unification with type families]
@@ -2007,7 +2017,7 @@ preCheck :: DynFlags -> Bool -> TcTyVar -> TcType -> MetaTyVarUpdateResult ()
 -- inside the kinds of variables it mentions.  For (d) we look deeply
 -- in coercions, and for (e) we do look in the kinds of course.
 
-preCheck dflags ty_fam_ok tv ty
+mtvu_check dflags ty_fam_ok tv ty
   = fast_check ty
   where
     ok :: MetaTyVarUpdateResult ()


=====================================
docs/users_guide/ghci.rst
=====================================
@@ -2968,7 +2968,7 @@ commonly used commands.
 
     Infers and prints the type of ⟨expression⟩.  For polymorphic types
     it instantiates the 'inferred' forall quantifiers (but not the
-    'specified' ones), solves constraints, and re-generalises.
+    'specified' ones; see :ref:`inferred-vs-specified`), solves constraints, and re-generalises.
 
     .. code-block:: none
 



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/126c219a502d2565d4d381a70ee3f464bce73a94...9f5ec17529213e447e708622289f2c32bb6b0739

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/126c219a502d2565d4d381a70ee3f464bce73a94...9f5ec17529213e447e708622289f2c32bb6b0739
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/20200914/75caf53f/attachment-0001.html>