{-# LANGUAGE ScopedTypeVariables, PatternSynonyms, DataKinds, PolyKinds,
             GADTs, TypeOperators, TypeFamilies #-}

module T13441 where

import Data.Functor.Identity

data FList f xs where
  FNil :: FList f '[]
  (:@) :: f x -> FList f xs -> FList f (x ': xs)

data Nat = Zero | Succ Nat

type family Length (xs :: [k]) :: Nat where
  Length '[]       = Zero
  Length (_ ': xs) = Succ (Length xs)

type family Replicate (n :: Nat) (x :: a) = (r :: [a]) where
  Replicate Zero     _ = '[]
  Replicate (Succ n) x = x ': Replicate n x

type Vec n a = FList Identity (Replicate n a)

-- Using explicitly-bidirectional pattern
pattern (:>) :: forall n a. n ~ Length (Replicate n a)
             => forall m. n ~ Succ m
             => a -> Vec m a -> Vec n a
pattern x :> xs <- Identity x :@ xs
  where
    x :> xs = Identity x :@ xs

-- Using implicitly-bidirectional pattern
pattern (:>>) :: forall n a. n ~ Length (Replicate n a)
             => forall m. n ~ Succ m
             => a -> Vec m a -> Vec n a
pattern x :>> xs = Identity x :@ xs