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 Changed 14 months ago by 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.

  • 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

comment:2 in reply to:  1 Changed 14 months ago by mniip

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

comment:3 Changed 14 months ago by bgamari

Milestone: 8.6.18.8.1

These won't be fixed for in GHC 8.6.

comment:4 Changed 9 months ago by osa1

Milestone: 8.8.18.10.1

Bumping milestones of low-priority tickets.

Note: See TracTickets for help on using tickets.