Slightly better `Coercible` errors.

This makes two real changes:
 - Equalities like (a ~R [a]) really *are* insoluble. Previously,
   GHC refused to give up when an occurs check bit on a representational
   equality. But for datatypes, it really should bail.

 - Now, GHC will sometimes report an occurs check error (in cases above)
   for representational equalities. Previously, it never did.

This "fixes" #10715, where by "fix", I mean clarifies the error message.
It's unclear how to do more to fix that ticket.

Test cases: typecheck/should_fail/T10715{,b}

8 files changed, 92 insertions, 8 deletions

diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index 3f0a198a88..4d92593f5d 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -1016,6 +1016,23 @@ and the Id newtype is unwrapped. This is assured by requiring only flat
 types in canEqTyVar *and* having the newtype-unwrapping check above
 the tyvar check in can_eq_nc.
 
+Note [Occurs check error]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+If we have an occurs check error, are we necessarily hosed? Say our
+tyvar is tv1 and the type it appears in is xi2. Because xi2 is function
+free, then if we're computing w.r.t. nominal equality, then, yes, we're
+hosed. Nothing good can come from (a ~ [a]). If we're computing w.r.t.
+representational equality, this is a little subtler. Once again, (a ~R [a])
+is a bad thing, but (a ~R N a) for a newtype N might be just fine. This
+means also that (a ~ b a) might be fine, because `b` might become a newtype.
+
+So, we must check: does tv1 appear in xi2 under any type constructor that
+is generative w.r.t. representational equality? That's what isTyVarUnderDatatype
+does. (The other name I considered, isTyVarUnderTyConGenerativeWrtReprEq was
+a bit verbose. And the shorter name gets the point across.)
+
+See also #10715, which induced this addition.
+
 -}
 
 canCFunEqCan :: CtEvidence
@@ -1091,12 +1108,14 @@ canEqTyVar2 dflags ev eq_rel swapped tv1 xi2
   | otherwise  -- Occurs check error
   = rewriteEqEvidence ev eq_rel swapped xi1 xi2 co1 co2
     `andWhenContinue` \ new_ev ->
