I tried to use a pattern synonym with a type family and got the following GHC error:
Pattern synonym ‘ZeroAB’ cannot be used here
(pattern synonyms cannot be promoted)
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE UndecidableInstances #-}
data AB = Ab { a :: Nat, b :: Nat}
pattern ZeroAB = Ab 0 0
type family Tf ab where
Tf ZeroAB = Ab 1 1
Tf _ = Ab 0 0
I haven’t found a corresponding issue on the GHC GitLab tracker, nor any discussion of this from the perspective of a potential language feature.
I think it could be useful to have a GHC extension that allows this capability. The syntax of type families is fairly limited, and switching from an atomic type parameter to a record type parameter often introduces additional boilerplate. Being able to reuse pattern synonyms at the type level could help make type-family definitions more concise and maintainable.
In general, the RHS of a PattSyn declaration can be an arbitrarily complex expression (often using ViewPatterns), and not necessarily yielding a datatype that’s promotable — that is, the compiler must evaluate the call to find out; possibly it hasn’t yet processed the PattSyn declaration[**]. TFs are already at the bleeding edge of type-trickery. So to me this sounds just too hard.
If you think this is an enhancement that would benefit the community, I suggest you raise a brief/informal ‘Issue’ on github. I think you’ll need a more persuasive use case than the one you give: I see no real saving or increase in expressivity.
[**] The PattSyn’s signature might itself be given using a TF call. So now we’re invading the compiler’s workstream.
I don’t think there is a fundamental difficulty here, it just hasn’t been implemented (yet). Pattern synonyms would need to be internally tagged as to whether they are promotable, and promotable pattern synonyms could be treated as type synonyms. It’s true that type families may occur in the pattern synonym’s type, but that’s also true for data constructors.
In fact, the example works if you manually add a type synonym definition
type ZeroAB = Ab 0 0
beside the pattern synonym. This could be annoying if it leads to needing to disambiguate between the type and pattern synonym (when they conceptually represent the same thing), but in most contexts GHC’s existing support for punned namespaces should be enough.
Is this a good idea though? Pattern synonyms are usually supposed to abstract the details of the actual access, but if we do this then changing a promotable pattern synonym to a non-promotable one becomes a breaking change.
If you require an explicit annotation on the pattern, like promotable pattern or basic pattern, the declaration of the pattern synonym opts in to using promotable pattern synonyms.
I like Adam’s type synonym trick. (Should have thought of it myself.) More to the point, I guess ‘promotable’ PattSyns are exactly those for which a type syn can be defined. Then …
a bit of Template Haskell to make two declarations; or
a bit of cpp.
In effect by declaring both, you’re saying: I hereby annotate the PattSyn to make it promotable.