Remove wc_insol from WantedConstraints
authorSimon Peyton Jones <simonpj@microsoft.com>
Mon, 9 Oct 2017 12:16:59 +0000 (13:16 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Wed, 11 Oct 2017 11:33:29 +0000 (12:33 +0100)
This patch is a pure refactoring, which I've wanted to do for
some time.  The main payload is

* Remove the wc_insol field from WantedConstraints;
  instead put all the insolubles in wc_simple

* Remove inert_insols from InertCans
  Instead put all the insolubles in inert_irreds

* Add a cc_insol flag to CIrredCan, to record that
  the constraint is definitely insoluble

Reasons

* Quite a bit of code gets slightly simpler
* Fewer concepts to keep separate
* Insolubles don't happen at all in production code that is
  just being recompiled, so previously there was a lot of
  moving-about of empty sets

A couple of error messages acutally improved.

19 files changed:
compiler/typecheck/TcCanonical.hs
compiler/typecheck/TcErrors.hs
compiler/typecheck/TcInteract.hs
compiler/typecheck/TcMType.hs
compiler/typecheck/TcRnMonad.hs
compiler/typecheck/TcRnTypes.hs
compiler/typecheck/TcRules.hs
compiler/typecheck/TcSMonad.hs
compiler/typecheck/TcSimplify.hs
compiler/typecheck/TcType.hs
testsuite/tests/deriving/should_fail/T3621.stderr
testsuite/tests/indexed-types/should_fail/T8518.hs
testsuite/tests/typecheck/should_compile/tc211.stderr
testsuite/tests/typecheck/should_fail/T12589.stderr
testsuite/tests/typecheck/should_fail/T13311.stderr
testsuite/tests/typecheck/should_fail/T7851.stderr
testsuite/tests/typecheck/should_fail/T8603.stderr
testsuite/tests/typecheck/should_fail/tcfail122.stderr
testsuite/tests/warnings/should_fail/CaretDiagnostics1.stderr

index 9045ec5..8d4d2a0 100644 (file)
@@ -78,10 +78,18 @@ last time through, so we can skip the classification step.
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 canonicalize :: Ct -> TcS (StopOrContinue Ct)
-canonicalize ct@(CNonCanonical { cc_ev = ev })
-  = do { traceTcS "canonicalize (non-canonical)" (ppr ct)
-       ; {-# SCC "canEvVar" #-}
-         canEvNC ev }
+canonicalize (CNonCanonical { cc_ev = ev })
+  = {-# SCC "canNC" #-}
+    case classifyPredType (ctEvPred ev) of
+      ClassPred cls tys     -> do traceTcS "canEvNC:cls" (ppr cls <+> ppr tys)
+                                  canClassNC ev cls tys
+      EqPred eq_rel ty1 ty2 -> do traceTcS "canEvNC:eq" (ppr ty1 $$ ppr ty2)
+                                  canEqNC    ev eq_rel ty1 ty2
+      IrredPred {}          -> do traceTcS "canEvNC:irred" (ppr (ctEvPred ev))
+                                  canIrred   ev
+
+canonicalize (CIrredCan { cc_ev = ev })
+  = canIrred ev
 
 canonicalize (CDictCan { cc_ev = ev, cc_class  = cls
                        , cc_tyargs = xis, cc_pend_sc = pend_sc })
@@ -104,21 +112,9 @@ canonicalize (CFunEqCan { cc_ev = ev
   = {-# SCC "canEqLeafFunEq" #-}
     canCFunEqCan ev fn xis1 fsk
 
-canonicalize (CIrredEvCan { cc_ev = ev })
-  = canIrred ev
 canonicalize (CHoleCan { cc_ev = ev, cc_hole = hole })
   = canHole ev hole
 
-canEvNC :: CtEvidence -> TcS (StopOrContinue Ct)
--- Called only for non-canonical EvVars
-canEvNC ev
-  = case classifyPredType (ctEvPred ev) of
-      ClassPred cls tys     -> do traceTcS "canEvNC:cls" (ppr cls <+> ppr tys)
-                                  canClassNC ev cls tys
-      EqPred eq_rel ty1 ty2 -> do traceTcS "canEvNC:eq" (ppr ty1 $$ ppr ty2)
-                                  canEqNC    ev eq_rel ty1 ty2
-      IrredPred {}          -> do traceTcS "canEvNC:irred" (ppr (ctEvPred ev))
-                                  canIrred   ev
 {-
 ************************************************************************
 *                                                                      *
@@ -500,7 +496,7 @@ canIrred old_ev
            ClassPred cls tys     -> canClassNC new_ev cls tys
            EqPred eq_rel ty1 ty2 -> canEqNC new_ev eq_rel ty1 ty2
            _                     -> continueWith $
-                                    CIrredEvCan { cc_ev = new_ev } } }
+                                    mkIrredCt new_ev } }
 
 canHole :: CtEvidence -> Hole -> TcS (StopOrContinue Ct)
 canHole ev hole
@@ -911,7 +907,7 @@ Here's another place where this reflexivity check is key:
 Consider trying to prove (f a) ~R (f a). The AppTys in there can't
 be decomposed, because representational equality isn't congruent with respect
 to AppTy. So, when canonicalising the equality above, we get stuck and
-would normally produce a CIrredEvCan. However, we really do want to
+would normally produce a CIrredCan. However, we really do want to
 be able to solve (f a) ~R (f a). So, in the representational case only,
 we do a reflexivity check.
 
@@ -958,7 +954,7 @@ can_eq_app :: CtEvidence       -- :: s1 t1 ~r s2 t2
 -- See Note [Decomposing equality], note {4}
 can_eq_app ev ReprEq _ _ _ _
   = do { traceTcS "failing to decompose representational AppTy equality" (ppr ev)
-       ; continueWith (CIrredEvCan { cc_ev = ev }) }
+       ; continueWith (mkIrredCt ev) }
           -- no need to call canEqFailure, because that flattens, and the
           -- types involved here are already flat
 
@@ -1031,7 +1027,7 @@ canTyConApp ev eq_rel tc1 tys1 tc2 tys2
   -- See Note [Skolem abstract data] (at tyConSkolem)
   | tyConSkolem tc1 || tyConSkolem tc2
   = do { traceTcS "canTyConApp: skolem abstract" (ppr tc1 $$ ppr tc2)
-       ; continueWith (CIrredEvCan { cc_ev = ev }) }
+       ; continueWith (mkIrredCt ev) }
 
   -- Fail straight away for better error messages
   -- See Note [Use canEqFailure in canDecomposableTyConApp]
@@ -1293,7 +1289,7 @@ canEqFailure ev ReprEq ty1 ty2
          vcat [ ppr ev, ppr ty1, ppr ty2, ppr xi1, ppr xi2 ]
        ; rewriteEqEvidence ev NotSwapped xi1 xi2 co1 co2
          `andWhenContinue` \ new_ev ->
-         continueWith (CIrredEvCan { cc_ev = new_ev }) }
+         continueWith (mkIrredCt new_ev) }
 
 -- | Call when canonicalizing an equality fails with utterly no hope.
 canEqHardFailure :: CtEvidence
@@ -1304,7 +1300,7 @@ canEqHardFailure ev ty1 ty2
        ; (s2, co2) <- flatten FM_SubstOnly ev ty2
        ; rewriteEqEvidence ev NotSwapped s1 s2 co1 co2
          `andWhenContinue` \ new_ev ->
-    do { emitInsoluble (mkNonCanonical new_ev)
+    do { emitInsoluble (mkInsolubleCt new_ev)
        ; stopWith new_ev "Definitely not equal" }}
 
 {-
@@ -1481,7 +1477,7 @@ canEqTyVar ev eq_rel swapped tv1 co1 ps_ty1 xi2 ps_xi2
              -- kind_ev :: (k1 :: *) ~ (k2 :: *)
        ; traceTcS "Hetero equality gives rise to derived kind equality" $
            ppr ev
-       ; continueWith (CIrredEvCan { cc_ev = ev }) }
+       ; continueWith (mkIrredCt ev) }
 
   where
     lhs = mkTyVarTy tv1 `mkCastTy` co1
@@ -1549,7 +1545,7 @@ canEqTyVar2 dflags ev eq_rel swapped tv1 co1 orhs
        ; rewriteEqEvidence ev swapped nlhs nrhs rewrite_co1 rewrite_co2
          `andWhenContinue` \ new_ev ->
          if isInsolubleOccursCheck eq_rel tv1 nrhs
