[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 mniip):

 Replying to [comment:1 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.

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