Opened 23 months ago
Closed 15 months ago
#10404 closed bug (fixed)
GHC panic when creating a monomorphised pattern synonym for GADT
Reported by: | Iceland_jack | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | 8.0.1 |
Component: | Compiler | Version: | 7.10.1-rc1 |
Keywords: | PatternSynonyms | Cc: | cactus, mpickering |
Operating System: | Linux | Architecture: | x86 |
Type of failure: | GHC rejects valid program | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | #11039 | Differential Rev(s): | |
Wiki Page: |
Description (last modified by )
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?
Attachments (1)
Change History (10)
Changed 23 months ago by
comment:1 Changed 23 months ago by
Description: | modified (diff) |
---|
comment:3 Changed 23 months ago by
Description: | modified (diff) |
---|
comment:4 Changed 23 months ago by
Description: | modified (diff) |
---|
A quick (but unsatisfying) solution is adding a tag:
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" ITag _succ n where Suc n = Fun₁ "suc" ITag succ n
comment:5 Changed 17 months ago by
Cc: | cactus mpickering added |
---|---|
Description: | modified (diff) |
Keywords: | PatternSynonyms added |
Milestone: | → 8.0.1 |
I can confirm the panic with ghc-7.11.20151019.
comment:6 Changed 17 months ago by
The panic is bad but the original example fails to compile because there is a misunderstanding with the signature. The following program compiles.
{-# LANGUAGE GADTs,PatternSynonyms #-} module Test where data Exp a where Fun :: (a -> b) -> (Exp a -> Exp b) pattern IntFun :: () => (a ~ Int) => (a -> b) -> (Exp a -> Exp b) pattern IntFun f x = Fun f x
Just giving one set of constraints correspond to provided constraints and an empty required constraints. In this case you want required constraints but empty provided constraints.
comment:7 Changed 16 months ago by
Related Tickets: | → #11039 |
---|
comment:8 Changed 16 months ago by
There is still some good stuff in here which would make tests. There is still the panic which is reported as #11039.
comment:9 Changed 15 months ago by
Resolution: | → fixed |
---|---|
Status: | new → closed |
Well #11039 is fixed so I think I'll close this too. Everything else here looks right.
I fear the existential makes my
Suc
example trickier than I thought, I welcome suggestions