Expand given superclasses more eagerly
authorSimon Peyton Jones <simonpj@microsoft.com>
Wed, 22 Jun 2016 13:17:58 +0000 (14:17 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Wed, 22 Jun 2016 21:21:15 +0000 (22:21 +0100)
This patch fixes Trac #12175, another delicate corner case of
Note [Instance and Given overlap] in TcInteract.

In #12175 we were not expanding given superclasses eagerly
enough. It was easy to fix, and is actually rather neater than
before.

See Note [Eagerly expand given superclasses] in TcCanonical.
The main change is to move the eager expansion of given superclasses
to canClassNC.

compiler/typecheck/TcCanonical.hs
compiler/typecheck/TcInteract.hs
compiler/typecheck/TcRnTypes.hs
compiler/typecheck/TcSMonad.hs
compiler/typecheck/TcSimplify.hs
testsuite/tests/indexed-types/should_compile/T12175.hs [new file with mode: 0644]
testsuite/tests/indexed-types/should_compile/all.T

index 256cf94..927832e 100644 (file)
@@ -3,7 +3,7 @@
 module TcCanonical(
      canonicalize,
      unifyDerived,
-     makeSuperClasses, mkGivensWithSuperClasses,
+     makeSuperClasses,
      StopOrContinue(..), stopWith, continueWith
   ) where
 
@@ -185,12 +185,23 @@ canEvNC ev
 -}
 
 canClassNC :: CtEvidence -> Class -> [Type] -> TcS (StopOrContinue Ct)
+-- "NC" means "non-canonical"; that is, we have got here
+-- from a NonCanonical constrataint, not from a CDictCan
 -- Precondition: EvVar is class evidence
-canClassNC ev cls tys = canClass ev cls tys (has_scs cls)
+canClassNC ev cls tys
+  | isGiven ev  -- See Note [Eagerly expand given superclasses]
+  = do { sc_cts <- mkStrictSuperClasses ev cls tys
+       ; emitWork sc_cts
+       ; canClass ev cls tys False }
+  | otherwise
+  = canClass ev cls tys (has_scs cls)
   where
     has_scs cls = not (null (classSCTheta cls))
 
-canClass :: CtEvidence -> Class -> [Type] -> Bool -> TcS (StopOrContinue Ct)
+canClass :: CtEvidence
+         -> Class -> [Type]
+         -> Bool            -- True <=> un-explored superclasses
+         -> TcS (StopOrContinue Ct)
 -- Precondition: EvVar is class evidence
 
 canClass ev cls tys pend_sc
@@ -249,15 +260,24 @@ Givens and Wanteds. But:
 
 So here's the plan:
 
-1. Generate superclasses for given (but not wanted) constraints;
-   see Note [Aggressively expand given superclasses].  However
-   stop if you encounter the same class twice.  That is, expand
-   eagerly, but have a conservative termination condition: see
+1. Eagerly generate superclasses for given (but not wanted)
+   constraints; see Note [Eagerly expand given superclasses].
+   This is done in canClassNC, when we take a non-canonical constraint
+   and cannonicalise it.
+
+   However stop if you encounter the same class twice.  That is,
+   expand eagerly, but have a conservative termination condition: see
    Note [Expanding superclasses] in TcType.
 
-2. Solve the wanteds as usual, but do /no/ expansion of superclasses
-   in solveSimpleGivens or solveSimpleWanteds.
-   See Note [Danger of adding superclasses during solving]
+2. Solve the wanteds as usual, but do no further expansion of
+   superclasses for canonical CDictCans in solveSimpleGivens or
+   solveSimpleWanteds; Note [Danger of adding superclasses during solving]
+
+   However, /do/ continue to eagerly expand superlasses for /given/
+   non-canonical constraints (canClassNC does this).  As Trac #12175
+   showed, a type-family application can expand to a class constraint,
+   and we want to see its superclasses for just the same reason as
+   Note [Eagerly expand given superclasses].
 
 3. If we have any remaining unsolved wanteds
         (see Note [When superclasses help] in TcRnTypes)
@@ -278,11 +298,11 @@ isPendingScDict holds).
 When we take a CNonCanonical or CIrredCan, but end up classifying it
 as a CDictCan, we set the cc_pend_sc flag to False.
 
-Note [Aggressively expand given superclasses]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-In step (1) of Note [The superclass story], why do we aggressively
-expand Given superclasses by one layer?  Mainly because of some very
-obscure cases like this:
+Note [Eagerly expand given superclasses]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In step (1) of Note [The superclass story], why do we eagerly expand
+Given superclasses by one layer?  Mainly because of some very obscure
+cases like this:
 
    instance Bad a => Eq (T a)
 
@@ -294,6 +314,19 @@ instance declaration; but then we are stuck with (Bad a).  Sigh.
 This is really a case of non-confluent proofs, but to stop our users
 complaining we expand one layer in advance.
 
+Note [Instance and Given overlap] in TcInteract.
+
+We also want to do this if we have
+
+   f :: F (T a) => blah
+
+where
+   type instance F (T a) = Ord (T a)
+
+So we may need to do a little work on the givens to expose the
+class that has the superclasses.  That's why the superclass
+expansion for Givens happens in canClassNC.
+
 Note [Why adding superclasses can help]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Examples of how adding superclasses can help:
@@ -361,23 +394,6 @@ Mind you, now that Wanteds cannot rewrite Derived, I think this particular
 situation can't happen.
   -}
 
-mkGivensWithSuperClasses :: CtLoc -> [EvId] -> TcS [Ct]
--- From a given EvId, make its Ct, plus the Ct's of its superclasses
--- See Note [The superclass story]
--- The loop-breaking here follows Note [Expanding superclasses] in TcType
---
--- Example:  class D a => C a
---           class C [a] => D a
--- makeGivensWithSuperClasses (C x) will return (C x, D x, C[x])
---   i.e. up to and including the first repetition of C
-mkGivensWithSuperClasses loc ev_ids = concatMapM go ev_ids
-  where
-    go ev_id = mk_superclasses emptyNameSet this_ev
-       where
-         this_ev = CtGiven { ctev_evar = ev_id
-                           , ctev_pred = evVarPred ev_id
-                           , ctev_loc = loc }
-
 makeSuperClasses :: [Ct] -> TcS [Ct]
 -- Returns strict superclasses, transitively, see Note [The superclasses story]
 -- See Note [The superclass story]
@@ -395,9 +411,14 @@ makeSuperClasses :: [Ct] -> TcS [Ct]
 makeSuperClasses cts = concatMapM go cts
   where
     go (CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys })
-          = mk_strict_superclasses (unitNameSet (className cls)) ev cls tys
+          = mkStrictSuperClasses ev cls tys
     go ct = pprPanic "makeSuperClasses" (ppr ct)
 
+mkStrictSuperClasses :: CtEvidence -> Class -> [Type] -> TcS [Ct]
+-- Return constraints for the strict superclasses of (c tys)
+mkStrictSuperClasses ev cls tys
+  = mk_strict_superclasses (unitNameSet (className cls)) ev cls tys
+
 mk_superclasses :: NameSet -> CtEvidence -> TcS [Ct]
 -- Return this constraint, plus its superclasses, if any
 mk_superclasses rec_clss ev
index a9f7bc6..452db5f 100644 (file)
@@ -1819,8 +1819,8 @@ Example, from the OutsideIn(X) paper:
        g :: forall a. Q [a] => [a] -> Int
        g x = wob x
 
-This will generate the impliation constraint:
-            Q [a] => (Q [beta], R beta [a])
+From 'g' we get the impliation constraint:
+            forall a. Q [a] => (Q [beta], R beta [a])
 If we react (Q [beta]) with its top-level axiom, we end up with a
 (P beta), which we have no way of discharging. On the other hand,
 if we react R beta [a] with the top-level we get  (beta ~ a), which
@@ -1833,7 +1833,8 @@ The partial solution is that:
   unifiable to this particular dictionary.
 
   We treat any meta-tyvar as "unifiable" for this purpose,
-  *including* untouchable ones
+  *including* untouchable ones.  But not skolems like 'a' in
+  the implication constraint above.
 
 The end effect is that, much as we do for overlapping instances, we
 delay choosing a class instance if there is a possibility of another
@@ -1877,7 +1878,8 @@ Other notes:
   and suppose we have -XNoMonoLocalBinds, so that we attempt to find the most
   general type for 'v'.  When generalising v's type we'll simplify its
   Q [alpha] constraint, but we don't have Q [a] in the 'givens', so we
-  will use the instance declaration after all. Trac #11948 was a case in point
+  will use the instance declaration after all. Trac #11948 was a case
+  in point.
 
 All of this is disgustingly delicate, so to discourage people from writing
 simplifiable class givens, we warn about signatures that contain them;#
