Better solving for representational equalities
authorSimon Peyton Jones <simonpj@microsoft.com>
Tue, 17 Oct 2017 15:32:25 +0000 (16:32 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Wed, 18 Oct 2017 07:31:01 +0000 (08:31 +0100)
This patch adds a bit of extra solving power for representational
equality constraints to fix Trac #14333

The main changes:

* Fix a buglet in TcType.isInsolubleOccursCheck which wrongly
  reported a definite occurs-check error for (a ~R# b a)

* Get rid of TcSMonad.emitInsolubles.  It had an ad-hoc duplicate-removal
  piece that is better handled in interactIrred, now that insolubles
  are Irreds.

  We need a little care to keep inert_count (which does not include
  insolubles) accurate.

* Refactor TcInteract.solveOneFromTheOther, to return a much simpler
  type.  It was just over-complicated before.

* Make TcInteract.interactIrred look for constraints that match
  either way around, in TcInteract.findMatchingIrreds

This wasn't hard and it cleaned up quite a bit of code.

compiler/typecheck/TcCanonical.hs
compiler/typecheck/TcInteract.hs
compiler/typecheck/TcSMonad.hs
compiler/typecheck/TcType.hs
testsuite/tests/typecheck/should_compile/T14333.hs [new file with mode: 0644]
testsuite/tests/typecheck/should_compile/all.T
testsuite/tests/typecheck/should_fail/FrozenErrorTests.hs

index 39f2def..e7f1259 100644 (file)
@@ -513,8 +513,8 @@ canHole ev hole
   = do { let ty = ctEvPred ev
        ; (xi,co) <- flatten FM_SubstOnly ev ty -- co :: xi ~ ty
        ; rewriteEvidence ev xi co `andWhenContinue` \ new_ev ->
-    do { emitInsoluble (CHoleCan { cc_ev = new_ev
-                                 , cc_hole = hole })
+    do { updInertIrreds (`snocCts` (CHoleCan { cc_ev = new_ev
+                                             , cc_hole = hole }))
        ; stopWith new_ev "Emit insoluble hole" } }
 
 {-
@@ -1310,8 +1310,7 @@ canEqHardFailure ev ty1 ty2
        ; (s2, co2) <- flatten FM_SubstOnly ev ty2
        ; rewriteEqEvidence ev NotSwapped s1 s2 co1 co2
          `andWhenContinue` \ new_ev ->
-    do { emitInsoluble (mkInsolubleCt new_ev)
-       ; stopWith new_ev "Definitely not equal" }}
+         continueWith (mkInsolubleCt new_ev) }
 
 {-
 Note [Decomposing TyConApps]
@@ -1555,21 +1554,18 @@ 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 (mkInsolubleCt new_ev)
+         then continueWith (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
-                 ; stopWith new_ev "Occurs check" }
 
+         else continueWith (mkIrredCt new_ev) }
              -- A representational equality with an occurs-check problem isn't
              -- insoluble! For example:
              --   a ~R b a
              -- We might learn that b is the newtype Id.
              -- But, the occurs-check certainly prevents the equality from being
              -- 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 (mkIrredCt new_ev) } }
   where
     role = eqRelRole eq_rel
 
index c9c647d..04ff0f8 100644 (file)
@@ -259,8 +259,9 @@ runTcPluginsGiven
        ; if null givens then return [] else
     do { p <- runTcPlugins plugins (givens,[],[])
        ; let (solved_givens, _, _) = pluginSolvedCts p
+             insols                = pluginBadCts p
        ; updInertCans (removeInertCts solved_givens)
-       ; mapM_ emitInsoluble (pluginBadCts p)
+       ; updInertIrreds (\irreds -> extendCtsList irreds insols)
        ; return (pluginNewCts p) } } }
 
 -- | Given a bag of (flattened, zonked) wanteds, invoke the plugins on
@@ -484,8 +485,6 @@ or, equivalently,
 
 -- Interaction result of  WorkItem <~> Ct
 
-type StopNowFlag = Bool    -- True <=> stop after this interaction
-
 interactWithInertsStage :: WorkItem -> TcS (StopOrContinue Ct)
 -- Precondition: if the workitem is a CTyEqCan then it will not be able to
 -- react with anything at this stage.
