Fix floating of equalities
authorSimon Peyton Jones <simonpj@microsoft.com>
Thu, 21 Dec 2017 14:13:54 +0000 (14:13 +0000)
committerSimon Peyton Jones <simonpj@microsoft.com>
Thu, 21 Dec 2017 14:14:21 +0000 (14:14 +0000)
This rather subtle patch fixes Trac #14584.  The problem was
that we'd allowed a coercion, bound in a nested scope, to escape
into an outer scope.

The main changes are

* TcSimplify.floatEqualities takes more care when floating
  equalities to make sure we don't float one out that mentions
  a locally-bound coercion.
  See Note [What prevents a constraint from floating]

* TcSimplify.emitResidualConstraints (which emits the residual
  constraints in simplifyInfer) now avoids burying the constraints
  for escaping CoVars inside the implication constraint.

* Since I had do to this stuff with CoVars, I moved the
  fancy footwork about not quantifying over CoVars from
  TcMType.quantifyTyVars to its caller
  TcSimplify.decideQuantifiedTyVars.  I think its other
  callers don't need to worry about all this CoVar stuff.

This turned out to be surprisigly tricky, and took me a solid
day to get right.  I think the result is reasonably neat, though,
and well documented with Notes.

compiler/typecheck/TcMType.hs
compiler/typecheck/TcSMonad.hs
compiler/typecheck/TcSimplify.hs
testsuite/tests/indexed-types/should_fail/T13877.stderr
testsuite/tests/partial-sigs/should_fail/T14584.hs [new file with mode: 0644]
testsuite/tests/partial-sigs/should_fail/T14584.stderr [new file with mode: 0644]
testsuite/tests/partial-sigs/should_fail/T14584a.hs [new file with mode: 0644]
testsuite/tests/partial-sigs/should_fail/T14584a.stderr [new file with mode: 0644]
testsuite/tests/partial-sigs/should_fail/all.T
testsuite/tests/typecheck/should_fail/VtaFail.stderr

index 83a3465..58b220b 100644 (file)
@@ -950,15 +950,11 @@ quantifyTyVars
 
 quantifyTyVars gbl_tvs dvs@(DV{ dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs })
   = do { traceTc "quantifyTyVars" (vcat [ppr dvs, ppr gbl_tvs])
-       ; let all_cvs = filterVarSet isCoVar $ dVarSetToVarSet dep_tkvs
-             dep_kvs = dVarSetElemsWellScoped $
+       ; let dep_kvs = dVarSetElemsWellScoped $
                        dep_tkvs `dVarSetMinusVarSet` gbl_tvs
-                                `dVarSetMinusVarSet` closeOverKinds all_cvs
-                 -- dVarSetElemsWellScoped: put the kind variables into
-                 --    well-scoped order.
-                 --    E.g.  [k, (a::k)] not the other way roud
-                 -- closeOverKinds all_cvs: do not quantify over coercion
-                 --    variables, or any any tvs that a covar depends on
+                       -- dVarSetElemsWellScoped: put the kind variables into
+                       --    well-scoped order.
+                       --    E.g.  [k, (a::k)] not the other way roud
 
              nondep_tvs = dVarSetElems $
                           (nondep_tkvs `minusDVarSet` dep_tkvs)
@@ -981,6 +977,7 @@ quantifyTyVars gbl_tvs dvs@(DV{ dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs })
        ; poly_kinds  <- xoptM LangExt.PolyKinds
        ; dep_kvs'    <- mapMaybeM (zonk_quant (not poly_kinds)) dep_kvs
        ; nondep_tvs' <- mapMaybeM (zonk_quant False)            nondep_tvs
+       ; let final_qtvs = dep_kvs' ++ nondep_tvs'
            -- Because of the order, any kind variables
            -- mentioned in the kinds of the nondep_tvs'
            -- now refer to the dep_kvs'
@@ -992,7 +989,11 @@ quantifyTyVars gbl_tvs dvs@(DV{ dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs })
                  , text "dep_kvs'" <+> pprTyVars dep_kvs'
                  , text "nondep_tvs'" <+> pprTyVars nondep_tvs' ])
 
-       ; return (dep_kvs' ++ nondep_tvs') }
+       -- We should never quantify over coercion variables; check this
+       ; let co_vars = filter isCoVar final_qtvs
+       ; MASSERT2( null co_vars, ppr co_vars )
+
+       ; return final_qtvs }
   where
     -- zonk_quant returns a tyvar if it should be quantified over;
     -- otherwise, it returns Nothing. The latter case happens for
index 7926e56..41a5097 100644 (file)
@@ -2724,10 +2724,9 @@ getTcEvBindsAndTCVs ev_binds_var
                  ; tcvs <- TcM.getTcEvTyCoVars ev_binds_var
                  ; return (bnds, tcvs) }
 
