Implement stopgap solution for #14728

It turns out that one can produce ill-formed Core by
combining `GeneralizedNewtypeDeriving`, `TypeInType`, and
`TypeFamilies`, as demonstrated in #14728. The root of the problem
is allowing the last parameter of a class to appear in a //kind// of
an associated type family, as our current approach to deriving
associated type family instances simply doesn't work well for that
situation.

Although it might be possible to properly implement this feature
today (see https://ghc.haskell.org/trac/ghc/ticket/14728#comment:3
for a sketch of how this might work), there does not currently exist
a performant implementation of the algorithm needed to accomplish
this. Until such an implementation surfaces, we will make this corner
case of `GeneralizedNewtypeDeriving` an error.

Test Plan: make test TEST="T14728a T14728b"

Reviewers: bgamari

Reviewed By: bgamari

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #14728

Differential Revision: https://phabricator.haskell.org/D4402

6 files changed, 92 insertions, 3 deletions

diff --git a/compiler/typecheck/TcDeriv.hs b/compiler/typecheck/TcDeriv.hs
index 2290bce936..b78cba7faa 100644
--- a/compiler/typecheck/TcDeriv.hs
+++ b/compiler/typecheck/TcDeriv.hs
@@ -1308,6 +1308,8 @@ mkNewTypeEqn
               && ats_ok
                  -- Check (b) from Note [GND and associated type families]
               && isNothing at_without_last_cls_tv
+                 -- Check (d) from Note [GND and associated type families]
+              && isNothing at_last_cls_tv_in_kinds
 
            -- Check that eta reduction is OK
            eta_ok = rep_tc_args `lengthAtLeast` nt_eta_arity
@@ -1324,6 +1326,12 @@ mkNewTypeEqn
 
            at_without_last_cls_tv
              = find (\tc -> last_cls_tv `notElem` tyConTyVars tc) atf_tcs
+           at_last_cls_tv_in_kinds
+             = find (\tc -> any (at_last_cls_tv_in_kind . tyVarKind)
+                                (tyConTyVars tc)
+                         || at_last_cls_tv_in_kind (tyConResKind tc)) atf_tcs
+           at_last_cls_tv_in_kind kind
+             = last_cls_tv `elemVarSet` exactTyCoVarsOfType kind
            at_tcs = classATs cls
            last_cls_tv = ASSERT( notNull cls_tyvars )
                          last cls_tyvars
@@ -1331,14 +1339,22 @@ mkNewTypeEqn
            cant_derive_err
               = vcat [ ppUnless eta_ok eta_msg
                      , ppUnless ats_ok ats_msg
-                     , maybe empty at_tv_msg
-                             at_without_last_cls_tv]
+                     , maybe empty at_without_last_cls_tv_msg
+                             at_without_last_cls_tv
+                     , maybe empty at_last_cls_tv_in_kinds_msg
+                             at_last_cls_tv_in_kinds
+                     ]
            eta_msg   = text "cannot eta-reduce the representation type enough"
            ats_msg   = text "the class has associated data types"
-           at_tv_msg at_tc = hang
+           at_without_last_cls_tv_msg at_tc = hang
              (text "the associated type" <+> quotes (ppr at_tc)
               <+> text "is not parameterized over the last type variable")
              2 (text "of the class" <+> quotes (ppr cls))
+           at_last_cls_tv_in_kinds_msg at_tc = hang
+             (text "the associated type" <+> quotes (ppr at_tc)
+              <+> text "contains the last type variable")
+            2 (text "of the class" <+> quotes (ppr cls)
+              <+> text "in a kind, which is not (yet) allowed")
 
        MASSERT( cls_tys `lengthIs` (classArity cls - 1) )
        case mb_strat of
@@ -1525,6 +1541,27 @@ However, we must watch out for three things:
     GHC's termination checker isn't sophisticated enough to conclude that the
     definition of T MyInt terminates, so UndecidableInstances is required.
 
