Commit 729a5e45 authored by Ryan Scott's avatar Ryan Scott

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
parent 18ceb148
......@@ -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)
......
......@@ -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
~~~~~~~~~~~~~~
......
[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)) []]]
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
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
{-# 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
|])
{-# 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
|])
......@@ -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]
......@@ -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 #-}
......
[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)) []]]
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)
......
......@@ -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)
......@@ -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'])
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment