#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 thomie)

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)

Panic.hs (220 bytes) - added by Iceland_jack 22 months ago.

Download all attachments as: .zip

Change History (10)

Changed 22 months ago by Iceland_jack

Attachment: Panic.hs added

comment:1 Changed 22 months ago by Iceland_jack

Description: modified (diff)

comment:2 Changed 22 months ago by Iceland_jack

I fear the existential makes my Suc example trickier than I thought, I welcome suggestions

Last edited 22 months ago by Iceland_jack (previous) (diff)

comment:3 Changed 22 months ago by Iceland_jack

Description: modified (diff)

comment:4 Changed 22 months ago by Iceland_jack

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
Last edited 22 months ago by Iceland_jack (previous) (diff)

comment:5 Changed 17 months ago by thomie

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 mpickering

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 15 months ago by mpickering

comment:8 Changed 15 months ago by mpickering

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 14 months ago by simonpj

Resolution: fixed
Status: newclosed

Well #11039 is fixed so I think I'll close this too. Everything else here looks right.

Note: See TracTickets for help on using tickets.