Higher rank types in pattern synonyms

{-# 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
   |         ^^^

Trac metadata

Trac field	Value
Version	8.4.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed milestone to %8.6.1

changed weight to 5

added Tbug Trac import typechecker labels

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 3

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

Very 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 then that type gets instantiated at the call site of x. So the scrutinee of the case has type alpha -> alpha, for some as-yet-unknown type alpha.

And that, of course, is not polymorphic enough.

• The type inference engine never generalises the scrutinee of a 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

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

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?

pattern N :: forall a r. () => () => r -> (a -> r) -> r
pattern J :: forall a r. a -> r -> (a -> r) -> r

Replying to [ticket:15416#comment:157359 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 3

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

Very 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 then that type gets instantiated at the call site of x. So the scrutinee of the 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 .. sm

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

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.

changed milestone to %8.8.1

These won't be fixed for in GHC 8.6.

changed milestone to %8.10.1

Bumping milestones of low-priority tickets.

added PatternSynonyms label

added Pnormal label

changed milestone to %9.0.1

changed milestone to %9.2.1

changed milestone to %⊥