Don't quantify implicit type variables when quoting type signatures in TH
authorRyan Scott <ryan.gl.scott@gmail.com>
Mon, 23 Jan 2017 14:06:04 +0000 (09:06 -0500)
committerRyan Scott <ryan.gl.scott@gmail.com>
Mon, 23 Jan 2017 14:06:04 +0000 (09:06 -0500)
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

13 files changed:
compiler/deSugar/DsMeta.hs
docs/users_guide/8.2.1-notes.rst
testsuite/tests/ghci/scripts/T11098.stdout
testsuite/tests/th/T10828.stderr
testsuite/tests/th/T11797.stderr
testsuite/tests/th/T13018.hs [new file with mode: 0644]
testsuite/tests/th/T13123.hs [new file with mode: 0644]
testsuite/tests/th/T5217.stderr
testsuite/tests/th/T7064.stdout
testsuite/tests/th/T8625.stdout
testsuite/tests/th/TH_RichKinds2.stderr
testsuite/tests/th/TH_pragma.stderr
testsuite/tests/th/all.T

index 9a76c81..b43f728 100644 (file)
@@ -237,6 +237,27 @@ So in repTopDs we bring the binders into scope with mkGenSyms and addBinds.
 And we use lookupOcc, rather than lookupBinder
 in repTyClD and repC.
 
+Note [Don't quantify implicit type variables in quotes]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If you're not careful, it's suprisingly easy to take this quoted declaration:
+
+  [d| idProxy :: forall proxy (b :: k). proxy b -> proxy b
+      idProxy x = x
+    |]
+
+and have Template Haskell turn it into this:
+
+  idProxy :: forall k proxy (b :: k). proxy b -> proxy b
+  idProxy x = x
+
+Notice that we explicitly quantifed the variable `k`! This is quite bad, as the
+latter declaration requires -XTypeInType, while the former does not. Not to
+mention that the latter declaration isn't even what the user wrote in the
+first place.
+
+Usually, the culprit behind these bugs is taking implicitly quantified type
+variables (often from the hsib_vars field of HsImplicitBinders) and putting
+them into a `ForallT` or `ForallC`. Doing so caused #13018 and #13123.
 -}
 
 -- represent associated family instances
