GHC panic when creating a monomorphised pattern synonym for GADT
I have an expression
{-# 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:
-- This works:
-- pattern IntFun :: (a -> b) -> (Exp a -> Exp b)
-- pattern IntFun f x = Fun f x
pattern IntFun :: (Int -> Int) -> (Exp Int -> Exp Int)
pattern IntFun f x = Fun f x
which results in
% 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:
pattern IntFun :: (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
pattern IntFun :: (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:
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?