Opened 3 years ago
Closed 3 years ago
#13018 closed bug (fixed)
TH-spliced pattern synonym declaration fails to typecheck
Reported by: | RyanGlScott | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | 8.2.1 |
Component: | Compiler (Type checker) | Version: | 8.0.1 |
Keywords: | PatternSynonyms | Cc: | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | GHC rejects valid program | Test Case: | th/T13018 |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | Phab:D2974 | |
Wiki Page: |
Description
This pattern synonyms typechecks without issue:
{-# LANGUAGE GADTs #-} {-# LANGUAGE PatternSynonyms #-} module Works where data T a where MkT :: Eq b => b -> T a pattern P :: b -> T a pattern P x <- MkT x
But if you try to create P
from a Template Haskell splice, it will fail to typecheck:
{-# LANGUAGE GADTs #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE TemplateHaskell #-} module Bug where data T a where MkT :: Eq b => b -> T a $([d| pattern P :: b -> T a; pattern P x <- MkT x |])
$ /opt/ghc/head/bin/ghc Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:9:3: error: • Couldn't match expected type ‘b0’ with actual type ‘b’ ‘b’ is a rigid type variable bound by a pattern with constructor: MkT :: forall a b. Eq b => b -> T a, in a pattern synonym declaration at Bug.hs:9:3-52 ‘b0’ is a rigid type variable bound by the signature for pattern synonym ‘P’ at Bug.hs:9:3-52 • In the declaration for pattern synonym ‘P’ • Relevant bindings include x_a4tP :: b (bound at Bug.hs:9:3)
Change History (18)
comment:1 Changed 3 years ago by
Cc: | PatternSynonyms removed |
---|---|
Keywords: | PatternSynonyms added |
comment:2 Changed 3 years ago by
comment:3 Changed 3 years ago by
Component: | Template Haskell → Compiler (Type checker) |
---|
It turns out this has nothing whatsoever to do with Template Haskell. The real culprit is forall
. That is, while this program compiles without issue:
{-# LANGUAGE GADTs #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ScopedTypeVariables #-} module M where data T a where MkT :: Eq b => b -> T a pattern P :: b -> T a pattern P x <- MkT x
Changing the pattern signature to this:
pattern P :: forall b a. b -> T a
causes the error to appear:
Bug.hs:10:20: error: • Couldn't match expected type ‘b’ with actual type ‘b1’ ‘b1’ is a rigid type variable bound by a pattern with constructor: MkT :: forall a b. Eq b => b -> T a, in a pattern synonym declaration at Bug.hs:10:16-20 ‘b’ is a rigid type variable bound by the signature for pattern synonym ‘P’ at Bug.hs:9:21 • In the declaration for pattern synonym ‘P’ • Relevant bindings include x :: b1 (bound at Bug.hs:10:20)
It turns out that when you quote a pattern synonym declaration with TH quotes, it implicitly adds the forall
behind the scenes, triggering this bug when you try to splice it back in.
comment:4 Changed 3 years ago by
Version: | 8.1 → 8.0.1 |
---|
It turns out this is a regression, since this program:
{-# LANGUAGE GADTs #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ScopedTypeVariables #-} module M where data T a where MkT :: Eq b => b -> T a pattern P :: forall b a. b -> T a pattern P x <- MkT x
compiles with GHC 7.10.3, but not with GHC 8.0.1, 8.0.2, or HEAD.
comment:5 follow-up: 6 Changed 3 years ago by
It's not a regression; it's a bug-fix! See Trac #11224.
Here's the note from TcTySigs
:
Note [The pattern-synonym signature splitting rule] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Given a pattern signature, we must split the kind-generalised variables, and the implicitly-bound variables into universal and existential. The rule is this (see discussion on Trac #11224): The universal tyvars are the ones mentioned in - univ_tvs: the user-specified (forall'd) universals - req_theta - res_ty The existential tyvars are all the rest
If you provide an explicit forall, they are all universals; but in this case we wanted 'b' to be an existential. According to these rules you can say
pattern P :: b -> T a or pattern P :: forall a. () => forall b. b -> T a
We neglected to put this rule in the user manual: that should be fixed. Matthew or Ryan, might you do that?
The TH problem is that TH is taking a quote with an implicit forall, and turning it into a TH data structure with an explicit forall. When that is converted back into HsSyn
it has an explicit forall, so we get pattern P :: forall b a. b -> T a
. So the round trip is not faithful.
I wonder if we could just genertate TH syntax with an implicit forall?
comment:6 Changed 3 years ago by
Thank you Simon, that's very helpful. I forgot about the need for two forall
s, and it turns out that as a workaround, you can fix the issue by specifying the forall
s manually. As evidence, this compiles:
{-# LANGUAGE GADTs #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TemplateHaskell #-} module M where data T a where MkT :: Eq b => b -> T a $([d| pattern P :: forall a. forall b. b -> T a pattern P x <- MkT x |])
So the only issue to investigate is why this:
$([d| pattern P :: b -> T a pattern P x <- MkT x |])
fails to infer the forall
s correctly.
Replying to simonpj:
I wonder if we could just genertate TH syntax with an implicit forall?
TH is already coming up with an implicit forall
, just in an incorrect way. Note that this:
$([d| pattern P :: b -> T a pattern P x <- MkT x |])
gets turned into this (as reported by -ddump-splices
):
[d| pattern P_a1iH :: b_a1iI -> T a_a1iJ pattern P_a1iH x_a1iK <- MkT x_a1iK |] ======> pattern P_a4tM :: forall b_a4tN a_a4tO. b_a4tN -> T a_a4tO pattern P_a4tM x_a4tP <- MkT x_a4tP
comment:7 Changed 3 years ago by
From a quick investigation, the problematic code seems to be repHsPatSynSigType in DsMeta
:
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 -> 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 , hsq_dependent = emptyNameSet } (univs, reqs, exis, provs, ty) = splitLHsPatSynTy body
In this particular example, all of univs
, reqs
, exis
, and provs
are []
. But impls
is [b,a]
, which causes th_univs
to be [b,a]
as well. In other words, that's why we see the incorrect forall b a. forall. b -> T a
type signature.
Is there a way to partition up impls
to get a
in th_univs
and b
in th_exis
?
comment:8 Changed 3 years ago by
I made some progress in investigating the pattern synonyms codebase. This "partitioning" I wondered about in comment:7 is described in Note [The pattern-synonym signature splitting rule]
:
Note [The pattern-synonym signature splitting rule] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Given a pattern signature, we must split the kind-generalised variables, and the implicitly-bound variables into universal and existential. The rule is this (see discussion on Trac #11224): The universal tyvars are the ones mentioned in - univ_tvs: the user-specified (forall'd) universals - req_theta - res_ty The existential tyvars are all the rest
And in tcCheckPatSynDecl, this is implemented like so:
let univ_fvs = closeOverKinds $ (tyCoVarsOfTypes (pat_ty : req_theta) `extendVarSetList` explicit_univ_tvs) (extra_univ, extra_ex) = partition ((`elemVarSet` univ_fvs) . binderVar) implicit_tvs univ_bndrs = extra_univ ++ mkTyVarBinders Specified explicit_univ_tvs ex_bndrs = extra_ex ++ mkTyVarBinders Specified explicit_ex_tvs univ_tvs = binderVars univ_bndrs ex_tvs = binderVars ex_bndrs
So I think in order to fix this bug, we'd just need to implement something analogous to the above in repHsPatSynSigType
. But I'm stuck: the code above requires calculating free variables using tyCoVarsOfTypes
, which takes [Type]
as an argument. But in repHsPatSynSigType
, we don't have Type
s, we have HsType
s! Is there an HsType
counterpart to tyCoVarsOfTypes
somewhere in the GHC codebase?
comment:9 Changed 3 years ago by
Agreed that the splitting rule must be implemented in the TH quoting mechanism. Check out RnTypes.extractHsTyRdrTyVars
and friends. If you have HsType Name
(instead of HsType RdrName
), you may be able to generalize these functions.
comment:10 Changed 3 years ago by
I'm not sure if the advice in comment:9 is feasible, sadly. Not only would you need to generalize extractHsTyRdrTyVars
to work over RdrName
s and Name
s (which I was able to do), you also have to overcome the issue that repHsPatSynSigType
lives in DsM
(i.e., TcRnIf DsGblEnv DsLclEnv
) but extractHsTyRdrTyVars
lives in RnM
(i.e., TcRnIf TcGblEnv TcLclEnv
).
I don't see a way to generalize the return type of extractHsTyRdrTyVars
in a way that wouldn't have an enormous ripple effect across tons of GHC API functions, so I'm giving up on this for now.
comment:11 Changed 3 years ago by
I made these functions monadic not too long ago. Looking back through, it seems the only RnM
action taken is addErrAt
from mixedVarsErr
(and the related xoptM
call). It wouldn't be hard to augment the FreeKiTyVars
structure to include a list of errors generated. Then, the whole lot of these functions could be made pure. This would seem to be an improvement -- especially in your case when you are not interested in error messages.
Alternatively, I've recently run into the need to have functions be used in both TcM
and DsM
, but the only monadic action, again, was error generation. It might be reasonable to have a ErrMonad
class with instances for both TcM
and DsM
; then these extractXXX
functions could be generalized over that class.
comment:12 Changed 3 years ago by
Agreed that the splitting rule must be implemented in the TH quoting mechanism.
I do not agree.
The business of TH is to reflect Haskell source code. In this case the Haskell source code signature is
pattern P :: b -> T a
That generates a LHsSigType
for the type. We should be able to round-trip that LHsSigType
through TH and get back the exact same thing. If we do that then, because it's the exact same thing, if it typechecked before it'll typecheck after the round trip.
What is happening, I think, is that we are getting back a LHsSigType
with more explicit quantification that the original one had. That's bad! We should get back the exact same thing.
I haven't dug deeper, but that must be possible, right?
I think it's the wrong thing for the TH (syntax-level) conversions to attempt to figure out what is quantified where. Just reproduce what the user wrote!
Simon
comment:13 Changed 3 years ago by
Well, there's certainly a technical issue in that quoting any function (not just pattern synonyms) will always add explicit quantification if it isn't present to begin with. For example:
λ> putStrLn $([d| id :: a -> a; id x = x |] >>= stringE . pprint) id_0 :: forall a_1 . a_1 -> a_1 id_0 x_2 = x_2 λ> putStrLn $([d| id :: a -> a; id x = x |] >>= stringE . show) [SigD id_6989586621679026833 (ForallT [PlainTV a_6989586621679026832] [] (AppT (AppT ArrowT (VarT a_6989586621679026832)) (VarT a_6989586621679026832))),FunD id_6989586621679026833 [Clause [VarP x_6989586621679026834] (NormalB (VarE x_6989586621679026834)) []]]
Note how the ForallT [PlainTV a_6989586621679026832] ...
gets added. So we'd need to be able to somehow preserve the fact that id
was originally quoted without explicit quantification. We'd need to do this for functions and pattern synonyms for sure (and maybe other declarations that I'm not thinking of right now?).
comment:14 Changed 3 years ago by
See also #13123, where a overeager quantification causes a different error.
comment:15 Changed 3 years ago by
Differential Rev(s): | → Phab:D2974 |
---|---|
Milestone: | → 8.2.1 |
Status: | new → patch |
Happily, having quoting respect implicitly quantified variables turned out to be simple. Phab:D2974 fixes this without needing to implement any splitting rule sorcery.
comment:16 Changed 3 years ago by
In light of Richard's suggestion on the Phab Diff, I've opened a GHC proposal to discuss the specifics of introducing ImplicitForallT
and ImplicitForallC
to contain implicitly quantified type variables in quoted type signatures.
comment:18 Changed 3 years ago by
Resolution: | → fixed |
---|---|
Status: | patch → closed |
Test Case: | → th/T13018 |
The quoting mechanism doesn't appear to be at fault here, since you can trigger the same bug using only
Language.Haskell.TH
: