Make approximateWC a bit clevererwip/T22194-flags

This MR fixes #23224: making approximateWC more clever

See the long `Note [ApproximateWC]` in GHC.Tc.Solver

All this is delicate and ad-hoc -- but it /has/ to be: we are
talking about inferring a type for a binding in the presence of
GADTs, type families and whatnot: known difficult territory.
We just try as hard as we can.

1 files changed, 94 insertions, 61 deletions

diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs
index 6c02ade8d2..d4dae8e31e 100644
--- a/compiler/GHC/Tc/Solver.hs
+++ b/compiler/GHC/Tc/Solver.hs
@@ -1142,7 +1142,7 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
    = do { -- When quantifying, we want to preserve any order of variables as they
           -- appear in partial signatures. cf. decideQuantifiedTyVars
           let psig_tv_tys = [ mkTyVarTy tv | sig <- partial_sigs
-                                          , (_,Bndr tv _) <- sig_inst_skols sig ]
+                                           , (_,Bndr tv _) <- sig_inst_skols sig ]
               psig_theta  = [ pred | sig <- partial_sigs
                                    , pred <- sig_inst_theta sig ]
 
@@ -1535,8 +1535,7 @@ decideQuantification
 decideQuantification skol_info infer_mode rhs_tclvl name_taus psigs candidates
   = do { -- Step 1: find the mono_tvs
        ; (candidates, co_vars, mono_tvs0)
-             <- decidePromotedTyVars infer_mode
-                                     name_taus psigs candidates
+             <- decidePromotedTyVars infer_mode name_taus psigs candidates
 
        -- Step 2: default any non-mono tyvars, and re-simplify
        -- This step may do some unification, but result candidates is zonked
@@ -1736,7 +1735,7 @@ decidePromotedTyVars infer_mode name_taus psigs candidates
              --   by some variable that is free in the env't
 
              mono_tvs = (mono_tvs2 `unionVarSet` constrained_tvs)
-                          `delVarSetList` psig_qtvs
+                        `delVarSetList` psig_qtvs
              -- (`delVarSetList` psig_qtvs): if the user has explicitly
              --   asked for quantification, then that request "wins"
              --   over the MR.
@@ -1755,6 +1754,8 @@ decidePromotedTyVars infer_mode name_taus psigs candidates
 
        ; traceTc "decidePromotedTyVars" $ vcat
            [ text "infer_mode =" <+> ppr infer_mode
+           , text "psigs =" <+> ppr psigs
+           , text "psig_qtvs =" <+> ppr psig_qtvs
            , text "mono_tvs0 =" <+> ppr mono_tvs0
            , text "no_quant =" <+> ppr no_quant
            , text "maybe_quant =" <+> ppr maybe_quant
@@ -1876,7 +1877,8 @@ decideQuantifiedTyVars skol_info name_taus psigs candidates
 -- See Note [pickQuantifiablePreds]
 pickQuantifiablePreds
   :: TyVarSet           -- Quantifying over these
-  -> TcTyVarSet         -- These ones are free in the enviroment
+  -> TcTyVarSet         -- mono_tvs0: variables mentioned a candidate
+                        --   constraint that come from some outer level
   -> TcThetaType        -- Proposed constraints to quantify
   -> TcM TcThetaType    -- A subset that we can actually quantify
 -- This function decides whether a particular constraint should be
@@ -1888,9 +1890,9 @@ pickQuantifiablePreds qtvs mono_tvs0 theta
                  mapMaybe (pick_me is_nested) theta) }
   where
     pick_me is_nested pred
-      | let pred_tvs = tyCoVarsOfType pred
+      = let pred_tvs = tyCoVarsOfType pred
             mentions_qtvs = pred_tvs `intersectsVarSet` qtvs
-      = case classifyPredType pred of
+        in case classifyPredType pred of
 
           ClassPred cls tys
             | Just {} <- isCallStackPred cls tys
@@ -2141,15 +2143,16 @@ Definitely not.  Since we're not quantifying over beta, it has been
 promoted; and then will be zapped to Any in the final zonk.  So we end
 up with a (perhaps exported) type involving
   forall a. Zork a (Z [Char]) Any => blah
