Fix a nasty superclass expansion bug
authorSimon Peyton Jones <simonpj@microsoft.com>
Mon, 8 Feb 2016 14:41:08 +0000 (14:41 +0000)
committerSimon Peyton Jones <simonpj@microsoft.com>
Mon, 8 Feb 2016 15:08:54 +0000 (15:08 +0000)
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.

compiler/typecheck/TcRnTypes.hs
compiler/typecheck/TcSMonad.hs
testsuite/tests/polykinds/T11523.hs [new file with mode: 0644]
testsuite/tests/polykinds/all.T
testsuite/tests/typecheck/should_fail/T5853.stderr

index 0474f74..7d7f265 100644 (file)
@@ -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
index edcedf7..9cb2b9b 100644 (file)
@@ -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]
     }
 
 ---------------
diff --git a/testsuite/tests/polykinds/T11523.hs b/testsuite/tests/polykinds/T11523.hs
new file mode 100644 (file)
index 0000000..0313b0c
--- /dev/null
@@ -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)
+-}
index 5fc689d..9fc15d5 100644 (file)
@@ -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, [''])
index ab2ad30..d9a8244 100644 (file)
@@ -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: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)