Opened 10 months ago

Closed 9 months 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 10 months ago by mpickering

Cc: PatternSynonyms removed
Keywords: PatternSynonyms added

comment:2 Changed 10 months ago by RyanGlScott

The quoting mechanism doesn't appear to be at fault here, since you can trigger the same bug using only Language.Haskell.TH:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TemplateHaskell #-}
module Bug where

import Language.Haskell.TH

data T a where
  MkT :: Eq b => b -> T a

$(do pName <- newName "P"
     aName <- newName "a"
     bName <- newName "b"
     xName <- newName "x"
     return [ PatSynSigD pName (ForallT [PlainTV bName,PlainTV aName] [] (ForallT [] [] (AppT (AppT ArrowT (VarT bName)) (AppT (ConT ''T) (VarT aName)))))
            , PatSynD pName (PrefixPatSyn [xName]) Unidir (ConP 'MkT [VarP xName])
            ]
 )

comment:3 Changed 10 months ago by RyanGlScott

Component: Template HaskellCompiler (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 10 months ago by RyanGlScott

Version: 8.18.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 Changed 10 months ago by simonpj

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 in reply to:  5 Changed 10 months ago by RyanGlScott

Thank you Simon, that's very helpful. I forgot about the need for two foralls, and it turns out that as a workaround, you can fix the issue by specifying the foralls 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 foralls 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 10 months ago by RyanGlScott

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 10 months ago by RyanGlScott

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 Types, we have HsTypes! Is there an HsType counterpart to tyCoVarsOfTypes somewhere in the GHC codebase?

comment:9 Changed 10 months ago by goldfire

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 10 months ago by RyanGlScott

I'm not sure if the advice in comment:9 is feasible, sadly. Not only would you need to generalize extractHsTyRdrTyVars to work over RdrNames and Names (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 10 months ago by goldfire

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 9 months ago by simonpj

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 9 months ago by RyanGlScott

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 9 months ago by RyanGlScott

See also #13123, where a overeager quantification causes a different error.

Last edited 9 months ago by RyanGlScott (previous) (diff)

comment:15 Changed 9 months ago by RyanGlScott

Differential Rev(s): Phab:D2974
Milestone: 8.2.1
Status: newpatch

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 9 months ago by RyanGlScott

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:17 Changed 9 months ago by Ryan Scott <ryan.gl.scott@…>

In 729a5e45/ghc:

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

comment:18 Changed 9 months ago by RyanGlScott

Resolution: fixed
Status: patchclosed
Test Case: th/T13018
Note: See TracTickets for help on using tickets.