-getTcEvBindsMap :: TcS EvBindMap
-getTcEvBindsMap
-  = do { ev_binds_var <- getTcEvBindsVar
-       ; wrapTcS $ TcM.getTcEvBindsMap ev_binds_var }
+getTcEvBindsMap :: EvBindsVar -> TcS EvBindMap
+getTcEvBindsMap ev_binds_var
+  = wrapTcS $ TcM.getTcEvBindsMap ev_binds_var
 
 unifyTyVar :: TcTyVar -> TcType -> TcS ()
 -- Unify a meta-tyvar with a type
index 6ebf27d..af04abe 100644 (file)
@@ -664,21 +664,19 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
        -- NB: quant_pred_candidates is already fully zonked
        -- NB: bound_theta are constraints we want to quantify over,
        --     /apart from/ the psig_theta, which we always quantify over
-       ; (qtvs, bound_theta) <- decideQuantification infer_mode rhs_tclvl
+       ; (qtvs, bound_theta, co_vars) <- decideQuantification infer_mode rhs_tclvl
                                                      name_taus partial_sigs
                                                      quant_pred_candidates
 
-        -- Emit an implication constraint for the
-        -- remaining constraints from the RHS.
         -- We must retain the psig_theta_vars, because we've used them in
         -- evidence bindings constructed by solveWanteds earlier
        ; psig_theta_vars  <- mapM zonkId       psig_theta_vars
        ; bound_theta_vars <- mapM TcM.newEvVar bound_theta
        ; let full_theta_vars = psig_theta_vars ++ bound_theta_vars
 
-       ; emitResidualImplication rhs_tclvl tc_lcl_env ev_binds_var
-                                 name_taus qtvs full_theta_vars
-                                 wanted_transformed
+       ; emitResidualConstraints rhs_tclvl tc_lcl_env ev_binds_var
+                                 name_taus co_vars qtvs
+                                 full_theta_vars wanted_transformed
 
          -- All done!
        ; traceTc "} simplifyInfer/produced residual implication for quantification" $
@@ -694,42 +692,88 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
 
 
 --------------------
-emitResidualImplication :: TcLevel -> TcLclEnv -> EvBindsVar
-                        -> [(Name, TcTauType)] -> [TcTyVar] -> [EvVar]
+emitResidualConstraints :: TcLevel -> TcLclEnv -> EvBindsVar
+                        -> [(Name, TcTauType)]
+                        -> VarSet -> [TcTyVar] -> [EvVar]
                         -> WantedConstraints -> TcM ()
-emitResidualImplication rhs_tclvl tc_lcl_env ev_binds_var
-                        name_taus qtvs full_theta_vars wanteds
- | isEmptyWC wanteds
- = return ()
- | otherwise
- = do { traceTc "emitResidualImplication" (ppr implic)
-      ; emitImplication implic }
- where
-   implic = Implic { ic_tclvl    = rhs_tclvl
-                   , ic_skols    = qtvs
-                   , ic_no_eqs   = False
-                   , ic_given    = full_theta_vars
-                   , ic_wanted   = wanteds
-                   , ic_status   = IC_Unsolved
-                   , ic_binds    = ev_binds_var
-                   , ic_info     = skol_info
-                   , ic_needed   = emptyVarSet
-                   , ic_env      = tc_lcl_env }
-
-   full_theta = map idType full_theta_vars
-   skol_info  = InferSkol [ (name, mkSigmaTy [] full_theta ty)
-                          | (name, ty) <- name_taus ]
-                        -- Don't add the quantified variables here, because
-                        -- they are also bound in ic_skols and we want them
-                        -- to be tidied uniformly
+-- Emit the remaining constraints from the RHS.
+-- See Note [Emitting the residual implication in simplifyInfer]
+emitResidualConstraints rhs_tclvl tc_lcl_env ev_binds_var
+                        name_taus co_vars qtvs full_theta_vars wanteds
+  | isEmptyWC wanteds
+  = return ()
+  | otherwise
+  = do { wanted_simple <- TcM.zonkSimples (wc_simple wanteds)
+       ; let (outer_simple, inner_simple) = partitionBag is_mono wanted_simple
+             is_mono ct = isWantedCt ct && ctEvId ct `elemVarSet` co_vars
+
+        ; tc_lvl <- TcM.getTcLevel
+        ; mapM_ (promoteTyVar tc_lvl) (tyCoVarsOfCtsList outer_simple)
+
+        ; unless (isEmptyCts outer_simple) $
+          do { traceTc "emitResidualConstrants:simple" (ppr outer_simple)
+             ; emitSimples outer_simple }
+
+        ; let inner_wanted = wanteds { wc_simple = inner_simple }
+              implic       = mk_implic inner_wanted
+        ; unless (isEmptyWC inner_wanted) $
+          do { traceTc "emitResidualConstraints:implic" (ppr implic)
+             ; emitImplication implic }
+     }
+  where
+    mk_implic inner_wanted
+       = Implic { ic_tclvl    = rhs_tclvl
+                , ic_skols    = qtvs
+                , ic_no_eqs   = False
+                , ic_given    = full_theta_vars
+                , ic_wanted   = inner_wanted
+                , ic_status   = IC_Unsolved
+                , ic_binds    = ev_binds_var
+                , ic_info     = skol_info
+                , ic_needed   = emptyVarSet
+                , ic_env      = tc_lcl_env }
+
+    full_theta = map idType full_theta_vars
+    skol_info  = InferSkol [ (name, mkSigmaTy [] full_theta ty)
+                           | (name, ty) <- name_taus ]
+                 -- Don't add the quantified variables here, because
+                 -- they are also bound in ic_skols and we want them
+                 -- to be tidied uniformly
 
 --------------------
 ctsPreds :: Cts -> [PredType]
 ctsPreds cts = [ ctEvPred ev | ct <- bagToList cts
                              , let ev = ctEvidence ct ]
 
