#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 offoo
, then this is an ordinary GADT program and typechecks fine.
- If we omit the pattern signature, it typechecks fine, and
:info C
sayspattern 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
sayspattern 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 3 years ago by
Owner: | set to cactus |
---|
comment:2 Changed 3 years ago by
Component: | Compiler → Compiler (Type checker) |
---|---|
Keywords: | PatternSynonyms added |
comment:3 Changed 3 years ago by
comment:4 Changed 3 years ago by
Milestone: | → 7.10.1 |
---|
7.8 doesn't have pattern synonym type signatures.
comment:5 Changed 3 years ago by
Version: | 7.8.4 → 7.10.1-rc1 |
---|
comment:6 Changed 3 years ago by
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 3 years ago by
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 3 years ago by
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 follow-up: 10 Changed 3 years ago by
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 typeT ty
, for anyty
; and you get evidence fort ~ Maybe a
. - But when you match against
P2
you can only match a value of typeT (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 Changed 3 years ago by
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 3 years ago by
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 3 years ago by
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 3 years ago by
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 3 years ago by
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 3 years ago by
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:17 Changed 3 years ago by
Status: | new → merge |
---|
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 3 years ago by
Resolution: | → fixed |
---|---|
Status: | merge → closed |
Merged to ghc-7.10
(via 53af4bb5cd4531f0615a2a60b6d213495261e41a).
comment:19 Changed 3 years ago by
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 3 years ago by
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 3 years ago by
The real question is why were these tests marked as broken against a closed ticket? Are they actually expected to work?
comment:22 Changed 3 years ago by
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.
... should this be remilestoned for 7.10.1 or will we need to do 7.8.5?