Use an Implication in 'deriving' error

Trac #11437 showed that erroneous constraints from a 'deriving'
clause need to be wrapped in an Implication to properly scope
their skolems.

The main change is in TcDeriv.simplifyDeriv; the call to
buildImplicationFor is new.

7 files changed, 59 insertions, 24 deletions

diff --git a/compiler/typecheck/TcDeriv.hs b/compiler/typecheck/TcDeriv.hs
index 6a0e6cbcdd..3abc491a14 100644
--- a/compiler/typecheck/TcDeriv.hs
+++ b/compiler/typecheck/TcDeriv.hs
@@ -29,6 +29,7 @@ import FamInstEnv
 import TcHsType
 import TcMType
 import TcSimplify
+import TcUnify( buildImplicationFor )
 import LoadIface( loadInterfaceForName )
 import Module( getModule )
 
@@ -1816,18 +1817,23 @@ simplifyDeriv pred tvs theta
                 -- We use *non-overlappable* (vanilla) skolems
                 -- See Note [Overlap and deriving]
 
-       ; let skol_set = mkVarSet tvs_skols
+       ; let skol_set  = mkVarSet tvs_skols
+             skol_info = DerivSkol pred
              doc = ptext (sLit "deriving") <+> parens (ppr pred)
+             mk_ct (PredOrigin t o t_or_k)
+                 = newWanted o (Just t_or_k) (substTy skol_subst t)
 
-       ; wanted <- mapM (\(PredOrigin t o t_or_k)
-                         -> newWanted o (Just t_or_k) (substTy skol_subst t)) theta
+       ; (wanted, tclvl) <- pushTcLevelM (mapM mk_ct theta)
 
        ; traceTc "simplifyDeriv" $
          vcat [ pprTvBndrs tvs $$ ppr theta $$ ppr wanted, doc ]
        ; residual_wanted <- simplifyWantedsTcM wanted
+            -- Result is zonked
+
+       ; let residual_simple = wc_simple residual_wanted
+             (good, bad) = partitionBagWith get_good residual_simple
+             unsolved    = residual_wanted { wc_simple = bad }
 
-       ; residual_simple <- zonkSimples (wc_simple residual_wanted)
-       ; let (good, bad) = partitionBagWith get_good residual_simple
                          -- See Note [Exotic derived instance contexts]
 
              get_good :: Ct -> Either PredType Ct
@@ -1848,7 +1854,12 @@ simplifyDeriv pred tvs theta
        -- constraints.  They'll come up again when we typecheck the
        -- generated instance declaration
        ; defer <- goptM Opt_DeferTypeErrors
-       ; unless defer (reportAllUnsolved (residual_wanted { wc_simple = bad }))
+       ; (implic, _) <- buildImplicationFor tclvl skol_info tvs_skols [] unsolved
+                   -- The buildImplication is just to bind the skolems, in
+                   -- case they are mentioned in error messages
+                   -- See Trac #11347
+       ; unless defer (reportAllUnsolved (mkImplicWC implic))
+
 
        ; let min_theta  = mkMinimalBySCs (bagToList good)
              subst_skol = zipTopTCvSubst tvs_skols $ mkTyVarTys tvs
diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs
index 007abf0804..14d5138e6d 100644
--- a/compiler/typecheck/TcInstDcls.hs
+++ b/compiler/typecheck/TcInstDcls.hs
@@ -830,7 +830,7 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
                                   , ic_skols  = inst_tyvars
                                   , ic_no_eqs = False
                                   , ic_given  = dfun_ev_vars
-                                  , ic_wanted = addImplics emptyWC sc_meth_implics
+                                  , ic_wanted = mkImplicWC sc_meth_implics
                                   , ic_status = IC_Unsolved
                                   , ic_binds  = Just dfun_ev_binds_var
                                   , ic_env    = env
diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs
index 7661d7f651..eda5b6e46b 100644
--- a/compiler/typecheck/TcPatSyn.hs
+++ b/compiler/typecheck/TcPatSyn.hs
@@ -257,7 +257,7 @@ tcCheckPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details
        -- Solve the constraints now, because we are about to make a PatSyn,
        -- which should not contain unification variables and the like (Trac #10997)
        -- Since all the inputs are implications the returned bindings will be empty
-       ; _ <- simplifyTop (emptyWC `addImplics` implics)
+       ; _ <- simplifyTop (mkImplicWC implics)
 
        -- ToDo: in the bidirectional case, check that the ex_tvs' are all distinct
        -- Otherwise we may get a type error when typechecking the builder,
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index d15e5bb9b4..7e0a737565 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -79,7 +79,8 @@ module TcRnTypes(
 
         WantedConstraints(..), insolubleWC, emptyWC, isEmptyWC,
         toDerivedWC,
-        andWC, unionsWC, addSimples, addImplics, mkSimpleWC, addInsols,
+        andWC, unionsWC, mkSimpleWC, mkImplicWC,
+        addInsols, addSimples, addImplics,
         tyCoVarsOfWC, dropDerivedWC, dropDerivedSimples, dropDerivedInsols,
         isDroppableDerivedLoc, insolubleImplic,
         arisesFromGivens,
@@ -1836,6 +1837,10 @@ mkSimpleWC cts
        , wc_impl = emptyBag
        , wc_insol = emptyBag }
 
+mkImplicWC :: Bag Implication -> WantedConstraints
+mkImplicWC implic
+  = WC { wc_simple = emptyBag, wc_impl = implic, wc_insol = emptyBag }
+
 isEmptyWC :: WantedConstraints -> Bool
 isEmptyWC (WC { wc_simple = f, wc_impl = i, wc_insol = n })
   = isEmptyBag f && isEmptyBag i && isEmptyBag n
@@ -2482,6 +2487,9 @@ data SkolemInfo
 
   | ClsSkol Class       -- Bound at a class decl
 
+  | DerivSkol Type      -- Bound by a 'deriving' clause;
+                        -- the type is the instance we are trying to derive
+
   | InstSkol            -- Bound at an instance decl
   | InstSC TypeSize     -- A "given" constraint obtained by superclass selection.
                         -- If (C ty1 .. tyn) is the largest class from
@@ -2526,6 +2534,7 @@ pprSkolInfo (SigSkol ctxt ty) = pprSigSkolInfo ctxt ty
 pprSkolInfo (IPSkol ips)      = ptext (sLit "the implicit-parameter binding") <> plural ips <+> ptext (sLit "for")
                                 <+> pprWithCommas ppr ips
 pprSkolInfo (ClsSkol cls)     = ptext (sLit "the class declaration for") <+> quotes (ppr cls)
+pprSkolInfo (DerivSkol pred)  = ptext (sLit "the deriving clause for") <+> quotes (ppr pred)
 pprSkolInfo InstSkol          = ptext (sLit "the instance declaration")
 pprSkolInfo (InstSC n)        = ptext (sLit "the instance declaration") <> ifPprDebug (parens (ppr n))
 pprSkolInfo DataSkol          = ptext (sLit "a data type declaration")
diff --git a/testsuite/tests/deriving/should_compile/T10561.stderr b/testsuite/tests/deriving/should_compile/T10561.stderr
index 3a158ddb9a..c74967ff43 100644
--- a/testsuite/tests/deriving/should_compile/T10561.stderr
+++ b/testsuite/tests/deriving/should_compile/T10561.stderr
@@ -1,5 +1,7 @@
 
 T10561.hs:10:52: error:
-    Couldn't match kind ‘k’ with ‘*’
-      arising from the first field of ‘Compose’ (type ‘f (g a)’)
-    When deriving the instance for (Functor (Compose f g))
+    • Couldn't match kind ‘k’ with ‘*’
+        arising from the first field of ‘Compose’ (type ‘f (g a)’)
+      ‘k’ is a rigid type variable bound by
+        the deriving clause for ‘Functor (Compose f g)’ at T10561.hs:10:52
+    • When deriving the instance for (Functor (Compose f g))
diff --git a/testsuite/tests/deriving/should_fail/T7148.stderr b/testsuite/tests/deriving/should_fail/T7148.stderr
index 84c8205fb2..afdd1f9d99 100644
--- a/testsuite/tests/deriving/should_fail/T7148.stderr
+++ b/testsuite/tests/deriving/should_fail/T7148.stderr
@@ -1,14 +1,18 @@
 
 T7148.hs:27:40: error:
-    Occurs check: cannot construct the infinite type: b ~ Tagged a b
-      arising from the coercion of the method ‘iso2’
-        from type ‘forall b. SameType b () -> SameType b b’
-          to type ‘forall b. SameType b () -> SameType b (Tagged a b)’
-    When deriving the instance for (IsoUnit (Tagged a b))
+    • Couldn't match type ‘b’ with ‘Tagged a b’
+        arising from the coercion of the method ‘iso2’
+          from type ‘forall b. SameType b () -> SameType b b’
+            to type ‘forall b. SameType b () -> SameType b (Tagged a b)’
+      ‘b’ is a rigid type variable bound by
+        the deriving clause for ‘IsoUnit (Tagged a b)’ at T7148.hs:27:40
+    • When deriving the instance for (IsoUnit (Tagged a b))
 
 T7148.hs:27:40: error:
-    Occurs check: cannot construct the infinite type: b ~ Tagged a b
-      arising from the coercion of the method ‘iso1’
-        from type ‘forall b. SameType () b -> SameType b b’
-          to type ‘forall b. SameType () b -> SameType (Tagged a b) b’
-    When deriving the instance for (IsoUnit (Tagged a b))
+    • Couldn't match type ‘b’ with ‘Tagged a b’
+        arising from the coercion of the method ‘iso1’
+          from type ‘forall b. SameType () b -> SameType b b’
+            to type ‘forall b. SameType () b -> SameType (Tagged a b) b’
+      ‘b’ is a rigid type variable bound by
+        the deriving clause for ‘IsoUnit (Tagged a b)’ at T7148.hs:27:40
+    • When deriving the instance for (IsoUnit (Tagged a b))
diff --git a/testsuite/tests/typecheck/should_fail/T11347.stderr b/testsuite/tests/typecheck/should_fail/T11347.stderr
index 1de61cdeca..6154984201 100644
--- a/testsuite/tests/typecheck/should_fail/T11347.stderr
+++ b/testsuite/tests/typecheck/should_fail/T11347.stderr
@@ -1,2 +1,11 @@
-dummy stderr:
-here should be something about roles _not_ "No skolem info"
+
+T11347.hs:6:41: error:
+    • Couldn't match representation of type ‘a’ with that of ‘b’
+        arising from the coercion of the method ‘unsafe’
+          from type ‘Id1 a -> Discern (Id1 a) b’
+            to type ‘Id2 a -> Discern (Id2 a) b’
+      ‘a’ is a rigid type variable bound by
+        the deriving clause for ‘UnsafeCast b (Id2 a)’ at T11347.hs:6:41
+      ‘b’ is a rigid type variable bound by
+        the deriving clause for ‘UnsafeCast b (Id2 a)’ at T11347.hs:6:41
+    • When deriving the instance for (UnsafeCast b (Id2 a))