[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:  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:                    |
-------------------------------------+-------------------------------------

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 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
>
> {{{#!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 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
>
> {{{#!hs
> 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:
>
> {{{#!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?

--

Comment (by Iceland_jack):

 A quick but unsatisfying solution was adding a tag:

 {{{#!hs
 data Tag ty where
   ITag :: Tag Int
   …

 data Exp a where
   Fun₁ :: Name -> Tag a          -> (a -> b)      -> (Exp a -> Exp b)
   Fun₂ :: Name -> Tag a -> Tag b -> (a -> b -> c) -> (Exp a -> Exp b ->
 Exp c)
   …

 pattern Suc :: Exp Int -> Exp Int
 pattern Suc n <- Fun₁ "suc" _succ n where
         Suc n =  Fun₁ "suc"  succ n
 }}}

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