Opened 14 months ago

Last modified 9 months ago

## #15416 new bug

# Higher rank types in pattern synonyms

Reported by: | mniip | Owned by: | |
---|---|---|---|

Priority: | normal | Milestone: | 8.10.1 |

Component: | Compiler (Type checker) | Version: | 8.4.3 |

Keywords: | PatternSynonyms | Cc: | |

Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |

Type of failure: | GHC rejects valid program | Test Case: | |

Blocked By: | Blocking: | ||

Related Tickets: | Differential Rev(s): | ||

Wiki Page: |

### Description

```
{-# LANGUAGE RankNTypes, PatternSynonyms, ViewPatterns #-}
```

Consider the following two pattern synonyms:

pattern N :: () => () => forall r. r -> (a -> r) -> r pattern N <- ((\f -> f Nothing Just) -> Nothing) where N = \n j -> n pattern J :: a -> forall r. r -> (a -> r) -> r pattern J x <- ((\f -> f Nothing Just) -> Just x) where J x = \n j -> j x

The pattern synonym type declaration syntax is very fragile and awkward wrt quantifiers but that's a story for another ticket.

Now consider four ways to write the same function: using pattern synonyms we've defined above vs. using the exact view patterns they were defiend with; and using a series of equations vs. an explicit `case of`

:

fooVPEqns, fooVPCase, fooPSEqns, fooPSCase :: (forall r. r -> (a -> r) -> r) -> Maybe a fooVPEqns ((\f -> f Nothing Just) -> Nothing) = Nothing fooVPEqns ((\f -> f Nothing Just) -> Just x) = Just x fooVPCase v = case v of ((\f -> f Nothing Just) -> Nothing) -> Nothing ((\f -> f Nothing Just) -> Just x) -> Just x fooPSEqns N = Nothing fooPSEqns (J x) = Just x fooPSCase v = case v of N -> Nothing J x -> Just x

Three of these compile and work fine, the fourth breaks:

QuantPatSyn.hs:22:9: error: • Couldn't match expected type ‘r0 -> (a -> r0) -> r0’ with actual type ‘forall r. r -> (a0 -> r) -> r’ • In the pattern: N In a case alternative: N -> Nothing In the expression: case v of N -> Nothing J x -> Just x • Relevant bindings include v :: forall r. r -> (a -> r) -> r (bound at QuantPatSyn.hs:21:11) fooPSCase :: (forall r. r -> (a -> r) -> r) -> Maybe a (bound at QuantPatSyn.hs:21:1) | 22 | N -> Nothing | ^ QuantPatSyn.hs:23:9: error: • Couldn't match expected type ‘r0 -> (a -> r0) -> r0’ with actual type ‘forall r. r -> (a -> r) -> r’ • In the pattern: J x In a case alternative: J x -> Just x In the expression: case v of N -> Nothing J x -> Just x • Relevant bindings include v :: forall r. r -> (a -> r) -> r (bound at QuantPatSyn.hs:21:11) fooPSCase :: (forall r. r -> (a -> r) -> r) -> Maybe a (bound at QuantPatSyn.hs:21:1) | 23 | J x -> Just x | ^^^

The exact wording of the error message (the appearance of `forall`

in the "actual type") makes me think this is an error on the typechecker's side: the part of the typechecker that handles pattern synonyms doesn't handle higher rank types correctly.

Another symptom can be observed with the following:

pattern V :: Void -> (forall r. r) pattern V x <- ((\f -> f) -> x) where V x = absurd x barVPEqns, barVPCase, barPSEqns, barPSCase :: (forall r. r) -> Void barVPEqns ((\f -> f) -> x) = x barVPCase v = case v of ((\f -> f) -> x) -> x barPSEqns (V x) = x barPSCase v = case v of V x -> x

QuantPatSyn.hs:43:9: error: • Cannot instantiate unification variable ‘r0’ with a type involving foralls: forall r. r GHC doesn't yet support impredicative polymorphism • In the pattern: V x In a case alternative: V x -> x In the expression: case v of { V x -> x } | 43 | V x -> x | ^^^

### Change History (4)

### comment:1 follow-up: 2 Changed 14 months ago by

### comment:2 Changed 14 months ago by

