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

11 May 2015

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

Old description:
...
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?
New description:

 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#comment:1
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler