Don't quantify implicit type variables when quoting type signatures in TH

Summary:
A bug was introduced in GHC 8.0 in which Template Haskell-quoted type
signatures would quantify _all_ their type variables, even the implicit ones.
This would cause splices like this:

```
$([d| idProxy :: forall proxy (a :: k). proxy a -> proxy a
      idProxy x = x
   |])
```

To splice back in something that was slightly different:

```
idProxy :: forall k proxy (a :: k). proxy a -> proxy a
idProxy x = x
```

Notice that the kind variable `k` is now explicitly quantified! What's worse,
this now requires the `TypeInType` extension to be enabled.

This changes the behavior of Template Haskell quoting to never explicitly
quantify type variables which are implicitly quantified in the source.

There are some other places where this behavior pops up too, including
class methods, type ascriptions, `SPECIALIZE` pragmas, foreign imports,
and pattern synonynms (#13018), so I fixed those too.

Fixes #13018 and #13123.

Test Plan: ./validate

Reviewers: simonpj, goldfire, austin, bgamari

Reviewed By: simonpj, goldfire

Subscribers: simonpj, mpickering, thomie

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

GHC Trac Issues: #13018, #13123

11 files changed, 60 insertions, 18 deletions

diff --git a/testsuite/tests/ghci/scripts/T11098.stdout b/testsuite/tests/ghci/scripts/T11098.stdout
index 2b86289e18..5a748053c3 100644
--- a/testsuite/tests/ghci/scripts/T11098.stdout
+++ b/testsuite/tests/ghci/scripts/T11098.stdout
@@ -1,3 +1,3 @@
-[SigD foo_1 (ForallT [PlainTV a_0] [] (AppT (AppT ArrowT (VarT a_0)) (VarT a_0))),FunD foo_1 [Clause [VarP x_2] (NormalB (VarE x_2)) []]]
+[SigD foo_1 (AppT (AppT ArrowT (VarT a_0)) (VarT a_0)),FunD foo_1 [Clause [VarP x_2] (NormalB (VarE x_2)) []]]
 "[SigD foo_ (AppT (AppT ArrowT (VarT _a_)) (VarT _a_)),FunD foo_ [Clause [VarP x_] (NormalB (VarE x_)) []]]"
 [SigD foo_6 (ForallT [PlainTV _a_5] [] (AppT (AppT ArrowT (VarT _a_5)) (VarT _a_5))),FunD foo_6 [Clause [VarP x_7] (NormalB (VarE x_7)) []]]
diff --git a/testsuite/tests/th/T10828.stderr b/testsuite/tests/th/T10828.stderr
index c361a15c7b..82509ec7b0 100644
--- a/testsuite/tests/th/T10828.stderr
+++ b/testsuite/tests/th/T10828.stderr
@@ -1,17 +1,17 @@
 data family D_0 a_1 :: * -> *
 data instance D_0 GHC.Types.Int GHC.Types.Bool :: * where
     DInt_2 :: D_0 GHC.Types.Int GHC.Types.Bool
-data E_3 where MkE_4 :: forall a_5 . a_5 -> E_3
+data E_3 where MkE_4 :: a_5 -> E_3
 data Foo_6 a_7 b_8 where
-    MkFoo_9, MkFoo'_10 :: forall a_11 b_12 . a_11 -> Foo_6 a_11 b_12
+    MkFoo_9, MkFoo'_10 :: a_11 -> Foo_6 a_11 b_12
 newtype Bar_13 :: * -> GHC.Types.Bool -> *
-  = MkBar_14 :: forall a_15 b_16 . a_15 -> Bar_13 a_15 b_16
+  = MkBar_14 :: a_15 -> Bar_13 a_15 b_16
 data T10828.T (a_0 :: *) where
     T10828.MkT :: forall (a_1 :: *) . a_1 -> a_1 -> T10828.T a_1
     T10828.MkC :: forall (a_2 :: *) (b_3 :: *) . Data.Type.Equality.~ a_2
-                                                                       GHC.Types.Int => {T10828.foo :: a_2,
-                                                                                         T10828.bar :: b_3} -> T10828.T GHC.Types.Int
+                                                                      GHC.Types.Int => {T10828.foo :: a_2,
+                                                                                        T10828.bar :: b_3} -> T10828.T GHC.Types.Int
 data T'_0 a_1 :: * where
-    MkT'_2 :: forall a_3 . a_3 -> a_3 -> T'_0 a_3
+    MkT'_2 :: a_3 -> a_3 -> T'_0 a_3
     MkC'_4 :: forall a_5 b_6 . a_5 ~ GHC.Types.Int => {foo_7 :: a_5,
                                                        bar_8 :: b_6} -> T'_0 GHC.Types.Int