@@ -623,27 +644,30 @@ repC (L _ (ConDeclH98 { con_name = con
        }
 
 repC (L _ (ConDeclGADT { con_names = cons
-                       , con_type = res_ty@(HsIB { hsib_vars = con_vars })}))
+                       , con_type = res_ty@(HsIB { hsib_vars = imp_tvs })}))
   | (details, res_ty', L _ [] , []) <- gadtDetails
-  , [] <- con_vars
+  , [] <- imp_tvs
     -- no implicit or explicit variables, no context = no need for a forall
   = do { let doc = text "In the constructor for " <+> ppr (head cons)
        ; (hs_details, gadt_res_ty) <-
            updateGadtResult failWithDs doc details res_ty'
        ; repGadtDataCons cons hs_details gadt_res_ty }
 
-  | (details,res_ty',ctxt, tvs) <- gadtDetails
+  | (details,res_ty',ctxt, exp_tvs) <- gadtDetails
   = do { let doc = text "In the constructor for " <+> ppr (head cons)
-             con_tvs = HsQTvs { hsq_implicit = []
-                              , hsq_explicit = (map (noLoc . UserTyVar . noLoc)
-                                                   con_vars) ++ tvs
+             con_tvs = HsQTvs { hsq_implicit  = imp_tvs
+                              , hsq_explicit  = exp_tvs
                               , hsq_dependent = emptyNameSet }
+             -- NB: Don't put imp_tvs into the hsq_explicit field above
+             -- See Note [Don't quantify implicit type variables in quotes]
        ; addTyVarBinds con_tvs $ \ ex_bndrs -> do
        { (hs_details, gadt_res_ty) <-
            updateGadtResult failWithDs doc details res_ty'
        ; c'    <- repGadtDataCons cons hs_details gadt_res_ty
        ; ctxt' <- repContext (unLoc ctxt)
-       ; rep2 forallCName ([unC ex_bndrs, unC ctxt', unC c']) } }
+       ; if null exp_tvs && null (unLoc ctxt)
+         then return c'
+         else rep2 forallCName ([unC ex_bndrs, unC ctxt', unC c']) } }
   where
      gadtDetails = gadtDeclDetails res_ty
 
@@ -737,18 +761,21 @@ rep_wc_ty_sig :: Name -> SrcSpan -> LHsSigWcType Name -> Located Name
     -- We must special-case the top-level explicit for-all of a TypeSig
     -- See Note [Scoped type variables in bindings]
 rep_wc_ty_sig mk_sig loc sig_ty nm
-  | HsIB { hsib_vars = implicit_tvs, hsib_body = hs_ty } <- hswc_body sig_ty
+  | HsIB { hsib_body = hs_ty } <- hswc_body sig_ty
   , (explicit_tvs, ctxt, ty) <- splitLHsSigmaTy hs_ty
   = do { nm1 <- lookupLOcc nm
        ; let rep_in_scope_tv tv = do { name <- lookupBinder (hsLTyVarName tv)
                                      ; repTyVarBndrWithKind tv name }
-             all_tvs = map (noLoc . UserTyVar . noLoc) implicit_tvs ++ explicit_tvs
-       ; th_tvs  <- repList tyVarBndrTyConName rep_in_scope_tv all_tvs
+       ; th_explicit_tvs <- repList tyVarBndrTyConName rep_in_scope_tv
+                                    explicit_tvs
+         -- NB: Don't pass any implicit type variables to repList above
+         -- See Note [Don't quantify implicit type variables in quotes]
+
        ; th_ctxt <- repLContext ctxt
        ; th_ty   <- repLTy ty
-       ; ty1 <- if null all_tvs && null (unLoc ctxt)
+       ; ty1 <- if null explicit_tvs && null (unLoc ctxt)
                 then return th_ty
-                else repTForall th_tvs th_ctxt th_ty
+                else repTForall th_explicit_tvs th_ctxt th_ty
        ; sig <- repProto mk_sig nm1 ty1
        ; return (loc, sig) }
 
@@ -887,35 +914,38 @@ repContext ctxt = do preds <- repList typeQTyConName repLTy ctxt
                      repCtxt preds
 
 repHsSigType :: LHsSigType Name -> DsM (Core TH.TypeQ)
-repHsSigType (HsIB { hsib_vars = vars
+repHsSigType (HsIB { hsib_vars = implicit_tvs
                    , hsib_body = body })
   | (explicit_tvs, ctxt, ty) <- splitLHsSigmaTy body
-  = addTyVarBinds (HsQTvs { hsq_implicit = []
-                          , hsq_explicit = map (noLoc . UserTyVar . noLoc) vars ++
-                                           explicit_tvs
+  = addTyVarBinds (HsQTvs { hsq_implicit = implicit_tvs
+                          , hsq_explicit = explicit_tvs
                           , hsq_dependent = emptyNameSet })
-                  $ \ th_tvs ->
+    -- NB: Don't pass implicit_tvs to the hsq_explicit field above
+    -- See Note [Don't quantify implicit type variables in quotes]
+                  $ \ th_explicit_tvs ->
     do { th_ctxt <- repLContext ctxt
        ; th_ty   <- repLTy ty
-       ; if null vars && null explicit_tvs && null (unLoc ctxt)
+       ; if null explicit_tvs && null (unLoc ctxt)
          then return th_ty
-         else repTForall th_tvs th_ctxt th_ty }
+         else repTForall th_explicit_tvs th_ctxt th_ty }
 
 repHsPatSynSigType :: LHsSigType Name -> DsM (Core TH.TypeQ)
 repHsPatSynSigType (HsIB { hsib_vars = implicit_tvs
                          , hsib_body = body })
-  = addTyVarBinds (newTvs (impls ++ univs)) $ \th_univs ->
-      addTyVarBinds (newTvs exis) $ \th_exis ->
+  = addTyVarBinds (newTvs implicit_tvs univs) $ \th_univs ->
+      addTyVarBinds (newTvs [] exis) $ \th_exis ->
     do { th_reqs  <- repLContext reqs
        ; th_provs <- repLContext provs
        ; th_ty    <- repLTy ty
        ; repTForall th_univs th_reqs =<< (repTForall th_exis th_provs th_ty) }
   where
-    impls = map (noLoc . UserTyVar . noLoc) implicit_tvs
-    newTvs tvs = HsQTvs
-      { hsq_implicit  = []
-      , hsq_explicit  = tvs
+    newTvs impl_tvs expl_tvs = HsQTvs
+      { hsq_implicit  = impl_tvs
+      , hsq_explicit  = expl_tvs
       , hsq_dependent = emptyNameSet }
+    -- NB: Don't pass impl_tvs to the hsq_explicit field above
+    -- See Note [Don't quantify implicit type variables in quotes]
+
     (univs, reqs, exis, provs, ty) = splitLHsPatSynTy body
 
 repHsSigWcType :: LHsSigWcType Name -> DsM (Core TH.TypeQ)
index 094fce9..7e75461 100644 (file)
@@ -148,6 +148,42 @@ Template Haskell
    be ambiguous in the presence of :ghc-flag:`-XPolyKinds`.
    (:ghc-ticket:`12646`)
 
+-  Quoted type signatures are more accurate with respect to implicitly
+   quantified type variables. Before, if you quoted this: ::
+
+     [d| id :: a -> a
+         id x = x
+       |]
+
+   then the code that Template Haskell would give back to you would actually be
+   this instead: ::
+
+     id :: forall a. a -> a
+     id x = x
+
+   That is, quoting would explicitly quantify all type variables, even ones
+   that were implicitly quantified in the source. This could be especially
+   harmful if a kind variable was implicitly quantified. For example, if
+   you took this quoted declaration: ::
+
+     [d| idProxy :: forall proxy (b :: k). proxy b -> proxy b
+         idProxy x = x
+       |]
+
+   and tried to splice it back in, you'd get this instead: ::
+
+     idProxy :: forall k proxy (b :: k). proxy b -> proxy b
+     idProxy x = x
+
+   Now ``k`` is explicitly quantified, and that requires turning on
+   :ghc-flag:`-XTypeInType`, whereas the original declaration did not!
+
+   Template Haskell quoting now respects implicit quantification in type
+   signatures, so the quoted declarations above now correctly leave the
+   type variables ``a`` and ``k`` as implicitly quantified.
+   (:ghc-ticket:`13018` and :ghc-ticket:`13123`)
+
+
 Runtime system
 ~~~~~~~~~~~~~~
 
index 2b86289..5a74805 100644 (file)
@@ -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)) []]]
index c361a15..82509ec 100644 (file)
@@ -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
index 1b43982..b978e63 100644 (file)
@@ -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 (file)
index 0000000..8b46d88
--- /dev/null
@@ -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 (file)
index 0000000..987283b
--- /dev/null
@@ -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
+    |])
index 17bbd7b..30797a8 100644 (file)
@@ -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]
index 3cbac10..63c3125 100644 (file)
@@ -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 #-}
index 8547e53..13e058d 100644 (file)
@@ -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)) []]]
index cb8868c..1182929 100644 (file)
@@ -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)
index ddd5998..1156ade 100644 (file)
@@ -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)
index 71ab096..917f315 100644 (file)
@@ -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'])