Commit e9ae0cae authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

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.
parent efba0546
......@@ -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) #-}
......@@ -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, [''])
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