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 |