[GHC] #12203: Allow constructors on LHS of (implicit) bidirectional pattern synonym

17 Jun 2016

      #12203: Allow constructors on LHS of (implicit) bidirectional pattern synonym
-------------------------------------+-------------------------------------
           Reporter:  ezyang         |             Owner:
               Type:  feature        |            Status:  new
  request                            |
           Priority:  low            |         Milestone:
          Component:  Compiler       |           Version:  8.0.1
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Inspired by the recent Ghostbuster paper
 http://www.cs.ox.ac.uk/people/timothy.zakian/ghostbuster.pdf , I was
 experimenting with using pattern synonyms to simulate GADTs. In the
 process, I noticed that we should be able to generalize the implicit
 bidirectional synonyms to allow constructors on the LHS.

 Consider this program:

 {{{
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE ViewPatterns #-}
 {-# LANGUAGE TypeOperators #-}
 {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
 module GhostBuster where

 import GHC.TypeLits

 newtype Vec a (n :: Nat) = Vec { unVec :: [a] }

 pattern VNil :: Vec a 0
 pattern VNil = Vec []

 pattern VCons :: a -> Vec a n -> Vec a (n + 1)
 pattern VCons x xs <- Vec (x : (Vec -> xs)) where
     VCons x (Vec xs) = Vec (x : xs)

 headVec :: Vec a (n + 1) -> a
 headVec (VCons x _) = x
 }}}

 In effect, we simulate a vector GADT using pattern synonyms to handle the
 newtype `Vec`.

 I would like it if I could specify the `VCons` pattern more simply, as
 just:

 {{{
 pattern VCons :: a -> Vec a n -> Vec a (n + 1)
 pattern VCons x (Vec xs) = Vec (x : xs)
 }}}

 And GHC would infer the correct pattern (the constructor can be read off
 immediately), automatically replacing occurrences of `xs` with a view
 pattern that reconstructs the constructors that were stripped off on the
 LHS.

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