index e007777..5494a07 100644 (file)
@@ -73,7 +73,7 @@ module TcRnTypes(
         isUserTypeErrorCt, getUserTypeErrorMsg,
         ctEvidence, ctLoc, setCtLoc, ctPred, ctFlavour, ctEqRel, ctOrigin,
         mkTcEqPredLikeEv,
-        mkNonCanonical, mkNonCanonicalCt,
+        mkNonCanonical, mkNonCanonicalCt, mkGivens,
         ctEvPred, ctEvLoc, ctEvOrigin, ctEvEqRel,
         ctEvTerm, ctEvCoercion, ctEvId,
         tyCoVarsOfCt, tyCoVarsOfCts,
@@ -1498,6 +1498,14 @@ mkNonCanonical ev = CNonCanonical { cc_ev = ev }
 mkNonCanonicalCt :: Ct -> Ct
 mkNonCanonicalCt ct = CNonCanonical { cc_ev = cc_ev ct }
 
+mkGivens :: CtLoc -> [EvId] -> [Ct]
+mkGivens loc ev_ids
+  = map mk ev_ids
+  where
+    mk ev_id = mkNonCanonical (CtGiven { ctev_evar = ev_id
+                                       , ctev_pred = evVarPred ev_id
+                                       , ctev_loc = loc })
+
 ctEvidence :: Ct -> CtEvidence
 ctEvidence = cc_ev
 
index fda039b..ea1220e 100644 (file)
@@ -55,7 +55,7 @@ module TcSMonad (
     getUnsolvedInerts,
     removeInertCts, getPendingScDicts,
     addInertCan, addInertEq, insertFunEq,
-    emitInsoluble, emitWorkNC,
+    emitInsoluble, emitWorkNC, emitWork,
 
     -- The Model
     InertModel, kickOutAfterUnification,
index 4b69749..f9a30c2 100644 (file)
@@ -30,7 +30,7 @@ import PrelNames
 import TcErrors
 import TcEvidence
 import TcInteract
-import TcCanonical   ( makeSuperClasses, mkGivensWithSuperClasses )
+import TcCanonical   ( makeSuperClasses )
 import TcMType   as TcM
 import TcRnMonad as TcM
 import TcSMonad  as TcS
@@ -446,7 +446,7 @@ tcCheckSatisfiability given_ids
        ; let given_loc = mkGivenLoc topTcLevel UnkSkol lcl_env
        ; (res, _ev_binds) <- runTcS $
              do { traceTcS "checkSatisfiability {" (ppr given_ids)
-                ; given_cts <- mkGivensWithSuperClasses given_loc (bagToList given_ids)
+                ; let given_cts = mkGivens given_loc (bagToList given_ids)
                      -- See Note [Superclasses and satisfiability]
                 ; insols <- solveSimpleGivens given_cts
                 ; insols <- try_harder insols
@@ -558,7 +558,7 @@ simplifyInfer rhs_tclvl apply_mr sigs name_taus wanteds
             <- setTcLevel rhs_tclvl $
                runTcSWithEvBinds False (Just ev_binds_var) $
                do { let loc = mkGivenLoc rhs_tclvl UnkSkol tc_lcl_env
-                  ; psig_givens <- mkGivensWithSuperClasses loc psig_theta_vars
+                        psig_givens = mkGivens loc psig_theta_vars
                   ; _ <- solveSimpleGivens psig_givens
                          -- See Note [Add signature contexts as givens]
                   ; solveWanteds wanteds }
@@ -1216,9 +1216,9 @@ solveImplication imp@(Implic { ic_tclvl  = tclvl
          -- Solve the nested constraints
        ; ((no_given_eqs, given_insols, residual_wanted), used_tcvs)
              <- nestImplicTcS m_ev_binds (mkVarSet (skols ++ given_ids)) tclvl $
-               do { let loc = mkGivenLoc tclvl info env
-                  ; givens_w_scs <- mkGivensWithSuperClasses loc given_ids
-                  ; given_insols <- solveSimpleGivens givens_w_scs
+               do { let loc    = mkGivenLoc tclvl info env
+                        givens = mkGivens loc given_ids
+                  ; given_insols <- solveSimpleGivens givens
 
                   ; residual_wanted <- solveWanteds wanteds
                         -- solveWanteds, *not* solveWantedsAndDrop, because
diff --git a/testsuite/tests/indexed-types/should_compile/T12175.hs b/testsuite/tests/indexed-types/should_compile/T12175.hs
new file mode 100644 (file)
index 0000000..4c277de
--- /dev/null
@@ -0,0 +1,36 @@
+{-# LANGUAGE ConstraintKinds, MultiParamTypeClasses, TypeFamilies,
+             UndecidableInstances #-}
+{-# LANGUAGE FlexibleContexts #-}
+
+module T12175 where
+
+import GHC.Exts
+
+class Foo a
+instance Foo a => Foo (a,b)
+
+type family TElt r :: Constraint
+type instance TElt r = (Foo r, ())
+-- type TElt r = (Foo r, Eq r)
+
+data CT r = CT [r]
+
+toCT :: Foo r => CT r -> CT r
+toCT = undefined
+
+foo :: CT (a,b) -> (CT a, CT b)
+foo = undefined
+
+unzipT :: TElt (a,b) => CT (a,b) -> (CT a, CT b)
+unzipT x = foo (toCT x)
+
+{-  Type checking for unzipT
+
+[G] TElt (a,b)
+    --> {by rewrite}                 (Foo (a,b), ())
+    --> {by superclasses of tuple}   Foo (a,b), ()
+
+toCT @(a,b)
+    --> [W] Foo (a,b)
+    --> {by instance decl}  Foo a    (insoluble)
+ -}
index bee76d2..31c9555 100644 (file)
@@ -275,3 +275,4 @@ test('T11361', normal, compile, ['-dunique-increment=-1'])
   # -dunique-increment=-1 doesn't work inside the file
 test('T11361a', normal, compile_fail, [''])
 test('T11581', normal, compile, [''])
+test('T12175', normal, compile, [''])