Fix #14060 by more conservatively annotating TH-reified types

Before, TH was quite generous in applying kind annotations to reified
type constructors whose result kind happened to mention type variables.
This could result in agonizingly large reified types, so this patch aims
to quell this a bit by adopting a more nuanced algorithm for determining
when a tycon application deserves a kind annotation.

This implements the algorithm laid out in
https://ghc.haskell.org/trac/ghc/ticket/14060#comment:1. I've updated
`Note [Kind annotations on TyConApps]` to reflect the new wisdom.
Essentially, instead of only checking if the result kind contains free
variables, we also check if any of those variables do not appear free in
injective positions in the argument kinds—only then do we put on a kind
annotation.

Bumps `haddock` submodule.

Test Plan: make test TEST=T14060

Reviewers: goldfire, austin, bgamari

Reviewed By: goldfire

Subscribers: rwbarton, thomie

GHC Trac Issues: #14060

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

6 files changed, 55 insertions, 9 deletions

diff --git a/testsuite/tests/th/T12403.stdout b/testsuite/tests/th/T12403.stdout
index 386b1c0a89..9b75e8b272 100644
--- a/testsuite/tests/th/T12403.stdout
+++ b/testsuite/tests/th/T12403.stdout
@@ -1,5 +1 @@
-data Main.T
-    = Main.T ((# , #) GHC.Types.Int
-                      GHC.Types.Int :: GHC.Prim.TYPE (GHC.Types.TupleRep ((GHC.Types.:) GHC.Types.LiftedRep
-                                                                                        ((GHC.Types.:) GHC.Types.LiftedRep
-                                                                                                       GHC.Types.[]))))
+data Main.T = Main.T ((# , #) GHC.Types.Int GHC.Types.Int)
diff --git a/testsuite/tests/th/T12478_1.stdout b/testsuite/tests/th/T12478_1.stdout
index f94db5992d..8437f925d5 100644
--- a/testsuite/tests/th/T12478_1.stdout
+++ b/testsuite/tests/th/T12478_1.stdout
@@ -1 +1 @@
-TyConI (DataD [] Main.T [] Nothing [NormalC Main.T [(Bang NoSourceUnpackedness NoSourceStrictness,SigT (AppT (AppT (UnboxedSumT 2) (ConT GHC.Types.Int)) (ConT GHC.Types.Char)) (AppT (ConT GHC.Prim.TYPE) (AppT (ConT GHC.Types.SumRep) (AppT (AppT (ConT GHC.Types.:) (ConT GHC.Types.LiftedRep)) (AppT (AppT (ConT GHC.Types.:) (ConT GHC.Types.LiftedRep)) (ConT GHC.Types.[]))))))]] [])
+TyConI (DataD [] Main.T [] Nothing [NormalC Main.T [(Bang NoSourceUnpackedness NoSourceStrictness,AppT (AppT (UnboxedSumT 2) (ConT GHC.Types.Int)) (ConT GHC.Types.Char))]] [])
diff --git a/testsuite/tests/th/T14060.hs b/testsuite/tests/th/T14060.hs
new file mode 100644
index 0000000000..5527b25b6e
--- /dev/null
+++ b/testsuite/tests/th/T14060.hs
@@ -0,0 +1,38 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeFamilyDependencies #-}
+{-# LANGUAGE TypeInType #-}
+module Main where
+
+import Data.Kind
+import Data.Proxy
+import Language.Haskell.TH hiding (Type)
+
+-- Anonymous tyvar binder example
+newtype Foo1 = Foo1 (Proxy '[False, True, False])
+
+-- Required (dependent) tyvar binder example
+type family Wurble k (a :: k) :: k
+newtype Foo2 a = Foo2 (Proxy (Wurble (Maybe a) Nothing))
+
+-- Non-injective type family example
+type family Foo3Fam1 (a :: Type) :: Type where
+  Foo3Fam1 a = a
+type family Foo3Fam2 (a :: Foo3Fam1 b) :: b
+newtype Foo3 = Foo3 (Proxy (Foo3Fam2 Int))
+
+-- Injective type family example
+type family Foo4Fam1 (a :: Type) = (r :: Type) | r -> a where
+  Foo4Fam1 a = a
+type family Foo4Fam2 (a :: Foo4Fam1 b) :: b
+newtype Foo4 = Foo4 (Proxy (Foo4Fam2 Int))
+
+$(return [])
+
+main :: IO ()
+main = do
+  putStrLn $(reify ''Foo1 >>= stringE . pprint)
+  putStrLn $(reify ''Foo2 >>= stringE . pprint)
+  putStrLn $(reify ''Foo3 >>= stringE . pprint)
+  putStrLn $(reify ''Foo4 >>= stringE . pprint)
diff --git a/testsuite/tests/th/T14060.stdout b/testsuite/tests/th/T14060.stdout
new file mode 100644
index 0000000000..c7668cfa3b
--- /dev/null
+++ b/testsuite/tests/th/T14060.stdout
@@ -0,0 +1,11 @@
+newtype Main.Foo1
+  = Main.Foo1 (Data.Proxy.Proxy ('(:) 'GHC.Types.False
+                                      ('(:) 'GHC.Types.True
+                                            ('(:) 'GHC.Types.False ('[] :: [GHC.Types.Bool])))))
+newtype Main.Foo2 (a_0 :: *)
+  = Main.Foo2 (Data.Proxy.Proxy (Main.Wurble (GHC.Base.Maybe a_0)
+                                             ('GHC.Base.Nothing :: GHC.Base.Maybe a_0)))
+newtype Main.Foo3
+  = Main.Foo3 (Data.Proxy.Proxy (Main.Foo3Fam2 GHC.Types.Int :: *))
+newtype Main.Foo4
+  = Main.Foo4 (Data.Proxy.Proxy (Main.Foo4Fam2 GHC.Types.Int))
diff --git a/testsuite/tests/th/T8953.stderr b/testsuite/tests/th/T8953.stderr
index c18589d69c..c724a8ea26 100644
--- a/testsuite/tests/th/T8953.stderr
+++ b/testsuite/tests/th/T8953.stderr
@@ -11,9 +11,9 @@ class T8953.PC (a_0 :: k_1)
 instance T8953.PC (a_2 :: *)
 instance T8953.PC (Data.Proxy.Proxy :: (k_3 -> *) -> *)
 type family T8953.F (a_0 :: *) :: k_1
-type instance T8953.F GHC.Types.Char = (T8953.G (T8953.T1 :: * ->
-                                                             (* -> *) -> *)
-                                                GHC.Types.Bool :: (* -> *) -> *)
+type instance T8953.F GHC.Types.Char = T8953.G (T8953.T1 :: * ->
+                                                            (* -> *) -> *)
+                                               GHC.Types.Bool
 type family T8953.G (a_0 :: k_1) :: k_1
 type instance T8953.G (T8953.T1 :: k1_2 ->
                                    k2_3 -> *) = (T8953.T2 :: k1_2 -> k2_3 -> *)
diff --git a/testsuite/tests/th/all.T b/testsuite/tests/th/all.T
index 29a6334f6b..5d61fa4880 100644
--- a/testsuite/tests/th/all.T
+++ b/testsuite/tests/th/all.T
@@ -393,3 +393,4 @@ test('T13837', normal, compile_fail, ['-v0 -dsuppress-uniques'])
 test('T13856', normal, compile, ['-v0 -ddump-splices -dsuppress-uniques'])
 test('T13887', normal, compile_and_run, ['-v0'])
 test('T13968', normal, compile_fail, ['-v0'])
+test('T14060', normal, compile_and_run, ['-v0'])