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

 Let's make it even simpler.  Use Richard's data type `T`, and consider
 {{{
 {-# LANGUAGE ViewPatterns, RankNTypes, GADTs  #-}
 module Foo where

 data T where
   T :: (forall a. Int -> a -> a) -> T

 g1 (T f) = (f 3 'c', f 3 True)

 g2 (T f) = let h = f 3
            in (h 'c', h True)

 g3 (T (id -> f)) = (f 3 'c', f 3 True)

 g4 (T ((\f -> f 3) -> h)) = (h 'c', h True)
 }}}
 Here we get

 * `g1` typechecks because `f` is bound to a polymorphic function.

 * `g2` does not typecheck, because the binding of `h` is not generalised
 (we have `MonoLocalBinds` when `GADTs` is on).  So `h` is monomorphic.

 * `g3` does not typecheck for the same reason.  It's akin to `g2` with `h
 = id f`; it desugars to something like
 {{{
 g3 (T ff) = let f = id ff
             in (f 3 'c', f 3 True)
 }}}

 * `g4` does not typecheck for the same reason.  It desugars to something
 like
 {{{
 g4 (T ff) = let h = (\f -> f 3) ff
             in (h 'c', h True)
 }}}

 So I don't think this has anything to do with the impredicativity magic
 for `($)`. It's just that
 binding a polymorphic variable in a pattern is a very delicate business.
 One could imagine
 generalising those extra let-bindings in the desugarings of `g3` and `g4`,
 but would be
 hard to do reliably -- that is why we have `MonoLocalBinds`.

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