Skip to content

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?

Edited by Thomas Miedema
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information