[commit: ghc] wip/ghc-8.0-det: Fix two buglets in 17eb241 noticed by Richard (6edd2a7)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : wip/ghc-8.0-det
Link       : http://ghc.haskell.org/trac/ghc/changeset/6edd2a71eb63ae7c94032c51675fb0998cfe21fc/ghc

>---------------------------------------------------------------

commit 6edd2a71eb63ae7c94032c51675fb0998cfe21fc
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Wed Apr 20 15:56:44 2016 +0100

    Fix two buglets in 17eb241 noticed by Richard
    
    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.


>---------------------------------------------------------------

6edd2a71eb63ae7c94032c51675fb0998cfe21fc
 compiler/typecheck/TcSimplify.hs | 29 +++++++++++++++--------------
 compiler/typecheck/TcType.hs     |  7 +------
 2 files changed, 16 insertions(+), 20 deletions(-)

diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs
index 70de14c..853976c 100644
--- a/compiler/typecheck/TcSimplify.hs
+++ b/compiler/typecheck/TcSimplify.hs
@@ -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 ]
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index 4f7d861..1e3f72b 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -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 )