From 924f749433e171cc92d5d4b97701381d2ef75726 Mon Sep 17 00:00:00 2001
From: Simon Peyton Jones <simonpj@microsoft.com>
Date: Fri, 14 Mar 2014 22:51:20 +0000
Subject: [PATCH] Unflatten the constraints of an inferred types (Trac #8889)
There was even a comment to warn about this possiblity,
and it finally showed up in practice! This patch fixes
it quite nicely, with commens to explain.
(cherry picked from commit 7a7af1ffc48f605cf365faf8fcef31ef4f13822b)
---
compiler/typecheck/TcMType.lhs | 2 +-
compiler/typecheck/TcSimplify.lhs | 44 ++++++++++++++++++++-----------
2 files changed, 29 insertions(+), 17 deletions(-)
diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs
index 2bed04c81cb2..b9f3d259fc9e 100644
--- a/compiler/typecheck/TcMType.lhs
+++ b/compiler/typecheck/TcMType.lhs
@@ -56,7 +56,7 @@ module TcMType (
zonkTcTyVarBndr, zonkTcType, zonkTcTypes, zonkTcThetaType,
zonkTcKind, defaultKindVarToStar,
- zonkEvVar, zonkWC, zonkId, zonkCt, zonkCts, zonkSkolemInfo,
+ zonkEvVar, zonkWC, zonkFlats, zonkId, zonkCt, zonkCts, zonkSkolemInfo,
tcGetGlobalTyVars,
) where
diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index 0fdd2ba3f5c5..af5772982600 100644
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -253,39 +253,50 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
; ev_binds_var <- newTcEvBinds
; wanted_transformed_incl_derivs
<- solveWantedsTcMWithEvBinds ev_binds_var wanteds solve_wanteds
- -- Post: wanted_transformed are zonked
+ -- Post: wanted_transformed_incl_derivs are zonked
-- Step 4) Candidates for quantification are an approximation of wanted_transformed
-- NB: Already the fixpoint of any unifications that may have happened
-- NB: We do not do any defaulting when inferring a type, this can lead
-- to less polymorphic types, see Note [Default while Inferring]
- -- Step 5) Minimize the quantification candidates
- -- Step 6) Final candidates for quantification
- -- We discard bindings, insolubles etc, because all we are
- -- care aout it
-
; tc_lcl_env <- TcRnMonad.getLclEnv
; let untch = tcl_untch tc_lcl_env
wanted_transformed = dropDerivedWC wanted_transformed_incl_derivs
; quant_pred_candidates -- Fully zonked
<- if insolubleWC wanted_transformed_incl_derivs
then return [] -- See Note [Quantification with errors]
- -- NB: must include derived errors
- else do { gbl_tvs <- tcGetGlobalTyVars
- ; let quant_cand = approximateWC wanted_transformed
+ -- NB: must include derived errors in this test,
+ -- hence "incl_derivs"
+
+ else do { let quant_cand = approximateWC wanted_transformed
meta_tvs = filter isMetaTyVar (varSetElems (tyVarsOfCts quant_cand))
- ; ((flats, _insols), _extra_binds) <- runTcS $
+ ; gbl_tvs <- tcGetGlobalTyVars
+ ; null_ev_binds_var <- newTcEvBinds
+ -- Miminise quant_cand. We are not interested in any evidence
+ -- produced, because we are going to simplify wanted_transformed
+ -- again later. All we want here is the predicates over which to
+ -- quantify.
+ --
+ -- If any meta-tyvar unifications take place (unlikely), we'll
+ -- pick that up later.
+
+ ; (flats, _insols) <- runTcSWithEvBinds null_ev_binds_var $
do { mapM_ (promoteAndDefaultTyVar untch gbl_tvs) meta_tvs
-- See Note [Promote _and_ default when inferring]
; _implics <- solveInteract quant_cand
; getInertUnsolved }
- ; return (map ctPred $ filter isWantedCt (bagToList flats)) }
- -- NB: Dimitrios is slightly worried that we will get
- -- family equalities (F Int ~ alpha) in the quantification
- -- candidates, as we have performed no further unflattening
- -- at this point. Nothing bad, but inferred contexts might
- -- look complicated.
+
+ ; flats' <- zonkFlats null_ev_binds_var untch $
+ filterBag isWantedCt flats
+ -- The quant_cand were already fully zonked, so this zonkFlats
+ -- really only unflattens the flattening that solveInteract
+ -- may have done (Trac #8889).
+ -- E.g. quant_cand = F a, where F :: * -> Constraint
+ -- We'll flatten to (alpha, F a ~ alpha)
+ -- fail to make any further progress and must unflatten again
+
+ ; return (map ctPred $ bagToList flats') }
-- NB: quant_pred_candidates is already the fixpoint of any
-- unifications that may have happened
@@ -326,6 +337,7 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
{ -- Step 7) Emit an implication
let minimal_flat_preds = mkMinimalBySCs bound
+ -- See Note [Minimize by Superclasses]
skol_info = InferSkol [ (name, mkSigmaTy [] minimal_flat_preds ty)
| (name, ty) <- name_taus ]
-- Don't add the quantified variables here, because
--
GitLab