+(d) For the time being, we do not allow the last type variable of the class to
+    appear in a /kind/ of an associated type family definition. For instance:
+
+    class C a where
+      type T1 a        -- OK
+      type T2 (x :: a) -- Illegal: a appears in the kind of x
+      type T3 y :: a   -- Illegal: a appears in the kind of (T3 y)
+
+    The reason we disallow this is because our current approach to deriving
+    associated type family instances—i.e., by unwrapping the newtype's type
+    constructor as shown above—is ill-equipped to handle the scenario when
+    the last type variable appears as an implicit argument. In the worst case,
+    allowing the last variable to appear in a kind can result in improper Core
+    being generated (see #14728).
+
+    There is hope for this feature being added some day, as one could
+    conceivably take a newtype axiom (which witnesses a coercion between a
+    newtype and its representation type) at lift that through each associated
+    type at the Core level. See #14728, comment:3 for a sketch of how this
+    might work. Until then, we disallow this featurette wholesale.
+
 ************************************************************************
 *                                                                      *
 \subsection[TcDeriv-normal-binds]{Bindings for the various classes}
diff --git a/testsuite/tests/deriving/should_fail/T14728a.hs b/testsuite/tests/deriving/should_fail/T14728a.hs
new file mode 100644
index 0000000000..28cf8e0ffc
--- /dev/null
+++ b/testsuite/tests/deriving/should_fail/T14728a.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+module T14728a where
+
+import Data.Functor.Identity
+import Data.Kind
+
+class C (a :: Type) where
+  type T a (x :: a) :: Type
+  type U z :: a
+
+instance C () where
+  type T () '() = Bool
+
+deriving instance C (Identity a)
+
+f :: T (Identity ()) ('Identity '())
+f = True
diff --git a/testsuite/tests/deriving/should_fail/T14728a.stderr b/testsuite/tests/deriving/should_fail/T14728a.stderr
new file mode 100644
index 0000000000..b76d073645
--- /dev/null
+++ b/testsuite/tests/deriving/should_fail/T14728a.stderr
@@ -0,0 +1,7 @@
+
+T14728a.hs:17:1: error:
+    • Can't make a derived instance of ‘C (Identity a)’
+        (even with cunning GeneralizedNewtypeDeriving):
+        the associated type ‘T’ contains the last type variable
+          of the class ‘C’ in a kind, which is not (yet) allowed
+    • In the stand-alone deriving instance for ‘C (Identity a)’
diff --git a/testsuite/tests/deriving/should_fail/T14728b.hs b/testsuite/tests/deriving/should_fail/T14728b.hs
new file mode 100644
index 0000000000..7fdfcb3b5e
--- /dev/null
+++ b/testsuite/tests/deriving/should_fail/T14728b.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+module T14728b where
+
+import Data.Functor.Identity
+import Data.Kind
+
+class C (a :: Type) where
+  type U z :: a
+
+instance C () where
+  type U z = '()
+
+deriving instance C (Identity a)
diff --git a/testsuite/tests/deriving/should_fail/T14728b.stderr b/testsuite/tests/deriving/should_fail/T14728b.stderr
new file mode 100644
index 0000000000..ee74f8b4da
--- /dev/null
+++ b/testsuite/tests/deriving/should_fail/T14728b.stderr
@@ -0,0 +1,7 @@
+
+T14728b.hs:16:1: error:
+    • Can't make a derived instance of ‘C (Identity a)’
+        (even with cunning GeneralizedNewtypeDeriving):
+        the associated type ‘U’ contains the last type variable
+          of the class ‘C’ in a kind, which is not (yet) allowed
+    • In the stand-alone deriving instance for ‘C (Identity a)’
diff --git a/testsuite/tests/deriving/should_fail/all.T b/testsuite/tests/deriving/should_fail/all.T
index c9b8469c3c..acd3486918 100644
--- a/testsuite/tests/deriving/should_fail/all.T
+++ b/testsuite/tests/deriving/should_fail/all.T
@@ -69,3 +69,5 @@ test('T12512', omit_ways(['ghci']), compile_fail, [''])
 test('T12801', normal, compile_fail, [''])
 test('T14365', [extra_files(['T14365B.hs','T14365B.hs-boot'])],
                multimod_compile_fail, ['T14365A',''])
+test('T14728a', normal, compile_fail, [''])
+test('T14728b', normal, compile_fail, [''])