diff --git a/testsuite/tests/th/T11797.stderr b/testsuite/tests/th/T11797.stderr
index 1b43982968..b978e63aff 100644
--- a/testsuite/tests/th/T11797.stderr
+++ b/testsuite/tests/th/T11797.stderr
@@ -1,2 +1,2 @@
 class Foo_0 a_1
-    where meth_2 :: forall b_3 . a_1 -> b_3 -> a_1
+    where meth_2 :: a_1 -> b_3 -> a_1
diff --git a/testsuite/tests/th/T13018.hs b/testsuite/tests/th/T13018.hs
new file mode 100644
index 0000000000..8b46d88cea
--- /dev/null
+++ b/testsuite/tests/th/T13018.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE TemplateHaskell #-}
+module T13018 where
+
+data T a where
+  MkT :: Eq b => b -> T a
+
+$([d| pattern P :: b -> T a
+      pattern P x <- MkT x
+    |])
diff --git a/testsuite/tests/th/T13123.hs b/testsuite/tests/th/T13123.hs
new file mode 100644
index 0000000000..987283be70
--- /dev/null
+++ b/testsuite/tests/th/T13123.hs
@@ -0,0 +1,30 @@
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TemplateHaskell #-}
+module T13123 where
+
+$([d| idProxy :: forall proxy (a :: k). proxy a -> proxy a
+      idProxy x = x
+    |])
+
+$([d| id2 :: Show a => a -> a
+      id2 x = x
+      {-# SPECIALIZE id2 :: forall proxy (a :: k). Show (proxy a)
+                         => proxy a -> proxy a #-}
+    |])
+
+$([d| wibble :: Maybe Int
+      wibble = (undefined :: forall proxy (a :: k). proxy a)
+    |])
+
+$([d| class Foo b where
+        bar         :: forall proxy (a :: k). proxy a -> b
+        default bar :: forall proxy (a :: k). proxy a -> b
+        bar = undefined
+    |])
+
+$([d| data GADT where
+        MkGADT :: forall proxy (a :: k). proxy a -> GADT
+    |])
diff --git a/testsuite/tests/th/T5217.stderr b/testsuite/tests/th/T5217.stderr
index 17bbd7b00e..30797a8934 100644
--- a/testsuite/tests/th/T5217.stderr
+++ b/testsuite/tests/th/T5217.stderr
@@ -9,6 +9,6 @@ T5217.hs:(6,3)-(9,53): Splicing declarations
     data T a b
       where
         T1 :: Int -> T Int Char
-        T2 :: forall a. () => a -> T a a
-        T3 :: forall a. () => a -> T [a] a
-        T4 :: forall a b. () => a -> b -> T b [a]
+        T2 :: a -> T a a
+        T3 :: a -> T [a] a
+        T4 :: a -> b -> T b [a]
diff --git a/testsuite/tests/th/T7064.stdout b/testsuite/tests/th/T7064.stdout
index 3cbac10ac9..63c3125972 100644
--- a/testsuite/tests/th/T7064.stdout
+++ b/testsuite/tests/th/T7064.stdout
@@ -17,7 +17,7 @@ instance GHC.Classes.Eq a_0 => GHC.Classes.Eq (T_1 a_0)
           {-# SPECIALISE instance GHC.Classes.Eq (T_1 GHC.Types.Int) #-}
 {-# RULES "rule1"
     GHC.Real.fromIntegral
-    = GHC.Base.id :: forall a_0 . a_0 -> a_0 #-}
+    = GHC.Base.id :: a_0 -> a_0 #-}
 {-# RULES "rule2" [1]
     forall (x_0 :: a_1) . GHC.Real.fromIntegral x_0
     = x_0 #-}
diff --git a/testsuite/tests/th/T8625.stdout b/testsuite/tests/th/T8625.stdout
index 8547e53fd6..13e058d15c 100644
--- a/testsuite/tests/th/T8625.stdout
+++ b/testsuite/tests/th/T8625.stdout
@@ -1,2 +1,2 @@
 [InstanceD Nothing [AppT (AppT EqualityT (VarT y_0)) (AppT (AppT ArrowT (VarT t_1)) (VarT t_1))] (AppT (ConT Ghci1.Member) (ConT GHC.Types.Bool)) []]
-[SigD f_4 (ForallT [PlainTV y_2,PlainTV t_3] [AppT (AppT EqualityT (VarT y_2)) (AppT (AppT ArrowT (VarT t_3)) (VarT t_3))] (AppT (AppT ArrowT (VarT y_2)) (VarT t_3))),FunD f_4 [Clause [VarP x_5] (NormalB (VarE x_5)) []]]
+[SigD f_4 (ForallT [] [AppT (AppT EqualityT (VarT y_2)) (AppT (AppT ArrowT (VarT t_3)) (VarT t_3))] (AppT (AppT ArrowT (VarT y_2)) (VarT t_3))),FunD f_4 [Clause [VarP x_5] (NormalB (VarE x_5)) []]]
diff --git a/testsuite/tests/th/TH_RichKinds2.stderr b/testsuite/tests/th/TH_RichKinds2.stderr
index cb8868c3dd..11829296e0 100644
--- a/testsuite/tests/th/TH_RichKinds2.stderr
+++ b/testsuite/tests/th/TH_RichKinds2.stderr
@@ -1,9 +1,8 @@
 
-TH_RichKinds2.hs:24:4: Warning:
+TH_RichKinds2.hs:24:4: warning:
     data SMaybe_0 :: (k_0 -> *) -> GHC.Base.Maybe k_0 -> * where
-    SNothing_2 :: forall s_3 . SMaybe_0 s_3 'GHC.Base.Nothing
-    SJust_4 :: forall s_5 a_6 . (s_5 a_6) -> SMaybe_0 s_5
-                                                      ('GHC.Base.Just a_6)
+    SNothing_2 :: SMaybe_0 s_3 'GHC.Base.Nothing
+    SJust_4 :: (s_5 a_6) -> SMaybe_0 s_5 ('GHC.Base.Just a_6)
 type instance TH_RichKinds2.Map f_7 '[] = '[]
 type instance TH_RichKinds2.Map f_8
                                 ('GHC.Types.: h_9 t_10) = 'GHC.Types.: (f_8 h_9)
diff --git a/testsuite/tests/th/TH_pragma.stderr b/testsuite/tests/th/TH_pragma.stderr
index ddd5998b39..1156adee27 100644
--- a/testsuite/tests/th/TH_pragma.stderr
+++ b/testsuite/tests/th/TH_pragma.stderr
@@ -11,6 +11,6 @@ TH_pragma.hs:(10,4)-(12,31): Splicing declarations
         {-# SPECIALISE INLINE [~1] bar :: Float -> Float #-}
         bar x = x * 10 |]
   ======>
-    bar :: forall a. Num a => a -> a
+    bar :: Num a => a -> a
     {-# SPECIALISE INLINE [~1] bar :: Float -> Float #-}
     bar x = (x * 10)
diff --git a/testsuite/tests/th/all.T b/testsuite/tests/th/all.T
index 71ab096bc8..917f3157a7 100644
--- a/testsuite/tests/th/all.T
+++ b/testsuite/tests/th/all.T
@@ -367,3 +367,5 @@ test('T12788', [], multimod_compile_fail,
      ['T12788.hs', '-v0 ' + config.ghc_th_way_flags])
 test('T12977', normal, compile, ['-v0'])
 test('T12993', normal, multimod_compile, ['T12993.hs', '-v0'])
+test('T13018', normal, compile, ['-v0'])
+test('T13123', normal, compile, ['-v0'])