-         then do { emitInsoluble (mkNonCanonical new_ev)
+         then do { emitInsoluble (mkInsolubleCt new_ev)
              -- If we have a ~ [a], it is not canonical, and in particular
              -- we don't want to rewrite existing inerts with it, otherwise
              -- we'd risk divergence in the constraint solver
@@ -1563,7 +1559,7 @@ canEqTyVar2 dflags ev eq_rel swapped tv1 co1 orhs
              -- canonical, and we might loop if we were to use it in rewriting.
          else do { traceTcS "Possibly-soluble occurs check"
                            (ppr nlhs $$ ppr nrhs)
-                 ; continueWith (CIrredEvCan { cc_ev = new_ev }) } }
+                 ; continueWith (mkIrredCt new_ev) } }
   where
     role = eqRelRole eq_rel
 
index 27569b5..525c6fb 100644 (file)
@@ -441,11 +441,10 @@ This only matters in instance declarations..
 -}
 
 reportWanteds :: ReportErrCtxt -> TcLevel -> WantedConstraints -> TcM ()
-reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_insol = insols, wc_impl = implics })
+reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_impl = implics })
   = do { traceTc "reportWanteds" (vcat [ text "Simples =" <+> ppr simples
-                                       , text "Insols =" <+> ppr insols
                                        , text "Suppress =" <+> ppr (cec_suppress ctxt)])
-       ; let tidy_cts = bagToList (mapBag (tidyCt env) (insols `unionBags` simples))
+       ; let tidy_cts = bagToList (mapBag (tidyCt env) simples)
        ; traceTc "rw2" (ppr tidy_cts)
 
          -- First deal with things that are utterly wrong
@@ -477,7 +476,7 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_insol = insols, wc_impl
     -- report1: ones that should *not* be suppresed by
     --          an insoluble somewhere else in the tree
     -- It's crucial that anything that is considered insoluble
-    -- (see TcRnTypes.trulyInsoluble) is caught here, otherwise
+    -- (see TcRnTypes.insolubleWantedCt) is caught here, otherwise
     -- we might suppress its error message, and proceed on past
     -- type checking to get a Lint error later
     report1 = [ ("custom_error", is_user_type_error,True, mkUserTypeErrorReporter)
@@ -936,9 +935,9 @@ coercion.
 
 Note [Do not report derived but soluble errors]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-The wc_simples include Derived constraints that have not been solved, but are
-not insoluble (in that case they'd be in wc_insols).  We do not want to report
-these as errors:
+The wc_simples include Derived constraints that have not been solved,
+but are not insoluble (in that case they'd be reported by 'report1').
+We do not want to report these as errors:
 
 * Superclass constraints. If we have an unsolved [W] Ord a, we'll also have
   an unsolved [D] Eq a, and we do not want to report that; it's just noise.
index df15e46..c9c647d 100644 (file)
@@ -201,16 +201,15 @@ solve_simple_wanteds :: WantedConstraints -> TcS (Int, WantedConstraints)
 -- Try solving these constraints
 -- Affects the unification state (of course) but not the inert set
 -- The result is not necessarily zonked
-solve_simple_wanteds (WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 })
+solve_simple_wanteds (WC { wc_simple = simples1, wc_impl = implics1 })
   = nestTcS $
     do { solveSimples simples1
-       ; (implics2, tv_eqs, fun_eqs, insols2, others) <- getUnsolvedInerts
+       ; (implics2, tv_eqs, fun_eqs, others) <- getUnsolvedInerts
        ; (unif_count, unflattened_eqs) <- reportUnifications $
                                           unflattenWanteds tv_eqs fun_eqs
             -- See Note [Unflatten after solving the simple wanteds]
        ; return ( unif_count
                 , WC { wc_simple = others `andCts` unflattened_eqs
-                     , wc_insol  = insols1 `andCts` insols2
                      , wc_impl   = implics1 `unionBags` implics2 }) }
 
 {- Note [The solveSimpleWanteds loop]
@@ -270,7 +269,7 @@ runTcPluginsGiven
 -- 'solveSimpleWanteds' should feed the updated wanteds back into the
 -- main solver.
 runTcPluginsWanted :: WantedConstraints -> TcS (Bool, WantedConstraints)
-runTcPluginsWanted wc@(WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 })
+runTcPluginsWanted wc@(WC { wc_simple = simples1, wc_impl = implics1 })
   | isEmptyBag simples1
   = return (False, wc)
   | otherwise
@@ -284,15 +283,17 @@ runTcPluginsWanted wc@(WC { wc_simple = simples1, wc_insol = insols1, wc_impl =
        ; let (_, _,                solved_wanted)   = pluginSolvedCts p
              (_, unsolved_derived, unsolved_wanted) = pluginInputCts p
              new_wanted                             = pluginNewCts p
+             insols                                 = pluginBadCts p
 
 -- SLPJ: I'm deeply suspicious of this
 --       ; updInertCans (removeInertCts $ solved_givens ++ solved_deriveds)
 
        ; mapM_ setEv solved_wanted
        ; return ( notNull (pluginNewCts p)
-                , WC { wc_simple = listToBag new_wanted `andCts` listToBag unsolved_wanted
-                                                        `andCts` listToBag unsolved_derived
-                     , wc_insol  = listToBag (pluginBadCts p) `andCts` insols1
+                , WC { wc_simple = listToBag new_wanted       `andCts`
+                                   listToBag unsolved_wanted  `andCts`
+                                   listToBag unsolved_derived `andCts`
+                                   listToBag insols
                      , wc_impl   = implics1 } ) } }
   where
     setEv :: (EvTerm,Ct) -> TcS ()
@@ -493,10 +494,10 @@ interactWithInertsStage wi
   = do { inerts <- getTcSInerts
        ; let ics = inert_cans inerts
        ; case wi of
-             CTyEqCan    {} -> interactTyVarEq ics wi
-             CFunEqCan   {} -> interactFunEq   ics wi
-             CIrredEvCan {} -> interactIrred   ics wi
-             CDictCan    {} -> interactDict    ics wi
+             CTyEqCan  {} -> interactTyVarEq ics wi
+             CFunEqCan {} -> interactFunEq   ics wi
+             CIrredCan {} -> interactIrred   ics wi
+             CDictCan  {} -> interactDict    ics wi
              _ -> pprPanic "interactWithInerts" (ppr wi) }
                 -- CHoleCan are put straight into inert_frozen, so never get here
                 -- CNonCanonical have been canonicalised
@@ -657,7 +658,7 @@ that this chain of events won't happen, but that's very fragile.)
 -- mean that (ty1 ~ ty2)
 interactIrred :: InertCans -> Ct -> TcS (StopOrContinue Ct)
 
-interactIrred inerts workItem@(CIrredEvCan { cc_ev = ev_w })
+interactIrred inerts workItem@(CIrredCan { cc_ev = ev_w })
   | let pred = ctEvPred ev_w
         (matching_irreds, others)
           = partitionBag (\ct -> ctPred ct `tcEqTypeNoKindCheck` pred)
index e89abe1..d7e6a5e 100644 (file)
@@ -1351,11 +1351,10 @@ zonkWC :: WantedConstraints -> TcM WantedConstraints
 zonkWC wc = zonkWCRec wc
 
 zonkWCRec :: WantedConstraints -> TcM WantedConstraints
-zonkWCRec (WC { wc_simple = simple, wc_impl = implic, wc_insol = insol })
+zonkWCRec (WC { wc_simple = simple, wc_impl = implic })
   = do { simple' <- zonkSimples simple
        ; implic' <- mapBagM zonkImplication implic
-       ; insol'  <- zonkSimples insol
-       ; return (WC { wc_simple = simple', wc_impl = implic', wc_insol = insol' }) }
+       ; return (WC { wc_simple = simple', wc_impl = implic' }) }
 
 zonkSimples :: Cts -> TcM Cts
 zonkSimples cts = do { cts' <- mapBagM zonkCt' cts
@@ -1366,10 +1365,12 @@ zonkCt' :: Ct -> TcM Ct
 zonkCt' ct = zonkCt ct
 
 {- Note [zonkCt behaviour]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
 zonkCt tries to maintain the canonical form of a Ct.  For example,
   - a CDictCan should stay a CDictCan;
   - a CTyEqCan should stay a CTyEqCan (if the LHS stays as a variable.).
   - a CHoleCan should stay a CHoleCan
+  - a CIrredCan should stay a CIrredCan with its cc_insol flag intact
 
 Why?, for example:
 - For CDictCan, the @TcSimplify.expandSuperClasses@ step, which runs after the
@@ -1380,21 +1381,27 @@ Why?, for example:
 
 - For CHoleCan, once we forget that it's a hole, we can never recover that info.
 
+- For CIrredCan we want to see if a constraint is insoluble with insolubleWC
+
 NB: we do not expect to see any CFunEqCans, because zonkCt is only
 called on unflattened constraints.
+
 NB: Constraints are always re-flattened etc by the canonicaliser in
 @TcCanonical@ even if they come in as CDictCan. Only canonical constraints that
 are actually in the inert set carry all the guarantees. So it is okay if zonkCt
 creates e.g. a CDictCan where the cc_tyars are /not/ function free.
 -}
+
 zonkCt :: Ct -> TcM Ct
 zonkCt ct@(CHoleCan { cc_ev = ev })
   = do { ev' <- zonkCtEvidence ev
        ; return $ ct { cc_ev = ev' } }
+
 zonkCt ct@(CDictCan { cc_ev = ev, cc_tyargs = args })
   = do { ev'   <- zonkCtEvidence ev
        ; args' <- mapM zonkTcType args
        ; return $ ct { cc_ev = ev', cc_tyargs = args' } }
+
 zonkCt ct@(CTyEqCan { cc_ev = ev, cc_tyvar = tv, cc_rhs = rhs })
   = do { ev'    <- zonkCtEvidence ev
        ; tv_ty' <- zonkTcTyVar tv
@@ -1404,6 +1411,11 @@ zonkCt ct@(CTyEqCan { cc_ev = ev, cc_tyvar = tv, cc_rhs = rhs })
                                       , cc_tyvar = tv'
                                       , cc_rhs   = rhs' } }
            Nothing  -> return (mkNonCanonical ev') }
+
+zonkCt ct@(CIrredCan { cc_ev = ev }) -- Preserve the cc_insol flag
+  = do { ev' <- zonkCtEvidence ev
+       ; return (ct { cc_ev = ev' }) }
+
 zonkCt ct
   = ASSERT( not (isCFunEqCan ct) )
   -- We do not expect to see any CFunEqCans, because zonkCt is only called on
index fd288eb..5121fb5 100644 (file)
@@ -1589,6 +1589,17 @@ Hence:
   - insolublesOnly in tryCaptureConstraints
   - emitConstraints in the Left case of captureConstraints
 
+Hover note that fresly-generated constraints like (Int ~ Bool), or
+((a -> b) ~ Int) are all CNonCanonical, and hence won't be flagged as
+insoluble.  The constraint solver does that.  So they'll be discarded.
+That's probably ok; but see th/5358 as a not-so-good example:
+   t1 :: Int
+   t1 x = x   -- Manifestly wrong
+
+   foo = $(...raises exception...)
+We report the exception, but not the bug in t1.  Oh well.  Possible
+solution: make TcUnify.uType spot manifestly-insoluble constraints.
+
 
 ************************************************************************
 *                                                                      *
index 3c7d67f..a109764 100644 (file)
@@ -70,12 +70,13 @@ module TcRnTypes(
         isEmptyCts, isCTyEqCan, isCFunEqCan,
         isPendingScDict, superClassesMightHelp,
         isCDictCan_Maybe, isCFunEqCan_maybe,
-        isCIrredEvCan, isCNonCanonical, isWantedCt, isDerivedCt,
+        isCNonCanonical, isWantedCt, isDerivedCt,
         isGivenCt, isHoleCt, isOutOfScopeCt, isExprHoleCt, isTypeHoleCt,
         isUserTypeErrorCt, getUserTypeErrorMsg,
         ctEvidence, ctLoc, setCtLoc, ctPred, ctFlavour, ctEqRel, ctOrigin,
         mkTcEqPredLikeEv,
         mkNonCanonical, mkNonCanonicalCt, mkGivens,
+        mkIrredCt, mkInsolubleCt,
         ctEvPred, ctEvLoc, ctEvOrigin, ctEvEqRel,
         ctEvTerm, ctEvCoercion, ctEvId,
         tyCoVarsOfCt, tyCoVarsOfCts,
@@ -83,9 +84,9 @@ module TcRnTypes(
 
         WantedConstraints(..), insolubleWC, emptyWC, isEmptyWC,
         andWC, unionsWC, mkSimpleWC, mkImplicWC,
-        addInsols, getInsolubles, insolublesOnly, addSimples, addImplics,
-        tyCoVarsOfWC, dropDerivedWC, dropDerivedSimples, dropDerivedInsols,
-        tyCoVarsOfWCList, trulyInsoluble,
+        addInsols, insolublesOnly, addSimples, addImplics,
+        tyCoVarsOfWC, dropDerivedWC, dropDerivedSimples,
+        tyCoVarsOfWCList, insolubleWantedCt, insolubleEqCt,
         isDroppableDerivedLoc, isDroppableDerivedCt, insolubleImplic,
         arisesFromGivens,
 
@@ -1619,13 +1620,20 @@ data Ct
                            --              superclasses as Givens
     }
 
-  | CIrredEvCan {  -- These stand for yet-unusable predicates
-      cc_ev :: CtEvidence   -- See Note [Ct/evidence invariant]
-        -- The ctev_pred of the evidence is
-        -- of form   (tv xi1 xi2 ... xin)
+  | CIrredCan {  -- These stand for yet-unusable predicates
+      cc_ev    :: CtEvidence,   -- See Note [Ct/evidence invariant]
+      cc_insol :: Bool   -- True  <=> definitely an error, can never be solved
+                         -- False <=> might be soluble
+
+        -- For the might-be-soluble case, the ctev_pred of the evidence is
+        -- of form   (tv xi1 xi2 ... xin)   with a tyvar at the head
         --      or   (tv1 ~ ty2)   where the CTyEqCan  kind invariant fails
         --      or   (F tys ~ ty)  where the CFunEqCan kind invariant fails
-        -- See Note [CIrredEvCan constraints]
+        -- See Note [CIrredCan constraints]
+
+        -- The definitely-insoluble case is for things like
+        --    Int ~ Bool      tycons don't match
+        --    a ~ [a]         occurs check
     }
 
   | CTyEqCan {  -- tv ~ rhs
@@ -1710,9 +1718,9 @@ distinguished by cc_hole:
     e.g.   f :: _ -> _
            f x = [x,True]
 
-Note [CIrredEvCan constraints]
+Note [CIrredCan constraints]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-CIrredEvCan constraints are used for constraints that are "stuck"
+CIrredCan constraints are used for constraints that are "stuck"
    - we can't solve them (yet)
    - we can't use them to solve other constraints
    - but they may become soluble if we substitute for some
@@ -1754,6 +1762,12 @@ mkNonCanonical ev = CNonCanonical { cc_ev = ev }
 mkNonCanonicalCt :: Ct -> Ct
 mkNonCanonicalCt ct = CNonCanonical { cc_ev = cc_ev ct }
 
+mkIrredCt :: CtEvidence -> Ct
+mkIrredCt ev = CIrredCan { cc_ev = ev, cc_insol = False }
+
+mkInsolubleCt :: CtEvidence -> Ct
+mkInsolubleCt ev = CIrredCan { cc_ev = ev, cc_insol = True }
+
 mkGivens :: CtLoc -> [EvId] -> [Ct]
 mkGivens loc ev_ids
   = map mk ev_ids
@@ -1806,7 +1820,9 @@ instance Outputable Ct where
          CDictCan { cc_pend_sc = pend_sc }
             | pend_sc   -> text "CDictCan(psc)"
             | otherwise -> text "CDictCan"
-         CIrredEvCan {}   -> text "CIrredEvCan"
+         CIrredCan { cc_insol = insol }
+            | insol     -> text "CIrredCan(insol)"
+            | otherwise -> text "CIrredCan(sol)"
          CHoleCan { cc_hole = hole } -> text "CHoleCan:" <+> ppr hole
 
 {-
@@ -1838,7 +1854,7 @@ tyCoFVsOfCt (CFunEqCan { cc_tyargs = tys, cc_fsk = fsk })
   = tyCoFVsOfTypes tys `unionFV` FV.unitFV fsk
                        `unionFV` tyCoFVsOfType (tyVarKind fsk)
 tyCoFVsOfCt (CDictCan { cc_tyargs = tys }) = tyCoFVsOfTypes tys
-tyCoFVsOfCt (CIrredEvCan { cc_ev = ev }) = tyCoFVsOfType (ctEvPred ev)
+tyCoFVsOfCt (CIrredCan { cc_ev = ev }) = tyCoFVsOfType (ctEvPred ev)
 tyCoFVsOfCt (CHoleCan { cc_ev = ev }) = tyCoFVsOfType (ctEvPred ev)
 tyCoFVsOfCt (CNonCanonical { cc_ev = ev }) = tyCoFVsOfType (ctEvPred ev)
 
@@ -1873,10 +1889,9 @@ tyCoVarsOfWCList = fvVarList . tyCoFVsOfWC
 -- computation. See Note [Deterministic FV] in FV.
 tyCoFVsOfWC :: WantedConstraints -> FV
 -- Only called on *zonked* things, hence no need to worry about flatten-skolems
-tyCoFVsOfWC (WC { wc_simple = simple, wc_impl = implic, wc_insol = insol })
+tyCoFVsOfWC (WC { wc_simple = simple, wc_impl = implic })
   = tyCoFVsOfCts simple `unionFV`
-    tyCoFVsOfBag tyCoFVsOfImplic implic `unionFV`
-    tyCoFVsOfCts insol
+    tyCoFVsOfBag tyCoFVsOfImplic implic
 
 -- | Returns free variables of Implication as a composable FV computation.
 -- See Note [Deterministic FV] in FV.
@@ -1891,6 +1906,13 @@ tyCoFVsOfImplic (Implic { ic_skols = skols
 tyCoFVsOfBag :: (a -> FV) -> Bag a -> FV
 tyCoFVsOfBag tvs_of = foldrBag (unionFV . tvs_of) emptyFV
 
+---------------------------
+dropDerivedWC :: WantedConstraints -> WantedConstraints
+-- See Note [Dropping derived constraints]
+dropDerivedWC wc@(WC { wc_simple = simples })
+  = wc { wc_simple = dropDerivedSimples simples }
+    -- The wc_impl implications are already (recursively) filtered
+
 --------------------------
 dropDerivedSimples :: Cts -> Cts
 -- Drop all Derived constraints, but make [W] back into [WD],
@@ -1902,10 +1924,13 @@ dropDerivedSimples simples = mapMaybeBag dropDerivedCt simples
 dropDerivedCt :: Ct -> Maybe Ct
 dropDerivedCt ct
   = case ctEvFlavour ev of
+      Given        -> Just ct  -- Presumably insoluble; keep
       Wanted WOnly -> Just (ct' { cc_ev = ev_wd })
       Wanted _     -> Just ct'
-      _            -> ASSERT( isDerivedCt ct ) Nothing
-                      -- simples are all Wanted or Derived
+      Derived | isDroppableDerivedLoc (ctLoc ct)
+              -> Nothing
+              | otherwise
+              -> Just ct
   where
     ev    = ctEvidence ct
     ev_wd = ev { ctev_nosh = WDeriv }
@@ -1921,13 +1946,6 @@ we might miss some fundeps.  Trac #13662 showed this up.
 See Note [The superclass story] in TcCanonical.
 -}
 
-
-dropDerivedInsols :: Cts -> Cts
--- See Note [Dropping derived constraints]
-dropDerivedInsols insols
-  = filterBag (not . isDroppableDerivedCt) insols
-              -- insols can include Given
-
 isDroppableDerivedCt :: Ct -> Bool
 isDroppableDerivedCt ct
   | isDerivedCt ct = isDroppableDerivedLoc (ctLoc ct)
@@ -2030,10 +2048,6 @@ isCDictCan_Maybe :: Ct -> Maybe Class
 isCDictCan_Maybe (CDictCan {cc_class = cls })  = Just cls
 isCDictCan_Maybe _              = Nothing
 
-isCIrredEvCan :: Ct -> Bool
-isCIrredEvCan (CIrredEvCan {}) = True
-isCIrredEvCan _                = False
-
 isCFunEqCan_maybe :: Ct -> Maybe (TyCon, [Type])
 isCFunEqCan_maybe (CFunEqCan { cc_fun = tc, cc_tyargs = xis }) = Just (tc, xis)
 isCFunEqCan_maybe _ = Nothing
@@ -2226,34 +2240,29 @@ v%************************************************************************
 data WantedConstraints
   = WC { wc_simple :: Cts              -- Unsolved constraints, all wanted
        , wc_impl   :: Bag Implication
-       , wc_insol  :: Cts              -- Insoluble constraints, can be
-                                       -- wanted, given, or derived
-                                       -- See Note [Insoluble constraints]
     }
 
 emptyWC :: WantedConstraints
-emptyWC = WC { wc_simple = emptyBag, wc_impl = emptyBag, wc_insol = emptyBag }
+emptyWC = WC { wc_simple = emptyBag, wc_impl = emptyBag }
 
 mkSimpleWC :: [CtEvidence] -> WantedConstraints
 mkSimpleWC cts
   = WC { wc_simple = listToBag (map mkNonCanonical cts)
-       , wc_impl = emptyBag
-       , wc_insol = emptyBag }
+       , wc_impl = emptyBag }
 
 mkImplicWC :: Bag Implication -> WantedConstraints
 mkImplicWC implic
-  = WC { wc_simple = emptyBag, wc_impl = implic, wc_insol = emptyBag }
+  = WC { wc_simple = emptyBag, wc_impl = implic }
 
 isEmptyWC :: WantedConstraints -> Bool
-isEmptyWC (WC { wc_simple = f, wc_impl = i, wc_insol = n })
-  = isEmptyBag f && isEmptyBag i && isEmptyBag n
+isEmptyWC (WC { wc_simple = f, wc_impl = i })
+  = isEmptyBag f && isEmptyBag i
 
 andWC :: WantedConstraints -> WantedConstraints -> WantedConstraints
-andWC (WC { wc_simple = f1, wc_impl = i1, wc_insol = n1 })
-      (WC { wc_simple = f2, wc_impl = i2, wc_insol = n2 })
+andWC (WC { wc_simple = f1, wc_impl = i1 })
+      (WC { wc_simple = f2, wc_impl = i2 })
   = WC { wc_simple = f1 `unionBags` f2
-       , wc_impl   = i1 `unionBags` i2
-       , wc_insol  = n1 `unionBags` n2 }
+       , wc_impl   = i1 `unionBags` i2 }
 
 unionsWC :: [WantedConstraints] -> WantedConstraints
 unionsWC = foldr andWC emptyWC
@@ -2268,28 +2277,17 @@ addImplics wc implic = wc { wc_impl = wc_impl wc `unionBags` implic }
 
 addInsols :: WantedConstraints -> Bag Ct -> WantedConstraints
 addInsols wc cts
-  = wc { wc_insol = wc_insol wc `unionBags` cts }
-
-getInsolubles :: WantedConstraints -> Cts
-getInsolubles = wc_insol
+  = wc { wc_simple = wc_simple wc `unionBags` cts }
 
 insolublesOnly :: WantedConstraints -> WantedConstraints
--- Keep only the insolubles
-insolublesOnly (WC { wc_insol = insols, wc_impl = implics })
-  = WC { wc_simple = emptyBag
-       , wc_insol  = insols
-       , wc_impl = mapBag implic_insols_only implics }
+-- Keep only the definitely-insoluble constraints
+insolublesOnly (WC { wc_simple = simples, wc_impl = implics })
+  = WC { wc_simple = filterBag insolubleWantedCt simples
+       , wc_impl   = mapBag implic_insols_only implics }
   where
     implic_insols_only implic
       = implic { ic_wanted = insolublesOnly (ic_wanted implic) }
 
-dropDerivedWC :: WantedConstraints -> WantedConstraints
--- See Note [Dropping derived constraints]
-dropDerivedWC wc@(WC { wc_simple = simples, wc_insol = insols })
-  = wc { wc_simple = dropDerivedSimples simples
-       , wc_insol  = dropDerivedInsols insols }
-    -- The wc_impl implications are already (recursively) filtered
-
 isSolvedStatus :: ImplicStatus -> Bool
 isSolvedStatus (IC_Solved {}) = True
 isSolvedStatus _              = False
@@ -2302,30 +2300,40 @@ insolubleImplic :: Implication -> Bool
 insolubleImplic ic = isInsolubleStatus (ic_status ic)
 
 insolubleWC :: WantedConstraints -> Bool
-insolubleWC (WC { wc_impl = implics, wc_insol = insols })
-  =  anyBag trulyInsoluble insols
+insolubleWC (WC { wc_impl = implics, wc_simple = simples })
+  =  anyBag insolubleWantedCt simples
   || anyBag insolubleImplic implics
 
-trulyInsoluble :: Ct -> Bool
--- Constraints in the wc_insol set which ARE NOT
--- treated as truly insoluble:
---   a) type holes, arising from PartialTypeSignatures,
---   b) "true" expression holes arising from TypedHoles
+insolubleWantedCt :: Ct -> Bool
+-- Definitely insoluble, in particular /excluding/ type-hole constraints
+insolubleWantedCt ct
+  | isGivenCt ct     = False              -- See Note [Given insolubles]
+  | isHoleCt ct      = isOutOfScopeCt ct  -- See Note [Insoluble holes]
+  | insolubleEqCt ct = True
+  | otherwise        = False
+
+insolubleEqCt :: Ct -> Bool
+-- Returns True of /equality/ constraints
+-- that are /definitely/ insoluble
+-- It won't detect some definite errors like
+--       F a ~ T (F a)
+-- where F is a type family, which actually has an occurs check
 --
--- An "expression hole" or "type hole" constraint isn't really an error
--- at all; it's a report saying "_ :: Int" here.  But an out-of-scope
--- variable masquerading as expression holes IS treated as truly
--- insoluble, so that it trumps other errors during error reporting.
--- Yuk!
-trulyInsoluble insol
-  | isHoleCt insol = isOutOfScopeCt insol
-  | otherwise      = not (isGivenCt insol) -- See Note [Given insolubles]
+-- The function is tuned for application /after/ constraint solving
+--       i.e. assuming canonicalisation has been done
+-- E.g.  It'll reply True  for     a ~ [a]
+--               but False for   [a] ~ a
+-- and
+--                   True for  Int ~ F a Int
+--               but False for  Maybe Int ~ F a Int Int
+--               (where F is an arity-1 type function)
+insolubleEqCt (CIrredCan { cc_insol = insol }) = insol
+insolubleEqCt _                                = False
 
 instance Outputable WantedConstraints where
-  ppr (WC {wc_simple = s, wc_impl = i, wc_insol = n})
+  ppr (WC {wc_simple = s, wc_impl = i})
    = text "WC" <+> braces (vcat
         [ ppr_bag (text "wc_simple") s
-        , ppr_bag (text "wc_insol") n
         , ppr_bag (text "wc_impl") i ])
 
 ppr_bag :: Outputable a => SDoc -> Bag a -> SDoc
@@ -2339,21 +2347,37 @@ ppr_bag doc bag
 Consider (Trac #14325, comment:)
     class (a~b) => C a b
 
-    foo :: C a b => a -> b
+    foo :: C a c => a -> c
     foo x = x
 
     hm3 :: C (f b) b => b -> f b
     hm3 x = foo x
 
-From the [G] C (f b) b we get the insoluble [G] f b ~# b.  Then we we also
-get an unsolved [W] C b (f b).  If trulyInsouble is true of this, we'll
-set cec_suppress to True, and suppress reports of the [W] C b (f b).  But we
+In the RHS of hm3, from the [G] C (f b) b we get the insoluble
+[G] f b ~# b.  Then we also get an unsolved [W] C b (f b).
+Residual implication looks like
+    forall b. C (f b) b => [G] f b ~# b
+                           [W] C f (f b)
+
+We do /not/ want to set the implication status to IC_Insoluble,
+because that'll suppress reports of [W] C b (f b).  But we
 may not report the insoluble [G] f b ~# b either (see Note [Given errors]
 in TcErrors), so we may fail to report anything at all!  Yikes.
 
-Bottom line: we must be certain to report anything trulyInsoluble.  Easiest
-way to guaranteed this is to make truly Insoluble false of Givens.
+Bottom line: insolubleWC (called in TcSimplify.setImplicationStatus)
+             should ignore givens even if they are insoluble.
 
+Note [Insoluble holes]
+~~~~~~~~~~~~~~~~~~~~~~
+Hole constraints that ARE NOT treated as truly insoluble:
+  a) type holes, arising from PartialTypeSignatures,
+  b) "true" expression holes arising from TypedHoles
+
+An "expression hole" or "type hole" constraint isn't really an error
+at all; it's a report saying "_ :: Int" here.  But an out-of-scope
+variable masquerading as expression holes IS treated as truly
+insoluble, so that it trumps other errors during error reporting.
+Yuk!
 
 ************************************************************************
 *                                                                      *
index c3919a3..fd7ce2f 100644 (file)
@@ -14,6 +14,7 @@ module TcRules ( tcRules ) where
 import GhcPrelude
 
 import HsSyn
+import TcRnTypes
 import TcRnMonad
 import TcSimplify
 import TcMType
@@ -329,7 +330,18 @@ simplifyRule name lhs_wanted rhs_wanted
        ; zonked_lhs_simples <- zonkSimples (wc_simple lhs_wanted)
 
        -- Note [The SimplifyRule Plan] step 3
-       ; let (quant_cts, no_quant_cts) = partitionBag (quantify_ct insoluble)
+       ; let quantify_ct :: Ct -> Bool
+             quantify_ct ct
+                | EqPred _ t1 t2 <- classifyPredType (ctPred ct)
+                = not (insoluble || t1 `tcEqType` t2)
+                  -- Note [RULE quantification over equalities]
+               | isHoleCt ct
+               = False  -- Don't quantify over type holes, obviously
+               | otherwise
+               = True
+
+       -- Note [The SimplifyRule Plan] step 3
+       ; let (quant_cts, no_quant_cts) = partitionBag quantify_ct
                                                       zonked_lhs_simples
 
        ; quant_evs <- mapM mk_quant_ev (bagToList quant_cts)
@@ -346,15 +358,6 @@ simplifyRule name lhs_wanted rhs_wanted
        ; return (quant_evs, lhs_wanted { wc_simple = no_quant_cts }) }
 
   where
-    quantify_ct :: Bool -> Ct -> Bool
-    quantify_ct insol ct
-      | EqPred _ t1 t2 <- classifyPredType (ctPred ct)
-      = not (insol || t1 `tcEqType` t2)
-        -- Note [RULE quantification over equalities]
-
-      | otherwise
-      = True
-
     mk_quant_ev :: Ct -> TcM EvVar
     mk_quant_ev ct
       | CtWanted { ctev_dest = dest, ctev_pred = pred } <- ctEvidence ct
index cec2735..6bc08ce 100644 (file)
@@ -426,8 +426,7 @@ emptyInert
                          , inert_dicts    = emptyDicts
                          , inert_safehask = emptyDicts
                          , inert_funeqs   = emptyFunEqs
-                         , inert_irreds   = emptyCts
-                         , inert_insols   = emptyCts }
+                         , inert_irreds   = emptyCts }
        , inert_flat_cache    = emptyExactFunEqs
        , inert_fsks          = []
        , inert_solved_dicts  = emptyDictMap }
@@ -629,10 +628,9 @@ data InertCans   -- See Note [Detailed InertCans Invariants] for more
               -- in TcSimplify
 
        , inert_irreds :: Cts
-              -- Irreducible predicates
-
-       , inert_insols :: Cts
-              -- Frozen errors (as non-canonicals)
+              -- Irreducible predicates that cannot be made canonical,
+              --     and which don't interact with others (e.g.  (c a))
+              -- and insoluble predicates (e.g.  Int ~ Bool, or a ~ [a])
 
        , inert_count :: Int
               -- Number of Wanted goals in
@@ -964,7 +962,7 @@ instance Outputable InertCans where
   ppr (IC { inert_eqs = eqs
           , inert_funeqs = funeqs, inert_dicts = dicts
           , inert_safehask = safehask, inert_irreds = irreds
-          , inert_insols = insols, inert_count = count })
+          , inert_count = count })
     = braces $ vcat
       [ ppUnless (isEmptyDVarEnv eqs) $
         text "Equalities:"
@@ -977,8 +975,6 @@ instance Outputable InertCans where
         text "Safe Haskell unsafe overlap =" <+> pprCts (dictsToBag safehask)
       , ppUnless (isEmptyCts irreds) $
         text "Irreds =" <+> pprCts irreds
-      , ppUnless (isEmptyCts insols) $
-        text "Insolubles =" <+> pprCts insols
       , text "Unsolved goals =" <+> int count
       ]
 
@@ -1420,7 +1416,7 @@ add_item :: InertCans -> Ct -> InertCans
 add_item ics item@(CFunEqCan { cc_fun = tc, cc_tyargs = tys })
   = ics { inert_funeqs = insertFunEq (inert_funeqs ics) tc tys item }
 
-add_item ics item@(CIrredEvCan { cc_ev = ev })
+add_item ics item@(CIrredCan { cc_ev = ev })
   = ics { inert_irreds = inert_irreds ics `Bag.snocBag` item
         , inert_count = bumpUnsolvedCount ev (inert_count ics) }
        -- The 'False' is because the irreducible constraint might later instantiate
@@ -1437,7 +1433,7 @@ add_item _ item
   = pprPanic "upd_inert set: can't happen! Inserting " $
     ppr item   -- CTyEqCan is dealt with by addInertEq
                -- Can't be CNonCanonical, CHoleCan,
-               -- because they only land in inert_insols
+               -- because they only land in inert_irreds
 
 bumpUnsolvedCount :: CtEvidence -> Int -> Int
 bumpUnsolvedCount ev n | isWanted ev = n+1
@@ -1475,7 +1471,6 @@ kick_out_rewritable new_fr new_tv ics@(IC { inert_eqs      = tv_eqs
                                         , inert_safehask = safehask
                                         , inert_funeqs   = funeqmap
                                         , inert_irreds   = irreds
-                                        , inert_insols   = insols
                                         , inert_count    = n })
   | not (new_fr `eqMayRewriteFR` new_fr)
   = (emptyWorkList, ics)
@@ -1492,14 +1487,12 @@ kick_out_rewritable new_fr new_tv ics@(IC { inert_eqs      = tv_eqs
                        , inert_safehask = safehask   -- ??
                        , inert_funeqs   = feqs_in
                        , inert_irreds   = irs_in
-                       , inert_insols   = insols_in
                        , inert_count    = n - workListWantedCount kicked_out }
 
-    kicked_out = WL { wl_eqs    = tv_eqs_out
-                    , wl_funeqs = feqs_out
-                    , wl_deriv  = []
-                    , wl_rest   = bagToList (dicts_out `andCts` irs_out
-                                             `andCts` insols_out)
+    kicked_out = WL { wl_eqs     = tv_eqs_out
+                    , wl_funeqs  = feqs_out
+                    , wl_deriv   = []
+                    , wl_rest    = bagToList (dicts_out `andCts` irs_out)
                     , wl_implics = emptyBag }
 
     (tv_eqs_out, tv_eqs_in) = foldDVarEnv kick_out_eqs ([], emptyDVarEnv) tv_eqs
@@ -1507,8 +1500,9 @@ kick_out_rewritable new_fr new_tv ics@(IC { inert_eqs      = tv_eqs
            -- See Note [Kicking out CFunEqCan for fundeps]
     (dicts_out,  dicts_in)  = partitionDicts   kick_out_ct dictmap
     (irs_out,    irs_in)    = partitionBag     kick_out_ct irreds
-    (insols_out, insols_in) = partitionBag     kick_out_ct insols
       -- Kick out even insolubles: See Note [Rewrite insolubles]
+      -- Of course we must kick out irreducibles like (c a), in case
+      -- we can rewrite 'c' to something more useful
 
     fr_may_rewrite :: CtFlavourRole -> Bool
     fr_may_rewrite fs = new_fr `eqMayRewriteFR` fs
@@ -1715,7 +1709,10 @@ getInertEqs :: TcS (DTyVarEnv EqualCtList)
 getInertEqs = do { inert <- getInertCans; return (inert_eqs inert) }
 
 getInertInsols :: TcS Cts
-getInertInsols = do { inert <- getInertCans; return (inert_insols inert) }
+-- Returns insoluble equality constraints
+-- specifically including Givens
+getInertInsols = do { inert <- getInertCans
+                    ; return (filterBag insolubleEqCt (inert_irreds inert)) }
 
 getInertGivens :: TcS [Ct]
 -- Returns the Given constraints in the inert set,
@@ -1754,7 +1751,6 @@ getPendingScDicts = updRetInertCans get_sc_dicts
 getUnsolvedInerts :: TcS ( Bag Implication
                          , Cts     -- Tyvar eqs: a ~ ty
                          , Cts     -- Fun eqs:   F a ~ ty
-                         , Cts     -- Insoluble
                          , Cts )   -- All others
 -- Return all the unsolved [Wanted] or [Derived] constraints
 --
@@ -1766,7 +1762,6 @@ getUnsolvedInerts
            , inert_funeqs = fun_eqs
            , inert_irreds = irreds
            , inert_dicts  = idicts
-           , inert_insols = insols
            } <- getInertCans
 
       ; let unsolved_tv_eqs  = foldTyEqs add_if_unsolved tv_eqs emptyCts
@@ -1774,19 +1769,16 @@ getUnsolvedInerts
             unsolved_irreds  = Bag.filterBag is_unsolved irreds
             unsolved_dicts   = foldDicts add_if_unsolved idicts emptyCts
             unsolved_others  = unsolved_irreds `unionBags` unsolved_dicts
-            unsolved_insols  = filterBag is_unsolved insols
 
       ; implics <- getWorkListImplics
 
       ; traceTcS "getUnsolvedInerts" $
         vcat [ text " tv eqs =" <+> ppr unsolved_tv_eqs
              , text "fun eqs =" <+> ppr unsolved_fun_eqs
-             , text "insols =" <+> ppr unsolved_insols
              , text "others =" <+> ppr unsolved_others
              , text "implics =" <+> ppr implics ]
 
-      ; return ( implics, unsolved_tv_eqs, unsolved_fun_eqs
-               , unsolved_insols, unsolved_others) }
+      ; return ( implics, unsolved_tv_eqs, unsolved_fun_eqs, unsolved_others) }
   where
     add_if_unsolved :: Ct -> Cts -> Cts
     add_if_unsolved ct cts | is_unsolved ct = ct `consCts` cts
@@ -1819,32 +1811,35 @@ isInInertEqs eqs tv rhs
 getNoGivenEqs :: TcLevel          -- TcLevel of this implication
                -> [TcTyVar]       -- Skolems of this implication
                -> TcS ( Bool      -- True <=> definitely no residual given equalities
-                      , Cts )     -- Insoluble constraints arising from givens
+                      , Cts )     -- Insoluble equalities arising from givens
 -- See Note [When does an implication have given equalities?]
 getNoGivenEqs tclvl skol_tvs
-  = do { inerts@(IC { inert_eqs = ieqs, inert_irreds = iirreds
-                    , inert_insols = insols })
+  = do { inerts@(IC { inert_eqs = ieqs, inert_irreds = irreds })
               <- getInertCans
-       ; let has_given_eqs = foldrBag ((||) . ev_given_here . ctEvidence) False
-                                      (iirreds `unionBags` insols)
+       ; let has_given_eqs = foldrBag ((||) . ct_given_here) False irreds
                           || anyDVarEnv eqs_given_here ieqs
+             insols = filterBag insolubleEqCt irreds
+                      -- Specifically includes ones that originated in some
+                      -- outer context but were refined to an insoluble by
+                      -- a local equality; so do /not/ add ct_given_here.
 
        ; traceTcS "getNoGivenEqs" (vcat [ ppr has_given_eqs, ppr inerts
                                         , ppr insols])
        ; return (not has_given_eqs, insols) }
   where
     eqs_given_here :: EqualCtList -> Bool
-    eqs_given_here [CTyEqCan { cc_tyvar = tv, cc_ev = ev }]
+    eqs_given_here [ct@(CTyEqCan { cc_tyvar = tv })]
                               -- Givens are always a sigleton
-      = not (skolem_bound_here tv) && ev_given_here ev
+      = not (skolem_bound_here tv) && ct_given_here ct
     eqs_given_here _ = False
 
-    ev_given_here :: CtEvidence -> Bool
+    ct_given_here :: Ct -> Bool
     -- True for a Given bound by the current implication,
     -- i.e. the current level
-    ev_given_here ev
-      =  isGiven ev
-      && tclvl == ctLocLevel (ctEvLoc ev)
+    ct_given_here ct =  isGiven ev
+                     && tclvl == ctLocLevel (ctEvLoc ev)
+        where
+          ev = ctEvidence ct
 
     skol_tv_set = mkVarSet skol_tvs
     skolem_bound_here tv -- See Note [Let-bound skolems]
@@ -1992,7 +1987,7 @@ removeInertCt is ct =
     CTyEqCan  { cc_tyvar = x,  cc_rhs    = ty } ->
       is { inert_eqs    = delTyEq (inert_eqs is) x ty }
 
-    CIrredEvCan {}   -> panic "removeInertCt: CIrredEvCan"
+    CIrredCan {}     -> panic "removeInertCt: CIrredEvCan"
     CNonCanonical {} -> panic "removeInertCt: CNonCanonical"
     CHoleCan {}      -> panic "removeInertCt: CHoleCan"
 
@@ -2601,8 +2596,7 @@ buildImplication skol_info skol_tvs givens (TcS thing_inside)
        ; let wc  = ASSERT2( null (wl_funeqs wl) && null (wl_rest wl) &&
                             null (wl_deriv wl) && null (wl_implics wl), ppr wl )
                    WC { wc_simple = listToCts eqs
-                      , wc_impl   = emptyBag
-                      , wc_insol  = emptyCts }
+                      , wc_impl   = emptyBag }
              imp = Implic { ic_tclvl  = new_tclvl
                           , ic_skols  = skol_tvs
                           , ic_no_eqs = True
@@ -2677,12 +2671,12 @@ emitInsoluble ct
        ; updInertTcS add_insol }
   where
     this_pred = ctPred ct
-    add_insol is@(IS { inert_cans = ics@(IC { inert_insols = old_insols }) })
+    add_insol is@(IS { inert_cans = ics@(IC { inert_irreds = old_irreds }) })
       | drop_it   = is
-      | otherwise = is { inert_cans = ics { inert_insols = old_insols `snocCts` ct } }
+      | otherwise = is { inert_cans = ics { inert_irreds = old_irreds `snocCts` ct } }
       where
         drop_it = isDroppableDerivedCt ct &&
-                  anyBag (tcEqType this_pred . ctPred) old_insols
+                  anyBag (tcEqType this_pred . ctPred) old_irreds
              -- See Note [Do not add duplicate derived insolubles]
 
 newTcRef :: a -> TcS (TcRef a)
@@ -2861,7 +2855,7 @@ Assume we have started with an implication:
 which we have simplified to:
 
   forall c. Eq c => { wc_simple = D [c] c [W]
-                    , wc_insols = (c ~ [c]) [D] }
+                                  (c ~ [c]) [D] }
 
 For some reason, e.g. because we floated an equality somewhere else,
 we might try to re-solve this implication. If we do not do a
@@ -2874,7 +2868,7 @@ constraints the second time:
 which will result in two Deriveds to end up in the insoluble set:
 
   wc_simple   = D [c] c [W]
-  wc_insols = (c ~ [c]) [D], (c ~ [c]) [D]
+               (c ~ [c]) [D], (c ~ [c]) [D]
 -}
 
 {- *********************************************************************
index 252708c..a5150e6 100644 (file)
@@ -124,7 +124,6 @@ simplifyTop wanteds
            ; TcM.writeTcRef errs_var emptyMessages
 
            ; warnAllUnsolved $ WC { wc_simple = unsafe_ol
-                                  , wc_insol = emptyCts
                                   , wc_impl = emptyBag }
 
            ; whyUnsafe <- fst <$> TcM.readTcRef errs_var
@@ -498,8 +497,7 @@ tcSubsumes ty_a ty_b = discardErrs $
     -- We don't want any insoluble or simple constraints left,
     -- but solved implications are ok (and neccessary for e.g. undefined)
     ; return (isEmptyBag (wc_simple rem)
-         && isEmptyBag (wc_insol rem)
-         && allBag (isSolvedStatus . ic_status) (wc_impl rem))
+              && allBag (isSolvedStatus . ic_status) (wc_impl rem))
     }
 
 ------------------
@@ -1267,13 +1265,14 @@ solveWantedsAndDrop wanted
 solveWanteds :: WantedConstraints -> TcS WantedConstraints
 -- so that the inert set doesn't mindlessly propagate.
 -- NB: wc_simples may be wanted /or/ derived now
-solveWanteds wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics })
+solveWanteds wc@(WC { wc_simple = simples, wc_impl = implics })
   = do { traceTcS "solveWanteds {" (ppr wc)
 
-       ; wc1 <- solveSimpleWanteds (simples `unionBags` insols)
-                -- Why solve 'insols'?  See Note [Rewrite insolubles] in TcSMonad
+       ; wc1 <- solveSimpleWanteds simples
+                -- Any insoluble constraints are in 'simples' and so get rewritten
+                -- See Note [Rewrite insolubles] in TcSMonad
 
-       ; let WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 } = wc1
+       ; let WC { wc_simple = simples1, wc_impl = implics1 } = wc1
 
        ; (floated_eqs, implics2) <- solveNestedImplications (implics `unionBags` implics1)
        ; (no_new_scs, simples2)  <- expandSuperClasses simples1
@@ -1285,7 +1284,6 @@ solveWanteds wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics
        ; final_wc <- simpl_loop 0 (solverIterations dflags) floated_eqs
                                 no_new_scs
                                 (WC { wc_simple = simples2
-                                    , wc_insol  = insols1
                                     , wc_impl   = implics2 })
 
        ; bb <- TcS.getTcEvBindsMap
@@ -1299,7 +1297,7 @@ simpl_loop :: Int -> IntWithInf -> Cts -> Bool
            -> WantedConstraints
            -> TcS WantedConstraints
 simpl_loop n limit floated_eqs no_new_deriveds
-           wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics })
+           wc@(WC { wc_simple = simples, wc_impl = implics })
   | isEmptyBag floated_eqs && no_new_deriveds
   = return wc  -- Done!
 
