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

[GHC]

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

Comment (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
 }}}

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15416#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler