#8968 closed bug (fixed)
Pattern synonyms and GADTs
Reported by: | kosmikus | Owned by: | cactus |
---|---|---|---|
Priority: | normal | Milestone: | 7.10.1 |
Component: | Compiler (Type checker) | Version: | 7.8.1-rc2 |
Keywords: | PatternSynonyms | Cc: | cactus, dimitris@… |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | GHC rejects valid program | Test Case: | |
Blocked By: | #8584 | Blocking: | |
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description
I think this one is different from #8966, but feel free to close one as duplicate if it turns out to be the same problem.
The following program (using GADTs and pattern synonyms, but not kind polymorphism or data kinds) fails to check with ghc-7.8.1-rc2, but I think it should:
{-# LANGUAGE GADTs, KindSignatures, PatternSynonyms #-} data X :: (* -> *) -> * -> * where Y :: f Int -> X f Int pattern C x = Y (Just x)
The error I get is the following:
PatKind.hs:6:18: Couldn't match type ‘t’ with ‘Maybe’ ‘t’ is untouchable inside the constraints (t1 ~ Int) bound by a pattern with constructor Y :: forall (f :: * -> *). f Int -> X f Int, in a pattern synonym declaration at PatKind.hs:6:15-24 ‘t’ is a rigid type variable bound by the inferred type of C :: X t t1 x :: Int at PatKind.hs:1:1 Expected type: t Int Actual type: Maybe Int In the pattern: Just x In the pattern: Y (Just x) PatKind.hs:6:18: Could not deduce (t ~ Maybe) from the context (t1 ~ Int) bound by the type signature for (Main.$WC) :: t1 ~ Int => Int -> X t t1 at PatKind.hs:6:9 ‘t’ is a rigid type variable bound by the type signature for (Main.$WC) :: t1 ~ Int => Int -> X t t1 at PatKind.hs:1:1 Expected type: t Int Actual type: Maybe Int Relevant bindings include ($WC) :: Int -> X t t1 (bound at PatKind.hs:6:9) In the first argument of ‘Y’, namely ‘(Just x)’ In the expression: Y (Just x)
Note that I'd be perfectly happy to provide a type signature for the pattern synonym, but I don't know of any syntax I could use. The Wiki page at https://ghc.haskell.org/trac/ghc/wiki/PatternSynonyms mentions I might be able to write
pattern C :: Int -> X Maybe Int
but this triggers a parse error.
Change History (26)
comment:1 Changed 3 years ago by
Cc: | cactus dimitris@… added |
---|
comment:2 Changed 3 years ago by
FWIW, I was assuming the problem that SPJ describes is the underlying problem here. I don't know the implementation, but I find it entirely reasonable that pattern synonyms for GADTs will in general require type signatures in order to disambiguate between incomparable types. That's why I started talking about type signatures for pattern synonyms in the first place.
comment:3 Changed 3 years ago by
We don't have frontend support for pattern synonym signatures (see #8584). However, this can be worked around using the technique described in #8584, so I was able to get your code to typecheck by modifying it as:
{-# LANGUAGE GADTs, KindSignatures, PatternSynonyms, ScopedTypeVariables #-} data X :: (* -> *) -> * -> * where Y :: f Int -> X f Int pattern C x = (Y (Just x) :: X Maybe Int)
comment:4 Changed 3 years ago by
Thanks. This is actually helping. However, it doesn't seem to work all the time.
Consider this small variation of my program above:
{-# LANGUAGE GADTs, KindSignatures, PatternSynonyms, ScopedTypeVariables #-} data X :: (* -> *) -> * -> * where Y :: f a -> X f (Maybe a) -- pattern C :: a -> X Maybe (Maybe a) pattern C x = Y (Just x) :: X Maybe (Maybe a)
The a
variable in the type signature cannot be quantified, because it's the type of x
. I don't seem to be able to give a type signature to x
on the LHS. The attempt
as given above results in an internal error:
PatKind.hs:7:44: GHC internal error: ‘a’ is not in scope during type checking, but it passed the renamer tcl_env of environment: [(a5PN, Identifier[x::a, <NotTopLevel>])] In an expression type signature: X Maybe (Maybe a) In the expression: Y (Just x) :: X Maybe (Maybe a) In an equation for ‘$WC’: ($WC) x = Y (Just x) :: X Maybe (Maybe a)
Any further ideas?
comment:6 follow-up: 7 Changed 3 years ago by
After thinking about this some more, I'm getting more confused.
How should pattern matching on these pattern synonyms work? Both P
in SPJ's example and C
in my examples are bidirectional pattern synonyms, and as an expression, it should be easy enough for GHC to type-check without a type signature. So why require one in this case? The expression type signature and pattern type signature must be the same, after all.
(Even for unidirectional ones, I'd argue that probably inferring a type for the pattern itself shouldn't be too difficult.)
The main question is whether such synonyms can then be used in order to trigger type refinement. It currently seems they cannot, no matter what type they have.
For my original example, consider this:
{-# LANGUAGE GADTs, KindSignatures, PatternSynonyms, ScopedTypeVariables #-} data X :: (* -> *) -> * -> * where Y :: f Int -> X f Int pattern C x = Y (Just x) :: X Maybe Int f :: X Maybe a -> a f (Y (Just x)) = x -- works f (C x) = x -- fails
For Simon's example, consider:
{-# LANGUAGE GADTs, PatternSynonyms, ScopedTypeVariables, RankNTypes #-} data T a b where MkT :: a -> T a Bool MkX :: T a b Q1 :: T Bool Bool Q2 :: T Bool b Q3 :: T b Bool Q4 :: T b b pattern P1 = MkT True :: T Bool Bool pattern P1a <- MkT True :: T Bool Bool pattern P2a <- MkT True :: forall b. T Bool b pattern P3a <- MkT True :: forall b. T b Bool pattern P4a <- MkT True :: forall b. T b b f :: T Bool b -> Bool f (MkT True) = True -- works f Q1 = True -- works f Q2 = undefined -- works f Q3 = True -- works f Q4 = True -- works f P1 = True -- fails f P1a = True -- fails f P2a = undefined -- fails f P3a = True -- fails f P4a = True -- fails
Is it unreasonable to expect this kind of thing to work?
comment:7 follow-up: 8 Changed 3 years ago by
Replying to kosmikus:
Both
P
in SPJ's example andC
in my examples are bidirectional pattern synonyms, and as an expression, it should be easy enough for GHC to type-check without a type signature. So why require one in this case? The expression type signature and pattern type signature must be the same, after all.
No, that statement sounds plausible, but it is not right. Consider
data T a where T1 :: a -> T a T2 :: T Int T3 :: T Bool
In an expression context, certainly, T2 :: T Int
, and T3 :: T Bool
. But not in a pattern context, otherwise this function would be ill-typed:
f (T1 _) = True f T2 = True f T3 = False
No, as a pattern, both T2
and T3
have type forall a. T a
; that is, they can soundly (without seg-faulting) match any value of type T <type>
. So f :: T a -> Bool
.
But try this:
g (T1 True) = True g T2 = True g T3 = False
Here the first equation means that applying g
to an argument of type T Int
, say, would be unsound. The pattern T1 True :: T Bool
, and indeed g :: T Bool -> Bool
, and the T2
clause is dead code.
The trouble is that (as we know well) in the presence of GADTs there may be no unique principal type, which is why OutsideIn requires type signatures to resolve the uncertainty. It's the same with pattern synonyms.
However, a key principle is that replacing pattern synonym by its definition should not change whether the program is well typed. So is is a bug that these two behave differently:
f :: X Maybe a -> a f (Y (Just x)) = x -- works f (C x) = x -- fails
The latter should not fail; it should behave precisely like the former.
Simon
comment:8 follow-up: 11 Changed 3 years ago by
Replying to simonpj:
Replying to kosmikus:
Both
P
in SPJ's example andC
in my examples are bidirectional pattern synonyms, and as an expression, it should be easy enough for GHC to type-check without a type signature. So why require one in this case? The expression type signature and pattern type signature must be the same, after all.No, that statement sounds plausible, but it is not right. Consider
data T a where T1 :: a -> T a T2 :: T Int T3 :: T BoolIn an expression context, certainly,
T2 :: T Int
, andT3 :: T Bool
. But not in a pattern context, otherwise this function would be ill-typed:f (T1 _) = True f T2 = True f T3 = FalseNo, as a pattern, both
T2
andT3
have typeforall a. T a
; that is, they can soundly (without seg-faulting) match any value of typeT <type>
. Sof :: T a -> Bool
.
Ok, we seem to have slightly different terminology when it comes to saying what the "type" of a pattern is. But terminology aside, I agree that T2
and T3
should be applicable in a context of type T a
. But the information that they're T Int
and T Bool
"as an expression" must still be around even during pattern matching, because the match causes type refinement accordingly.
So in one way or another for a constructor such as T2
there seem to be *two* types that are important, namely T Int
and forall a. T a
.
The trouble is that (as we know well) in the presence of GADTs there may be no unique principal type, which is why OutsideIn requires type signatures to resolve the uncertainty. It's the same with pattern synonyms.
This is what I also thought at first, but what I'm no longer convinced about.
Let's go back to your example:
data T a b where MkT :: a -> T a Bool MkX :: T a b pattern P = MkT True
So I guess we agree than "as an expression", P
must be of type T Bool Bool
. You say that "as a pattern", it could have either of
P :: T Bool b P :: T b b
Yes, ok, but should this information be necessary to provide with the pattern synonym? Isn't this something that should be derived from the type signature of the function in which it is used?
Shouldn't I be able to write
f :: T Bool b -> b f P = False
and also
g :: T b b -> b g P = False
just like I can write
f :: T Bool b -> b f (MkT True) = False
as well as
g :: T b b -> b g (MkT True) = False
If I'd be forced to provide a type signature for the pattern synonym P
picking one of the two "pattern types", then P
would be necessarily more limited in its use than its expansion.
comment:9 follow-up: 10 Changed 3 years ago by
The above discussion sheds light on the "not in scope" error. Of course, it's a GHC panic, so it's not right. But that's because there really is a problem.
- As a pattern
Y (Just x) :: X Maybe a
- As a expression
Y (Just x) :: X Maybe Int
, and requiresx::Int
.
So it's not clear that a single signature for the two ways of looking at the RHS makes sense at all! It look as though we need one for its use as a pattern and one for its use as an expression. Sigh.
Mind you, the "type as an expression" is easily inferred, as you mention. So perhaps the pattern signature (once we have them) can be taken as applying only to the pattern, not the expression?
comment:10 Changed 3 years ago by
So it's not clear that a single signature for the two ways of looking at the RHS makes sense at all! It look as though we need one for its use as a pattern and one for its use as an expression. Sigh.
Yes.
Mind you, the "type as an expression" is easily inferred, as you mention. So perhaps the pattern signature (once we have them) can be taken as applying only to the pattern, not the expression?
I guess it's not clear to me if the other information isn't available as well, if the synonym is used in a function that has a type signature. Is there really a theoretical need to supply a signature for the "pattern type"? See my example in the other comment, I actually wouldn't like to have to pick one.
comment:11 follow-up: 12 Changed 3 years ago by
Replying to kosmikus:
Yes, ok, but should this information be necessary to provide with the pattern synonym? Isn't this something that should be derived from the type signature of the function in which it is used?
Yes, it should be provided with the pattern synonym. No, it should not be derived form the use. Here's why.
As you go on to show, the "derive from use" idea is more flexible, but it is fundamentally non-modular: you can only understand when a pattern synonym will typecheck by expanding it! The whole point about pattern synonyms is that you don't need to think about their implementation (expansion); you can reason about them using only their interface.
To take an analogy, go back to GADTs:
data T a where T1 :: T Bool T2 :: T Char f T1 = True
Does f :: T a -> Bool
or f :: T a -> a
? You could say "look to the uses". Here are two calls
(f 'x' && True) -- Needs f :: T a -> Bool (ord (f 'x')) -- Needs f :: T a -> a
If you inline f
(akin to expanding the pattern synonym), you can make both typecheck. But we don't inline functions: we give them a single, principal type, and use that at every call site. It's just the same with pattern synonyms.
Simon
comment:12 follow-up: 13 Changed 3 years ago by
I agree completely with the function example. I'm just sure about whether the pattern synonym situation is really analogous. The reason is that in
data T a b where MkT :: a -> T a Bool MkX :: T a b pattern P = MkT True
I could just pretend that P
is another constructor of T
:
data T a b where MkT :: a -> T a Bool MkX :: T a b P :: T Bool Bool
Then both f
and g
as shown above using P
would type-check. So if for P
as a constructor, the information that the "expression type" is T Bool Bool
and the "target type" is T a b
is sufficient, then why can't we do the same for P
as a pattern synonym. That's still modular, IMHO.
comment:13 follow-up: 14 Changed 3 years ago by
I could just pretend that
P
is another constructor ofT
:data T a b where MkT :: a -> T a Bool MkX :: T a b P :: T Bool Bool
Alas, no. If the definition of T really did have that constructor P, then GADT-style type refinement would take place when you match on P. So for example, this would typecheck:
f :: T a b -> a -> Bool f P v = v && True
But obviously the expansion does not:
f :: T a b -> a -> Bool f (MkT x) v = v && True
Moreover, these are terribly simple examples. In general a pattern synonym might mention dozens of constructor from dozens of types. Which of those types would you like to pretend the pattern synonym constructor is from?
This is what I mean by modularity: no matter how complicated the right hand side of the pattern synonym, I want the client (of the library defining the pattern synonym) to be able to use it by knowing only its type -- just like he can for a function exported by a library.
Simon
comment:14 Changed 3 years ago by
Alas, no. If the definition of T really did have that constructor P, then GADT-style type refinement would take place when you match on P. So for example, this would typecheck:
f :: T a b -> a -> Bool f P v = v && TrueBut obviously the expansion does not:
f :: T a b -> a -> Bool f (MkT x) v = v && True
The expansion is MkT True
, but it doesn't matter. Nice example. I'm almost convinced, although I'll have to think about this a bit longer.
Moreover, these are terribly simple examples. In general a pattern synonym might mention dozens of constructor from dozens of types. Which of those types would you like to pretend the pattern synonym constructor is from?
I don't pretend that I have thought this through. I have only played with pattern synonyms for a few days so far, and I don't completely understand the possibilities of the interaction with ViewPatterns yet. However, in the case of bidirectional pattern synonyms I'd expect a pattern synonym to have a clear "target type".
This is what I mean by modularity: no matter how complicated the right hand side of the pattern synonym, I want the client (of the library defining the pattern synonym) to be able to use it by knowing only its type -- just like he can for a function exported by a library.
Yes, that's certainly a valid goal.
Ok, for now, let's try to summarize: Every (bidirectional) pattern actually has two types, an "expression type" and a "pattern type".
If I understand your proposal correctly, you're saying that pattern type signatures should allow the user specify the pattern type, because the expression type should in general be easy to infer.
So I should be able to say
pattern P :: T Bool b pattern P = MkT True
or for my original example
pattern C :: Int -> X Maybe a pattern C x = Y (Just x)
So perhaps GHCi should print both types rather than only the expression type on :t
, something like:
GHCi> :t C pattern C :: Int -> X Maybe a C :: Int -> X Maybe Int GHCi> :t P pattern P :: T Bool b P :: T Bool Bool
And perhaps for consistency even for normal data constructors?
GHCi> :t MkT pattern MkT :: a -> T a b MkT :: a -> T a Bool
comment:15 follow-up: 16 Changed 3 years ago by
I think that is roughly right, yes. But the pattern type you give above gives no clue that type refinement takes place when you match on it, and a client of C
definitely needs to know that.
I think we can print the type of C
and MkT
like this:
GHCi> :t MkT MkT :: (b~Bool) => a -> T a b GHCi> :t C C :: (a~Int) => Int -> X Maybe a GHCi> pattern D x = MkT (Just x) GHCi> :t D D :: (b~Bool) => a -> T (Maybe a) b
These types work nicely both in expressions and patterns.
- In expressions they are precisely equivalent to
a -> T a Bool
andInt -> Maybe Int
respectively. - In patterns, pattern matching binds evidence for the equality. In Gergo's terminology, matching against
MkT
"provides"(b~Bool)
; this refinement is available in the case alternative.
The pattern synonym D is a nice example:
- The result type
T (Maybe a) b
says thatD
must only match types of that shape, i.e. where the first arg ofT
is aMaybe
. - The
(b~Bool) =>
says that when you match onD
you get that type refinement available in the case alternative.
So this actually a single signature that tells you all you need to know, both for matching and for use in expressions. Good!
I should mention that internally the type of a GADT constructor like MkT
really is as displayed here, namely MkT :: (b~Bool) => a -> T a b
.
(There is a twist for what Gergo calls "required" constraints, which arise in view patterns and literal patterns, but let's ignore that for now.)
Simon
comment:16 Changed 3 years ago by
I think that is roughly right, yes. But the pattern type you give above gives no clue that type refinement takes place when you match on it, and a client of
C
definitely needs to know that.
That's why I proposed to show both types, but ...
I think we can print the type of
C
andMkT
like this:GHCi> :t MkT MkT :: (b~Bool) => a -> T a b GHCi> :t C C :: (a~Int) => Int -> X Maybe a GHCi> pattern D x = MkT (Just x) GHCi> :t D D :: (b~Bool) => a -> T (Maybe a) bThese types work nicely both in expressions and patterns.
Yes, I'm certainly happy with this as well. In fact, I had briefly considered making this suggestion. (I think back in GHC 6, GADT constructor types were actually displayed using a similar syntax.) My only worry is that it's slightly subtle that in these cases (where it's a type signature for a constructor or pattern synonym), inlining an equality constraint makes a difference, whereas for expressions it doesn't. But I guess that having two different type signatures printed wouldn't be any easier to understand.
The pattern synonym D is a nice example:
- The result type
T (Maybe a) b
says thatD
must only match types of that shape, i.e. where the first arg ofT
is aMaybe
.- The
(b~Bool) =>
says that when you match onD
you get that type refinement available in the case alternative.So this actually a single signature that tells you all you need to know, both for matching and for use in expressions. Good!
Yes, ok.
I should mention that internally the type of a GADT constructor like
MkT
really is as displayed here, namelyMkT :: (b~Bool) => a -> T a b
.
Also good.
comment:17 Changed 3 years ago by
Oh, I forgot. What does this then imply for explicit type signature on pattern synonyms? Do you propose to still allow
pattern D :: a -> T (Maybe a) b pattern D x = MkT (Just x)
(arguing that the "expression type" is easy to infer) or should the user also be forced to write
pattern D :: (b ~ Bool) => a -> T (Maybe a) b pattern D x = MkT (Just x)
?
I think the latter would certainly be more consistent then?
comment:18 Changed 3 years ago by
Yes, I think it would have to be the latter.
Several open issues remain:
- We need pattern signatures. The workaround (of a signature embedded in the pattern) doesn't work too well for these more complicated types.
- In fact having signatures embedded in a pattern synonym is problematic, because signatures behave differently in patterns and in terms.
g x = Just x :: Maybe a f (Just x :: Maybe a) = x
Ing
, the type signature is implicitly quantified, so it really meansJust x :: forall a. Maybe a
, and the definition will therefore be rejected. But in the definition off
, the 'a' in the pattern is a binding occurrence, that scopes over the RHS; there is no implicit quantification.
I'm inclined simply to disallow signature in the RHS of a pattern synonym.
- We have no good syntax for the required/provided issue. I thought this was written up on the Pattern Synonym wiki page but it isn't.
comment:20 Changed 3 years ago by
Keywords: | pattern synonyms added |
---|
comment:21 Changed 3 years ago by
Owner: | set to cactus |
---|
I have started working on adding pattern synonym signatures, in the branch wip/T8968
. So far, it seems I will have to go with a syntax like
pattern type Eq b => Single a Bool b :: Num a => T a
instead of
pattern Eq b => Single a Bool b :: Num a => T a
to make parsing unambiguous between pattern synonym definitions and pattern synonym signatures.
comment:22 Changed 3 years ago by
Milestone: | → 7.10.1 |
---|---|
Summary: | Pattern synonyms and GADTs → Type signatures for pattern synonyms |
Type: | bug → feature request |
comment:23 Changed 3 years ago by
Blocked By: | 8584 added |
---|
comment:24 Changed 3 years ago by
Summary: | Type signatures for pattern synonyms → Pattern synonyms and GADTs |
---|---|
Type: | feature request → bug |
comment:26 Changed 3 years ago by
Keywords: | PatternSynonyms added; pattern synonyms removed |
---|
Harump. This is a real shortcoming in the pattern-synonym stuff. Consider
What type should pattern P have? It could be
Both would work, because pattern matching on
MkT
ensures thatb~Bool
. But neither is more general than the other. So GHC rejects it, with the (confusing) errors.(There are two errors, one
P
in matching and one forP
in an expression. I think we can fix that part by failing earlier.)This ambiguity is the cause of the error kosmikus came across, I think. In the OutsideIn algorithm we insist on a type signature for functions like this. My conclusion
But first, have I analysed this right? Copying Dimitrios.
Simon