RFC: Concrete syntax for pattern synonym type signatures

Dr. ERDI Gergo gergo at erdi.hu
Mon Nov 3 10:13:24 UTC 2014


Background
----------

As explained on
https://ghc.haskell.org/trac/ghc/wiki/PatternSynonyms#Staticsemantics
the type of a pattern synonym can be fully described with the
following pieces of information:

* If the pattern synonym is bidirectional
* Universially-bound type variables, and required constraints on them
* The type of the pattern itself, closed over the universially-bound type variables
* Existentially-bound type variables, and the constraints provided by them
* The types of the arguments, closed over the universially and
   existentially bound type variables

Here's an example showing all of these axes in action:

     data T a b where
       MkT :: (Eq a, Ord b, Show c) => a -> (b, b) -> c -> T a b

     pattern P x y = MkT 5 (y, True) x

In this case:

* The name of the pattern synonym is `P`
* The pattern synonym is bidirectional
* The universially-bound tyvars/required constraints are `forall a. Num a`
* The type of the pattern is `T a Bool`
* The existentially-bound tyvars/provided constraints are
   `forall c. (Eq a, Ord Bool, Show c)`
* The type of the arguments are `c` and `Bool`.

The problem, then, is finding a concrete syntax that captures all of
this information. This syntax is needed for at least two purposes:

* Showing pattern synonym type information in Haddock/GHCi
* Pattern synonym type signatures (#8584)

Current state of things
-----------------------

GHCi 7.8.3 shows the type above as:

pattern (Eq t, Ord Bool, Show c) => P c Bool :: Num t => (T t Bool)

Not only does it not show directionality, I think this is very
confusing in every other way as well, especially with explicit foralls:

pattern forall c. (Eq t, Ord Bool, Show c) => P c Bool :: forall t. Num t 
=> (T t Bool)

I am currently working on implementing #8584, which means I need to
parse these type signatures. I managed to get the above monstrosity to
parse (unambigiously from actual pattern synonym definitions) by
throwing in an extra 'type' keyword:

pattern type (Eq t, Ord Bool, Show c) => P c Bool :: Num t => (T t Bool)

Request for help
----------------

Surely we can do better than that! So let's come up with a nice syntax
for pattern synonym type signatures. It will be used in the pattern
synonym type signature annotations of GHC 7.10, and we could also
retrofit it into GHC 7.8.4 and its Haddock, so that documentation
generated with today's tools will look consistent with code you will
be able to enter in tomorrow's version.

Bye,
 	Gergo


More information about the ghc-devs mailing list