Opened 2 years ago

Closed 2 years ago

Last modified 20 months ago

#9953 closed bug (fixed)

Pattern synonyms don't work with GADTs

Reported by: simonpj Owned by: cactus
Priority: normal Milestone: 7.10.1
Component: Compiler (Type checker) Version: 7.10.1-rc1
Keywords: PatternSynonyms Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

Consider this variant of test T8968-1:

{-# LANGUAGE GADTs, KindSignatures, PatternSynonyms #-}
module ShouldCompile where

data X :: * -> * where
  Y :: a -> X (Maybe a)

pattern C :: a -> X (Maybe a)
pattern C x = Y x

foo :: X t -> t
foo (C x) = Just x
  • If we had (Y x) instead of (C x) in the LHS of foo, then this is an ordinary GADT program and typechecks fine.
  • If we omit the pattern signature, it typechecks fine, and :info C says
    pattern C :: t ~ Maybe a => a -> X t 	-- Defined in ‘ShouldCompile’
    
  • But as written, it fails with
    Foo.hs:11:6:
        Couldn't match type ‘t’ with ‘Maybe a0’
          ‘t’ is a rigid type variable bound by
              the type signature for: foo :: X t -> t at Foo.hs:10:8
        Expected type: X t
          Actual type: X (Maybe a0)
        Relevant bindings include foo :: X t -> t (bound at Foo.hs:11:1)
        In the pattern: C x
        In an equation for ‘foo’: foo (C x) = Just x
    
    Moreover, :info C says
    pattern C :: a -> X (Maybe a) 	-- Defined at Foo.hs:8:9
    

Do you see the difference? In the former, the "prov_theta" equality constraint is explicit, but in the latter it's implicit.

The exact thing happens for DataCons. It's handled via the dcEqSpec field. Essentially PatSyn should have a new field for the implicit equality constraints. And, just as for data consructors, we need to generate the equality constraints, and the existentials that are needed, when we process the signature. Use the code in TcTyClsDecls.rejigConRes (perhaps needs a better name).

This is all pretty serious. Without fixing it, GADT-style pattern signatures are all but useless.

Change History (23)

comment:1 Changed 2 years ago by simonpj

Owner: set to cactus

comment:2 Changed 2 years ago by cactus

Component: CompilerCompiler (Type checker)
Keywords: PatternSynonyms added

comment:3 Changed 2 years ago by carter

... should this be remilestoned for 7.10.1 or will we need to do 7.8.5?

comment:4 Changed 2 years ago by cactus

Milestone: 7.10.1

7.8 doesn't have pattern synonym type signatures.

comment:5 Changed 2 years ago by cactus

Version: 7.8.47.10.1-rc1

comment:6 Changed 2 years ago by cactus

I almost have this working in the wip/T9953 branch. However, there is one tricky question, very much related to #9954: what do we do with required constraints that mention some GADT indices?

For example, if pattern C also happened to have a required constraint, e.g. Eq a, where would we put that, if a is no longer a universally-quantified type argument of C? What would be the type of C's matcher?

comment:7 Changed 2 years ago by cactus

Here's a hopefully more enlightening description of the problem in ticket:9953#comment:6. Suppose we have this setup:

{-# LANGUAGE GADTs, PatternSynonyms, ViewPatterns #-}
data X t where
  Y :: a -> X (Maybe a)

f :: (Eq a) => a -> a
f = id

-- inferred type:
-- pattern C1 :: t ~ Maybe a => a -> X t
pattern C1 x = Y x

pattern C2 :: a -> X (Maybe a)
pattern C2 x = Y x

pattern C3 :: () => (Eq a) => a -> X (Maybe a)
pattern C3 x = Y (f -> x)

The difference between C1's inferred type and C2's type is the subject of this ticket; with the point being that we should be reconstructing C1's type from the signature given for C2.

The types of the matchers generated are as follows:

$mC1 :: forall r t.           X t         -> (forall a. (t ~ Maybe a) => a -> r) -> (Void# -> r) -> r
$mC2 :: forall r a.           X (Maybe a) -> (                           a -> r) -> (Void# -> r) -> r
$mC3 :: forall r a. (Eq a) => X (Maybe a) -> (                           a -> r) -> (Void# -> r) -> r

If C2 got the same type as C1, what would be the analogous type for C3? What would be $mC3's type in that case?

comment:8 Changed 2 years ago by simonpj

The inferred type of C1 should be isomoprhic to the declared type of C2. That is you should be able to declare C2's type as

pattern C2 :: (t ~ Maybe a) => a -> X t

if you want. Just as you can in a GADT declaration: the data constructor decl

  C :: arg1 -> arg2 -> T (Maybe a)

is precisely equivalent to (i.e. indistinguishable from)

  C :: (t ~ Maybe a) => arg1 -> arg2 -> T t

In the same way, you should be able to declare C3's type as

pattern C3 :: (t ~ Maybe a) => (Eq a) => a -> X t

if you want.

As discussed in #9954, C3 is simply ill typed.

Does that resolve it?

Simon

comment:9 Changed 2 years ago by simonpj

In email Gergo showed the following example:

data T1 a where
   MkT1 :: a -> T1 (Maybe a)

-- Inferred type pattern P1 :: (t ~ Maybe a) => a -> T t
pattern P1 x <- MkT x

-- Inferred type pattern P2 :: a -> [Maybe a]
pattern P2 x <- [Just x]

When real data constructors are concerned, the types

   T1 :: a -> T1 (Maybe a)
   T1 :: (t ~ Maybe a) => a -> T t

are absolutely equivalent. But the two types are not equivalent for pattern synonyms.

  • When you match against P1 can match a value of type T ty, for any ty; and you get evidence for t ~ Maybe a.
  • But when you match against P2 you can only match a value of type T (Maybe ty); and you get no equality evidence.

The difference is manifest in the different inferred types for P1 and P2.

Principle: you should be able to tell the behaviour of a pattern synonym whose implementation is hidden, just from its type. So the types of P1 and P2 are really different.

The same principle should apply to explicit, user-supplied type signatures. So if you say

pattern P1 :: a -> T (Maybe a)

it should typecheck all right, but you can then only pattern match on values of type T (Maybe ty).

In short, if you want GADT-like behaviour for a pattern synonym, you can get it only by giving explicit equality constraints in the signature, and not by having a complex result type (as you can do for real data constructors).

I had missed this point entirely in my earlier comments -- thank you Gergo for pointing it out.

Are we agreed on that?

Then we can return to the implementation!

But I think the user manual deserves a careful look, to make sure that it articulates these points.

Simon

comment:10 in reply to:  9 Changed 2 years ago by goldfire

Replying to simonpj:

In short, if you want GADT-like behaviour for a pattern synonym, you can get it only by giving explicit equality constraints in the signature, and not by having a complex result type (as you can do for real data constructors).

Yech. This means that declaring a pattern synonym for a GADT data constructor requires writing the type differently than the idiomatic way to do it for data constructors.

I think a second principle might be this: The type signature for a pattern should mean the same thing that it would for a data constructor.

It strikes me that this problem is precisely the same as the required vs. produced distinction. In your P2, t ~ Maybe a is a requirement; in your P1, it's provided.

I don't have a better concrete suggestion at the moment, sadly.

comment:11 Changed 2 years ago by simonpj

No, it's quite different to the produced/required distinction. The produced/required distinction is for things like matching against (Just 34), which required (Num a, Eq a) to perform the match.

And my point is that we cannot say that the type signature for a pattern should mean the same thing that it would for a data constructor; the type signatures for P1 and P2 make this clear. It may be sad but it's absolutely ineluctable.

Simon

comment:12 Changed 2 years ago by goldfire

Here's the example in play:

data T1 a where
   MkT1 :: a -> T1 (Maybe a)

-- Inferred type pattern P1 :: (t ~ Maybe a) => a -> T t
pattern P1 x <- MkT x

-- Inferred type pattern P2 :: a -> [Maybe a]
pattern P2 x <- [Just x]

Couldn't we write these type signatures as

pattern P1 :: (t ~ Maybe a) => () => a -> T  t
pattern P2 :: () => (t ~ Maybe a) => a -> [t]

?

And, I disagree with Simon's conclusion that we cannot have pattern type signatures mean the same as data constructor signatures. We could decide than any non-uniformity in the result type of a pattern signature means a provided equality, just like a GADT. Then, the syntax of the type for P2 would have to change to something else -- after all, P2 is not the synonym of any valid data constructor.

As we're thinking about this, it strikes me that there is some relationship between the current debate and the distinction between GADTs and data families. For example:

data G a where
  MkGInt :: G Int

data family H a
data instance H Int where
  MkHInt :: H Int

MkGInt is a GADT constructor that provides an equality when matching. MkHInt, on the other hand, requires the equality when matching. Yet both have the same type signature. So, something a little confusing is going on here. Do pattern synonyms work properly with data families?

comment:13 Changed 2 years ago by simonpj

Well Richard, you are proposing that you can write P1's type signature just like T1's. Fair enough, I can see some merit; indeed it was my initial position. But then you must write P2's type signature in some other way. What other way do you propose??

Since we already have two different ways to write the signature, we are at liberty to decide that those two different ways define two different behaviours; and that is what I am proposing. Yes, we could invent a third way, but that introduces a whole new raft of complications. (E.g. can you use that third way in a GADT declaration? For an ordinary function? etc)

I'm totally open to considering alternative. But until we have one, let's get on with implementing the proposal we have. That is often illuminating; and if we come up with a better idea meanwhile we can retro-fit it easily enough.

For data families, I think it should all work fine. But indeed we should check.

Simon

comment:14 Changed 2 years ago by cactus

I have no idea what the proposal is anymore... which I find a bit worrying, given I am supposed to implement it.

Right now, on master as of 6f818e08, this is the behaviour you get:

{-# LANGUAGE GADTs, KindSignatures, PatternSynonyms #-}
module ShouldCompile where

data X b where
  Y :: [a] -> X (Maybe a)

pattern C1 :: [a] -> X (Maybe a)
pattern C1 x <- Y x

pattern C2 x <- Y x

pattern C3 :: (t ~ Maybe a) => [a] -> X t
pattern C3 x <- Y x

with this setup, you get

λ» :i C1
pattern C1 :: [a] -> X (Maybe a) 	-- Defined at T9953-3.hs:8:9
λ» :i C2
pattern C2 :: t ~ Maybe a => [a] -> X t
  	-- Defined at T9953-3.hs:10:9
λ» :i C3
pattern C3 :: t ~ Maybe a => [a] -> X t
  	-- Defined at T9953-3.hs:13:9

Isn't this exactly the behaviour specified by Simon's latest comment?

comment:15 Changed 2 years ago by simonpj

Correct. The original ticket description says "Without fixing it, GADT-style pattern signatures are all but useless", and the conclusion of the discussion is that we can't use GADT-style pattern signatures!

So yes, all that remains is to review the user manual to ensure that it makes this point explicit. I don't think we need any implementation changes. (Contrary to my initial supposition.)

Simon

comment:16 Changed 2 years ago by Simon Peyton Jones <simonpj@…>

In 8e774ba1c0fb38a1e01d156734c8a1acf0b1e59b/ghc:

Improve documentation of pattern synonyms, to reflect conclusion of Trac #9953

comment:17 Changed 2 years ago by simonpj

Status: newmerge

OK I fixed the user manual myself. Let's merge the change into 7.10 (assuming that the prior stuff about pattern signatures is in, which I think it is).

Simoin

comment:18 Changed 2 years ago by thoughtpolice

Resolution: fixed
Status: mergeclosed

Merged to ghc-7.10 (via 53af4bb5cd4531f0615a2a60b6d213495261e41a).

comment:19 Changed 20 months ago by bgamari

It appears that there are still two tests marked as broken due to this issue (T8968-1 and T8968-3). They appear to be fixed by either 28096b274a3803b8a479c5dd94ebda655a15566c or 953648127cea2836ec134b03a966695ac0b36434 (both commits by Simon PJ). Simon, is this an expected consequence of this rework?

comment:20 Changed 20 months ago by simonpj

I'm looking at it; it's tricky stuff. Meanwhile, you could make validate work again, opening a ticket for this issue, so that everyone else was not inconvenienced.

comment:21 Changed 20 months ago by bgamari

The real question is why were these tests marked as broken against a closed ticket? Are they actually expected to work?

comment:22 Changed 20 months ago by simonpj

OK. I believe the "expect-broken" is because we get (odd-looking) error

T8968-1.hs:8:9: warning:
    Redundant constraint: Maybe a ~ Maybe a
    In the type signature for: C :: a -> X Maybe (Maybe a)

Now one of the minor changes in

commit 953648127cea2836ec134b03a966695ac0b36434
Author: Simon Peyton Jones <simonpj@microsoft.com>
Date:   Wed Aug 5 14:24:54 2015 +0100

    Tidy up and refactor wildcard handling

was to add a new UserTypeCtxt for pattern synonyms, namely PatSynCtxt. Previously I used FunSigCtxt.

Then in TcSimplify.warnRedundantGivens I treat PatSynCtxt (like most others) as "do't report redundant constraints". So the behaviour changes: redundant constraints are no longer reported for pattern synonyms.

So, just remove the expect-broken; it's fine for them to pass. I suppose that warning abour redundant constraints in pattern-synonym signatures might be a good thing, but that's a battle for another day.

comment:23 Changed 20 months ago by Simon Peyton Jones <simonpj@…>

In 294553e9/ghc:

T8968-1 and -3 should pass

See Trac #9953, comment:22.
Note: See TracTickets for help on using tickets.