@@ -503,58 +502,63 @@ interactWithInertsStage wi
                 -- CNonCanonical have been canonicalised
 
 data InteractResult
-   = IRKeep      -- Keep the existing inert constraint in the inert set
-   | IRReplace   -- Replace the existing inert constraint with the work item
-   | IRDelete    -- Delete the existing inert constraint from the inert set
+   = KeepInert   -- Keep the inert item, and solve the work item from it
+                 -- (if the latter is Wanted; just discard it if not)
+   | KeepWork    -- Keep the work item, and solve the intert item from it
 
 instance Outputable InteractResult where
-  ppr IRKeep    = text "keep"
-  ppr IRReplace = text "replace"
-  ppr IRDelete  = text "delete"
+  ppr KeepInert = text "keep inert"
+  ppr KeepWork  = text "keep work-item"
 
 solveOneFromTheOther :: CtEvidence  -- Inert
                      -> CtEvidence  -- WorkItem
-                     -> TcS (InteractResult, StopNowFlag)
--- Preconditions:
--- 1) inert and work item represent evidence for the /same/ predicate
--- 2) ip/class/irred constraints only; not used for equalities
+                     -> TcS InteractResult
+-- Precondition:
+-- * inert and work item represent evidence for the /same/ predicate
+--
+-- We can always solve one from the other: even if both are wanted,
+-- although we don't rewrite wanteds with wanteds, we can combine
+-- two wanteds into one by solving one from the other
+
 solveOneFromTheOther ev_i ev_w
   | isDerived ev_w         -- Work item is Derived; just discard it
-  = return (IRKeep, True)
+  = return KeepInert
 
-  | isDerived ev_i            -- The inert item is Derived, we can just throw it away,
-  = return (IRDelete, False)  -- The ev_w is inert wrt earlier inert-set items,
-                              -- so it's safe to continue on from this point
+  | isDerived ev_i     -- The inert item is Derived, we can just throw it away,
+  = return KeepWork    -- The ev_w is inert wrt earlier inert-set items,
+                       -- so it's safe to continue on from this point
 
   | CtWanted { ctev_loc = loc_w } <- ev_w
   , prohibitedSuperClassSolve (ctEvLoc ev_i) loc_w
-  = do { traceTcS "prohibitedClassSolve1" (ppr ev_i $$ ppr ev_w)
-       ; return (IRDelete, False) }
+  = -- inert must be Given
+    do { traceTcS "prohibitedClassSolve1" (ppr ev_i $$ ppr ev_w)
+       ; return KeepWork }
 
-  | CtWanted { ctev_dest = dest } <- ev_w
+  | CtWanted {} <- ev_w
        -- Inert is Given or Wanted
-  = do { setWantedEvTerm dest (ctEvTerm ev_i)
-       ; return (IRKeep, True) }
+  = return KeepInert
+
+  -- From here on the work-item is Given
 
-  | CtWanted { ctev_loc = loc_i } <- ev_i   -- Work item is Given
+  | CtWanted { ctev_loc = loc_i } <- ev_i
   , prohibitedSuperClassSolve (ctEvLoc ev_w) loc_i
   = do { traceTcS "prohibitedClassSolve2" (ppr ev_i $$ ppr ev_w)
-       ; return (IRKeep, False) } -- Just discard the un-usable Given
-                                  -- This never actually happens because
-                                  -- Givens get processed first
+       ; return KeepInert }      -- Just discard the un-usable Given
+                                 -- This never actually happens because
+                                 -- Givens get processed first
 
-  | CtWanted { ctev_dest = dest } <- ev_i
-  = do { setWantedEvTerm dest (ctEvTerm ev_w)
-       ; return (IRReplace, True) }
+  | CtWanted {} <- ev_i
+  = return KeepWork
 
-  -- So they are both Given
+  -- From here on both are Given
   -- See Note [Replacement vs keeping]
+
   | lvl_i == lvl_w
   = do { binds <- getTcEvBindsMap
-       ; return (same_level_strategy binds, True) }
+       ; return (same_level_strategy binds) }
 
   | otherwise   -- Both are Given, levels differ
