Commit d3573e4a authored by Simon Peyton Jones's avatar Simon Peyton Jones Committed by Ben Gamari

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.

(cherry picked from commit e9ae0cae)
parent 77cdf60c
......@@ -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
{-# 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) #-}
......@@ -590,3 +590,4 @@ test('T14488', normal, compile, [''])
test('T13032', normal, compile, [''])
test('T14590', normal, compile, ['-fdefer-type-errors -fno-max-valid-substitutions'])
test('T14273', normal, compile, ['-fdefer-type-errors -fno-max-valid-substitutions'])
test('T14732', normal, compile, [''])
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