-{- Note [Add signature contexts as givens]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [Emitting the residual implication in simplifyInfer]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+   f = e
+where f's type is infeered to be something like (a, Proxy k (Int |> co))
+and we have an as-yet-unsolved, or perhaps insoluble, constraint
+   [W] co :: Type ~ k
+We can't form types like (forall co. blah), so we can't generalise over
+the coercion variable, and hence we can't generalise over things free in
+its kind, in the case 'k'.  But we can still generalise over 'a'.  So
+we'll generalise to
+   f :: forall a. (a, Proxy k (Int |> co))
+Now we do NOT want to form the residual implication constraint
+   forall a. [W] co :: Type ~ k
+because then co's eventual binding (which will be a value binding if we
+use -fdefer-type-errors) won't scope over the entire binding for 'f' (whose
+type mentions 'co').  Instead, just as we don't generalise over 'co', we
+should not bury its constraint inside the implication.  Instead, we must
+put it outside.
+
+That is the reason for the partitionBag in emitResidualConstraints,
+which takes the CoVars free in the inferred type, and pulls their
+constraints out.  (NB: this set of CoVars should be
+closed-over-kinds.)
+
+All rather subtle; see Trac #14584.
+
+Note [Add signature contexts as givens]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider this (Trac #11016):
   f2 :: (?x :: Int) => _
   f2 = ?x
@@ -812,7 +856,8 @@ decideQuantification
   -> [TcIdSigInst]         -- Partial type signatures (if any)
   -> [PredType]            -- Candidate theta; already zonked
   -> TcM ( [TcTyVar]       -- Quantify over these (skolems)
-         , [PredType] )    -- and this context (fully zonked)
+         , [PredType]      -- and this context (fully zonked)
+         , VarSet)
 -- See Note [Deciding quantification]
 decideQuantification infer_mode rhs_tclvl name_taus psigs candidates
   = do { -- Step 1: find the mono_tvs
@@ -824,7 +869,7 @@ decideQuantification infer_mode rhs_tclvl name_taus psigs candidates
        ; candidates <- defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates
 
        -- Step 3: decide which kind/type variables to quantify over
-       ; qtvs <- decideQuantifiedTyVars mono_tvs name_taus psigs candidates
+       ; (qtvs, co_vars) <- decideQuantifiedTyVars mono_tvs name_taus psigs candidates
 
        -- Step 4: choose which of the remaining candidate
        --         predicates to actually quantify over
@@ -839,9 +884,10 @@ decideQuantification infer_mode rhs_tclvl name_taus psigs candidates
            (vcat [ text "infer_mode:"   <+> ppr infer_mode
                  , text "candidates:"   <+> ppr candidates
                  , text "mono_tvs:"     <+> ppr mono_tvs
+                 , text "co_vars:"      <+> ppr co_vars
                  , text "qtvs:"         <+> ppr qtvs
                  , text "theta:"        <+> ppr theta ])
-       ; return (qtvs, theta) }
+       ; return (qtvs, theta, co_vars) }
 
 ------------------
 decideMonoTyVars :: InferMode
@@ -849,7 +895,7 @@ decideMonoTyVars :: InferMode
                  -> [TcIdSigInst]
                  -> [PredType]
                  -> TcM (TcTyCoVarSet, [PredType])
--- Decide which tyvars cannot be generalised:
+-- Decide which tyvars and covars cannot be generalised:
 --   (a) Free in the environment
 --   (b) Mentioned in a constraint we can't generalise
 --   (c) Connected by an equality to (a) or (b)
@@ -862,9 +908,9 @@ decideMonoTyVars infer_mode name_taus psigs candidates
        ; psig_qtvs <- mapM zonkTcTyVarToTyVar $
                       concatMap (map snd . sig_inst_skols) psigs
 
-       ; gbl_tvs <- tcGetGlobalTyCoVars
-       ; let eq_constraints  = filter isEqPred candidates
-             mono_tvs1       = growThetaTyVars eq_constraints gbl_tvs
+       ; mono_tvs0 <- tcGetGlobalTyCoVars
+       ; let eq_constraints = filter isEqPred candidates
+             mono_tvs1     = growThetaTyVars eq_constraints mono_tvs0
 
              constrained_tvs = (growThetaTyVars eq_constraints
                                                (tyCoVarsOfTypes no_quant)
@@ -873,7 +919,7 @@ decideMonoTyVars infer_mode name_taus psigs candidates
              -- constrained_tvs: the tyvars that we are not going to
              -- quantify solely because of the moonomorphism restriction
              --
-             -- (`minusVarSet` mono_tvs`): a type variable is only
+             -- (`minusVarSet` mono_tvs1`): a type variable is only
              --   "constrained" (so that the MR bites) if it is not
              --   free in the environment (Trac #13785)
              --
@@ -891,11 +937,12 @@ decideMonoTyVars infer_mode name_taus psigs candidates
        ; when (case infer_mode of { ApplyMR -> warn_mono; _ -> False}) $
          do { taus <- mapM (TcM.zonkTcType . snd) name_taus
             ; warnTc (Reason Opt_WarnMonomorphism)
-                     (constrained_tvs `intersectsVarSet` tyCoVarsOfTypes taus)
-                     mr_msg }
+                (constrained_tvs `intersectsVarSet` tyCoVarsOfTypes taus)
+                mr_msg }
 
        ; traceTc "decideMonoTyVars" $ vcat
-           [ text "gbl_tvs =" <+> ppr gbl_tvs
+           [ text "mono_tvs0 =" <+> ppr mono_tvs0
+           , text "mono_tvs1 =" <+> ppr mono_tvs1
            , text "no_quant =" <+> ppr no_quant
            , text "maybe_quant =" <+> ppr maybe_quant
            , text "eq_constraints =" <+> ppr eq_constraints
@@ -987,8 +1034,10 @@ decideQuantifiedTyVars
    -> [(Name,TcType)]   -- Annotated theta and (name,tau) pairs
    -> [TcIdSigInst]     -- Partial signatures
    -> [PredType]        -- Candidates, zonked
-   -> TcM [TyVar]
+   -> TcM ([TyVar], CoVarSet)
 -- Fix what tyvars we are going to quantify over, and quantify them
+-- Also return CoVars that appear free in the final quatified types
+--   we can't quantify over these, and we must make sure they are in scope
 decideQuantifiedTyVars mono_tvs name_taus psigs candidates
   = do {     -- Why psig_tys? We try to quantify over everything free in here
              -- See Note [Quantification and partial signatures]
@@ -997,14 +1046,24 @@ decideQuantifiedTyVars mono_tvs name_taus psigs candidates
                                                   , (_,tv) <- sig_inst_skols sig ]
        ; psig_theta <- mapM TcM.zonkTcType [ pred | sig <- psigs
                                                   , pred <- sig_inst_theta sig ]
-       ; tau_tys <- mapM (TcM.zonkTcType . snd) name_taus
+       ; tau_tys  <- mapM (TcM.zonkTcType . snd) name_taus
+       ; mono_tvs <- TcM.zonkTyCoVarsAndFV mono_tvs
 
        ; let -- Try to quantify over variables free in these types
              psig_tys = psig_tv_tys ++ psig_theta
              seed_tys = psig_tys ++ tau_tys
 
              -- Now "grow" those seeds to find ones reachable via 'candidates'
-             grown_tvs = growThetaTyVars candidates (tyCoVarsOfTypes seed_tys)
+             grown_tcvs = growThetaTyVars candidates (tyCoVarsOfTypes seed_tys)
+
+       -- We cannot quantify a type over a coercion (term-level) variable
+       -- So, if any CoVars appear in grow_tcvs (they might for example
+       -- appear in a cast in a type) we must remove them from the quantified
+       -- variables, along with any type variables free in their kinds
+       -- E.g.  If we can't quantify over co :: k~Type, then we can't
+       --       quantify over k either!  Hence closeOverKinds
+       ; let co_vars    = filterVarSet isCoVar grown_tcvs
+             proto_qtvs = grown_tcvs `minusVarSet` closeOverKinds co_vars
 
        -- Now we have to classify them into kind variables and type variables
        -- (sigh) just for the benefit of -XNoPolyKinds; see quantifyTyVars
@@ -1015,33 +1074,37 @@ decideQuantifiedTyVars mono_tvs name_taus psigs candidates
        ; let DV {dv_kvs = cand_kvs, dv_tvs = cand_tvs}
                       = candidateQTyVarsOfTypes $
                         psig_tys ++ candidates ++ tau_tys
-             pick     = (`dVarSetIntersectVarSet` grown_tvs)
+             pick     = (`dVarSetIntersectVarSet` proto_qtvs)
              dvs_plus = DV { dv_kvs = pick cand_kvs, dv_tvs = pick cand_tvs }
 
-       ; mono_tvs <- TcM.zonkTyCoVarsAndFV mono_tvs
-       ; quantifyTyVars mono_tvs dvs_plus }
+       ; traceTc "decideQuantifiedTyVars" (vcat
+           [ text "seed_tys =" <+> ppr seed_tys
+           , text "seed_tcvs =" <+> ppr (tyCoVarsOfTypes seed_tys)
+           , text "grown_tcvs =" <+> ppr grown_tcvs
+           , text "co_vars =" <+> ppr co_vars
+           , text "proto_qtvs =" <+> ppr proto_qtvs])
+
+       ; qtvs <- quantifyTyVars mono_tvs dvs_plus
+       ; return (qtvs, co_vars) }
 
 ------------------
-growThetaTyVars :: ThetaType -> TyCoVarSet -> TyVarSet
+growThetaTyVars :: ThetaType -> TyCoVarSet -> TyCoVarSet
 -- See Note [Growing the tau-tvs using constraints]
--- NB: only returns tyvars, never covars
-growThetaTyVars theta tvs
-  | null theta = tvs_only
-  | otherwise  = filterVarSet isTyVar $
-                 transCloVarSet mk_next seed_tvs
+growThetaTyVars theta tcvs
+  | null theta = tcvs
+  | otherwise  = transCloVarSet mk_next seed_tcvs
   where
-    tvs_only = filterVarSet isTyVar tvs
-    seed_tvs = tvs `unionVarSet` tyCoVarsOfTypes ips
+    seed_tcvs = tcvs `unionVarSet` tyCoVarsOfTypes ips
     (ips, non_ips) = partition isIPPred theta
                          -- See Note [Inheriting implicit parameters] in TcType
 
     mk_next :: VarSet -> VarSet -- Maps current set to newly-grown ones
     mk_next so_far = foldr (grow_one so_far) emptyVarSet non_ips
-    grow_one so_far pred tvs
-       | pred_tvs `intersectsVarSet` so_far = tvs `unionVarSet` pred_tvs
-       | otherwise                          = tvs
+    grow_one so_far pred tcvs
+       | pred_tcvs `intersectsVarSet` so_far = tcvs `unionVarSet` pred_tcvs
+       | otherwise                           = tcvs
        where
-         pred_tvs = tyCoVarsOfType pred
+         pred_tcvs = tyCoVarsOfType pred
 
 {- Note [Promote momomorphic tyvars]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1303,7 +1366,8 @@ solveWanteds wc@(WC { wc_simple = simples, wc_impl = implics })
                                 (WC { wc_simple = simples2
                                     , wc_impl   = implics2 })
 
-       ; bb <- TcS.getTcEvBindsMap
+       ; ev_binds_var <- getTcEvBindsVar
+       ; bb <- TcS.getTcEvBindsMap ev_binds_var
        ; traceTcS "solveWanteds }" $
                  vcat [ text "final wc =" <+> ppr final_wc
                       , text "current evbinds  =" <+> ppr (evBindMapBinds bb) ]
@@ -1459,7 +1523,8 @@ solveImplication imp@(Implic { ic_tclvl  = tclvl
                   ; return (no_eqs, given_insols, residual_wanted) }
 
        ; (floated_eqs, residual_wanted)
-             <- floatEqualities skols no_given_eqs residual_wanted
+             <- floatEqualities skols given_ids ev_binds_var
+                                no_given_eqs residual_wanted
 
        ; traceTcS "solveImplication 2"
            (ppr given_insols $$ ppr residual_wanted)
@@ -2034,7 +2099,7 @@ no evidence for a fundep equality), but equality superclasses do matter (since
 they carry evidence).
 -}
 
-floatEqualities :: [TcTyVar] -> Bool
+floatEqualities :: [TcTyVar] -> [EvId] -> EvBindsVar -> Bool
                 -> WantedConstraints
                 -> TcS (Cts, WantedConstraints)
 -- Main idea: see Note [Float Equalities out of Implications]
@@ -2051,7 +2116,8 @@ floatEqualities :: [TcTyVar] -> Bool
 --
 -- Subtleties: Note [Float equalities from under a skolem binding]
 --             Note [Skolem escape]
-floatEqualities skols no_given_eqs
+--             Note [What prevents a constraint from floating]
+floatEqualities skols given_ids ev_binds_var no_given_eqs
                 wanteds@(WC { wc_simple = simples })
   | not no_given_eqs  -- There are some given equalities, so don't float
   = return (emptyBag, wanteds)   -- Note [Float Equalities out of Implications]
@@ -2062,37 +2128,59 @@ floatEqualities skols no_given_eqs
          -- variables, and we /must/ see them.  Otherwise we may float
          -- constraints that mention the skolems!
          simples <- TcS.zonkSimples simples
+       ; binds   <- TcS.getTcEvBindsMap ev_binds_var
 
        -- Now we can pick the ones to float
-       ; let (float_eqs, remaining_simples) = partitionBag (usefulToFloat skol_set) simples
-             skol_set = mkVarSet skols
+       -- The constraints are un-flattened and de-canonicalised
+       ; let seed_skols = mkVarSet skols     `unionVarSet`
+                          mkVarSet given_ids `unionVarSet`
+                          foldEvBindMap add_one emptyVarSet binds
+             add_one bind acc = extendVarSet acc (evBindVar bind)
+             -- seed_skols: See Note [What prevents a constraint from floating] (1,2,3)
+
+             (eqs, non_eqs)        = partitionBag is_eq_ct simples
+             extended_skols        = transCloVarSet (extra_skols eqs) seed_skols
+             (flt_eqs, no_flt_eqs) = partitionBag (is_floatable extended_skols) eqs
+             remaining_simples = non_eqs `andCts` no_flt_eqs
+             -- extended_skols: See Note [What prevents a constraint from floating] (3)
 
        -- Promote any unification variables mentioned in the floated equalities
        -- See Note [Promoting unification variables]
        ; outer_tclvl <- TcS.getTcLevel
        ; mapM_ (promoteTyVarTcS outer_tclvl)
-               (tyCoVarsOfCtsList float_eqs)
+               (tyCoVarsOfCtsList flt_eqs)
 
        ; traceTcS "floatEqualities" (vcat [ text "Skols =" <+> ppr skols
+                                          , text "Extended skols =" <+> ppr extended_skols
                                           , text "Simples =" <+> ppr simples
-                                          , text "Floated eqs =" <+> ppr float_eqs])
-       ; return ( float_eqs
-                , wanteds { wc_simple = remaining_simples } ) }
-
-usefulToFloat :: VarSet        -- ^ the skolems in the implication
-              -> Ct -> Bool
-usefulToFloat skol_set ct   -- The constraint is un-flattened and de-canonicalised
-  = is_meta_var_eq pred &&
-    (tyCoVarsOfType pred `disjointVarSet` skol_set)
+                                          , text "Eqs =" <+> ppr eqs
+                                          , text "Floated eqs =" <+> ppr flt_eqs])
+       ; return ( flt_eqs, wanteds { wc_simple = remaining_simples } ) }
+
   where
-    pred = ctPred ct
+    is_floatable :: VarSet -> Ct -> Bool
+    is_floatable skols ct
+      | isDerivedCt ct = not (tyCoVarsOfCt ct `intersectsVarSet` skols)
+      | otherwise      = not (ctEvId ct `elemVarSet` skols)
+
+    is_eq_ct ct | CTyEqCan {} <- ct      = True
+                | is_homo_eq (ctPred ct) = True
+                | otherwise              = False
+
+    extra_skols :: Cts -> VarSet -> VarSet
+    extra_skols eqs skols = foldrBag extra_skol emptyVarSet eqs
+       where
+         extra_skol ct acc
+           | isDerivedCt ct                           = acc
+           | tyCoVarsOfCt ct `intersectsVarSet` skols = extendVarSet acc (ctEvId ct)
+           | otherwise                                = acc
 
       -- Float out alpha ~ ty, or ty ~ alpha
       -- which might be unified outside
       -- See Note [Which equalities to float]
-    is_meta_var_eq pred
+    is_homo_eq pred
       | EqPred NomEq ty1 ty2 <- classifyPredType pred
-      , is_homogeneous ty1 ty2
+      , typeKind ty1 `tcEqType` typeKind ty2
       = case (tcGetTyVar_maybe ty1, tcGetTyVar_maybe ty2) of
           (Just tv1, _) -> float_tv_eq tv1 ty2
           (_, Just tv2) -> float_tv_eq tv2 ty1
