Allow constructors on LHS of (implicit) bidirectional pattern synonym

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.

Trac metadata

Trac field	Value
Version	8.0.1
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	low
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture