From: Simon Peyton Jones
Date: Mon, 8 Feb 2016 14:41:08 +0000 (+0000)
Subject: Fix a nasty superclass expansion bug
XGitTag: ghc8.3start~2471
XGitUrl: https://git.haskell.org/ghc.git/commitdiff_plain/43e02d1270701a1043be67f078cf2b1a85047feb
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.

diff git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index 0474f74..7d7f265 100644
 a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ 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 nonimlicitparameter 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 nonimlicitparameter 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
diff git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index edcedf7..9cb2b9b 100644
 a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ 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 "kickingout". 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
+ workitem [G] a ~ [b], model has [D] b ~ a.
+ We need a shadow [D] a ~ [b] in the worklist
+ 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.
 workitem [G] a ~ [b], model has [D] b ~ a.
 We must not add the given to the model asis. Instead,
 we put a shadow [D] a ~ [b] in the worklist
 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 metatyvar 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]
}

diff git a/testsuite/tests/polykinds/T11523.hs b/testsuite/tests/polykinds/T11523.hs
new file mode 100644
index 0000000..0313b0c
 /dev/null
+++ b/testsuite/tests/polykinds/T11523.hs
@@ 0,0 +1,89 @@
+{# 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)
+}
diff git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 5fc689d..9fc15d5 100644
 a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ 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, [''])
diff git a/testsuite/tests/typecheck/should_fail/T5853.stderr b/testsuite/tests/typecheck/should_fail/T5853.stderr
index ab2ad30..d9a8244 100644
 a/testsuite/tests/typecheck/should_fail/T5853.stderr
+++ b/testsuite/tests/typecheck/should_fail/T5853.stderr
@@ 1,23 +1,23 @@
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:257
 â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)