Banish reportFloatingViaTvs to the shadow realm (#15831, #16181)

GHC used to reject programs of this form:

```
newtype Age = MkAge Int
  deriving Eq via Const Int a
```

That's because an earlier implementation of `DerivingVia` would
generate the following instance:

```
instance Eq Age where
  (==) = coerce @(Const Int a -> Const Int a -> Bool)
                @(Age         -> Age         -> Bool)
                (==)
```

Note that the `a` in `Const Int a` is not bound anywhere, which
causes all sorts of issues. I figured that no one would ever want to
write code like this anyway, so I simply banned "floating" `via` type
variables like `a`, checking for their presence in the aptly named
`reportFloatingViaTvs` function.

`reportFloatingViaTvs` ended up being implemented in a subtly
incorrect way, as #15831 demonstrates. Following counsel with the
sage of gold fire, I decided to abandon `reportFloatingViaTvs`
entirely and opt for a different approach that would _accept_
the instance above. This is because GHC now generates this instance
instead:

```
instance forall a. Eq Age where
  (==) = coerce @(Const Int a -> Const Int a -> Bool)
                @(Age         -> Age         -> Bool)
                (==)
```

Notice that we now explicitly quantify the `a` in
`instance forall a. Eq Age`, so everything is peachy scoping-wise.
See `Note [Floating `via` type variables]` in `TcDeriv` for the full
scoop.

A pleasant benefit of this refactoring is that it made it much easier
to catch the problem observed in #16181, so this patch fixes that
issue too.

Fixes #15831. Fixes #16181.

13 files changed, 206 insertions, 19 deletions

diff --git a/testsuite/tests/deriving/should_compile/T15831.hs b/testsuite/tests/deriving/should_compile/T15831.hs
new file mode 100644
index 0000000000..309c8a8e3a
--- /dev/null
+++ b/testsuite/tests/deriving/should_compile/T15831.hs
@@ -0,0 +1,33 @@
+{-# LANGUAGE DerivingVia #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+module T15831 where
+
+import Data.Functor.Const (Const(..))
+import GHC.Exts (Any)
+
+newtype Age = MkAge Int
+  deriving Eq
+    via Const Int Any
+  deriving Ord
+    via Const Int (Any :: k)
+  deriving Read
+    via (forall k. Const Int (Any :: k))
+  deriving Show
+    via Const Int a
+  deriving Enum
+    via Const Int (a :: k)
+  deriving Bounded
+    via (forall a. Const Int a)
+  deriving Num
+    via (forall k (a :: k). Const Int a)
+
+newtype Age2 = MkAge2 Int
+deriving via                     Const Int Any         instance Eq      Age2
+deriving via                     Const Int (Any :: k)  instance Ord     Age2
+deriving via (forall k.          Const Int (Any :: k)) instance Read    Age2
+deriving via                     Const Int a           instance Show    Age2
+deriving via                     Const Int (a :: k)    instance Enum    Age2
+deriving via (forall a.          Const Int a)          instance Bounded Age2
+deriving via (forall k (a :: k). Const Int a)          instance Num     Age2
diff --git a/testsuite/tests/deriving/should_compile/all.T b/testsuite/tests/deriving/should_compile/all.T
index 1c1b4d546a..a12cf95c28 100644
--- a/testsuite/tests/deriving/should_compile/all.T
+++ b/testsuite/tests/deriving/should_compile/all.T
@@ -115,5 +115,6 @@ test('T15290c', normal, compile, [''])
 test('T15290d', normal, compile, [''])
 test('T15398', normal, compile, [''])
 test('T15637', normal, compile, [''])
+test('T15831', normal, compile, [''])
 test('T16179', normal, compile, [''])
 test('T16518', normal, compile, [''])
diff --git a/testsuite/tests/deriving/should_fail/T10598_fail4.stderr b/testsuite/tests/deriving/should_fail/T10598_fail4.stderr
index 7d724d07bd..e5447d9489 100644
--- a/testsuite/tests/deriving/should_fail/T10598_fail4.stderr
+++ b/testsuite/tests/deriving/should_fail/T10598_fail4.stderr
@@ -1,4 +1,4 @@
 
-T10598_fail4.hs:3:1: error:
+T10598_fail4.hs:4:12: error:
     Illegal deriving strategy: stock
     Use DerivingStrategies to enable this extension
diff --git a/testsuite/tests/deriving/should_fail/T15831.stderr b/testsuite/tests/deriving/should_fail/T15831.stderr
new file mode 100644
index 0000000000..886645a3c1
--- /dev/null
+++ b/testsuite/tests/deriving/should_fail/T15831.stderr
@@ -0,0 +1,6 @@
+
+T15831.hs:9:12: error:
+    • Type variable ‘k’ is bound in the ‘via’ type ‘Const
+                                                      @{k} Int (Any @k)’
+      but is not mentioned in the derived class ‘Eq’, which is illegal
+    • In the newtype declaration for ‘Age’
diff --git a/testsuite/tests/deriving/should_fail/T16181.hs b/testsuite/tests/deriving/should_fail/T16181.hs
new file mode 100644
index 0000000000..29692dd1a1
--- /dev/null
+++ b/testsuite/tests/deriving/should_fail/T16181.hs
@@ -0,0 +1,25 @@
+{-# LANGUAGE DerivingVia #-}
+{-# LANGUAGE KindSignatures #-}
+module T16181 where
+
+import Control.Monad.Trans.Class
+import Control.Monad.Reader
+import Data.Functor.Const (Const(..))
+import Data.Functor.Classes
+import Data.Kind
+import Data.Proxy
+
+newtype FlipConst a b = FlipConst b
+  deriving (Show1, Eq1) via (Const b)
+
+data Foo m x = Foo { foo :: m x }
+newtype Q x m a = Q {unQ :: Foo m x -> m a}
+    deriving (Functor, Applicative, Monad, MonadReader (Foo m x)) via (ReaderT (Foo m x) m)
+    deriving MonadTrans via (ReaderT (Foo m x))
+
+class C (f :: Type -> Type) where
+  m :: Proxy f -> String
+instance C (Either a) where
+  m _ = "Either"
+data T a
+  deriving C via Either a
diff --git a/testsuite/tests/deriving/should_fail/T16181.stderr b/testsuite/tests/deriving/should_fail/T16181.stderr
new file mode 100644
index 0000000000..cbac319a2c
--- /dev/null
+++ b/testsuite/tests/deriving/should_fail/T16181.stderr
@@ -0,0 +1,19 @@
+
+T16181.hs:13:13: error:
+    • Cannot eta-reduce to an instance of form
+        instance (...) => Show1 (FlipConst a)
+    • In the newtype declaration for ‘FlipConst’
+
+T16181.hs:13:20: error:
+    • Cannot eta-reduce to an instance of form
+        instance (...) => Eq1 (FlipConst a)
+    • In the newtype declaration for ‘FlipConst’
+
+T16181.hs:18:14: error:
+    • Cannot eta-reduce to an instance of form
+        instance (...) => MonadTrans (Q x)
+    • In the newtype declaration for ‘Q’
+
+T16181.hs:25:12: error:
+    • Cannot eta-reduce to an instance of form instance (...) => C T
+    • In the data declaration for ‘T’
diff --git a/testsuite/tests/deriving/should_fail/all.T b/testsuite/tests/deriving/should_fail/all.T
index bbef97bec7..bd2c55983a 100644
--- a/testsuite/tests/deriving/should_fail/all.T
+++ b/testsuite/tests/deriving/should_fail/all.T
@@ -73,8 +73,10 @@ test('T14728b', normal, compile_fail, [''])
 test('T14916', normal, compile_fail, [''])
 test('T15073', [extra_files(['T15073a.hs'])], multimod_compile_fail,
                ['T15073', '-v0'])
+test('T16181', normal, compile_fail, [''])
 test('T16923', normal, compile_fail, [''])
 test('deriving-via-fail', normal, compile_fail, [''])
 test('deriving-via-fail2', normal, compile_fail, [''])
 test('deriving-via-fail3', normal, compile_fail, [''])
 test('deriving-via-fail4', normal, compile_fail, [''])
+test('deriving-via-fail5', normal, compile_fail, [''])
diff --git a/testsuite/tests/deriving/should_fail/deriving-via-fail.hs b/testsuite/tests/deriving/should_fail/deriving-via-fail.hs
index fbae1e7d13..3fa8009638 100644
--- a/testsuite/tests/deriving/should_fail/deriving-via-fail.hs
+++ b/testsuite/tests/deriving/should_fail/deriving-via-fail.hs
@@ -13,7 +13,3 @@ newtype Foo2 a b = Foo2 (a -> b)
     via fooo
 
 data Foo3 deriving Eq via (forall a. a)
-
-newtype Foo4 a = Foo4 a
-deriving via (Identity b)
-  instance Show (Foo4 a)
diff --git a/testsuite/tests/deriving/should_fail/deriving-via-fail.stderr b/testsuite/tests/deriving/should_fail/deriving-via-fail.stderr
index 51907e02cf..5179f53c03 100644
--- a/testsuite/tests/deriving/should_fail/deriving-via-fail.stderr
+++ b/testsuite/tests/deriving/should_fail/deriving-via-fail.stderr
@@ -1,16 +1,28 @@
 
 deriving-via-fail.hs:9:34: error:
-    Type variable ‘b’ is bound in the ‘via’ type ‘(Identity b)’
-    but is not mentioned in the derived class ‘Show’, which is illegal
+    • Couldn't match representation of type ‘a’ with that of ‘b’
+        arising from the coercion of the method ‘showsPrec’
+          from type ‘Int -> Identity b -> ShowS’
+            to type ‘Int -> Foo1 a -> ShowS’
+      ‘a’ is a rigid type variable bound by
+        the deriving clause for ‘Show (Foo1 a)’
+        at deriving-via-fail.hs:9:34-37
+      ‘b’ is a rigid type variable bound by
+        the deriving clause for ‘Show (Foo1 a)’
+        at deriving-via-fail.hs:9:34-37
+    • When deriving the instance for (Show (Foo1 a))
 
 deriving-via-fail.hs:12:12: error:
-    Type variable ‘fooo’ is bound in the ‘via’ type ‘fooo’
-    but is not mentioned in the derived class ‘Category’, which is illegal
+    • Cannot derive instance via ‘fooo’
+        Class ‘Category’ expects an argument of kind ‘* -> * -> *’,
+        but ‘fooo’ has kind ‘*’
+    • In the newtype declaration for ‘Foo2’
 
 deriving-via-fail.hs:15:20: error:
-    Type variable ‘a’ is bound in the ‘via’ type ‘(forall a. a)’
-    but is not mentioned in the derived class ‘Eq’, which is illegal
-
-deriving-via-fail.hs:19:12: error:
-    Type variable ‘b’ is bound in the ‘via’ type ‘(Identity b)’
-    but is not mentioned in the derived instance ‘Show (Foo4 a)’, which is illegal
+    • Couldn't match representation of type ‘a’ with that of ‘Foo3’
+        arising from the coercion of the method ‘==’
+          from type ‘a -> a -> Bool’ to type ‘Foo3 -> Foo3 -> Bool’
+      ‘a’ is a rigid type variable bound by
+        the deriving clause for ‘Eq Foo3’
+        at deriving-via-fail.hs:15:20-21
+    • When deriving the instance for (Eq Foo3)
diff --git a/testsuite/tests/deriving/should_fail/deriving-via-fail3.stderr b/testsuite/tests/deriving/should_fail/deriving-via-fail3.stderr
index f2af73a01f..43c395e5cd 100644
--- a/testsuite/tests/deriving/should_fail/deriving-via-fail3.stderr
+++ b/testsuite/tests/deriving/should_fail/deriving-via-fail3.stderr
@@ -1,4 +1,4 @@
 
-deriving-via-fail3.hs:3:1: error:
+deriving-via-fail3.hs:3:20: error:
     Illegal deriving strategy: via
     Use DerivingVia to enable this extension
diff --git a/testsuite/tests/deriving/should_fail/deriving-via-fail4.stderr b/testsuite/tests/deriving/should_fail/deriving-via-fail4.stderr
index caa2bfe93b..9c4ee15209 100644
--- a/testsuite/tests/deriving/should_fail/deriving-via-fail4.stderr
+++ b/testsuite/tests/deriving/should_fail/deriving-via-fail4.stderr
@@ -6,13 +6,13 @@ deriving-via-fail4.hs:14:12: error:
     • When deriving the instance for (Eq F1)
 
 deriving-via-fail4.hs:17:13: error:
-    • Couldn't match representation of type ‘a1’ with that of ‘a’
+    • Couldn't match representation of type ‘a’ with that of ‘a1’
         arising from the coercion of the method ‘c’
           from type ‘a -> a -> Bool’ to type ‘a -> F2 a1 -> Bool’
-      ‘a1’ is a rigid type variable bound by
+      ‘a’ is a rigid type variable bound by
         the deriving clause for ‘C a (F2 a1)’
         at deriving-via-fail4.hs:17:13-15
-      ‘a’ is a rigid type variable bound by
+      ‘a1’ is a rigid type variable bound by
         the deriving clause for ‘C a (F2 a1)’
         at deriving-via-fail4.hs:17:13-15
     • When deriving the instance for (C a (F2 a1))
diff --git a/testsuite/tests/deriving/should_fail/deriving-via-fail5.hs b/testsuite/tests/deriving/should_fail/deriving-via-fail5.hs
new file mode 100644
index 0000000000..7baf6c728a
--- /dev/null
+++ b/testsuite/tests/deriving/should_fail/deriving-via-fail5.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE DerivingVia #-}
+{-# LANGUAGE StandaloneDeriving #-}
+module DerivingViaFail5 where
+
+import Data.Functor.Identity
+
+newtype Foo4 a = Foo4 a
+deriving via (Identity b)
+  instance Show (Foo4 a)
diff --git a/testsuite/tests/deriving/should_fail/deriving-via-fail5.stderr b/testsuite/tests/deriving/should_fail/deriving-via-fail5.stderr
new file mode 100644
index 0000000000..0e20ce480e
--- /dev/null
+++ b/testsuite/tests/deriving/should_fail/deriving-via-fail5.stderr
@@ -0,0 +1,84 @@
+
+deriving-via-fail5.hs:8:1: error:
+    • Couldn't match representation of type ‘a’ with that of ‘b’
+        arising from a use of ‘GHC.Prim.coerce’
+      ‘a’ is a rigid type variable bound by
+        the instance declaration
+        at deriving-via-fail5.hs:(8,1)-(9,24)
+      ‘b’ is a rigid type variable bound by
+        the instance declaration
+        at deriving-via-fail5.hs:(8,1)-(9,24)
+    • In the expression:
+          GHC.Prim.coerce
+            @(Int -> Identity b -> ShowS)
+            @(Int -> Foo4 a -> ShowS)
+            (showsPrec @(Identity b)) ::
+            Int -> Foo4 a -> ShowS
+      In an equation for ‘showsPrec’:
+          showsPrec
+            = GHC.Prim.coerce
+                @(Int -> Identity b -> ShowS)
+                @(Int -> Foo4 a -> ShowS)
+                (showsPrec @(Identity b)) ::
+                Int -> Foo4 a -> ShowS
+      When typechecking the code for ‘showsPrec’
+        in a derived instance for ‘Show (Foo4 a)’:
+        To see the code I am typechecking, use -ddump-deriv
+      In the instance declaration for ‘Show (Foo4 a)’
+    • Relevant bindings include
+        showsPrec :: Int -> Foo4 a -> ShowS
+          (bound at deriving-via-fail5.hs:8:1)
+
+deriving-via-fail5.hs:8:1: error:
+    • Couldn't match representation of type ‘a’ with that of ‘b’
+        arising from a use of ‘GHC.Prim.coerce’
+      ‘a’ is a rigid type variable bound by
+        the instance declaration
+        at deriving-via-fail5.hs:(8,1)-(9,24)
+      ‘b’ is a rigid type variable bound by
+        the instance declaration
+        at deriving-via-fail5.hs:(8,1)-(9,24)
+    • In the expression:
+          GHC.Prim.coerce
+            @(Identity b -> String) @(Foo4 a -> String) (show @(Identity b)) ::
+            Foo4 a -> String
+      In an equation for ‘show’:
+          show
+            = GHC.Prim.coerce
+                @(Identity b -> String) @(Foo4 a -> String) (show @(Identity b)) ::
+                Foo4 a -> String
+      When typechecking the code for ‘show’
+        in a derived instance for ‘Show (Foo4 a)’:
+        To see the code I am typechecking, use -ddump-deriv
+      In the instance declaration for ‘Show (Foo4 a)’
+    • Relevant bindings include
+        show :: Foo4 a -> String (bound at deriving-via-fail5.hs:8:1)
+
+deriving-via-fail5.hs:8:1: error:
+    • Couldn't match representation of type ‘a’ with that of ‘b’
+        arising from a use of ‘GHC.Prim.coerce’
+      ‘a’ is a rigid type variable bound by
+        the instance declaration
+        at deriving-via-fail5.hs:(8,1)-(9,24)
+      ‘b’ is a rigid type variable bound by
+        the instance declaration
+        at deriving-via-fail5.hs:(8,1)-(9,24)
+    • In the expression:
+          GHC.Prim.coerce
+            @([] (Identity b) -> ShowS)
+            @([] (Foo4 a) -> ShowS)
+            (showList @(Identity b)) ::
+            [] (Foo4 a) -> ShowS
+      In an equation for ‘showList’:
+          showList
+            = GHC.Prim.coerce
+                @([] (Identity b) -> ShowS)
+                @([] (Foo4 a) -> ShowS)
+                (showList @(Identity b)) ::
+                [] (Foo4 a) -> ShowS
+      When typechecking the code for ‘showList’
+        in a derived instance for ‘Show (Foo4 a)’:
+        To see the code I am typechecking, use -ddump-deriv
+      In the instance declaration for ‘Show (Foo4 a)’
+    • Relevant bindings include
+        showList :: [Foo4 a] -> ShowS (bound at deriving-via-fail5.hs:8:1)