[GHC] #14058: Cannot bundle pattern synonym with exported data family

GHC ghc-devs at haskell.org
Sun Jul 30 04:46:57 UTC 2017


#14058: Cannot bundle pattern synonym with exported data family
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  feature        |            Status:  new
  request                            |
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.1
           Keywords:                 |  Operating System:  Unknown/Multiple
  PatternSynonyms                    |
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 I'd like to write this code:

 {{{#!hs
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
 module Foo (Sing(.., SCons)) where

 data family Sing (a :: k)

 data instance Sing (z :: [a]) where
   SNil :: Sing '[]
   (:%) :: Sing x -> Sing xs -> Sing (x:xs)

 pattern SCons :: forall a (z :: [a]). ()
               => forall (x :: a) (xs :: [a]). z ~ (x:xs)
               => Sing x -> Sing xs -> Sing z
 pattern SCons x xs = (:%) x xs
 {-# COMPLETE SNil, SCons #-}
 }}}

 But alas, GHC will not let me:

 {{{
 $ ghci Bug.hs
 GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Foo              ( Bug.hs, interpreted )

 Bug.hs:7:13: error:
     • Pattern synonyms can be bundled only with datatypes.
     • In the pattern synonym: SCons
       In the export: Sing(.., SCons)
   |
 7 | module Foo (Sing(.., SCons)) where
   |             ^^^^^^^^^^^^^^^
 Failed, 0 modules loaded.
 }}}

 Can this restriction be lifted for data families?

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


More information about the ghc-tickets mailing list