[GHC] #14552: GHC panic on pattern synonym

[GHC]

#14552: GHC panic on pattern synonym
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.3
      Resolution:                    |             Keywords:
                                     |  PatternSynonyms, TypeInType,
                                     |  ViewPatterns
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 Simon asked me to take a look at this pattern synonym, as there are deeper
 issues here.

 Here is a much simpler scenario with similar issues:

 {{{#!hs
 data T where
   T :: (forall a. Int -> a -> a) -> T

 pattern PT x <- T (($ 3) -> x)
 }}}

 What type should `PT` have? Here are two possibilities: (renaming for
 clarity, but both have the same definition)

 {{{#!hs
 pattern PT1 :: forall a. (a -> a) -> T
 pattern PT2 :: (forall a. a -> a) -> T
 }}}

 These synonyms correspond to the following two matchers:

 {{{#!hs
 matcher1 :: forall r a. T -> ((a -> a) -> r) -> r
 matcher1 (T f) k = k (f 3)

 matcher2 :: forall r. T -> ((forall a. a -> a) -> r) -> r
 matcher2 (T f) k = k (f 3)
 }}}

 Both type-check. The second is more general than the first, even though
 the first is what GHC infers for the definition if given the chance. So,
 which matcher should we generate for `PT`?

 However, I've just played a trick on you. Notice that I inlined the use of
 `($)` in my matchers. Interestingly, `matcher2` does not type check
 without this inlining:

 {{{#!hs
 matcher2 (T (($ 3) -> x)) k = k x   -- does not type-check
 }}}

 This fails because it contains an unsaturated use of `($)`, and
 unsaturated uses of `($)` do not get the pseudo-impredicative magic that
 saturated uses of `($)` get. So, really, `matcher1` is the only
 possibility. (Indeed, GHC infers a pattern type of `forall a. (a -> a) ->
 T` for `PT`.)

 In the original program, the question above (where to generalize) isn't
 properly formed. That's because the equivalent of the `a` here (called
 `aa` in the example) has an existentially-bound kind, so it can't possibly
 scope over the whole matcher type. (In other words, it can't be like
 `matcher1`.) As I've already argued, it also can't be like `matcher2`
 (because `($)` isn't impredicative in this scenario). So, it must be like
 `matcher3`:

 {{{#!hs
 matcher3 :: forall r. T -> ((Any -> Any) -> r) -> r
 matcher3 (T (($ 3) -> x)) k = k x
 }}}

 This is a bit silly, but it's the best we can do if we can't generalize
 over `a`. In the original program, this is really

 {{{#!hs
 matcher :: Exp xs t -> (forall k (f :: k --> Type). Exp xs (f @@ Any) ->
 r) -> r
 matcher (TLam (Proxy :: Proxy this_f) (($ (Proxy @Any)) -> z)) k = k @_
 @this_f z
 }}}

 Probably not what the user wanted, but I don't see how we can do better
 without an impredicative unsaturated `($)`.

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