Commit 61191dee authored by Simon Peyton Jones's avatar Simon Peyton Jones

Fix two buglets in 17eb2419 noticed by Richard

These are corner cases in
   17eb2419 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.
parent 353d8ae6
...@@ -594,10 +594,10 @@ simplifyInfer rhs_tclvl apply_mr sigs name_taus wanteds ...@@ -594,10 +594,10 @@ simplifyInfer rhs_tclvl apply_mr sigs name_taus wanteds
-- Decide what type variables and constraints to quantify -- Decide what type variables and constraints to quantify
; zonked_taus <- mapM (TcM.zonkTcType . snd) name_taus ; 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) ; (qtvs, bound_theta)
<- decideQuantification apply_mr sigs name_taus <- 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 -- Promote any type variables that are free in the inferred type
-- of the function: -- of the function:
...@@ -611,24 +611,25 @@ simplifyInfer rhs_tclvl apply_mr sigs name_taus wanteds ...@@ -611,24 +611,25 @@ simplifyInfer rhs_tclvl apply_mr sigs name_taus wanteds
-- we don't quantify over beta (since it is fixed by envt) -- we don't quantify over beta (since it is fixed by envt)
-- so we must promote it! The inferred type is just -- so we must promote it! The inferred type is just
-- f :: beta -> beta -- 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 -- decideQuantification turned some meta tyvars into
-- quantified skolems, so we have to zonk again -- quantified skolems, so we have to zonk again
; let phi_tvs = tyCoVarsOfTypes bound_theta ; let phi_tkvs = tyCoVarsOfTypes bound_theta -- Already zonked
`unionVarSet` zonked_tau_tvs `unionVarSet` zonked_tau_tkvs
promote_tkvs = closeOverKinds phi_tkvs `delVarSetList` qtvs
promote_tvs = closeOverKinds phi_tvs `delVarSetList` qtvs ; MASSERT2( closeOverKinds promote_tkvs `subVarSet` promote_tkvs
; MASSERT2( closeOverKinds promote_tvs `subVarSet` promote_tvs , ppr phi_tkvs $$
, ppr phi_tvs $$ ppr (closeOverKinds phi_tkvs) $$
ppr (closeOverKinds phi_tvs) $$ ppr promote_tkvs $$
ppr promote_tvs $$ ppr (closeOverKinds promote_tkvs) )
ppr (closeOverKinds promote_tvs) )
-- we really don't want a type to be promoted when its kind isn't! -- we really don't want a type to be promoted when its kind isn't!
-- promoteTyVar ignores coercion variables -- promoteTyVar ignores coercion variables
; outer_tclvl <- TcM.getTcLevel ; outer_tclvl <- TcM.getTcLevel
; mapM_ (promoteTyVar outer_tclvl) (varSetElems promote_tvs) ; mapM_ (promoteTyVar outer_tclvl) (varSetElems promote_tkvs)
-- Emit an implication constraint for the -- Emit an implication constraint for the
-- remaining constraints from the RHS -- remaining constraints from the RHS
...@@ -654,8 +655,8 @@ simplifyInfer rhs_tclvl apply_mr sigs name_taus wanteds ...@@ -654,8 +655,8 @@ simplifyInfer rhs_tclvl apply_mr sigs name_taus wanteds
; traceTc "} simplifyInfer/produced residual implication for quantification" $ ; traceTc "} simplifyInfer/produced residual implication for quantification" $
vcat [ text "quant_pred_candidates =" <+> ppr quant_pred_candidates vcat [ text "quant_pred_candidates =" <+> ppr quant_pred_candidates
, text "zonked_taus" <+> ppr zonked_taus , text "zonked_taus" <+> ppr zonked_taus
, text "zonked_tau_tvs=" <+> ppr zonked_tau_tvs , text "zonked_tau_dvs=" <+> ppr zonked_tau_dvs
, text "promote_tvs=" <+> ppr promote_tvs , text "promote_tvs=" <+> ppr promote_tkvs
, text "bound_theta =" <+> ppr bound_theta , text "bound_theta =" <+> ppr bound_theta
, text "qtvs =" <+> ppr qtvs , text "qtvs =" <+> ppr qtvs
, text "implic =" <+> ppr implic ] , text "implic =" <+> ppr implic ]
......
...@@ -932,12 +932,7 @@ split_dep_vars = go ...@@ -932,12 +932,7 @@ split_dep_vars = go
go (LitTy {}) = mempty go (LitTy {}) = mempty
go (CastTy ty co) = go ty `mappend` Pair (tyCoVarsOfCo co) go (CastTy ty co) = go ty `mappend` Pair (tyCoVarsOfCo co)
emptyVarSet emptyVarSet
go (CoercionTy co) = go_co co go (CoercionTy co) = Pair (tyCoVarsOfCo co) emptyVarSet
go_co co = let Pair ty1 ty2 = coercionKind co in
-- co :: ty1 ~ ty2
go ty1 `mappend` go ty2
{- {-
************************************************************************ ************************************************************************
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment