From e9ae0cae9eb6a340473b339b5711ae76c6bdd045 Mon Sep 17 00:00:00 2001 From: Simon Peyton Jones Date: Wed, 31 Jan 2018 14:25:50 +0000 Subject: [PATCH] Look inside implications in simplifyRule Trac #14732 was a perpelexing bug in which -fdefer-typed-holes caused a mysterious type error in a RULE. This turned out to be because we are more aggressive about creating implications when deferring (see TcUnify.implicationNeeded), and the rule mechanism hadn't caught up. This fixes it. --- compiler/typecheck/TcRules.hs | 105 ++++++++++++------ .../tests/typecheck/should_compile/T14732.hs | 34 ++++++ .../tests/typecheck/should_compile/all.T | 1 + 3 files changed, 109 insertions(+), 31 deletions(-) create mode 100644 testsuite/tests/typecheck/should_compile/T14732.hs diff --git a/compiler/typecheck/TcRules.hs b/compiler/typecheck/TcRules.hs index fd7ce2f9fa..75e4025ac2 100644 --- a/compiler/typecheck/TcRules.hs +++ b/compiler/typecheck/TcRules.hs @@ -25,8 +25,10 @@ import TcEnv import TcUnify( buildImplicationFor ) import TcEvidence( mkTcCoVarCo ) import Type +import TyCon( isTypeFamilyTyCon ) import Id import Var( EvVar ) +import VarSet import BasicTypes ( RuleName ) import SrcLoc import Outputable @@ -254,7 +256,7 @@ where 'alpha' is the type that connects the two. If we glom them all together, and solve the RHS constraint first, we might solve with alpha := Bool. But then we'd end up with a RULE like - RULE: f 3 |> (co :: T Int ~ Booo) = True + RULE: f 3 |> (co :: T Int ~ Bool) = True which is terrible. We want @@ -310,52 +312,36 @@ simplifyRule :: RuleName -- NB: This consumes all simple constraints on the LHS, but not -- any LHS implication constraints. simplifyRule name lhs_wanted rhs_wanted - = do { -- We allow ourselves to unify environment - -- variables: runTcS runs with topTcLevel - ; lhs_clone <- cloneWC lhs_wanted - ; rhs_clone <- cloneWC rhs_wanted - + = do { -- Note [The SimplifyRule Plan] step 1 -- First solve the LHS and *then* solve the RHS -- Crucially, this performs unifications - -- See Note [Solve order for RULES] - -- See Note [Simplify cloned constraints] - ; insoluble <- runTcSDeriveds $ - do { lhs_resid <- solveWanteds lhs_clone - ; rhs_resid <- solveWanteds rhs_clone - ; return ( insolubleWC lhs_resid || - insolubleWC rhs_resid ) } + -- Why clone? See Note [Simplify cloned constraints] + ; lhs_clone <- cloneWC lhs_wanted + ; rhs_clone <- cloneWC rhs_wanted + ; runTcSDeriveds $ + do { _ <- solveWanteds lhs_clone + ; _ <- solveWanteds rhs_clone + -- Why do them separately? + -- See Note [Solve order for RULES] + ; return () } -- Note [The SimplifyRule Plan] step 2 - ; zonked_lhs_simples <- zonkSimples (wc_simple lhs_wanted) + ; lhs_wanted <- zonkWC lhs_wanted + ; let (quant_cts, residual_lhs_wanted) = getRuleQuantCts lhs_wanted -- Note [The SimplifyRule Plan] step 3 - ; let quantify_ct :: Ct -> Bool - quantify_ct ct - | EqPred _ t1 t2 <- classifyPredType (ctPred ct) - = not (insoluble || t1 `tcEqType` t2) - -- Note [RULE quantification over equalities] - | isHoleCt ct - = False -- Don't quantify over type holes, obviously - | otherwise - = True - - -- Note [The SimplifyRule Plan] step 3 - ; let (quant_cts, no_quant_cts) = partitionBag quantify_ct - zonked_lhs_simples - ; quant_evs <- mapM mk_quant_ev (bagToList quant_cts) ; traceTc "simplifyRule" $ vcat [ text "LHS of rule" <+> doubleQuotes (ftext name) , text "lhs_wanted" <+> ppr lhs_wanted , text "rhs_wanted" <+> ppr rhs_wanted - , text "zonked_lhs_simples" <+> ppr zonked_lhs_simples , text "quant_cts" <+> ppr quant_cts - , text "no_quant_cts" <+> ppr no_quant_cts + , text "residual_lhs_wanted" <+> ppr residual_lhs_wanted ] - ; return (quant_evs, lhs_wanted { wc_simple = no_quant_cts }) } + ; return (quant_evs, residual_lhs_wanted) } where mk_quant_ev :: Ct -> TcM EvVar @@ -368,3 +354,60 @@ simplifyRule name lhs_wanted rhs_wanted ; fillCoercionHole hole (mkTcCoVarCo ev_id) ; return ev_id } mk_quant_ev ct = pprPanic "mk_quant_ev" (ppr ct) + + +getRuleQuantCts :: WantedConstraints -> (Cts, WantedConstraints) +-- Extract all the constraints we can quantify over, +-- also returning the depleted WantedConstraints +-- +-- NB: we must look inside implications, because with +-- -fdefer-type-errors we generate implications rather eagerly; +-- see TcUnify.implicationNeeded. Not doing so caused Trac #14732. +-- +-- Unlike simplifyInfer, we don't leave the WantedConstraints unchanged, +-- and attempt to solve them from the quantified constraints. That +-- nearly works, but fails for a constraint like (d :: Eq Int). +-- We /do/ want to quantify over it, but the short-cut solver +-- (see TcInteract Note [Shortcut solving]) ignores the quantified +-- and instead solves from the top level. +-- +-- So we must partition the WantedConstraints ourselves +-- Not hard, but tiresome. + +getRuleQuantCts wc + = float_wc emptyVarSet wc + where + float_wc :: TcTyCoVarSet -> WantedConstraints -> (Cts, WantedConstraints) + float_wc skol_tvs (WC { wc_simple = simples, wc_impl = implics }) + = ( simple_yes `andCts` implic_yes + , WC { wc_simple = simple_no, wc_impl = implics_no }) + where + (simple_yes, simple_no) = partitionBag (rule_quant_ct skol_tvs) simples + (implic_yes, implics_no) = mapAccumBagL (float_implic skol_tvs) + emptyBag implics + + float_implic :: TcTyCoVarSet -> Cts -> Implication -> (Cts, Implication) + float_implic skol_tvs yes1 imp + = (yes1 `andCts` yes2, imp { ic_wanted = no }) + where + (yes2, no) = float_wc new_skol_tvs (ic_wanted imp) + new_skol_tvs = skol_tvs `extendVarSetList` ic_skols imp + + rule_quant_ct :: TcTyCoVarSet -> Ct -> Bool + rule_quant_ct skol_tvs ct + | EqPred _ t1 t2 <- classifyPredType (ctPred ct) + , not (ok_eq t1 t2) + = False -- Note [RULE quantification over equalities] + | isHoleCt ct + = False -- Don't quantify over type holes, obviously + | otherwise + = tyCoVarsOfCt ct `disjointVarSet` skol_tvs + + ok_eq t1 t2 + | t1 `tcEqType` t2 = False + | otherwise = is_fun_app t1 || is_fun_app t2 + + is_fun_app ty -- ty is of form (F tys) where F is a type function + = case tyConAppTyCon_maybe ty of + Just tc -> isTypeFamilyTyCon tc + Nothing -> False diff --git a/testsuite/tests/typecheck/should_compile/T14732.hs b/testsuite/tests/typecheck/should_compile/T14732.hs new file mode 100644 index 0000000000..4fa070ed09 --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T14732.hs @@ -0,0 +1,34 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# OPTIONS_GHC -fdefer-type-errors -O #-} +-- Oddly this bug was only triggered with -fdefer-type-errors +-- The -O ensures that the RULE is processed + +module T14732 where + +import Prelude hiding (zip, zipWith) + +zipWith :: (a -> b -> c) + -> Bundle v a + -> Bundle v b + -> Bundle v c +zipWith = undefined + +class GVector (v :: * -> *) a +instance GVector Vector a + +data Bundle (v :: * -> *) a +data Vector a +class Unbox a + +stream :: GVector v a => v a -> Bundle v a +{-# INLINE [1] stream #-} +stream = undefined + +zip :: (Unbox a, Unbox b) => Vector a -> Vector b -> Vector (a, b) +{-# INLINE [1] zip #-} +zip = undefined +{-# RULES "stream/zip [Vector.Unboxed]" forall as bs . + stream (zip as bs) = zipWith (,) (stream as) + (stream bs) #-} diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T index 9e6898190d..795e1730a9 100644 --- a/testsuite/tests/typecheck/should_compile/all.T +++ b/testsuite/tests/typecheck/should_compile/all.T @@ -591,3 +591,4 @@ test('T14488', normal, compile, ['']) test('T14590', normal, compile, ['-fdefer-type-errors -fno-max-valid-substitutions']) test('T13032', normal, compile, ['']) test('T14273', normal, compile, ['-fdefer-type-errors -fno-max-valid-substitutions']) +test('T14732', normal, compile, ['']) -- GitLab