@@ -2104,16 +2192,6 @@ usefulToFloat skol_set ct   -- The constraint is un-flattened and de-canonicalis
       =  isMetaTyVar tv1
       && (not (isSigTyVar tv1) || isTyVarTy ty2)
 
-    is_homogeneous ty1 ty2
-      = not has_heterogeneous_form ||  -- checking the shape is quicker
-                                       -- than looking at kinds
-        typeKind ty1 `tcEqType` typeKind ty2
-
-    has_heterogeneous_form = case ct of
-      CIrredCan {}     -> True
-      CNonCanonical {} -> True
-      _                -> False
-
 
 {- Note [Float equalities from under a skolem binding]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2177,6 +2255,36 @@ skolem has escaped!
 But it's ok: when we float (Maybe beta[2] ~ gamma[1]), we promote beta[2]
 to beta[1], and that means the (a ~ beta[1]) will be stuck, as it should be.
 
+Note [What prevents a constraint from floating]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+What /prevents/ a constraint from floating?  If it mentions one of the
+"bound variables of the implication".  What are they?
+
+The "bound variables of the implication" are
+
+  1. The skolem type variables `ic_skols`
+
+  2. The "given" evidence variables `ic_given`.  Example:
+         forall a. (co :: t1 ~# t2) =>  [W] co : (a ~# b |> co)
+
+  3. The binders of all evidence bindings in `ic_binds`. Example
+         forall a. (d :: t1 ~ t2)
+            EvBinds { (co :: t1 ~# t2) = superclass-sel d }
+            => [W] co : (a ~# b |> co)
+     Here `co` is gotten by superclass selection from `d`.
+
+  4. And the evidence variable of any equality constraint whose type
+     mentions a bound variable.  Example:
+        forall k. [W] co1 :: t1 ~# t2 |> co2
+            [W] co2 :: k ~# *
+     Here, since `k` is bound, so is `co2` and hence so is `co1`.
+
+Here (1,2,3) are handled by the "seed_skols" calculation, and
+(4) is done by the transCloVarSet call.
+
+The possible dependence on givens, and evidence bindings, is more
+subtle than we'd realised at first.  See Trac #14584.
+
 
 *********************************************************************************
 *                                                                               *
index a90a4dd..9dc8534 100644 (file)
@@ -2,7 +2,9 @@
 T13877.hs:65:17: error:
     • Couldn't match type ‘Apply p (x : xs)’ with ‘p (x : xs)’
       Expected type: Sing x
-                     -> Sing xs -> App [a] (':->) * p xs -> App [a] (':->) * p (x : xs)
+                     -> Sing xs
+                     -> App [a1] (':->) * p xs
+                     -> App [a1] (':->) * p (x : xs)
         Actual type: Sing x -> Sing xs -> (p @@ xs) -> p @@ (x : xs)
     • In the expression: listElimPoly @(:->) @a @p @l
       In an equation for ‘listElimTyFun’:
@@ -10,14 +12,14 @@ T13877.hs:65:17: error:
     • Relevant bindings include
         listElimTyFun :: Sing l
                          -> (p @@ '[])
-                         -> (forall (x :: a) (xs :: [a]).
+                         -> (forall (x :: a1) (xs :: [a1]).
                              Sing x -> Sing xs -> (p @@ xs) -> p @@ (x : xs))
                          -> p @@ l
           (bound at T13877.hs:65:1)
 
 T13877.hs:65:41: error:
     • Expecting one more argument to ‘p’
-      Expected kind ‘(-?>) [a] * (':->)’, but ‘p’ has kind ‘[a] ~> *’
+      Expected kind ‘(-?>) [a1] * (':->)’, but ‘p’ has kind ‘[a1] ~> *’
     • In the type ‘p’
       In the expression: listElimPoly @(:->) @a @p @l
       In an equation for ‘listElimTyFun’:
@@ -25,7 +27,7 @@ T13877.hs:65:41: error:
     • Relevant bindings include
         listElimTyFun :: Sing l
                          -> (p @@ '[])
-                         -> (forall (x :: a) (xs :: [a]).
+                         -> (forall (x :: a1) (xs :: [a1]).
                              Sing x -> Sing xs -> (p @@ xs) -> p @@ (x : xs))
                          -> p @@ l
           (bound at T13877.hs:65:1)
diff --git a/testsuite/tests/partial-sigs/should_fail/T14584.hs b/testsuite/tests/partial-sigs/should_fail/T14584.hs
new file mode 100644 (file)
index 0000000..508725e
--- /dev/null
@@ -0,0 +1,56 @@
+{-# OPTIONS_GHC -fdefer-type-errors #-}     -- Very important to this bug!
+{-# Language PartialTypeSignatures #-}
+{-# Language TypeFamilyDependencies, KindSignatures #-}
+{-# Language PolyKinds #-}
+{-# Language DataKinds #-}
+{-# Language TypeFamilies #-}
+{-# Language RankNTypes #-}
+{-# Language NoImplicitPrelude #-}
+{-# Language FlexibleContexts #-}
+{-# Language MultiParamTypeClasses #-}
+{-# Language GADTs #-}
+{-# Language ConstraintKinds #-}
+{-# Language FlexibleInstances #-}
+{-# Language TypeOperators #-}
+{-# Language ScopedTypeVariables #-}
+{-# Language DefaultSignatures #-}
+{-# Language FunctionalDependencies #-}
+{-# Language UndecidableSuperClasses #-}
+{-# Language UndecidableInstances #-}
+{-# Language TypeInType #-}
+{-# Language AllowAmbiguousTypes #-}
+{-# Language InstanceSigs, TypeApplications #-}
+
+module T14584 where
+
+import Data.Monoid
+import Data.Kind
+
+data family Sing (a::k)
+
+class SingKind k where
+  type Demote k = (res :: Type) | res -> k
+  fromSing :: Sing (a::k) -> Demote k
+
+class SingI (a::k) where
+  sing :: Sing a
+
+data ACT  :: Type -> Type -> Type
+data MHOM :: Type -> Type -> Type
+
+type m %%-  a  = ACT  m a  -> Type
+type m %%-> m' = MHOM m m' -> Type
+
+class Monoid m => Action (act :: m %%- a) where
+  act :: m -> (a -> a)
+
+class (Monoid m, Monoid m') => MonHom (mhom :: m %%-> m') where
+  monHom :: m -> m'
+
+data MonHom_Distributive m :: (m %%- a) -> (a %%-> a)
+
+type Good k = (Demote k ~ k, SingKind k)
+
+instance (Action act, Monoid a, Good m) => MonHom (MonHom_Distributive m act :: a %%-> a) where
+  monHom :: a -> a
+  monHom = act @_ @_ @act (fromSing @m (sing @m @a :: Sing _))
diff --git a/testsuite/tests/partial-sigs/should_fail/T14584.stderr b/testsuite/tests/partial-sigs/should_fail/T14584.stderr
new file mode 100644 (file)
index 0000000..65c2381
--- /dev/null
@@ -0,0 +1,21 @@
+
+T14584.hs:56:50: warning: [-Wdeferred-type-errors (in -Wdefault)]
+    • Expected kind ‘m1’, but ‘a’ has kind ‘*’
+    • In the type ‘a’
+      In the second argument of ‘fromSing’, namely
+        ‘(sing @m @a :: Sing _)’
+      In the fourth argument of ‘act’, namely
+        ‘(fromSing @m (sing @m @a :: Sing _))’
+
+T14584.hs:56:60: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘a :: m’
+      Where: ‘a’, ‘m’ are rigid type variables bound by
+               the instance declaration
+               at T14584.hs:54:10-89
+    • In an expression type signature: Sing _
+      In the second argument of ‘fromSing’, namely
+        ‘(sing @m @a :: Sing _)’
+      In the fourth argument of ‘act’, namely
+        ‘(fromSing @m (sing @m @a :: Sing _))’
+    • Relevant bindings include
+        monHom :: a -> a (bound at T14584.hs:56:3)
diff --git a/testsuite/tests/partial-sigs/should_fail/T14584a.hs b/testsuite/tests/partial-sigs/should_fail/T14584a.hs
new file mode 100644 (file)
index 0000000..016295a
--- /dev/null
@@ -0,0 +1,16 @@
+{-# OPTIONS_GHC -fdefer-type-errors #-}     -- Very important to this bug!
+{-# Language PartialTypeSignatures #-}
+{-# Language KindSignatures #-}
+{-# Language PolyKinds #-}
+{-# Language ScopedTypeVariables #-}
+{-# Language AllowAmbiguousTypes #-}
+{-# Language TypeApplications #-}
+
+module T14584a where
+
+f :: forall m. ()
+f = id @m :: _
+
+g :: forall m. ()
+g = let h = id @m
+    in h
diff --git a/testsuite/tests/partial-sigs/should_fail/T14584a.stderr b/testsuite/tests/partial-sigs/should_fail/T14584a.stderr
new file mode 100644 (file)
index 0000000..d6be3fc
--- /dev/null
@@ -0,0 +1,24 @@
+
+T14584a.hs:12:5: warning: [-Wdeferred-type-errors (in -Wdefault)]
+    • Couldn't match expected type ‘()’ with actual type ‘m -> m’
+    • In the expression: id @m :: _
+      In an equation for ‘f’: f = id @m :: _
+
+T14584a.hs:12:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘m -> m’
+      Where: ‘m’, ‘k’ are rigid type variables bound by
+               the type signature for:
+                 f :: forall k2 (m :: k2). ()
+               at T14584a.hs:11:1-17
+    • In an expression type signature: _
+      In the expression: id @m :: _
+      In an equation for ‘f’: f = id @m :: _
+    • Relevant bindings include f :: () (bound at T14584a.hs:12:1)
+
+T14584a.hs:16:8: warning: [-Wdeferred-type-errors (in -Wdefault)]
+    • Couldn't match expected type ‘()’ with actual type ‘m -> m’
+    • Probable cause: ‘h’ is applied to too few arguments
+      In the expression: h
+      In the expression: let h = id @m in h
+      In an equation for ‘g’: g = let h = id @m in h
+    • Relevant bindings include h :: m -> m (bound at T14584a.hs:15:9)
index 91509c4..b974ce8 100644 (file)
@@ -67,3 +67,5 @@ test('T12732', normal, compile_fail, ['-fobject-code -fdefer-typed-holes'])
 test('T14040a', normal, compile_fail, [''])
 test('T14449', normal, compile_fail, [''])
 test('T14479', normal, compile_fail, [''])
+test('T14584', normal, compile, [''])
+test('T14584a', normal, compile, [''])
index 17486df..a995801 100644 (file)
@@ -6,12 +6,6 @@ VtaFail.hs:7:16: error:
       In an equation for ‘answer_nosig’:
           answer_nosig = pairup_nosig @Int @Bool 5 True
 
-VtaFail.hs:12:26: error:
-    • No instance for (Num Bool) arising from a use of ‘addOne’
-    • In the expression: addOne @Bool 5
-      In an equation for ‘answer_constraint_fail’:
-          answer_constraint_fail = addOne @Bool 5
-
 VtaFail.hs:14:17: error:
     • Cannot apply expression of type ‘p0 -> p0’
       to a visible type argument ‘Int’