Fix two buglets in 17eb241 noticed by Richard
authorSimon Peyton Jones <simonpj@microsoft.com>
Wed, 20 Apr 2016 14:56:44 +0000 (15:56 +0100)
committerBartosz Nitka <niteria@gmail.com>
Mon, 25 Jul 2016 14:31:58 +0000 (07:31 -0700)
These are corner cases in
   17eb241 Refactor computing dependent type vars
and I couldn't even come up with a test case

* In TcSimplify.simplifyInfer, in the promotion step, be sure
  to promote kind variables as well as type variables.

* In TcType.spiltDepVarsOfTypes, the CoercionTy case, be sure
  to get the free coercion variables too.

(cherry picked from commit 61191deee82d315a9279f11615e379d7c231dc51)

compiler/typecheck/TcSimplify.hs
compiler/typecheck/TcType.hs

index 70de14c..853976c 100644 (file)
@@ -604,10 +604,10 @@ simplifyInfer rhs_tclvl apply_mr sigs name_taus wanteds
 
        -- Decide what type variables and constraints to quantify
        ; zonked_taus <- mapM (TcM.zonkTcType . snd) name_taus
-       ; let zonked_tau_tkvs = splitDepVarsOfTypes zonked_taus
+       ; let zonked_tau_dvs = splitDepVarsOfTypes zonked_taus
        ; (qtvs, bound_theta)
            <- decideQuantification apply_mr sigs name_taus
-                                   quant_pred_candidates zonked_tau_tkvs
+                                   quant_pred_candidates zonked_tau_dvs
 
          -- Promote any type variables that are free in the inferred type
          -- of the function:
@@ -621,24 +621,25 @@ simplifyInfer rhs_tclvl apply_mr sigs name_taus wanteds
          -- we don't quantify over beta (since it is fixed by envt)
          -- so we must promote it!  The inferred type is just
          --   f :: beta -> beta
-       ; zonked_tau_tvs <- TcM.zonkTyCoVarsAndFV (dv_tvs zonked_tau_tkvs)
+       ; zonked_tau_tkvs <- TcM.zonkTyCoVarsAndFV $
+                            dv_kvs zonked_tau_dvs `unionVarSet` dv_tvs zonked_tau_dvs
               -- decideQuantification turned some meta tyvars into
               -- quantified skolems, so we have to zonk again
 
-       ; let phi_tvs = tyCoVarsOfTypes bound_theta
-                       `unionVarSet` zonked_tau_tvs
+       ; let phi_tkvs = tyCoVarsOfTypes bound_theta  -- Already zonked
+                        `unionVarSet` zonked_tau_tkvs
+             promote_tkvs = closeOverKinds phi_tkvs `delVarSetList` qtvs
 
-             promote_tvs = closeOverKinds phi_tvs `delVarSetList` qtvs
-       ; MASSERT2( closeOverKinds promote_tvs `subVarSet` promote_tvs
-                 , ppr phi_tvs $$
-                   ppr (closeOverKinds phi_tvs) $$
-                   ppr promote_tvs $$
-                   ppr (closeOverKinds promote_tvs) )
+       ; MASSERT2( closeOverKinds promote_tkvs `subVarSet` promote_tkvs
+                 , ppr phi_tkvs $$
+                   ppr (closeOverKinds phi_tkvs) $$
+                   ppr promote_tkvs $$
+                   ppr (closeOverKinds promote_tkvs) )
            -- we really don't want a type to be promoted when its kind isn't!
 
            -- promoteTyVar ignores coercion variables
        ; outer_tclvl <- TcM.getTcLevel
-       ; mapM_ (promoteTyVar outer_tclvl) (varSetElems promote_tvs)
+       ; mapM_ (promoteTyVar outer_tclvl) (varSetElems promote_tkvs)
 
            -- Emit an implication constraint for the
            -- remaining constraints from the RHS
@@ -664,8 +665,8 @@ simplifyInfer rhs_tclvl apply_mr sigs name_taus wanteds
        ; traceTc "} simplifyInfer/produced residual implication for quantification" $
          vcat [ text "quant_pred_candidates =" <+> ppr quant_pred_candidates
               , text "zonked_taus" <+> ppr zonked_taus
-              , text "zonked_tau_tvs=" <+> ppr zonked_tau_tvs
-              , text "promote_tvs=" <+> ppr promote_tvs
+              , text "zonked_tau_dvs=" <+> ppr zonked_tau_dvs
+              , text "promote_tvs=" <+> ppr promote_tkvs
               , text "bound_theta =" <+> ppr bound_theta
               , text "qtvs =" <+> ppr qtvs
               , text "implic =" <+> ppr implic ]
index 4f7d861..1e3f72b 100644 (file)
@@ -931,12 +931,7 @@ split_dep_vars = go
     go (LitTy {})                = mempty
     go (CastTy ty co)            = go ty `mappend` Pair (tyCoVarsOfCo co)
                                                         emptyVarSet
-    go (CoercionTy co)           = go_co co
-
-    go_co co = let Pair ty1 ty2 = coercionKind co in
-                   -- co :: ty1 ~ ty2
-               go ty1 `mappend` go ty2
-
+    go (CoercionTy co)           = Pair (tyCoVarsOfCo co) emptyVarSet
 
 isTouchableOrFmv ctxt_tclvl tv
   = ASSERT2( isTcTyVar tv, ppr tv )