-No no no.  We never want to show the programmer a type with `Any` in it.
+No no no:
+
+  Key principle: we never want to show the programmer
+                 a type with `Any` in it.
 
 What we really want (to catch the Zork example) is this:
-Hence, for a top-level binding, we eliminate the candidate from the
-pool, by asking
 
-   Do not quantify over the constraint if it mentions a variable that is
-   (a) not quantified (i.e. is determined by the type environment), but
-   (b) do not appear literally in the environment (mono_tvs0)?
+   Quantify over the constraint only if all its free variables are
+   (a) quantified, or
+   (b) appears in the type of something in the environment (mono_tvs0).
 
 To understand (b) consider
 
@@ -2163,14 +2166,24 @@ In `f1` should we quantify over that `(C b alpha)`?  Answer: since `alpha`
 is free in the type envt, yes we should.  After all, if we'd typechecked
 `intify` first, we'd have set `alpha := Int`, and /then/ we'd certainly
 quantify.  The delicate Zork situation applies when beta is completely
-unconstrained -- except by the fudep.
-
-However this subtle reasoning is needed only for /top-level/ declarations.
-For /nested/ decls we can see all the calls, so we'll instantiate that
-quantifed `Zork a (Z [Char]) beta` constraint at call sites, and either solve
-it or not (probably not).  We won't be left with a still-callable function
-with Any in its type.  So for nested definitions we don't make this tricky
-test.
+unconstrained (not free in the environment) -- except by the fundep.
+
+Another way to put it: let's say `alpha` is in `mono_tvs0`. It must be that
+some variable `x` has `alpha` free in its type. If we are at top-level (and we
+are, because nested decls don't go through this path all), then `x` must also
+be at top-level. And, by induction, `x` will not have Any in its type when all
+is said and done. The induction is well-founded because, if `x` is mutually
+recursive with the definition at hand, then their constraints get processed
+together (or `x` has a type signature, in which case the type doesn't have
+`Any`). So the key thing is that we must not introduce a new top-level
+unconstrained variable here.
+
+However this regrettably-subtle reasoning is needed only for /top-level/
+declarations.  For /nested/ decls we can see all the calls, so we'll
+instantiate that quantifed `Zork a (Z [Char]) beta` constraint at call sites,
+and either solve it or not (probably not).  We won't be left with a
+still-callable function with Any in its type.  So for nested definitions we
+don't make this tricky test.
 
 Historical note: we had a different, and more complicated test
 before, but it was utterly wrong: #23199.
@@ -3187,32 +3200,41 @@ defaultTyVarTcS the_tv
   | otherwise
   = return False  -- the common case
 
-approximateWC :: Bool -> WantedConstraints -> Cts
+approximateWC :: Bool   -- See Wrinkle (W3) in Note [ApproximateWC]
+              -> WantedConstraints
+              -> Cts
 -- Second return value is the depleted wc
--- Third return value is YesFDsCombined <=> multiple constraints for the same fundep floated
 -- Postcondition: Wanted Cts
 -- See Note [ApproximateWC]
 -- See Note [floatKindEqualities vs approximateWC]
 approximateWC float_past_equalities wc
-  = float_wc emptyVarSet wc
+  = float_wc False emptyVarSet wc
   where
-    float_wc :: TcTyCoVarSet -> WantedConstraints -> Cts
-    float_wc trapping_tvs (WC { wc_simple = simples, wc_impl = implics })
-      = filterBag (is_floatable trapping_tvs) simples `unionBags`
-        concatMapBag (float_implic trapping_tvs) implics
-    float_implic :: TcTyCoVarSet -> Implication -> Cts
-    float_implic trapping_tvs imp
-      | float_past_equalities || ic_given_eqs imp /= MaybeGivenEqs
-      = float_wc new_trapping_tvs (ic_wanted imp)
-      | otherwise   -- Take care with equalities
-      = emptyCts    -- See (1) under Note [ApproximateWC]
+    float_wc :: Bool           -- True <=> there are enclosing equalities
+             -> TcTyCoVarSet   -- Enclosing skolem binders
+             -> WantedConstraints -> Cts
+    float_wc encl_eqs trapping_tvs (WC { wc_simple = simples, wc_impl = implics })
+      = filterBag (is_floatable encl_eqs trapping_tvs) simples `unionBags`
+        concatMapBag (float_implic encl_eqs trapping_tvs) implics
+
+    float_implic :: Bool -> TcTyCoVarSet -> Implication -> Cts
+    float_implic encl_eqs trapping_tvs imp
+      = float_wc new_encl_eqs new_trapping_tvs (ic_wanted imp)
       where
         new_trapping_tvs = trapping_tvs `extendVarSetList` ic_skols imp
-
-    is_floatable skol_tvs ct
-       | isGivenCt ct     = False
-       | insolubleEqCt ct = False
-       | otherwise        = tyCoVarsOfCt ct `disjointVarSet` skol_tvs
+        new_encl_eqs = encl_eqs || ic_given_eqs imp == MaybeGivenEqs
+
+    is_floatable encl_eqs skol_tvs ct
+       | isGivenCt ct                                = False
+       | insolubleEqCt ct                            = False
+       | tyCoVarsOfCt ct `intersectsVarSet` skol_tvs = False
+       | otherwise
+       = case classifyPredType (ctPred ct) of
+           EqPred {}     -> float_past_equalities || not encl_eqs
+                                  -- See Wrinkle (W1)
+           ClassPred {}  -> True  -- See Wrinkle (W2)
+           IrredPred {}  -> True  -- ..both in Note [ApproximateWC]
+           ForAllPred {} -> False
 
 {- Note [ApproximateWC]
 ~~~~~~~~~~~~~~~~~~~~~~~
@@ -3225,28 +3247,39 @@ out from inside, if they are not captured by skolems.
 The same function is used when doing type-class defaulting (see the call
 to applyDefaultingRules) to extract constraints that might be defaulted.
 
-There is one caveat:
-
-1.  When inferring most-general types (in simplifyInfer), we do *not*
-    float anything out if the implication binds equality constraints,
-    because that defeats the OutsideIn story.  Consider
-       data T a where
-         TInt :: T Int
-         MkT :: T a
-
-       f TInt = 3::Int
-
-    We get the implication (a ~ Int => res ~ Int), where so far we've decided
-      f :: T a -> res
-    We don't want to float (res~Int) out because then we'll infer
-      f :: T a -> Int
-    which is only on of the possible types. (GHC 7.6 accidentally *did*
-    float out of such implications, which meant it would happily infer
-    non-principal types.)
-
-   HOWEVER (#12797) in findDefaultableGroups we are not worried about
-   the most-general type; and we /do/ want to float out of equalities.
-   Hence the boolean flag to approximateWC.
+Wrinkle (W1)
+  When inferring most-general types (in simplifyInfer), we
+  do *not* float an equality constraint if the implication binds
+  equality constraints, because that defeats the OutsideIn story.
+  Consider data T a where TInt :: T Int MkT :: T a
+
+         f TInt = 3::Int
+
+  We get the implication (a ~ Int => res ~ Int), where so far we've decided
+     f :: T a -> res
+  We don't want to float (res~Int) out because then we'll infer
+     f :: T a -> Int
+  which is only on of the possible types. (GHC 7.6 accidentally *did*
+  float out of such implications, which meant it would happily infer
+  non-principal types.)
+
+Wrinkle (W2)
+  We do allow /class/ constraints to float, even if
+  the implication binds equalities.  This is a subtle point: see #23224.
+  In principle, a class constraint might ultimately be satisfiable from
+  a constraint bound by an implication (see #19106 for an example of this
+  kind), but it's extremely obscure and I was unable to construct a
+  concrete example.  In any case, in super-subtle cases where this might
+  make a difference, you would be much better advised to simply write a
+  type signature.
+
+  I included IrredPred here too, for good measure.  In general,
+  abstracting over more constraints does no harm.
+
+Wrinkle (W3)
+  In findDefaultableGroups we are not worried about the
+  most-general type; and we /do/ want to float out of equalities
+  (#12797).  Hence the boolean flag to approximateWC.
 
 ------ Historical note -----------
 There used to be a second caveat, driven by #8155