Commit 43e02d12 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Fix a nasty superclass expansion bug

This patch fixes Trac #11523.

* The basic problem was that TcRnTypes.superClassesMightHelp was
  returning True of a Derived constraint, and that led to us
  expanding Given superclasses, which produced the same Derived
  constraint again, and so on infinitely.  We really want to do
  this only if there are unsolve /Wanted/ contraints!

* On the way I made TcSMonad.getUnsolvedInerts a bit more
  discriminating about which Derived equalities it returns;
  see Note [Unsolved Derived equalities] in TcSMonad

* Lots of new comments in TcSMonad.
parent 6252b70a
......@@ -1793,11 +1793,10 @@ superClassesMightHelp :: Ct -> Bool
-- expose more equalities or functional dependencies) might help to
-- solve this constraint. See Note [When superclases help]
superClassesMightHelp ct
| CDictCan { cc_class = cls } <- ct
, cls `hasKey` ipClassKey
= False
| otherwise
= True
= isWantedCt ct && not (is_ip ct)
where
is_ip (CDictCan { cc_class = cls }) = isIPClass cls
is_ip _ = False
{- Note [When superclasses help]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......@@ -1805,26 +1804,35 @@ First read Note [The superclass story] in TcCanonical.
We expand superclasses and iterate only if there is at unsolved wanted
for which expansion of superclasses (e.g. from given constraints)
might actually help. Usually the answer is "yes" but for implicit
paramters it is "no". If we have [W] ?x::ty, expanding superclasses
won't help:
- Superclasses can't be implicit parameters
- If we have a [G] ?x:ty2, then we'll have another unsolved
[D] ty ~ ty2 (from the functional dependency)
which will trigger superclass expansion.
It's a bit of a special case, but it's easy to do. The runtime cost
is low because the unsolved set is usually empty anyway (errors
aside), and the first non-imlicit-parameter will terminate the search.
The special case is worth it (Trac #11480, comment:2) because it
applies to CallStack constraints, which aren't type errors. If we have
f :: (C a) => blah
f x = ...undefined...
we'll get a CallStack constraint. If that's the only unsolved constraint
it'll eventually be solved by defaulting. So we don't want to emit warnings
about hitting the simplifier's iteration limit. A CallStack constraint
really isn't an unsolved constraint; it can always be solved by defaulting.
might actually help. The function superClassesMightHelp tells if
doing this superclass expansion might help solve this constraint.
Note that
* Superclasses help only for Wanted constraints. Derived constraints
are not really "unsolved" and we certainly don't want them to
trigger superclass expansion. This was a good part of the loop
in Trac #11523
* Even for Wanted constraints, we say "no" for implicit paramters.
we have [W] ?x::ty, expanding superclasses won't help:
- Superclasses can't be implicit parameters
- If we have a [G] ?x:ty2, then we'll have another unsolved
[D] ty ~ ty2 (from the functional dependency)
which will trigger superclass expansion.
It's a bit of a special case, but it's easy to do. The runtime cost
is low because the unsolved set is usually empty anyway (errors
aside), and the first non-imlicit-parameter will terminate the search.
The special case is worth it (Trac #11480, comment:2) because it
applies to CallStack constraints, which aren't type errors. If we have
f :: (C a) => blah
f x = ...undefined...
we'll get a CallStack constraint. If that's the only unsolved
constraint it'll eventually be solved by defaulting. So we don't
want to emit warnings about hitting the simplifier's iteration
limit. A CallStack constraint really isn't an unsolved
constraint; it can always be solved by defaulting.
-}
singleCt :: Ct -> Cts
......
......@@ -554,8 +554,10 @@ Result
data InertCans -- See Note [Detailed InertCans Invariants] for more
= IC { inert_model :: InertModel
-- See Note [inert_model: the inert model]
, inert_eqs :: TyVarEnv EqualCtList
-- See Note [inert_eqs: the inert equalities]
-- All Given/Wanted CTyEqCans; index is the LHS tyvar
, inert_funeqs :: FunEqMap Ct
......@@ -664,6 +666,10 @@ Note [inert_model: the inert model]
- A Derived "shadow copy" for every Given or Wanted (a ~N ty) in
inert_eqs.
* The model is not subject to "kicking-out". Reason: we make a Derived
shadow copy of any Given/Wanted (a ~ ty), and that Derived copy will
be fully rewritten by the model before it is added
* The principal reason for maintaining the model is to generate
equalities that tell us how to unify a variable: that is, what
Mark Jones calls "improvement". The same idea is sometimes also
......@@ -1101,33 +1107,39 @@ Note [Adding an inert canonical constraint the InertCans]
* Adding a *nominal* CTyEqCan (a ~N ty) to the inert set (TcSMonad.addInertEq).
* Always (G/W/D) kick out constraints that can be rewritten
(respecting flavours) by the new constraint. This is done
by kickOutRewritable.
(A) Always (G/W/D) kick out constraints that can be rewritten
(respecting flavours) by the new constraint. This is done
by kickOutRewritable.
(B) Applies only to nominal equalities: a ~ ty. Four cases:
Then, when adding:
[Representational] [G/W/D] a ~R ty:
Just add it to inert_eqs
* [Derived] a ~N ty
1. Add (a~ty) to the model
NB: 'a' cannot be in fv(ty), because the constraint is canonical.
[Derived Nominal] [D] a ~N ty:
1. Add (a~ty) to the model
NB: 'a' cannot be in fv(ty), because the constraint is canonical.
2. (DShadow) Do emitDerivedShadows
For every inert G/W constraint c, st
(a) (a~ty) can rewrite c (see Note [Emitting shadow constraints]),
and
(b) the model cannot rewrite c
kick out a Derived *copy*, leaving the original unchanged.
Reason for (b) if the model can rewrite c, then we have already
generated a shadow copy
2. (DShadow) Do emitDerivedShadows
For every inert G/W constraint c, st
(a) (a~ty) can rewrite c (see Note [Emitting shadow constraints]),
and
(b) the model cannot rewrite c
kick out a Derived *copy*, leaving the original unchanged.
Reason for (b) if the model can rewrite c, then we have already
generated a shadow copy
* [Given/Wanted] a ~N ty
[Given/Wanted Nominal] [G/W] a ~N ty:
1. Add it to inert_eqs
2. Emit [D] a~ty
As a result of (2), the current model will rewrite the new [D] a~ty
during canonicalisation, and then it'll be added to the model using
the steps of [Derived] above.
Step (2) is needed to allow the current model to fully
rewrite [D] a~ty before adding it using the [Derived Nominal]
steps above.
* [Representational equalities] a ~R ty: just add it to inert_eqs
We must do this even for Givens, because
work-item [G] a ~ [b], model has [D] b ~ a.
We need a shadow [D] a ~ [b] in the work-list
When we process it, we'll rewrite to a ~ [a] and get an occurs check
* Unifying a:=ty, is like adding [G] a~ty, but we can't make a [D]
......@@ -1207,21 +1219,11 @@ add_inert_eq ics@(IC { inert_count = n
| ReprEq <- eq_rel
= return new_ics
-- | isGiven ev
-- = return (new_ics { inert_model = extendVarEnv old_model tv ct }) }
-- No no! E.g.
-- work-item [G] a ~ [b], model has [D] b ~ a.
-- We must not add the given to the model as-is. Instead,
-- we put a shadow [D] a ~ [b] in the work-list
-- When we process it, we'll rewrite to a ~ [a] and get an occurs check
| isDerived ev
= do { emitDerivedShadows ics tv
; return (ics { inert_model = extendVarEnv old_model tv ct }) }
-- Nominal equality (tv ~N ty), Given/Wanted
-- See Note [Emitting shadow constraints]
| otherwise -- modelCanRewrite old_model rw_tvs -- Shadow of new ct isn't inert; emit it
| otherwise -- Given/Wanted Nominal equality [W] tv ~N ty
= do { emitNewDerived loc pred
; return new_ics }
where
......@@ -1722,8 +1724,10 @@ getUnsolvedInerts
, inert_dicts = idicts
, inert_insols = insols
, inert_model = model } <- getInertCans
; keep_derived <- keepSolvingDeriveds
; let der_tv_eqs = foldVarEnv (add_der tv_eqs) emptyCts model -- Want to float these
; let der_tv_eqs = foldVarEnv (add_der_eq keep_derived tv_eqs)
emptyCts model
unsolved_tv_eqs = foldTyEqs add_if_unsolved tv_eqs der_tv_eqs
unsolved_fun_eqs = foldFunEqs add_if_unsolved fun_eqs emptyCts
unsolved_irreds = Bag.filterBag is_unsolved irreds
......@@ -1743,8 +1747,10 @@ getUnsolvedInerts
-- Keep even the given insolubles
-- so that we can report dead GADT pattern match branches
where
add_der tv_eqs ct cts
add_der_eq keep_derived tv_eqs ct cts
-- See Note [Unsolved Derived equalities]
| CTyEqCan { cc_tyvar = tv, cc_rhs = rhs } <- ct
, isMetaTyVar tv || keep_derived
, not (isInInertEqs tv_eqs tv rhs) = ct `consBag` cts
| otherwise = cts
add_if_unsolved :: Ct -> Cts -> Cts
......@@ -1856,7 +1862,20 @@ prohibitedSuperClassSolve from_loc solve_loc
| otherwise
= False
{-
{- Note [Unsolved Derived equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In getUnsolvedInerts, we return a derived equality from the model
for two possible reasons:
* Because it is a candidate for floating out of this implication.
We only float equalities with a meta-tyvar on the left, so we only
pull those out here.
* If we are only solving derived constraints (i.e. tcs_need_derived
is true; see Note [Solving for Derived constraints]), then we
those Derived constraints are effectively unsolved, and we need
them!
Note [When does an implication have given equalities?]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider an implication
......@@ -2252,6 +2271,16 @@ All you can do is
Filling in a dictionary evidence variable means to create a binding
for it, so TcS carries a mutable location where the binding can be
added. This is initialised from the innermost implication constraint.
Note [Solving for Derived constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Sometimes we invoke the solver on a bunch of Derived constraints, not to
generate any evidence, but just to cause unification side effects or to
produce a simpler set of constraints. If that is what we are doing, we
should do two things differently:
a) Don't stop when you've solved all the Wanteds; instead keep going
if there are any Deriveds in the work queue.
b) In getInertUnsolved, include Derived ones
-}
data TcSEnv
......@@ -2277,9 +2306,8 @@ data TcSEnv
-- See also Note [Tracking redundant constraints] in TcSimplify
tcs_need_deriveds :: Bool
-- should we keep trying to solve even if all the unsolved
-- constraints are Derived? Usually False, but used whenever
-- toDerivedWC is used.
-- Keep solving, even if all the unsolved constraints are Derived
-- See Note [Solving for Derived constraints]
}
---------------
......
{-# language KindSignatures #-}
{-# language PolyKinds #-}
{-# language DataKinds #-}
{-# language TypeFamilies #-}
{-# language RankNTypes #-}
{-# language NoImplicitPrelude #-}
{-# language FlexibleContexts #-}
{-# language MultiParamTypeClasses #-}
{-# language GADTs #-}
{-# language ConstraintKinds #-}
{-# language FlexibleInstances #-}
{-# language TypeOperators #-}
{-# language ScopedTypeVariables #-}
{-# language DefaultSignatures #-}
{-# language FunctionalDependencies #-}
{-# language UndecidableSuperClasses #-}
{-# language UndecidableInstances #-}
{-# language TypeInType #-}
module T11523 where
import GHC.Types (Constraint, Type)
import qualified Prelude
type Cat i = i -> i -> Type
newtype Y (p :: i -> j -> Type) (a :: j) (b :: i) = Y { getY :: p b a }
class Vacuous (a :: i)
instance Vacuous a
class (Functor p, Dom p ~ Op p, Cod p ~ Nat p (->)) => Category (p :: Cat i) where
type Op p :: Cat i
type Op p = Y p
type Ob p :: i -> Constraint
type Ob p = Vacuous
class (Category (Dom f), Category (Cod f)) => Functor (f :: i -> j) where
type Dom f :: Cat i
type Cod f :: Cat j
class (Functor f, Dom f ~ p, Cod f ~ q) => Fun (p :: Cat i) (q :: Cat j) (f :: i -> j) | f -> p q
instance (Functor f, Dom f ~ p, Cod f ~ q) => Fun (p :: Cat i) (q :: Cat j) (f :: i -> j)
data Nat (p :: Cat i) (q :: Cat j) (f :: i -> j) (g :: i -> j)
instance (Category p, Category q) => Category (Nat p q) where
type Ob (Nat p q) = Fun p q
instance (Category p, Category q) => Functor (Nat p q) where
type Dom (Nat p q) = Y (Nat p q)
type Cod (Nat p q) = Nat (Nat p q) (->)
instance (Category p, Category q) => Functor (Nat p q f) where
type Dom (Nat p q f) = Nat p q
type Cod (Nat p q f) = (->)
instance Category (->)
instance Functor ((->) e) where
type Dom ((->) e) = (->)
type Cod ((->) e) = (->)
instance Functor (->) where
type Dom (->) = Y (->)
type Cod (->) = Nat (->) (->)
instance (Category p, Op p ~ Y p) => Category (Y p) where
type Op (Y p) = p
instance (Category p, Op p ~ Y p) => Functor (Y p a) where
type Dom (Y p a) = Y p
type Cod (Y p a) = (->)
instance (Category p, Op p ~ Y p) => Functor (Y p) where
type Dom (Y p) = p
type Cod (Y p) = Nat (Y p) (->)
{-
Given: Category p, Op p ~ Y p
--> Category p, Op p ~ Y p
Functor p, Dom p ~ Op p, Cod p ~ Nat p (->)
--> Category p, Op p ~ Y p
Functor p, Dom p ~ Op p, Cod p ~ Nat p (->)
Category (Dom p), Category (Cod p)
-}
......@@ -136,3 +136,4 @@ test('T11459', normal, compile_fail, [''])
test('T11466', normal, compile_fail, [''])
test('T11480a', normal, compile, [''])
test('T11480b', normal, compile, [''])
test('T11523', normal, compile, [''])
T5853.hs:15:46: error:
• Could not deduce: Subst t2 (Elem t1) ~ t1
• Could not deduce: Subst t1 (Elem t2) ~ t2
arising from a use of ‘<$>’
from the context: (F t,
Elem t ~ Elem t,
Elem t1 ~ Elem t1,
Subst t (Elem t1) ~ t1,
Subst t1 (Elem t) ~ t,
F t2,
Elem t2 ~ Elem t2,
Elem t ~ Elem t,
Subst t (Elem t2) ~ t2,
Subst t2 (Elem t) ~ t,
Subst t (Elem t2) ~ t2)
F t1,
Elem t1 ~ Elem t1,
Elem t ~ Elem t,
Subst t1 (Elem t) ~ t,
Subst t (Elem t1) ~ t1)
bound by the RULE "map/map" at T5853.hs:15:2-57
‘t1’ is a rigid type variable bound by
‘t2’ is a rigid type variable bound by
the RULE "map/map" at T5853.hs:15:2
• In the expression: (f . g) <$> xs
When checking the transformation rule "map/map"
• Relevant bindings include
f :: Elem t -> Elem t1 (bound at T5853.hs:15:19)
g :: Elem t2 -> Elem t (bound at T5853.hs:15:21)
xs :: t2 (bound at T5853.hs:15:23)
f :: Elem t -> Elem t2 (bound at T5853.hs:15:19)
g :: Elem t1 -> Elem t (bound at T5853.hs:15:21)
xs :: t1 (bound at T5853.hs:15:23)
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