@@ -1330,14 +1328,13 @@ simpl_loop n limit floated_eqs no_new_deriveds
        -- solveSimples may make progress if either float_eqs hold
        ; (unifs1, wc1) <- reportUnifications $
                           solveSimpleWanteds $
-                          floated_eqs `unionBags` simples `unionBags` insols
+                          floated_eqs `unionBags` simples
             -- Notes:
-            --   - Why solve 'insols'?  See Note [Rewrite insolubles] in TcSMonad
             --   - Put floated_eqs first so they get solved first
             --     NB: the floated_eqs may include /derived/ equalities
             --     arising from fundeps inside an implication
 
-       ; let WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 } = wc1
+       ; let WC { wc_simple = simples1, wc_impl = implics1 } = wc1
        ; (no_new_scs, simples2) <- expandSuperClasses simples1
 
        -- We have already tried to solve the nested implications once
@@ -1350,7 +1347,6 @@ simpl_loop n limit floated_eqs no_new_deriveds
 
        ; simpl_loop (n+1) limit floated_eqs2 no_new_scs
                     (WC { wc_simple = simples2
-                        , wc_insol  = insols1
                         , wc_impl   = implics2 }) }
 
 
@@ -1451,6 +1447,8 @@ solveImplication imp@(Implic { ic_tclvl  = tclvl
        ; traceTcS "solveImplication 2"
            (ppr given_insols $$ ppr residual_wanted)
        ; let final_wanted = residual_wanted `addInsols` given_insols
+             -- Don't lose track of the insoluble givens,
+             -- which signal unreachable code; put them in ic_wanted
 
        ; res_implic <- setImplicationStatus (imp { ic_no_eqs = no_given_eqs
                                                  , ic_wanted = final_wanted })
@@ -1488,7 +1486,7 @@ setImplicationStatus implic@(Implic { ic_binds  = ev_binds_var
 
  | some_unsolved
  = do { traceTcS "setImplicationStatus" $
-        vcat [ppr givens $$ ppr simples $$ ppr insols $$ ppr mb_implic_needs]
+        vcat [ppr givens $$ ppr simples $$ ppr mb_implic_needs]
       ; return $ Just $
         implic { ic_status = IC_Unsolved
                , ic_needed = new_discarded_needs
@@ -1529,17 +1527,15 @@ setImplicationStatus implic@(Implic { ic_binds  = ev_binds_var
                  then Nothing
                  else Just final_implic }
  where
-   WC { wc_simple = simples, wc_impl = implics, wc_insol = insols } = wc
+   WC { wc_simple = simples, wc_impl = implics } = wc
 
    some_insoluble = insolubleWC wc
-   some_unsolved = not (isEmptyBag simples && isEmptyBag insols)
+   some_unsolved = not (isEmptyBag simples)
                  || isNothing mb_implic_needs
 
    pruned_simples = dropDerivedSimples simples
-   pruned_insols  = dropDerivedInsols insols
    (pruned_implics, discarded_needs) = partitionBagWith discard_me implics
    pruned_wc = wc { wc_simple = pruned_simples
-                  , wc_insol  = pruned_insols
                   , wc_impl   = pruned_implics }
    new_discarded_needs = foldrBag unionVarSet old_discarded_needs discarded_needs
 
@@ -1800,10 +1796,9 @@ approximateWC float_past_equalities wc
   where
     float_wc :: TcTyCoVarSet -> WantedConstraints -> Cts
     float_wc trapping_tvs (WC { wc_simple = simples, wc_impl = implics })
-      = filterBag is_floatable simples `unionBags`
+      = filterBag (is_floatable trapping_tvs) simples `unionBags`
         do_bag (float_implic trapping_tvs) implics
       where
-        is_floatable ct = tyCoVarsOfCt ct `disjointVarSet` trapping_tvs
 
     float_implic :: TcTyCoVarSet -> Implication -> Cts
     float_implic trapping_tvs imp
@@ -1813,9 +1808,16 @@ approximateWC float_past_equalities wc
       = emptyCts    -- See (1) under Note [ApproximateWC]
       where
         new_trapping_tvs = trapping_tvs `extendVarSetList` ic_skols imp
+
     do_bag :: (a -> Bag c) -> Bag a -> Bag c
     do_bag f = foldrBag (unionBags.f) emptyBag
 
+    is_floatable skol_tvs ct
+       | isGivenCt ct     = False
+       | isHoleCt ct      = False
+       | insolubleEqCt ct = False
+       | otherwise        = tyCoVarsOfCt ct `disjointVarSet` skol_tvs
+
 {- Note [ApproximateWC]
 ~~~~~~~~~~~~~~~~~~~~~~~
 approximateWC takes a constraint, typically arising from the RHS of a
@@ -2088,7 +2090,7 @@ usefulToFloat skol_set ct   -- The constraint is un-flattened and de-canonicalis
         typeKind ty1 `tcEqType` typeKind ty2
 
     has_heterogeneous_form = case ct of
-      CIrredEvCan {}   -> True
+      CIrredCan {}     -> True
       CNonCanonical {} -> True
       _                -> False
 
index 103c9cc..32614b7 100644 (file)
@@ -81,7 +81,7 @@ module TcType (
   hasIPPred, isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy,
   isPredTy, isTyVarClassPred, isTyVarExposed, isInsolubleOccursCheck,
   checkValidClsArgs, hasTyVarHead,
-  isRigidEqPred, isRigidTy,
+  isRigidTy,
 
   ---------------------------------
   -- Misc type manipulators
@@ -2203,21 +2203,6 @@ isRigidTy ty
   | isForAllTy ty                           = True
   | otherwise                               = False
 
-isRigidEqPred :: TcLevel -> PredTree -> Bool
--- ^ True of all Nominal equalities that are solidly insoluble
--- This means all equalities *except*
---   * Meta-tv non-SigTv on LHS
---   * Meta-tv SigTv on LHS, tyvar on right
-isRigidEqPred tc_lvl (EqPred NomEq ty1 _)
-  | Just tv1 <- tcGetTyVar_maybe ty1
-  = ASSERT2( tcIsTcTyVar tv1, ppr tv1 )
-    not (isMetaTyVar tv1) || isTouchableMetaTyVar tc_lvl tv1
-
-  | otherwise  -- LHS is not a tyvar
-  = True
-
-isRigidEqPred _ _ = False  -- Not an equality
-
 {-
 ************************************************************************
 *                                                                      *
index 88004bb..ec68e81 100644 (file)
@@ -1,9 +1,15 @@
 
 T3621.hs:24:43: error:
-    • No instance for (MonadState state (State s))
-        arising from the 'deriving' clause of a data type declaration
-      Possible fix:
-        use a standalone 'deriving instance' declaration,
-          so you can specify the instance context yourself
+    • Couldn't match type ‘s’ with ‘state’
+        arising from a functional dependency between:
+          constraint ‘MonadState state (State s)’
+            arising from the 'deriving' clause of a data type declaration
+          instance ‘MonadState s1 (State s1)’ at T3621.hs:21:10-31
+      ‘s’ is a rigid type variable bound by
+        the deriving clause for ‘MonadState state (WrappedState s)’
+        at T3621.hs:24:43-58
+      ‘state’ is a rigid type variable bound by
+        the deriving clause for ‘MonadState state (WrappedState s)’
+        at T3621.hs:24:43-58
     • When deriving the instance for (MonadState
                                         state (WrappedState s))
index 52d5440..666ddd0 100644 (file)
@@ -14,4 +14,4 @@ callCont :: Continuation c => c -> (Z c) -> (B c) -> Maybe (F c)
 callCont c z b = rpt (4 :: Int) c z b
     where
         rpt 0 c' z' b' = fromJust (fst <$> (continue c' z' b'))
-        rpt i c' z' b' = let c'' = fromJust (snd <$> (continue c' z' b')) in rpt (i-1) c''
\ No newline at end of file
+        rpt i c' z' b' = let c'' = fromJust (snd <$> (continue c' z' b')) in rpt (i-1) c''
index c57c59b..3342cf7 100644 (file)
@@ -1,7 +1,7 @@
 
 tc211.hs:20:8: error:
     • Couldn't match expected type ‘forall a. a -> a’
-                  with actual type ‘a1 -> a1
+                  with actual type ‘a3 -> a3
     • In the expression:
           (:) ::
             (forall a. a -> a) -> [forall a. a -> a] -> [forall a. a -> a]
@@ -16,15 +16,15 @@ tc211.hs:20:8: error:
                 (head foo) foo
 
 tc211.hs:25:8: error:
-    • Couldn't match type ‘a3 -> a3’ with ‘forall a. a -> a’
+    • Couldn't match type ‘a1 -> a1’ with ‘forall a. a -> a’
       Expected type: [forall a. a -> a]
-        Actual type: [a3 -> a3]
+        Actual type: [a1 -> a1]
     • In the expression: (head foo) : (tail foo)
       In an equation for ‘barr’: barr = (head foo) : (tail foo)
 
 tc211.hs:25:20: error:
-    • Couldn't match type ‘forall a. a -> a’ with ‘a3 -> a3
-      Expected type: [a3 -> a3]
+    • Couldn't match type ‘forall a. a -> a’ with ‘a1 -> a1
+      Expected type: [a1 -> a1]
         Actual type: [forall a. a -> a]
     • In the second argument of ‘(:)’, namely ‘(tail foo)’
       In the expression: (head foo) : (tail foo)
@@ -32,7 +32,7 @@ tc211.hs:25:20: error:
 
 tc211.hs:62:18: error:
     • Couldn't match expected type ‘forall a. a -> a’
-                  with actual type ‘a0 -> a0
+                  with actual type ‘a2 -> a2
     • In the expression:
           Cons ::
             (forall a. a -> a)
@@ -52,21 +52,21 @@ tc211.hs:62:18: error:
 
 tc211.hs:68:8: error:
     • Couldn't match expected type ‘forall a. a -> a’
-                  with actual type ‘a2 -> a2
+                  with actual type ‘a0 -> a0
     • In the expression:
           Cons ::
             ((forall a. a -> a)
-            -> List (forall a. a -> a) -> List (forall a. a -> a))
+             -> List (forall a. a -> a) -> List (forall a. a -> a))
       In the expression:
         (Cons ::
            ((forall a. a -> a)
-           -> List (forall a. a -> a) -> List (forall a. a -> a)))
+            -> List (forall a. a -> a) -> List (forall a. a -> a)))
           (\ x -> x) Nil
       In an equation for ‘xs2’:
           xs2
             = (Cons ::
                  ((forall a. a -> a)
-                 -> List (forall a. a -> a) -> List (forall a. a -> a)))
+                  -> List (forall a. a -> a) -> List (forall a. a -> a)))
                 (\ x -> x) Nil
 
 tc211.hs:76:9: error:
index f77d645..5e92f3a 100644 (file)
@@ -1,8 +1,8 @@
 
-T12589.hs:13:3: error: Variable not in scope: (&) :: t0 -> t1 -> t
+T12589.hs:13:3: error: Variable not in scope: (&) :: t1 -> t0 -> t
 
 T12589.hs:13:5: error:
-    • Cannot instantiate unification variable ‘t1
+    • Cannot instantiate unification variable ‘t0
       with a type involving foralls:
         (forall a. Bounded a => f0 a) -> h0 f0 xs0
         GHC doesn't yet support impredicative polymorphism
index 923f378..d739d21 100644 (file)
@@ -1,7 +1,7 @@
 
 T13311.hs:9:3: error:
-    • Couldn't match expected type ‘IO a1
-                  with actual type ‘Maybe a0 -> Maybe b0’
+    • Couldn't match expected type ‘IO a0
+                  with actual type ‘Maybe a1 -> Maybe b0’
     • Probable cause: ‘f’ is applied to too few arguments
       In a stmt of a 'do' block: f
       In the expression:
index 1a0274f..0e1964e 100644 (file)
@@ -1,7 +1,7 @@
 
 T7851.hs:5:10: error:
-    • Couldn't match expected type ‘IO a1
-                  with actual type ‘a0 -> IO ()’
+    • Couldn't match expected type ‘IO a0
+                  with actual type ‘a1 -> IO ()’
     • Probable cause: ‘print’ is applied to too few arguments
       In a stmt of a 'do' block: print
       In the expression:
