Opened 3 years ago

Closed 2 years ago

Last modified 2 years ago

#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 simonpj

Cc: cactus dimitris@… added

Harump. This is a real shortcoming in the pattern-synonym stuff. Consider

data T a b where
	MkT :: a -> T a Bool
	MkX :: T a b

pattern P = MkT True

What type should pattern P have? It could be

	P :: T Bool b
or	P :: T b b

Both would work, because pattern matching on MkT ensures that b~Bool. But neither is more general than the other. So GHC rejects it, with the (confusing) errors.

T8968.hs:9:17:
    Couldn't match expected type ‘t’ with actual type ‘Bool’
      ‘t’ is untouchable
        inside the constraints (t1 ~ Bool)
        bound by a pattern with constructor
                   MkT :: forall a. a -> T a Bool,
                 in a pattern synonym declaration
        at T8968.hs:9:13-20
      ‘t’ is a rigid type variable bound by
          the inferred type of P :: T t t1 at T8968.hs:1:1
    In the pattern: True
    In the pattern: MkT True

T8968.hs:9:17:
    Could not deduce (t ~ Bool)
    from the context (t1 ~ Bool)
      bound by the type signature for T8968.$WP :: t1 ~ Bool => T t t1
      at T8968.hs:9:9
      ‘t’ is a rigid type variable bound by
          the type signature for T8968.$WP :: t1 ~ Bool => T t t1
          at T8968.hs:1:1
    Relevant bindings include $WP :: T t t1 (bound at T8968.hs:9:9)
    In the first argument of ‘MkT’, namely ‘True’
    In the expression: MkT True

(There are two errors, one P in matching and one for P 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

  • We need signatures for pattern synonyms. Do such signatures exist yet?
  • Ideally we would find a more civilised way to reject such programs, perhaps suggesting a signature.

But first, have I analysed this right? Copying Dimitrios.

Simon

Last edited 3 years ago by simonpj (previous) (diff)

comment:2 Changed 3 years ago by kosmikus

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 cactus

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 kosmikus

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:5 Changed 3 years ago by Simon Peyton Jones <simonpj@…>

In 50bfd4219157473fac47c70993fc2023a162a7f3/ghc:

Improve error reporting for untouchable type variables

This change adds a suggestion
    Possible fix: add a type signature for ‘f’
when we have a GADT-style definition with a
type we can't figure out.

See Note [Suggest adding a type signature] in TcErrors.

This initially came up in the discussion of Trac #8968.

comment:6 Changed 3 years ago by kosmikus

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 in reply to:  6 ; Changed 3 years ago by simonpj

Replying to kosmikus:

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.

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

Last edited 3 years ago by simonpj (previous) (diff)

comment:8 in reply to:  7 ; Changed 3 years ago by kosmikus

Replying to simonpj:

Replying to kosmikus:

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.

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.

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 Changed 3 years ago by simonpj

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 requires x::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 in reply to:  9 Changed 3 years ago by kosmikus

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 in reply to:  8 ; Changed 3 years ago by simonpj

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 in reply to:  11 ; Changed 3 years ago by kosmikus

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 in reply to:  12 ; Changed 3 years ago by simonpj

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

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 in reply to:  13 Changed 3 years ago by kosmikus

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

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
Last edited 3 years ago by kosmikus (previous) (diff)

comment:15 Changed 3 years ago by simonpj

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 and Int -> 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 that D must only match types of that shape, i.e. where the first arg of T is a Maybe.
  • The (b~Bool) => says that when you match on D 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

Last edited 3 years ago by simonpj (previous) (diff)

comment:16 in reply to:  15 Changed 3 years ago by kosmikus

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 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.

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 that D must only match types of that shape, i.e. where the first arg of T is a Maybe.
  • The (b~Bool) => says that when you match on D 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, namely MkT :: (b~Bool) => a -> T a b.

Also good.

comment:17 Changed 3 years ago by kosmikus

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 simonpj

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
    
    In g, the type signature is implicitly quantified, so it really means Just x :: forall a. Maybe a, and the definition will therefore be rejected. But in the definition of f, 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:19 Changed 3 years ago by simonpj

See also #9226, which is another instance of this.

comment:20 Changed 3 years ago by cactus

Keywords: pattern synonyms added

comment:21 Changed 3 years ago by cactus

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 cactus

Milestone: 7.10.1
Summary: Pattern synonyms and GADTsType signatures for pattern synonyms
Type: bugfeature request

comment:23 Changed 3 years ago by cactus

Blocked By: 8584 added

comment:24 Changed 3 years ago by cactus

Summary: Type signatures for pattern synonymsPattern synonyms and GADTs
Type: feature requestbug

comment:25 Changed 2 years ago by cactus

Resolution: fixed
Status: newclosed

Fixed as part of #8584.

comment:26 Changed 2 years ago by cactus

Keywords: PatternSynonyms added; pattern synonyms removed
Note: See TracTickets for help on using tickets.