
#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