index 2ee5ad4..d22d13f 100644 (file)
@@ -1,9 +1,6 @@
 
 T8603.hs:33:17: error:
-    • Couldn't match kind ‘* -> *’ with ‘*’
-      When matching types
-        t0 :: (* -> *) -> * -> *
-        (->) :: * -> * -> *
+    • Couldn't match type ‘RV a1’ with ‘StateT s RV a0’
       Expected type: [Integer] -> StateT s RV a0
         Actual type: t0 ((->) [a1]) (RV a1)
     • The function ‘lift’ is applied to two arguments,
@@ -13,3 +10,5 @@ T8603.hs:33:17: error:
       In the expression:
         do prize <- lift uniform [1, 2, ....]
            return False
+    • Relevant bindings include
+        testRVState1 :: RVState s Bool (bound at T8603.hs:32:1)
index 29a1576..0ac1419 100644 (file)
@@ -1,6 +1,6 @@
 
 tcfail122.hs:8:9: error:
-    • Couldn't match kind ‘* -> *’ with ‘*’
+    • Couldn't match kind ‘*’ with ‘* -> *’
       When matching types
         c0 :: (* -> *) -> *
         a :: * -> *
index 15dedf0..532ca18 100644 (file)
@@ -1,6 +1,6 @@
 
 CaretDiagnostics1.hs:(5,3)-(7,16): error:
-    • Couldn't match expected type ‘IO a1’ with actual type ‘Int’
+    • Couldn't match expected type ‘IO a0’ with actual type ‘Int’
     • In a stmt of a 'do' block:
         10000000000000000000000000000000000000 + 2 + (3 :: Int)
       In the expression:
@@ -45,7 +45,7 @@ CaretDiagnostics1.hs:8:31-44: error:
   |                               ^^^^^^^^^^^^^^
 
 CaretDiagnostics1.hs:13:7-11: error:
-    • Couldn't match expected type ‘a0 -> a0’ with actual type ‘[Char]’
+    • Couldn't match expected type ‘a1 -> a1’ with actual type ‘[Char]’
     • In the pattern: "γηξ"
       In a case alternative: "γηξ" -> () '0'
       In the expression: case id of { "γηξ" -> () '0' }