Replying to simonpj:

You are treading on thin ice. Consider this

f1 :: (forall a. a->a) -> Int f1 (x :: forall b. b->b) = x 3 f2 :: (forall a. a->a) -> Int f2 x = case x of (y :: forall b. b->b) -> y 3You might expect

`f1`

and`f2`

to behave the same, because`f2`

only replaces inline pattern matching with a case-expression.But

`f1`

as accepted and`f2`

is rejected thus* Couldn't match expected type `a0 -> a0' with actual type `forall b. b -> b' * When checking that the pattern signature: forall b. b -> b fits the type of its context: a0 -> a0 In the pattern: y :: forall b. b -> b In a case alternative: (y :: forall b. b -> b) -> y 3 | 10 | (y :: forall b. b->b) -> y 3Very similar to the failure you see. Why?

- In
`f1`

the higher-rank type inference machinery "pushes down" the type of the argument, from`f1`

's type signature, into the pattern`(x :: forall b. b->b)`

.

- But in
`f2`

, the variable`x`

indeed gets type`forall b. b->b`

(via this same push-down mechanism, but thenthat type gets instantiated at the call site of. So the scrutinee of the`x`

`case`

has type`alpha -> alpha`

, for some as-yet-unknown type`alpha`

.And that, of course, is not polymorphic enough.

Wouldn't `alpha`

be a unification variable in this case and therefore be polymorphic just enough?

- The type inference engine never generalises the scrutinee of a
`case`

. (I suppose one could revisit that, though I do not know how.)

Consider if desugaring came before typechecking. This wouldn't be a problem because this isn't a case-of in the Core sense. Can't say I have a solution but maybe it's worth taking a look at typechecking a *haskell* case-of based on what *Core* constructs it desugars into?

I hope that explains why your fourth example breaks.

When we first did pattern synonyms I expected the types to always be of form

K :: t1 -> ... -> tn -> T s1 .. smwhere

`T`

is a data type. We loosened that up a bit to allow arbitrary return types. (I forget what the motivation was; I wonder if anyone else remembers? There may be a ticket.)

That does indeed explain the extreme awkwardness of the current syntax. The part where `P => Q => A -> B -> C`

bizzarely stands for `P => ((Q *> (A, B)) <-> C)`

.

What you are doing is putting a

`forall`

in that return position. I never considered that! It would be interesting to see a compelling motivation for doing this. Eg why don't you say this?pattern N :: forall a r. () => () => r -> (a -> r) -> r pattern J :: forall a r. a -> r -> (a -> r) -> r

Because then reversing the equations gets you `forall a r`

I can match on a scrutinee of type `r -> (a -> r) -> r`

and bind a variable of type `a`

. This is clearly not what we want here (`r`

is rigid, but we demand `r ~ Maybe`

), and the definition of `J`

doens't typecheck under that signature.

### comment:4 Changed 9 months ago by

Milestone: | 8.8.1 → 8.10.1 |
---|

Bumping milestones of low-priority tickets.

**Note:**See TracTickets for help on using tickets.

You are treading on thin ice. Consider this

You might expect

`f1`

and`f2`

to behave the same, because`f2`

only replaces inline pattern matching with a case-expression.But

`f1`

as accepted and`f2`

is rejected thusVery similar to the failure you see. Why?

`f1`

the higher-rank type inference machinery "pushes down" the type of the argument, from`f1`

's type signature, into the pattern`(x :: forall b. b->b)`

.`f2`

, the variable`x`

indeed gets type`forall b. b->b`

(via this same push-down mechanism, but thenthat type gets instantiated at the call site of. So the scrutinee of the`x`

`case`

has type`alpha -> alpha`

, for some as-yet-unknown type`alpha`

.And that, of course, is not polymorphic enough.

`case`

. (I suppose one could revisit that, though I do not know how.)I hope that explains why your fourth example breaks.

When we first did pattern synonyms I expected the types to always be of form

where

`T`

is a data type. We loosened that up a bit to allow arbitrary return types. (I forget what the motivation was; I wonder if anyone else remembers? There may be a ticket.)What you are doing is putting a

`forall`

in that return position. I never considered that! It would be interesting to see a compelling motivation for doing this. Eg why don't you say this?