-    case eq_rel of
-      NomEq  -> do { emitInsoluble (mkNonCanonical new_ev)
+    if eq_rel == NomEq || isTyVarUnderDatatype tv1 xi2
+      -- See Note [Occurs check error]
+
+    then do { emitInsoluble (mkNonCanonical 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" }
+            ; stopWith new_ev "Occurs check" }
 
         -- A representational equality with an occurs-check problem isn't
         -- insoluble! For example:
@@ -1104,9 +1123,9 @@ canEqTyVar2 dflags ev eq_rel swapped tv1 xi2
         -- 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.
-      ReprEq -> do { traceTcS "Occurs-check in representational equality"
+    else do { traceTcS "Occurs-check in representational equality"
                               (ppr xi1 $$ ppr xi2)
-                   ; continueWith (CIrredEvCan { cc_ev = new_ev }) }
+            ; continueWith (CIrredEvCan { cc_ev = new_ev }) }
   where
     role = eqRelRole eq_rel
     xi1  = mkTyVarTy tv1
diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs
index f91968dc97..7ef0d94331 100644
--- a/compiler/typecheck/TcErrors.hs
+++ b/compiler/typecheck/TcErrors.hs
@@ -963,7 +963,10 @@ mkTyVarEqErr dflags ctxt extra ct oriented tv1 ty2
                             -- be oriented the other way round;
                             -- see TcCanonical.canEqTyVarTyVar
   || isSigTyVar tv1 && not (isTyVarTy ty2)
-  || ctEqRel ct == ReprEq  -- the cases below don't really apply to ReprEq
+  || pprTrace "RAE1" (ppr ct $$ ppr tv1 $$ ppr ty2 $$
+                      ppr (isTyVarUnderDatatype tv1 ty2))
+     (ctEqRel ct == ReprEq && not (isTyVarUnderDatatype tv1 ty2))
+     -- the cases below don't really apply to ReprEq (except occurs check)
   = mkErrorMsgFromCt ctxt ct (vcat [ misMatchOrCND ctxt ct oriented ty1 ty2
                                    , extraTyVarInfo ctxt tv1 ty2
                                    , extra ])
@@ -975,7 +978,8 @@ mkTyVarEqErr dflags ctxt extra ct oriented tv1 ty2
   = mkErrorMsgFromCt ctxt ct $ (kindErrorMsg (mkTyVarTy tv1) ty2 $$ extra)
 
   | OC_Occurs <- occ_check_expand
-  , NomEq <- ctEqRel ct      -- reporting occurs check for Coercible is strange
+  , ctEqRel ct == NomEq || isTyVarUnderDatatype tv1 ty2
+         -- See Note [Occurs check error] in TcCanonical
   = do { let occCheckMsg = addArising (ctOrigin ct) $
                            hang (text "Occurs check: cannot construct the infinite type:")
                               2 (sep [ppr ty1, char '~', ppr ty2])
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index 3a25a39b4c..465efcca63 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -68,7 +68,7 @@ module TcType (
   isDoubleTy, isFloatTy, isIntTy, isWordTy, isStringTy,
   isIntegerTy, isBoolTy, isUnitTy, isCharTy,
   isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy,
-  isPredTy, isTyVarClassPred, isTyVarExposed,
+  isPredTy, isTyVarClassPred, isTyVarExposed, isTyVarUnderDatatype,
   checkValidClsArgs, hasTyVarHead,
   isRigidEqPred, isRigidTy,
 
@@ -1466,6 +1466,25 @@ isTyVarExposed tv (AppTy fun arg) = isTyVarExposed tv fun
                                  || isTyVarExposed tv arg
 isTyVarExposed _  (ForAllTy {})   = False
 
+-- | Does the given tyvar appear under a type generative w.r.t.
+-- representational equality? See Note [Occurs check error] in
+-- TcCanonical for the motivation for this function.
+isTyVarUnderDatatype :: TcTyVar -> TcType -> Bool
+isTyVarUnderDatatype tv = go False
+  where
+    go under_dt ty | Just ty' <- tcView ty = go under_dt ty'
+    go under_dt (TyVarTy tv') = under_dt && (tv == tv')
+    go under_dt (TyConApp tc tys) = let under_dt' = under_dt ||
+                                                    isGenerativeTyCon tc
+                                                      Representational
+                                    in any (go under_dt') tys
+    go _        (LitTy {}) = False
+    go _        (FunTy arg res) = go True arg || go True res
+    go under_dt (AppTy fun arg) = go under_dt fun || go under_dt arg
+    go under_dt (ForAllTy tv' inner_ty)
+      | tv' == tv = False
+      | otherwise = go under_dt inner_ty
+
 isRigidTy :: TcType -> Bool
 isRigidTy ty
   | Just (tc,_) <- tcSplitTyConApp_maybe ty = isGenerativeTyCon tc Nominal
diff --git a/testsuite/tests/typecheck/should_fail/T10715.hs b/testsuite/tests/typecheck/should_fail/T10715.hs
new file mode 100644
index 0000000000..969abd5cf2
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T10715.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE FlexibleContexts #-}
+module T10715 where
+
+import Data.Coerce (coerce, Coercible)
+import Data.Ord ( Down )  -- convenient newtype
+
+data X a
+
+doCoerce :: Coercible a (X a) => a -> X a
+doCoerce = coerce
diff --git a/testsuite/tests/typecheck/should_fail/T10715.stderr b/testsuite/tests/typecheck/should_fail/T10715.stderr
new file mode 100644
index 0000000000..e6f85a5256
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T10715.stderr
@@ -0,0 +1,15 @@
+
+T10715.hs:9:13: error:
+    Couldn't match representation of type ‘a’ with that of ‘X a’
+    ‘a’ is a rigid type variable bound by
+        the type signature for:
+          doCoerce :: Coercible a (X a) => a -> X a
+        at T10715.hs:9:13
+    Inaccessible code in
+      the type signature for:
+        doCoerce :: Coercible a (X a) => a -> X a
+    In the ambiguity check for the type signature for ‘doCoerce’:
+      doCoerce :: forall a. Coercible a (X a) => a -> X a
+    To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
+    In the type signature for ‘doCoerce’:
+      doCoerce :: Coercible a (X a) => a -> X a
diff --git a/testsuite/tests/typecheck/should_fail/T10715b.hs b/testsuite/tests/typecheck/should_fail/T10715b.hs
new file mode 100644
index 0000000000..b2418b9b62
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T10715b.hs
@@ -0,0 +1,7 @@
+module T10715b where
+
+-- test error message: should complain about an occurs check
+
+import Data.Coerce
+
+foo = coerce `asTypeOf` head
diff --git a/testsuite/tests/typecheck/should_fail/T10715b.stderr b/testsuite/tests/typecheck/should_fail/T10715b.stderr
new file mode 100644
index 0000000000..47c85bb145
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T10715b.stderr
@@ -0,0 +1,8 @@
+
+T10715b.hs:7:7: error:
+    Occurs check: cannot construct the infinite type: b ~ [b]
+      arising from a use of ‘coerce’
+    Relevant bindings include foo :: [b] -> b (bound at T10715b.hs:7:1)
+    In the first argument of ‘asTypeOf’, namely ‘coerce’
+    In the expression: coerce `asTypeOf` head
+    In an equation for ‘foo’: foo = coerce `asTypeOf` head
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 0a0281a587..a005bc5f29 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -386,3 +386,5 @@ test('ExpandSynsFail3', normal, compile_fail, ['-fprint-expanded-synonyms'])
 test('ExpandSynsFail4', normal, compile_fail, ['-fprint-expanded-synonyms'])
 test('T10698', expect_broken(10698), compile_fail, [''])
 test('T10836', normal, compile_fail, [''])
+test('T10715', normal, compile_fail, [''])
+test('T10715b', normal, compile_fail, [''])