-  = return (different_level_strategy, True)
+  = return (different_level_strategy)
   where
      pred  = ctEvPred ev_i
      loc_i = ctEvLoc ev_i
@@ -563,25 +567,26 @@ solveOneFromTheOther ev_i ev_w
      lvl_w = ctLocLevel loc_w
 
      different_level_strategy
-       | isIPPred pred, lvl_w > lvl_i = IRReplace
-       | lvl_w < lvl_i                = IRReplace
-       | otherwise                    = IRKeep
+       | isIPPred pred, lvl_w > lvl_i = KeepWork
+       | lvl_w < lvl_i                = KeepWork
+       | otherwise                    = KeepInert
 
      same_level_strategy binds        -- Both Given
        | GivenOrigin (InstSC s_i) <- ctLocOrigin loc_i
        = case ctLocOrigin loc_w of
-            GivenOrigin (InstSC s_w) | s_w < s_i -> IRReplace
-                                     | otherwise -> IRKeep
-            _                                    -> IRReplace
+            GivenOrigin (InstSC s_w) | s_w < s_i -> KeepWork
+                                     | otherwise -> KeepInert
+            _                                    -> KeepWork
 
        | GivenOrigin (InstSC {}) <- ctLocOrigin loc_w
-       = IRKeep
+       = KeepInert
 
        | has_binding binds ev_w
        , not (has_binding binds ev_i)
-       = IRReplace
+       = KeepWork
 
-       | otherwise = IRKeep
+       | otherwise
+       = KeepInert
 
      has_binding binds ev = isJust (lookupEvBind binds (ctEvId ev))
 
@@ -658,31 +663,130 @@ 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@(CIrredCan { cc_ev = ev_w })
-  | let pred = ctEvPred ev_w
-        (matching_irreds, others)
-          = partitionBag (\ct -> ctPred ct `tcEqTypeNoKindCheck` pred)
-                         (inert_irreds inerts)
-  , (ct_i : rest) <- bagToList matching_irreds
-  , let ctev_i = ctEvidence ct_i
+interactIrred inerts workItem@(CIrredCan { cc_ev = ev_w, cc_insol = insoluble })
+  | insoluble  -- For insolubles, don't allow the constaint to be dropped
+               -- which can happen with solveOneFromTheOther, so that
+               -- we get distinct error messages with -fdefer-type-errors
+               -- See Note [Do not add duplicate derived insolubles]
+  , not (isDroppableDerivedCt workItem)
+  = continueWith workItem
+
+  | let (matching_irreds, others) = findMatchingIrreds (inert_irreds inerts) ev_w
+  , ((ct_i, swap) : rest) <- bagToList matching_irreds
+  , let ev_i = ctEvidence ct_i
   = ASSERT( null rest )
-    do { (inert_effect, stop_now) <- solveOneFromTheOther ctev_i ev_w
-       ; case inert_effect of
-            IRKeep    -> return ()
-            IRDelete  -> updInertIrreds (\_ -> others)
-            IRReplace -> updInertIrreds (\_ -> others `snocCts` workItem)
-                         -- These const upd's assume that solveOneFromTheOther
-                         -- has no side effects on InertCans
-       ; if stop_now then
-            return (Stop ev_w (text "Irred equal" <+> parens (ppr inert_effect)))
-       ; else
-            continueWith workItem }
+    do { what_next <- solveOneFromTheOther ev_i ev_w
+       ; traceTcS "iteractIrred" (ppr workItem $$ ppr what_next $$ ppr ct_i)
+       ; case what_next of
+            KeepInert -> do { setEvBindIfWanted ev_w (swap_me swap ev_i)
+                            ; return (Stop ev_w (text "Irred equal" <+> parens (ppr what_next))) }
+            KeepWork ->  do { setEvBindIfWanted ev_i (swap_me swap ev_w)
+                            ; updInertIrreds (\_ -> others)
+                            ; continueWith workItem } }
 
   | otherwise
   = continueWith workItem
 
+  where
+    swap_me :: SwapFlag -> CtEvidence -> EvTerm
+    swap_me swap ev
+      = case swap of
+           NotSwapped -> ctEvTerm ev
+           IsSwapped  -> EvCoercion (mkTcSymCo (evTermCoercion (ctEvTerm ev)))
+
 interactIrred _ wi = pprPanic "interactIrred" (ppr wi)
 
+findMatchingIrreds :: Cts -> CtEvidence -> (Bag (Ct, SwapFlag), Bag Ct)
+findMatchingIrreds irreds ev
+  | EqPred eq_rel1 lty1 rty1 <- classifyPredType pred
+    -- See Note [Solving irreducible equalities]
+  = partitionBagWith (match_eq eq_rel1 lty1 rty1) irreds
+  | otherwise
+  = partitionBagWith match_non_eq irreds
+  where
+    pred = ctEvPred ev
+    match_non_eq ct
+      | ctPred ct `tcEqTypeNoKindCheck` pred = Left (ct, NotSwapped)
+      | otherwise                            = Right ct
+
+    match_eq eq_rel1 lty1 rty1 ct
+      | EqPred eq_rel2 lty2 rty2 <- classifyPredType (ctPred ct)
+      , eq_rel1 == eq_rel2
+      , Just swap <- match_eq_help lty1 rty1 lty2 rty2
+      = Left (ct, swap)
+      | otherwise
+      = Right ct
+
+    match_eq_help lty1 rty1 lty2 rty2
+      | lty1 `tcEqTypeNoKindCheck` lty2, rty1 `tcEqTypeNoKindCheck` rty2
+      = Just NotSwapped
+      | lty1 `tcEqTypeNoKindCheck` rty2, rty1 `tcEqTypeNoKindCheck` lty2
+      = Just IsSwapped
+      | otherwise
+      = Nothing
+
+{- Note [Solving irreducible equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider (Trac #14333)
+  [G] a b ~R# c d
+  [W] c d ~R# a b
+Clearly we should be able to solve this! Even though the constraints are
+not decomposable. We solve this when looking up the work-item in the
+irreducible constraints to look for an identical one.  When doing this
+lookup, findMatchingIrreds spots the equality case, and matches either
+way around. It has to return a swap-flag so we can generate evidence
+that is the right way round too.
+
+Note [Do not add duplicate derived insolubles]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In general we *must* add an insoluble (Int ~ Bool) even if there is
+one such there already, because they may come from distinct call
+sites.  Not only do we want an error message for each, but with
+-fdefer-type-errors we must generate evidence for each.  But for
+*derived* insolubles, we only want to report each one once.  Why?
+
+(a) A constraint (C r s t) where r -> s, say, may generate the same fundep
+    equality many times, as the original constraint is successively rewritten.
+
+(b) Ditto the successive iterations of the main solver itself, as it traverses
+    the constraint tree. See example below.
+
+Also for *given* insolubles we may get repeated errors, as we
+repeatedly traverse the constraint tree.  These are relatively rare
+anyway, so removing duplicates seems ok.  (Alternatively we could take
+the SrcLoc into account.)
+
+Note that the test does not need to be particularly efficient because
+it is only used if the program has a type error anyway.
+
+Example of (b): assume a top-level class and instance declaration:
+
+  class D a b | a -> b
+  instance D [a] [a]
+
+Assume we have started with an implication:
+
+  forall c. Eq c => { wc_simple = D [c] c [W] }
+
+which we have simplified to:
+
+  forall c. Eq c => { wc_simple = D [c] c [W]
+                                  (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
+dropDerivedWC, then we will end up trying to solve the following
+constraints the second time:
+
+  (D [c] c) [W]
+  (c ~ [c]) [D]
+
+which will result in two Deriveds to end up in the insoluble set:
+
+  wc_simple   = D [c] c [W]
+               (c ~ [c]) [D], (c ~ [c]) [D]
+-}
+
 {-
 *********************************************************************************
 *                                                                               *
@@ -864,32 +968,29 @@ IncoherentInstances is `1`. If we were to do the optimization, the output of
 
 interactDict :: InertCans -> Ct -> TcS (StopOrContinue Ct)
 interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs = tys })
-  | Just ctev_i <- lookupInertDict inerts (ctEvLoc ev_w) cls tys
+  | Just ev_i <- lookupInertDict inerts (ctEvLoc ev_w) cls tys
   = -- There is a matching dictionary in the inert set
     do { -- First to try to solve it /completely/ from top level instances
          -- See Note [Shortcut solving]
          dflags <- getDynFlags
-       ; try_inst_res <- shortCutSolver dflags ev_w ctev_i
+       ; try_inst_res <- shortCutSolver dflags ev_w ev_i
        ; case try_inst_res of
-           Just evs -> do
-             { flip mapM_ evs $ \(ev_t, ct_ev, cls, typ) -> do
-               { setWantedEvBind (ctEvId ct_ev) ev_t
-               ; addSolvedDict ct_ev cls typ }
-             ; stopWith ev_w "interactDict/solved from instance" }
+           Just evs -> do { flip mapM_ evs $ \ (ev_t, ct_ev, cls, typ) ->
+                               do { setWantedEvBind (ctEvId ct_ev) ev_t
+                                  ; addSolvedDict ct_ev cls typ }
+                          ; stopWith ev_w "interactDict/solved from instance" }
 
            -- We were unable to solve the [W] constraint from in-scope instances
            -- so we solve it from the matching inert we found
            Nothing ->  do
-             { (inert_effect, stop_now) <- solveOneFromTheOther ctev_i ev_w
-             ; traceTcS "lookupInertDict" (ppr inert_effect <+> ppr stop_now)
-             ; case inert_effect of
-                 IRKeep    -> return ()
-                 IRDelete  -> updInertDicts $ \ ds -> delDict ds cls tys
-                 IRReplace -> updInertDicts $ \ ds -> addDict ds cls tys workItem
-             ; if stop_now then
-                 return $ Stop ev_w (text "Dict equal" <+> parens (ppr inert_effect))
-               else
-                 continueWith workItem } }
+             { what_next <- solveOneFromTheOther ev_i ev_w
+             ; traceTcS "lookupInertDict" (ppr what_next)
+             ; case what_next of
+                 KeepInert -> do { setEvBindIfWanted ev_w (ctEvTerm ev_i)
+                                 ; return $ Stop ev_w (text "Dict equal" <+> parens (ppr what_next)) }
+                 KeepWork  -> do { setEvBindIfWanted ev_i (ctEvTerm ev_w)
+                                 ; updInertDicts $ \ ds -> delDict ds cls tys
+                                 ; continueWith workItem } } }
 
   | cls `hasKey` ipClassKey
   , isGiven ev_w
@@ -908,9 +1009,9 @@ shortCutSolver :: DynFlags
                -> TcS (Maybe [(EvTerm, CtEvidence, Class, [TcPredType])])
                       -- Everything we need to bind a solution for the work item
                       -- and add the solved Dict to the cache in the main solver.
-shortCutSolver dflags ev_w ctev_i
+shortCutSolver dflags ev_w ev_i
   | isWanted ev_w
- && isGiven ctev_i
+ && isGiven ev_i
  -- We are about to solve a [W] constraint from a [G] constraint. We take
  -- a moment to see if we can get a better solution using an instance.
  -- Note that we only do this for the sake of performance. Exactly the same
index 6bc08ce..3038def 100644 (file)
@@ -57,7 +57,7 @@ module TcSMonad (
     getUnsolvedInerts,
     removeInertCts, getPendingScDicts,
     addInertCan, addInertEq, insertFunEq,
-    emitInsoluble, emitWorkNC, emitWork,
+    emitWorkNC, emitWork,
     isImprovable,
 
     -- The Model
@@ -251,8 +251,16 @@ workListSize (WL { wl_eqs = eqs, wl_funeqs = funeqs, wl_deriv = ders, wl_rest =
   = length eqs + length funeqs + length rest + length ders
 
 workListWantedCount :: WorkList -> Int
+-- Count the things we need to solve
+-- excluding the insolubles (c.f. inert_count)
 workListWantedCount (WL { wl_eqs = eqs, wl_rest = rest })
-  = count isWantedCt eqs + count isWantedCt rest
+  = count isWantedCt eqs + count is_wanted rest
+  where
+    is_wanted ct
+     | CIrredCan { cc_ev = ev, cc_insol = insol } <- ct
+     = not insol && isWanted ev
+     | otherwise
+     = isWantedCt ct
 
 extendWorkListEq :: Ct -> WorkList -> WorkList
 extendWorkListEq ct wl = wl { wl_eqs = ct : wl_eqs wl }
@@ -1416,14 +1424,12 @@ 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@(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
-       -- to an equality.
-       -- But since we try to simplify first, if there's a constraint function FC with
-       --    type instance FC Int = Show
-       -- we'll reduce a constraint (FC Int a) to Show a, and never add an inert irreducible
+add_item ics@(IC { inert_irreds = irreds, inert_count = count })
+         item@(CIrredCan { cc_ev = ev, cc_insol = insoluble })
+  = ics { inert_irreds = irreds `Bag.snocBag` item
+        , inert_count  = if insoluble
+                         then count  -- inert_count does not include insolubles
+                         else bumpUnsolvedCount ev count }
 
 add_item ics item@(CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys })
   = ics { inert_dicts = addDict (inert_dicts ics) cls tys item
@@ -2664,21 +2670,6 @@ emitWork cts
   = do { traceTcS "Emitting fresh work" (vcat (map ppr cts))
        ; updWorkListTcS (extendWorkListCts cts) }
 
-emitInsoluble :: Ct -> TcS ()
--- Emits a non-canonical constraint that will stand for a frozen error in the inerts.
-emitInsoluble ct
-  = do { traceTcS "Emit insoluble" (ppr ct $$ pprCtLoc (ctLoc ct))
-       ; updInertTcS add_insol }
-  where
-    this_pred = ctPred ct
-    add_insol is@(IS { inert_cans = ics@(IC { inert_irreds = old_irreds }) })
-      | drop_it   = is
-      | otherwise = is { inert_cans = ics { inert_irreds = old_irreds `snocCts` ct } }
-      where
-        drop_it = isDroppableDerivedCt ct &&
-                  anyBag (tcEqType this_pred . ctPred) old_irreds
-             -- See Note [Do not add duplicate derived insolubles]
-
 newTcRef :: a -> TcS (TcRef a)
 newTcRef x = wrapTcS (TcM.newTcRef x)
 
@@ -2820,56 +2811,6 @@ zonkSimples cts = wrapTcS (TcM.zonkSimples cts)
 zonkWC :: WantedConstraints -> TcS WantedConstraints
 zonkWC wc = wrapTcS (TcM.zonkWC wc)
 
-{-
-Note [Do not add duplicate derived insolubles]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-In general we *must* add an insoluble (Int ~ Bool) even if there is
-one such there already, because they may come from distinct call
-sites.  Not only do we want an error message for each, but with
--fdefer-type-errors we must generate evidence for each.  But for
-*derived* insolubles, we only want to report each one once.  Why?
-
-(a) A constraint (C r s t) where r -> s, say, may generate the same fundep
-    equality many times, as the original constraint is successively rewritten.
-
-(b) Ditto the successive iterations of the main solver itself, as it traverses
-    the constraint tree. See example below.
-
-Also for *given* insolubles we may get repeated errors, as we
-repeatedly traverse the constraint tree.  These are relatively rare
-anyway, so removing duplicates seems ok.  (Alternatively we could take
-the SrcLoc into account.)
-
-Note that the test does not need to be particularly efficient because
-it is only used if the program has a type error anyway.
-
-Example of (b): assume a top-level class and instance declaration:
-
-  class D a b | a -> b
-  instance D [a] [a]
-
-Assume we have started with an implication:
-
-  forall c. Eq c => { wc_simple = D [c] c [W] }
-
-which we have simplified to:
-
-  forall c. Eq c => { wc_simple = D [c] c [W]
-                                  (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
-dropDerivedWC, then we will end up trying to solve the following
-constraints the second time:
-
-  (D [c] c) [W]
-  (c ~ [c]) [D]
-
-which will result in two Deriveds to end up in the insoluble set:
-
-  wc_simple   = D [c] c [W]
-               (c ~ [c]) [D], (c ~ [c]) [D]
--}
 
 {- *********************************************************************
 *                                                                      *
index 32614b7..4d65fcd 100644 (file)
@@ -2181,7 +2181,9 @@ isInsolubleOccursCheck eq_rel tv ty
     go ty | Just ty' <- tcView ty = go ty'
     go (TyVarTy tv') = tv == tv' || go (tyVarKind tv')
     go (LitTy {})    = False
-    go (AppTy t1 t2) = go t1 || go t2
+    go (AppTy t1 t2) = case eq_rel of  -- See Note [AppTy and ReprEq]
+                         NomEq  -> go t1 || go t2
+                         ReprEq -> go t1
     go (FunTy t1 t2) = go t1 || go t2
     go (ForAllTy (TvBndr tv' _) inner_ty)
       | tv' == tv = False
@@ -2196,6 +2198,18 @@ isInsolubleOccursCheck eq_rel tv ty
 
     role = eqRelRole eq_rel
 
+{- Note [AppTy and ReprEq]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider   a ~R# b a
+           a ~R# a b
+
+The former is /not/ a definite error; we might instantiate 'b' with Id
+   newtype Id a = MkId a
+but the latter /is/ a definite error.
+
+On the other hand, with nominal equality, both are definite errors
+-}
+
 isRigidTy :: TcType -> Bool
 isRigidTy ty
   | Just (tc,_) <- tcSplitTyConApp_maybe ty = isGenerativeTyCon tc Nominal
diff --git a/testsuite/tests/typecheck/should_compile/T14333.hs b/testsuite/tests/typecheck/should_compile/T14333.hs
new file mode 100644 (file)
index 0000000..f4cd3bd
--- /dev/null
@@ -0,0 +1,20 @@
+module T14333 where
+
+import Data.Coerce
+
+bad :: Coercible (a b) (c d) => c d -> a b
+bad = coerce
+
+bad2 :: Coercible (c d) (a b) => c d -> a b
+bad2 = coerce
+
+bad3 :: Coercible (a b) b => b -> a b
+bad3 = coerce
+
+bad4 :: Coercible b (a b) => b -> a b
+bad4 = coerce
+
+newtype Id a = MkId a
+
+foo :: Id Int
+foo = bad3 (3 :: Int)
index 6f855df..ac18cce 100644 (file)
@@ -577,3 +577,4 @@ test('T14149', normal, compile, [''])
 test('T14154', normal, compile, [''])
 test('T14158', normal, compile, [''])
 test('T13943', normal, compile, ['-fsolve-constant-dicts'])
+test('T14333', normal, compile, [''])
index 390333c..ae29c2d 100644 (file)
@@ -1,23 +1,23 @@
 {-# LANGUAGE RankNTypes, GADTs, TypeFamilies #-}
-module Test where 
+module Test where
 
 
-data T a where 
-  MkT :: a -> T a 
-  MkT3 :: forall a. (a ~ Bool) => T a 
+data T a where
+  MkT :: a -> T a
+  MkT3 :: forall a. (a ~ Bool) => T a
 
--- Mismatches in givens 
-bloh :: T Int -> () 
-bloh x = case x of 
-           MkT3 -> () 
+-- Mismatches in givens
+bloh :: T Int -> ()
+bloh x = case x of
+           MkT3 -> ()
 
-type family F a b 
+type family F a b
 type family G a b
-type instance F a Bool = a 
+type instance F a Bool = a
 type instance G a Char = a
 
 goo1 :: forall a b. (F a b ~ [a]) => b -> a  -> a
-goo1 = undefined 
+goo1 = undefined
 
 goo2 :: forall a. G a Char ~ [Int] => a -> a
 goo2 = undefined
@@ -31,16 +31,16 @@ test3 = goo1 False (goo2 undefined)
 
 
 -- A frozen occurs check, now transformed to both a decomposition and occurs check
-data M a where 
-  M :: M a 
+data M a where
+  M :: M a
 data T2 a b where
-  T2 :: T2 a b 
+  T2 :: T2 a b
 
-goo3 :: forall a b. F a b ~ T2 (M a) a => b -> a -> a 
+goo3 :: forall a b. F a b ~ T2 (M a) a => b -> a -> a
 goo3 = undefined
 
 goo4 :: forall a c. G a Char ~ T2 (T2 c c) c => a -> a
-goo4 = undefined 
+goo4 = undefined
 
 test4 = goo4 (goo3 False undefined)
 test5 = goo3 False (goo4 undefined)