From 2c58bef19ee9d245d4344c2ccb4b41e90d91c35a Mon Sep 17 00:00:00 2001
From: Simon Peyton Jones <simonpj@microsoft.com>
Date: Mon, 14 Apr 2014 13:33:27 +0100
Subject: [PATCH] Work in progress on better generalisation technology
There's a long explanation in Trac #8995. This branch just
captures where I'm up to.
---
compiler/typecheck/FunDeps.lhs | 42 +---------
compiler/typecheck/TcBinds.lhs | 9 +-
compiler/typecheck/TcMType.lhs | 4 +-
compiler/typecheck/TcRnDriver.lhs | 5 +-
compiler/typecheck/TcRnMonad.lhs | 14 +++-
compiler/typecheck/TcSMonad.lhs | 4 +-
compiler/typecheck/TcSimplify.lhs | 124 +++++++++++++++++++---------
compiler/typecheck/TcTyClsDecls.lhs | 4 +-
compiler/typecheck/TcType.lhs | 5 +-
compiler/typecheck/TcUnify.lhs | 2 +-
10 files changed, 116 insertions(+), 97 deletions(-)
diff --git a/compiler/typecheck/FunDeps.lhs b/compiler/typecheck/FunDeps.lhs
index 1dc96aa03721..5ff7cdadb6ee 100644
--- a/compiler/typecheck/FunDeps.lhs
+++ b/compiler/typecheck/FunDeps.lhs
@@ -13,7 +13,7 @@ module FunDeps (
Equation(..), pprEquation,
improveFromInstEnv, improveFromAnother,
checkInstCoverage, checkFunDeps,
- growThetaTyVars, pprFundeps
+ pprFundeps
) where
#include "HsVersions.h"
@@ -36,46 +36,6 @@ import Data.Maybe ( isJust )
\end{code}
-%************************************************************************
-%* *
-\subsection{Close type variables}
-%* *
-%************************************************************************
-
-Note [Growing the tau-tvs using constraints]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-(growThetaTyVars insts tvs) is the result of extending the set
- of tyvars tvs using all conceivable links from pred
-
-E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e}
-Then growThetaTyVars preds tvs = {a,b,c}
-
-Notice that
- growThetaTyVars is conservative if v might be fixed by vs
- => v `elem` grow(vs,C)
-
-\begin{code}
-growThetaTyVars :: ThetaType -> TyVarSet -> TyVarSet
--- See Note [Growing the tau-tvs using constraints]
-growThetaTyVars theta tvs
- | null theta = tvs
- | otherwise = fixVarSet mk_next tvs
- where
- mk_next tvs = foldr grow_one tvs theta
- grow_one pred tvs = growPredTyVars pred tvs `unionVarSet` tvs
-
-growPredTyVars :: PredType
- -> TyVarSet -- The set to extend
- -> TyVarSet -- TyVars of the predicate if it intersects the set,
-growPredTyVars pred tvs
- | isIPPred pred = pred_tvs -- Always quantify over implicit parameers
- | pred_tvs `intersectsVarSet` tvs = pred_tvs
- | otherwise = emptyVarSet
- where
- pred_tvs = tyVarsOfType pred
-\end{code}
-
-
%************************************************************************
%* *
\subsection{Generate equations from functional dependencies}
diff --git a/compiler/typecheck/TcBinds.lhs b/compiler/typecheck/TcBinds.lhs
index 8b2928c8c86e..5713125c83fb 100644
--- a/compiler/typecheck/TcBinds.lhs
+++ b/compiler/typecheck/TcBinds.lhs
@@ -30,7 +30,6 @@ import TcMType
import PatSyn
import ConLike
import Type( tidyOpenType )
-import FunDeps( growThetaTyVars )
import TyCon
import TcType
import TysPrim
@@ -553,7 +552,8 @@ tcPolyInfer
-> [(Origin, LHsBind Name)]
-> TcM (LHsBinds TcId, [TcId], TopLevelFlag)
tcPolyInfer rec_tc prag_fn tc_sig_fn mono closed bind_list
- = do { ((binds', mono_infos), wanted)
+ = tcPushUntouchables $
+ do { ((binds', mono_infos), wanted)
<- captureConstraints $
tcMonoBinds rec_tc tc_sig_fn LetLclBndr bind_list
@@ -609,10 +609,9 @@ mkExport prag_fn qtvs theta (poly_name, mb_sig, mono_id)
-- In the inference case (no signature) this stuff figures out
-- the right type variables and theta to quantify over
-- See Note [Impedence matching]
- my_tvs2 = closeOverKinds (growThetaTyVars theta (tyVarsOfType mono_ty))
+ (my_tvs2, my_theta) = growThetaTyVars (const True) (tyVarsOfType mono_ty) theta
+ my_tvs = filter (`elemVarSet` closeOverKinds my_tvs2) qtvs -- Maintain original order
-- Include kind variables! Trac #7916
- my_tvs = filter (`elemVarSet` my_tvs2) qtvs -- Maintain original order
- my_theta = filter (quantifyPred my_tvs2) theta
inferred_poly_ty = mkSigmaTy my_tvs my_theta mono_ty
; poly_id <- addInlinePrags poly_id prag_sigs
diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs
index b9f3d259fc9e..dac807e98a3a 100644
--- a/compiler/typecheck/TcMType.lhs
+++ b/compiler/typecheck/TcMType.lhs
@@ -284,7 +284,7 @@ newSigTyVar name kind
newMetaDetails :: MetaInfo -> TcM TcTyVarDetails
newMetaDetails info
= do { ref <- newMutVar Flexi
- ; untch <- getUntouchables
+ ; untch <- tcGetUntouchables
; return (MetaTv { mtv_info = info, mtv_ref = ref, mtv_untch = untch }) }
\end{code}
@@ -755,7 +755,7 @@ zonkEvVar var = do { ty' <- zonkTcType (varType var)
zonkWC :: EvBindsVar -- May add new bindings for wanted family equalities in here
-> WantedConstraints -> TcM WantedConstraints
zonkWC binds_var wc
- = do { untch <- getUntouchables
+ = do { untch <- tcGetUntouchables
; zonkWCRec binds_var untch wc }
zonkWCRec :: EvBindsVar
diff --git a/compiler/typecheck/TcRnDriver.lhs b/compiler/typecheck/TcRnDriver.lhs
index 90d7151c69af..667355938aaa 100644
--- a/compiler/typecheck/TcRnDriver.lhs
+++ b/compiler/typecheck/TcRnDriver.lhs
@@ -1794,8 +1794,9 @@ tcRnExpr hsc_env rdr_expr
-- it might have a rank-2 type (e.g. :t runST)
uniq <- newUnique ;
let { fresh_it = itName uniq (getLoc rdr_expr) } ;
- ((_tc_expr, res_ty), lie) <- captureConstraints $
- tcInferRho rn_expr ;
+ (((_tc_expr, res_ty), _), lie) <- captureConstraints $
+ captureUntouchables $
+ tcInferRho rn_expr ;
((qtvs, dicts, _, _), lie_top) <- captureConstraints $
{-# SCC "simplifyInfer" #-}
simplifyInfer True {- Free vars are closed -}
diff --git a/compiler/typecheck/TcRnMonad.lhs b/compiler/typecheck/TcRnMonad.lhs
index b3d37f61780e..6dd4df9859b8 100644
--- a/compiler/typecheck/TcRnMonad.lhs
+++ b/compiler/typecheck/TcRnMonad.lhs
@@ -1126,12 +1126,18 @@ captureUntouchables thing_inside
thing_inside
; return (res, untch') }
-getUntouchables :: TcM Untouchables
-getUntouchables = do { env <- getLclEnv
+tcPushUntouchables :: TcM a -> TcM a
+tcPushUntouchables thing_inside
+ = do { env <- getLclEnv
+ ; let untch' = pushUntouchables (tcl_untch env)
+ ; setLclEnv (env { tcl_untch = untch' }) thing_inside }
+
+tcGetUntouchables :: TcM Untouchables
+tcGetUntouchables = do { env <- getLclEnv
; return (tcl_untch env) }
-setUntouchables :: Untouchables -> TcM a -> TcM a
-setUntouchables untch thing_inside
+tcSetUntouchables :: Untouchables -> TcM a -> TcM a
+tcSetUntouchables untch thing_inside
= updLclEnv (\env -> env { tcl_untch = untch }) thing_inside
isTouchableTcM :: TcTyVar -> TcM Bool
diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index b7faf153caa7..229ab6b23927 100644
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/compiler/typecheck/TcSMonad.lhs
@@ -1125,7 +1125,7 @@ nestImplicTcS ref inner_untch inerts (TcS thing_inside)
, tcs_implics = panic "nextImplicTcS: implics"
-- NB: Both these are initialised by withWorkList
}
- ; res <- TcM.setUntouchables inner_untch $
+ ; res <- TcM.tcSetUntouchables inner_untch $
thing_inside nest_env
#ifdef DEBUG
@@ -1250,7 +1250,7 @@ getTcEvBinds :: TcS EvBindsVar
getTcEvBinds = TcS (return . tcs_ev_binds)
getUntouchables :: TcS Untouchables
-getUntouchables = wrapTcS TcM.getUntouchables
+getUntouchables = wrapTcS TcM.tcGetUntouchables
getGivenInfo :: TcS a -> TcS (Bool, [TcTyVar], a)
-- Run thing_inside, returning info on
diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index 64ef3fed4b56..f97c3abc1d21 100644
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -1,6 +1,6 @@
\begin{code}
module TcSimplify(
- simplifyInfer, quantifyPred,
+ simplifyInfer, growThetaTyVars,
simplifyAmbiguityCheck,
simplifyDefault,
simplifyRule, simplifyTop, simplifyInteractive,
@@ -18,7 +18,6 @@ import TcSMonad as TcS
import TcInteract
import Kind ( isKind, defaultKind_maybe )
import Inst
-import FunDeps ( growThetaTyVars )
import Type ( classifyPredType, PredTree(..), getClassPredTys_maybe )
import Class ( Class )
import Var
@@ -266,7 +265,7 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
; quant_pred_candidates -- Fully zonked
<- if insolubleWC wanted_transformed_incl_derivs
then return [] -- See Note [Quantification with errors]
- -- NB: must include derived errors in this test,
+ -- NB: must include derived errors in this test,
-- hence "incl_derivs"
else do { let quant_cand = approximateWC wanted_transformed
@@ -276,7 +275,7 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
-- 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.
+ -- quantify.
--
-- If any meta-tyvar unifications take place (unlikely), we'll
-- pick that up later.
@@ -291,10 +290,10 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
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).
+ -- 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
+ -- fail to make any further progress and must unflatten again
; return (map ctPred $ bagToList flats') }
@@ -302,33 +301,46 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
-- unifications that may have happened
; gbl_tvs <- tcGetGlobalTyVars
; zonked_tau_tvs <- TcM.zonkTyVarsAndFV (tyVarsOfTypes (map snd name_taus))
- ; let poly_qtvs = growThetaTyVars quant_pred_candidates zonked_tau_tvs
- `minusVarSet` gbl_tvs
- pbound = filter (quantifyPred poly_qtvs) quant_pred_candidates
+ ; let constrained_tvs
+ | apply_mr = tyVarsOfTypes quant_pred_candidates
+ | otherwise = tyVarsOfTypes (snd (growThetaTyVars (const True) gbl_tvs (filter isEqPred quant_pred_candidates)))
+
+ all_constrained_tvs = gbl_tvs `unionVarSet` constrained_tvs
+
+ (poly_qtvs, bound)
+ | apply_mr = (zonked_tau_tvs `minusVarSet` all_constrained_tvs, [])
+ | otherwise = growThetaTyVars (\tv -> not (tv `elemVarSet` all_constrained_tvs))
+ zonked_tau_tvs quant_pred_candidates
-- Monomorphism restriction
- constrained_tvs = tyVarsOfTypes pbound `unionVarSet` gbl_tvs
- mr_bites = apply_mr && not (null pbound)
+ mr_bites = not (constrained_tvs `subVarSet` gbl_tvs)
+
+#ifdef DEBUG
+ ; let check_untch str bad_tvs
+ = WARN( not (null bad_tvs),
+ hang (text ("Bad generalisation: " ++ str))
+ 2 (vcat [ppr untch, ppr bad_tvs]) )
+ return ()
- ; (qtvs, bound) <- if mr_bites
- then do { qtvs <- quantifyTyVars constrained_tvs zonked_tau_tvs
- ; return (qtvs, []) }
- else do { qtvs <- quantifyTyVars gbl_tvs poly_qtvs
- ; return (qtvs, pbound) }
+ ; check_untch "gbl tvs" (filter (isTouchableMetaTyVar untch) (varSetElems gbl_tvs))
+ ; check_untch "qtvs" (filterOut (isTouchableMetaTyVar untch) (varSetElems poly_qtvs))
+#endif
+
+ ; qtvs <- quantifyTyVars all_constrained_tvs poly_qtvs
; traceTc "simplifyWithApprox" $
vcat [ ptext (sLit "quant_pred_candidates =") <+> ppr quant_pred_candidates
+ , ptext (sLit "mr_bites =") <+> ppr mr_bites
, ptext (sLit "gbl_tvs=") <+> ppr gbl_tvs
, ptext (sLit "zonked_tau_tvs=") <+> ppr zonked_tau_tvs
- , ptext (sLit "pbound =") <+> ppr pbound
- , ptext (sLit "bbound =") <+> ppr bound
+ , ptext (sLit "bound =") <+> ppr bound
, ptext (sLit "poly_qtvs =") <+> ppr poly_qtvs
, ptext (sLit "constrained_tvs =") <+> ppr constrained_tvs
- , ptext (sLit "mr_bites =") <+> ppr mr_bites
, ptext (sLit "qtvs =") <+> ppr qtvs ]
; if null qtvs && null bound
then do { traceTc "} simplifyInfer/no implication needed" empty
+ ; mapM_ (promoteTyVarTcM (popUntouchables untch)) (varSetElems constrained_tvs)
; emitConstraints wanted_transformed
-- Includes insolubles (if -fdefer-type-errors)
-- as well as flats and implications
@@ -345,7 +357,12 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
-- tidied uniformly
; minimal_bound_ev_vars <- mapM TcM.newEvVar minimal_flat_preds
- ; let implic = Implic { ic_untch = pushUntouchables untch
+
+ ; mapM_ (promoteTyVarTcM (popUntouchables untch)) $
+ varSetElems ((zonked_tau_tvs `unionVarSet` tyVarsOfTypes minimal_flat_preds) `minusVarSet` poly_qtvs)
+
+ ; unless (isEmptyWC wanted_transformed) $
+ do { let implic = Implic { ic_untch = untch
, ic_skols = qtvs
, ic_no_eqs = False
, ic_fsks = [] -- wanted_tansformed arose only from solveWanteds
@@ -356,25 +373,47 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
, ic_binds = ev_binds_var
, ic_info = skol_info
, ic_env = tc_lcl_env }
- ; emitImplication implic
- ; traceTc "} simplifyInfer/produced residual implication for quantification" $
- vcat [ ptext (sLit "implic =") <+> ppr implic
- -- ic_skols, ic_given give rest of result
- , ptext (sLit "qtvs =") <+> ppr qtvs
- , ptext (sLit "spb =") <+> ppr quant_pred_candidates
- , ptext (sLit "bound =") <+> ppr bound ]
+ ; emitImplication implic
+ ; traceTc "} simplifyInfer/produced residual implication for quantification" $
+ vcat [ ptext (sLit "implic =") <+> ppr implic
+ -- ic_skols, ic_given give rest of result
+ , ptext (sLit "qtvs =") <+> ppr qtvs
+ , ptext (sLit "spb =") <+> ppr quant_pred_candidates
+ , ptext (sLit "bound =") <+> ppr bound ] }
; return ( qtvs, minimal_bound_ev_vars
, mr_bites, TcEvBinds ev_binds_var) } }
-quantifyPred :: TyVarSet -- Quantifying over these
- -> PredType -> Bool -- True <=> quantify over this wanted
-quantifyPred qtvs pred
- | isIPPred pred = True -- Note [Inheriting implicit parameters]
- | otherwise = tyVarsOfType pred `intersectsVarSet` qtvs
+growThetaTyVars :: (TcTyVar -> Bool) -> TyVarSet -> ThetaType -> (TyVarSet, ThetaType)
+-- See Note [Growing the tau-tvs using constraints]
+growThetaTyVars quantify_tv tvs theta
+ = go (filterVarSet quantify_tv tvs) [] [] theta
+ where
+ go tvs _ q_preds [] = (tvs, q_preds)
+ go tvs non_q_preds q_preds (pred:preds)
+ | not quantify_me = go tvs (pred:non_q_preds) q_preds preds
+ | pred_tvs `subVarSet` tvs = go tvs non_q_preds (pred:q_preds) preds
+ | otherwise = go (tvs `unionVarSet` pred_tvs)
+ [] (pred:q_preds)
+ (non_q_preds ++ preds)
+ where
+ pred_tvs = filterVarSet quantify_tv (tyVarsOfType pred)
+ quantify_me = isIPPred pred || pred_tvs `intersectsVarSet` tvs
\end{code}
+Note [Growing the tau-tvs using constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+(growThetaTyVars insts tvs) is the result of extending the set
+ of tyvars tvs using all conceivable links from pred
+
+E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e}
+Then growThetaTyVars preds tvs = {a,b,c}
+
+Notice that
+ growThetaTyVars is conservative if v might be fixed by vs
+ => v `elem` grow(vs,C)
+
Note [Inheriting implicit parameters]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this:
@@ -860,6 +899,15 @@ promoteTyVar untch tv
| otherwise
= return ()
+promoteTyVarTcM :: Untouchables -> TcTyVar -> TcM ()
+promoteTyVarTcM untch tv
+ | isFloatedTouchableMetaTyVar untch tv
+ = do { cloned_tv <- TcM.cloneMetaTyVar tv
+ ; let rhs_tv = setMetaTyVarUntouchables cloned_tv untch
+ ; writeMetaTyVar tv (mkTyVarTy rhs_tv) }
+ | otherwise
+ = return ()
+
promoteAndDefaultTyVar :: Untouchables -> TcTyVarSet -> TyVar -> TcS ()
-- See Note [Promote _and_ default when inferring]
promoteAndDefaultTyVar untch gbl_tvs tv
@@ -1155,14 +1203,16 @@ with two implications and a class with a functional dependency.
class C x y | x -> y
instance C [a] [a]
- (I1) [untch=beta]forall b. 0 => F Int ~ [beta]
- (I2) [untch=beta]forall c. 0 => F Int ~ [[alpha]] /\ C beta [c]
+ (I1) forall(1) b. 0 => F Int ~ [beta(0)]
+ (I2) forall(1) c. 0 => F Int ~ [[alpha(1)]] /\ C beta(0) [c]
We float (F Int ~ [beta]) out of I1, and we float (F Int ~ [[alpha]]) out of I2.
They may react to yield that (beta := [alpha]) which can then be pushed inwards
-the leftover of I2 to get (C [alpha] [a]) which, using the FunDep, will mean that
-(alpha := a). In the end we will have the skolem 'b' escaping in the untouchable
-beta! Concrete example is in indexed_types/should_fail/ExtraTcsUntch.hs:
+the leftover of I2 to get (C [alpha] [c]) which, using the FunDep, will mean that
+(alpha := c). In the end we will have the skolem 'c' escaping. By promoting alpha
+to level 0, we stop this happening.
+
+Concrete example is in indexed_types/should_fail/ExtraTcsUntch.hs:
class C x y | x -> y where
op :: x -> y -> ()
diff --git a/compiler/typecheck/TcTyClsDecls.lhs b/compiler/typecheck/TcTyClsDecls.lhs
index 3a589a9ce1e1..fc0f3500f36c 100644
--- a/compiler/typecheck/TcTyClsDecls.lhs
+++ b/compiler/typecheck/TcTyClsDecls.lhs
@@ -29,7 +29,7 @@ import TcEnv
import TcValidity
import TcHsSyn
import TcBinds( tcRecSelBinds )
-import FunDeps( growThetaTyVars )
+import TcSimplify( growThetaTyVars )
import TcTyDecls
import TcClassDcl
import TcHsType
@@ -1619,7 +1619,7 @@ checkValidClass cls
-- Here, MonadState has a fundep m->b, so newBoard is fine
-- The check is disabled for nullary type classes,
-- since there is no possible ambiguity
- ; let grown_tyvars = growThetaTyVars theta (mkVarSet tyvars)
+ ; let (grown_tyvars, _) = growThetaTyVars (const True) (mkVarSet tyvars) theta
; checkTc (arity == 0 || tyVarsOfType tau `intersectsVarSet` grown_tyvars)
(noClassTyVarErr cls sel_id)
diff --git a/compiler/typecheck/TcType.lhs b/compiler/typecheck/TcType.lhs
index 08c7a627ce59..907ef451cb12 100644
--- a/compiler/typecheck/TcType.lhs
+++ b/compiler/typecheck/TcType.lhs
@@ -22,7 +22,7 @@ module TcType (
TcTyVar, TcTyVarSet, TcKind, TcCoVar,
-- Untouchables
- Untouchables(..), noUntouchables, pushUntouchables, isTouchable,
+ Untouchables(..), noUntouchables, pushUntouchables, popUntouchables, isTouchable,
--------------------------------
-- MetaDetails
@@ -435,6 +435,9 @@ noUntouchables = Untouchables 0 -- 0 = outermost level
pushUntouchables :: Untouchables -> Untouchables
pushUntouchables (Untouchables us) = Untouchables (us+1)
+popUntouchables :: Untouchables -> Untouchables
+popUntouchables (Untouchables us) = ASSERT( us > 0 ) Untouchables (us-1)
+
isFloatedTouchable :: Untouchables -> Untouchables -> Bool
isFloatedTouchable (Untouchables ctxt_untch) (Untouchables tv_untch)
= ctxt_untch < tv_untch
diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs
index 94b6aebeb543..d1d897fb440b 100644
--- a/compiler/typecheck/TcUnify.lhs
+++ b/compiler/typecheck/TcUnify.lhs
@@ -557,7 +557,7 @@ uType_defer origin ty1 ty2
--------------
-- unify_np (short for "no push" on the origin stack) does the work
uType origin orig_ty1 orig_ty2
- = do { untch <- getUntouchables
+ = do { untch <- tcGetUntouchables
; traceTc "u_tys " $ vcat
[ text "untch" <+> ppr untch
, sep [ ppr orig_ty1, text "~", ppr orig_ty2]
--
GitLab