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