Commit 261dd83c authored by Simon Peyton Jones's avatar Simon Peyton Jones

Fix TcLevel manipulation in TcDerivInfer.simplifyDeriv

The level numbers we were getting simply didn't obey the
invariant (ImplicInv) in TcType
   Note [TcLevel and untouchable type variables]

That leads to chaos. Easy to fix.  I improved the documentation.

I also added an assertion in TcSimplify that checks that
level numbers go up by 1 as we dive inside implications, so
that we catch the problem at source rather than than through
its obscure consequences.

That in turn showed up that TcRules was also generating
constraints that didn't obey (ImplicInv), so I fixed that too.
I have no idea what consequences were lurking behing that
bug, but anyway now it's fixed.  Hooray.
parent e53c113d
......@@ -679,26 +679,34 @@ simplifyDeriv pred tvs thetas
; pure wanteds }
-- See [STEP DAC BUILD]
-- Generate the implication constraints constraints to solve with the
-- skolemized variables
; wanteds <- mapM mk_wanteds thetas
-- Generate the implication constraints, one for each method, to solve
-- with the skolemized variables. Start "one level down" because
-- we are going to wrap the result in an implication with tvs_skols,
-- in step [DAC RESIDUAL]
; (wanteds, tc_lvl) <- pushTcLevelM $
mapM mk_wanteds thetas
; traceTc "simplifyDeriv inputs" $
vcat [ pprTyVars tvs $$ ppr thetas $$ ppr wanteds, doc ]
-- See [STEP DAC SOLVE]
-- Simplify the constraints
; solved_implics <- runTcSDeriveds $ solveWantedsAndDrop
$ unionsWC wanteds
-- Simplify the constraints, starting at the same level at which
-- they are generated (c.f. the call to runTcSWithEvBinds in
-- simplifyInfer)
; solved_wanteds <- setTcLevel tc_lvl $
runTcSDeriveds $
solveWantedsAndDrop $
unionsWC wanteds
-- It's not yet zonked! Obviously zonk it before peering at it
; solved_implics <- zonkWC solved_implics
; solved_wanteds <- zonkWC solved_wanteds
-- See [STEP DAC HOIST]
-- Split the resulting constraints into bad and good constraints,
-- building an @unsolved :: WantedConstraints@ representing all
-- the constraints we can't just shunt to the predicates.
-- See Note [Exotic derived instance contexts]
; let residual_simple = approximateWC True solved_implics
; let residual_simple = approximateWC True solved_wanteds
(bad, good) = partitionBagWith get_good residual_simple
get_good :: Ct -> Either Ct PredType
......@@ -730,10 +738,9 @@ simplifyDeriv pred tvs thetas
-- See [STEP DAC RESIDUAL]
; min_theta_vars <- mapM newEvVar min_theta
; tc_lvl <- getTcLevel
; (leftover_implic, _)
<- buildImplicationFor (pushTcLevel tc_lvl) skol_info tvs_skols
min_theta_vars solved_implics
<- buildImplicationFor tc_lvl skol_info tvs_skols
min_theta_vars solved_wanteds
-- This call to simplifyTop is purely for error reporting
-- See Note [Error reporting for deriving clauses]
-- See also Note [Exotic derived instance contexts], which are caught
......@@ -815,24 +822,28 @@ it would
[STEP DAC BUILD]
So that's what we do. We build the constraint (call it C1)
forall b. Ix b => (Show (Maybe s), Ix cc,
Maybe s -> b -> String
~ Maybe s -> cc -> String)
forall[2] b. Ix b => (Show (Maybe s), Ix cc,
Maybe s -> b -> String
~ Maybe s -> cc -> String)
Here:
* The level of this forall constraint is forall[2], because we are later
going to wrap it in a forall[1] in [STEP DAC RESIDUAL]
Here, the 'b' comes from the quantified type variable in the expected type
of bar (i.e., 'to_anyclass_skols' in 'ThetaOrigin'). The 'cc' is a unification
variable that comes from instantiating the quantified type variable 'c' in
$gdm_bar's type (i.e., 'to_anyclass_metas' in 'ThetaOrigin).
* The 'b' comes from the quantified type variable in the expected type
of bar (i.e., 'to_anyclass_skols' in 'ThetaOrigin'). The 'cc' is a unification
variable that comes from instantiating the quantified type variable 'c' in
$gdm_bar's type (i.e., 'to_anyclass_metas' in 'ThetaOrigin).
The (Ix b) constraint comes from the context of bar's type
(i.e., 'to_wanted_givens' in 'ThetaOrigin'). The (Show (Maybe s)) and (Ix cc)
constraints come from the context of $gdm_bar's type
(i.e., 'to_anyclass_givens' in 'ThetaOrigin').
* The (Ix b) constraint comes from the context of bar's type
(i.e., 'to_wanted_givens' in 'ThetaOrigin'). The (Show (Maybe s)) and (Ix cc)
constraints come from the context of $gdm_bar's type
(i.e., 'to_anyclass_givens' in 'ThetaOrigin').
The equality constraint (Maybe s -> b -> String) ~ (Maybe s -> cc -> String)
comes from marrying up the instantiated type of $gdm_bar with the specified
type of bar. Notice that the type variables from the instance, 's' in this
case, are global to this constraint.
* The equality constraint (Maybe s -> b -> String) ~ (Maybe s -> cc -> String)
comes from marrying up the instantiated type of $gdm_bar with the specified
type of bar. Notice that the type variables from the instance, 's' in this
case, are global to this constraint.
Note that it is vital that we instantiate the `c` in $gdm_bar's type with a new
unification variable for each iteration of simplifyDeriv. If we re-use the same
......@@ -841,8 +852,8 @@ such as Trac #14933.
Similarly for 'baz', givng the constraint C2
forall. Eq (Maybe s) => (Ord a, Show a,
Maybe s -> Maybe s -> Bool
forall[2]. Eq (Maybe s) => (Ord a, Show a,
Maybe s -> Maybe s -> Bool
~ Maybe s -> Maybe s -> Bool)
In this case baz has no local quantification, so the implication
......@@ -853,9 +864,9 @@ variables.
We can combine these two implication constraints into a single
constraint (C1, C2), and simplify, unifying cc:=b, to get:
forall b. Ix b => Show a
forall[2] b. Ix b => Show a
/\
forall. Eq (Maybe s) => (Ord a, Show a)
forall[2]. Eq (Maybe s) => (Ord a, Show a)
[STEP DAC HOIST]
Let's call that (C1', C2'). Now we need to hoist the unsolved
......@@ -874,7 +885,7 @@ And that's what GHC uses for CX.
In this case we have solved all the leftover constraints, but what if
we don't? Simple! We just form the final residual constraint
forall s. CX => (C1',C2')
forall[1] s. CX => (C1',C2')
and simplify that. In simple cases it'll succeed easily, because CX
literally contains the constraints in C1', C2', but if there is anything
......
......@@ -64,35 +64,23 @@ tcRuleDecls (HsRules _ src decls)
tcRuleDecls (XRuleDecls _) = panic "tcRuleDecls"
tcRule :: RuleDecl GhcRn -> TcM (RuleDecl GhcTcId)
tcRule (HsRule (HsRuleRn fv_lhs fv_rhs) name act hs_bndrs lhs rhs)
= addErrCtxt (ruleCtxt $ snd $ unLoc name) $
do { traceTc "---- Rule ------" (pprFullRuleName name)
tcRule (HsRule fvs rname@(L _ (_,name))
act hs_bndrs lhs rhs)
= addErrCtxt (ruleCtxt name) $
do { traceTc "---- Rule ------" (pprFullRuleName rname)
-- Note [Typechecking rules]
; (vars, bndr_wanted) <- captureConstraints $
tcRuleBndrs hs_bndrs
-- bndr_wanted constraints can include wildcard hole
-- constraints, which we should not forget about.
-- It may mention the skolem type variables bound by
-- the RULE. c.f. Trac #10072
; (stuff, tc_lvl) <- pushTcLevelM $
generateRuleConstraints hs_bndrs lhs rhs
; let (id_bndrs, tv_bndrs) = partition isId vars
; (lhs', lhs_wanted, rhs', rhs_wanted, rule_ty)
<- tcExtendTyVarEnv tv_bndrs $
tcExtendIdEnv id_bndrs $
do { -- See Note [Solve order for RULES]
((lhs', rule_ty), lhs_wanted) <- captureConstraints (tcInferRho lhs)
; (rhs', rhs_wanted) <- captureConstraints $
tcMonoExpr rhs (mkCheckExpType rule_ty)
; return (lhs', lhs_wanted, rhs', rhs_wanted, rule_ty) }
; let ( id_bndrs, lhs', lhs_wanted, rhs', rhs_wanted, rule_ty) = stuff
; traceTc "tcRule 1" (vcat [ pprFullRuleName name
; traceTc "tcRule 1" (vcat [ pprFullRuleName rname
, ppr lhs_wanted
, ppr rhs_wanted ])
; let all_lhs_wanted = bndr_wanted `andWC` lhs_wanted
; (lhs_evs, residual_lhs_wanted) <- simplifyRule (snd $ unLoc name)
all_lhs_wanted
rhs_wanted
; (lhs_evs, residual_lhs_wanted)
<- simplifyRule name tc_lvl lhs_wanted rhs_wanted
-- SimplfyRule Plan, step 4
-- Now figure out what to quantify over
......@@ -113,7 +101,7 @@ tcRule (HsRule (HsRuleRn fv_lhs fv_rhs) name act hs_bndrs lhs rhs)
; gbls <- tcGetGlobalTyCoVars -- Even though top level, there might be top-level
-- monomorphic bindings from the MR; test tc111
; qtkvs <- quantifyTyVars gbls forall_tkvs
; traceTc "tcRule" (vcat [ pprFullRuleName name
; traceTc "tcRule" (vcat [ pprFullRuleName rname
, ppr forall_tkvs
, ppr qtkvs
, ppr rule_ty
......@@ -125,19 +113,44 @@ tcRule (HsRule (HsRuleRn fv_lhs fv_rhs) name act hs_bndrs lhs rhs)
-- For the LHS constraints we must solve the remaining constraints
-- (a) so that we report insoluble ones
-- (b) so that we bind any soluble ones
; let skol_info = RuleSkol (snd (unLoc name))
; (lhs_implic, lhs_binds) <- buildImplicationFor topTcLevel skol_info qtkvs
; let skol_info = RuleSkol name
; (lhs_implic, lhs_binds) <- buildImplicationFor tc_lvl skol_info qtkvs
lhs_evs residual_lhs_wanted
; (rhs_implic, rhs_binds) <- buildImplicationFor topTcLevel skol_info qtkvs
; (rhs_implic, rhs_binds) <- buildImplicationFor tc_lvl skol_info qtkvs
lhs_evs rhs_wanted
; emitImplications (lhs_implic `unionBags` rhs_implic)
; return (HsRule (HsRuleRn fv_lhs fv_rhs)name act
; return (HsRule fvs rname act
(map (noLoc . RuleBndr noExt . noLoc) (qtkvs ++ tpl_ids))
(mkHsDictLet lhs_binds lhs')
(mkHsDictLet rhs_binds rhs')) }
tcRule (XRuleDecl _) = panic "tcRule"
generateRuleConstraints :: [LRuleBndr GhcRn] -> LHsExpr GhcRn -> LHsExpr GhcRn
-> TcM ( [TcId]
, LHsExpr GhcTc, WantedConstraints
, LHsExpr GhcTc, WantedConstraints
, TcType )
generateRuleConstraints hs_bndrs lhs rhs
= do { (vars, bndr_wanted) <- captureConstraints $
tcRuleBndrs hs_bndrs
-- bndr_wanted constraints can include wildcard hole
-- constraints, which we should not forget about.
-- It may mention the skolem type variables bound by
-- the RULE. c.f. Trac #10072
; let (id_bndrs, tv_bndrs) = partition isId vars
; tcExtendTyVarEnv tv_bndrs $
tcExtendIdEnv id_bndrs $
do { -- See Note [Solve order for RULES]
((lhs', rule_ty), lhs_wanted) <- captureConstraints (tcInferRho lhs)
; (rhs', rhs_wanted) <- captureConstraints $
tcMonoExpr rhs (mkCheckExpType rule_ty)
; let all_lhs_wanted = bndr_wanted `andWC` lhs_wanted
; return (id_bndrs, lhs', all_lhs_wanted, rhs', rhs_wanted, rule_ty) } }
-- Slightly curious that tv_bndrs is not returned
tcRuleBndrs :: [LRuleBndr GhcRn] -> TcM [Var]
tcRuleBndrs []
= return []
......@@ -307,6 +320,7 @@ terrible, so we avoid the problem by cloning the constraints.
-}
simplifyRule :: RuleName
-> TcLevel -- Level at which to solve the constraints
-> WantedConstraints -- Constraints from LHS
-> WantedConstraints -- Constraints from RHS
-> TcM ( [EvVar] -- Quantify over these LHS vars
......@@ -314,7 +328,7 @@ simplifyRule :: RuleName
-- See Note [The SimplifyRule Plan]
-- NB: This consumes all simple constraints on the LHS, but not
-- any LHS implication constraints.
simplifyRule name lhs_wanted rhs_wanted
simplifyRule name tc_lvl lhs_wanted rhs_wanted
= do {
-- Note [The SimplifyRule Plan] step 1
-- First solve the LHS and *then* solve the RHS
......@@ -322,12 +336,13 @@ simplifyRule name lhs_wanted rhs_wanted
-- 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
; setTcLevel tc_lvl $
runTcSDeriveds $
do { _ <- solveWanteds lhs_clone
; _ <- solveWanteds rhs_clone
-- Why do them separately?
-- See Note [Solve order for RULES]
; return () }
; return () }
-- Note [The SimplifyRule Plan] step 2
; lhs_wanted <- zonkWC lhs_wanted
......
......@@ -1495,6 +1495,8 @@ solveImplication imp@(Implic { ic_tclvl = tclvl
= do { inerts <- getTcSInerts
; traceTcS "solveImplication {" (ppr imp $$ text "Inerts" <+> ppr inerts)
; when debugIsOn check_tc_level
-- Solve the nested constraints
; (no_given_eqs, given_insols, residual_wanted)
<- nestImplicTcS ev_binds_var tclvl $
......@@ -1538,6 +1540,15 @@ solveImplication imp@(Implic { ic_tclvl = tclvl
; return (floated_eqs, res_implic) }
where
-- TcLevels must be strictly increasing (see (ImplicInv) in
-- Note [TcLevel and untouchable type variables] in TcType),
-- and in fact I thinkthey should always increase one level at a time.
check_tc_level = do { cur_lvl <- TcS.getTcLevel
; MASSERT2( tclvl == pushTcLevel cur_lvl
, text "Cur lvl =" <+> ppr cur_lvl $$
text "Imp lvl =" <+> ppr tclvl ) }
----------------------
setImplicationStatus :: Implication -> TcS (Maybe Implication)
-- Finalise the implication returned from solveImplication:
......
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module T15290b where
import Data.Coerce
import Data.Kind
type Representational1 m = (forall a b. Coercible a b => Coercible (m a) (m b) :: Constraint)
class Representational1 f => Functor' f where
fmap' :: (a -> b) -> f a -> f b
class Functor' f => Applicative' f where
pure' :: a -> f a
(<*>@) :: f (a -> b) -> f a -> f b
class Functor' t => Traversable' t where
traverse' :: Applicative' f => (a -> f b) -> t a -> f (t b)
-- Typechecks
newtype T1 m a = MkT1 (m a) deriving (Functor', Traversable')
T15290b.hs:28:49: error:
• Couldn't match representation of type ‘f (m b)’
with that of ‘f (T1 m b)’
arising from the coercion of the method ‘traverse'’
from type ‘forall (f :: * -> *) a b.
Applicative' f =>
(a -> f b) -> m a -> f (m b)’
to type ‘forall (f :: * -> *) a b.
Applicative' f =>
(a -> f b) -> T1 m a -> f (T1 m b)’
NB: We cannot know what roles the parameters to ‘f’ have;
we must assume that the role is nominal
• When deriving the instance for (Traversable' (T1 m))
......@@ -13,3 +13,4 @@ test('T15231', normal, compile_fail, [''])
test('T15290', normal, compile, [''])
test('T15290a', normal, compile_fail, [''])
test('T15290b', normal, compile_fail, [''])
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