[GHC] #10404: GHC panic when creating a monomorphised pattern synonym for GADT

[GHC]

#10404: GHC panic when creating a monomorphised pattern synonym for GADT
-------------------------------------+-------------------------------------
              Reporter:              |             Owner:
  Iceland_jack                       |            Status:  new
                  Type:  bug         |         Milestone:
              Priority:  normal      |           Version:  7.10.1-rc1
             Component:  Compiler    |  Operating System:  Linux
              Keywords:              |   Type of failure:  GHC rejects
          Architecture:  x86         |  valid program
             Test Case:              |        Blocked By:
              Blocking:              |   Related Tickets:
Differential Revisions:              |
-------------------------------------+-------------------------------------
 I have an expression

 {{{#!hs
 {-# LANGUAGE GADTs           #-}
 {-# LANGUAGE PatternSynonyms #-}

 data Exp a where
   Fun :: (a -> b) - (Exp a -> Exp b)
 }}}

 and I want to create a pattern synonym for Int-expressions:

 {{{#!hs
 -- This works:
 --   pattern :: (a -> b) -> (Exp a -> Exp b)
 --   pattern IntFun f x = Fun f x

 pattern :: (Int -> Int) -> (Exp Int -> Exp Int)
 pattern IntFun f x = Fun f x
 }}}

 which results in

 {{{#!hs
 % ghci -ignore-dot-ghci Panic.hs
 GHCi, version 7.10.0.20150316: http://www.haskell.org/ghc/  :? for help
 [1 of 1] Compiling Main             ( Panic.hs, interpreted )

 Panic.hs:8:28:
     Couldn't match type ‘a’ with ‘Int’
       ‘a’ is a rigid type variable bound by
           a pattern with constructor
             Fun :: forall b a. (a -> b) -> Exp a -> Exp b,
           in a pattern synonym declaration
           at Panic.hs:8:22
     Expected type: Int -> Int
       Actual type: a -> Int
     Relevant bindings include
       b :: Exp a (bound at Panic.hs:8:28)
       a :: a -> Int (bound at Panic.hs:8:26)
 Failed, modules loaded: none.
 }}}

 So I try to be sneaky:

 {{{#!hs
 pattern :: (a ~ Int) => (a -> b) -> (Exp a -> Exp b)
 pattern IntFun f x = Fun f x

 -- % ghci -ignore-dot-ghci Panic.hs
 -- …
 --     Couldn't match type ‘a’ with ‘Int’
 --       ‘a’ is a rigid type variable bound by
 --           the type signature for IntFun :: (a1 -> b) -> Exp a1 -> Exp b
 --           at Panic.hs:8:22
 }}}

 and if I constrain both type variables it panics

 {{{#!hs
 pattern :: (a ~ Int, b ~ Int) => (a -> b) -> (Exp a -> Exp b)
 pattern IntFun f x = Fun f x

 --     Couldn't match type ‘b’ with ‘Int’
 --       ‘b’ is untouchable
 --         inside the constraints ()
 --         bound by the type signature for
 --                    IntFun :: (a1 -> b) -> Exp a1 -> Exp b
 --         at Panic.hs:8:9-14ghc: panic! (the 'impossible' happened)
 --   (GHC version 7.10.0.20150316 for i386-unknown-linux):
 --         No skolem info: b_alF[sk]
 --
 -- Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug
 }}}

 The final version should look like:

 {{{#!hs
 type Name = String
 data Exp a where
   Fun :: Name -> (a -> b) -> (Exp a -> Exp b)
   ...

 pattern Suc :: Exp Int -> Exp Int
 pattern Suc n <- Fun _     _     n where
         Suc n =  Fun "suc" (+ 1) n
 }}}

 Shouldn't this work?

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