RFC: Concrete syntax for pattern synonym type signatures

[Richard Eisenberg]

How about

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

or

> pattern type forall a. Num a => P <- forall c. (Eq a, Ord Bool, Show c) => c -> Bool -> T a Bool

for a unidirectional pattern. (Note that `::` became `<-`.)

This resembles the syntax for GADT-style data constructors, but with the universal constraints listed.

This may not be (much) better than the original form, but I like that it corresponds closely with at least one piece of existing syntax.

Richard

On Nov 3, 2014, at 5:13 AM, "Dr. ERDI Gergo" <gergo at erdi.hu> wrote:

> 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
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://www.haskell.org/mailman/listinfo/ghc-devs