[GHC] #15416: Higher rank types in pattern synonyms

19 Jul 2018

      #15416: Higher rank types in pattern synonyms
-------------------------------------+-------------------------------------
           Reporter:  mniip          |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.4.3
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
  PatternSynonyms                    |
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 {{{#!hs
 {-# LANGUAGE RankNTypes, PatternSynonyms, ViewPatterns #-}
 }}}
 Consider the following two pattern synonyms:

 {{{#!hs
 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`:

 {{{#!hs
 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:
 {{{#!hs
 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:

 {{{#!hs
 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
 }}}
 {{{#!hs
 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
    |         ^^^
 }}}

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15416
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler