Dependent pair types in Haskell

DPair.hs

{-# LANGUAGE GADTs, ExistentialQuantification         #-}
{-# LANGUAGE DataKinds, KindSignatures, TypeOperators #-}
{-# LANGUAGE PolyKinds                                #-}
{-# LANGUAGE StandaloneDeriving                       #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ConstraintKinds #-}

-- Inspired by the dependent-sum package

import           Data.Proxy
import           GHC.TypeLits
import           Prelude.Extras

data DPair tag f = forall a. !(tag a) :=> f a
data DPair' tag f a = !(tag a) :-> f a

data DPair'' tag f c = forall a. c a => !(tag a) :--> f a

extract :: DPair' tag f a -> Proxy a
extract _ = Proxy

unpair :: DPair tag f -> Proxy a
unpair _ = Proxy

-- TODO: !!! Check to see if this is the generalization that should be used !!!
unpair'' :: DPair'' tag f ((~) a) -> f a
unpair'' (_ :--> fa) = fa

data Vect a (n :: Nat) where
  Nil  ::                  Vect a 0
  Cons :: a -> Vect a n -> Vect a (n + 1)

deriving instance Show a => Show (Vect a n)

data Fin a where
  Zero :: Fin 0
  Succ :: Fin n -> Fin (n + 1)

deriving instance Show (Fin a)

dfilter :: (a -> Bool) -> Vect a n -> DPair Fin (Vect a)
dfilter _ Nil = Zero :=> Nil
dfilter p (Cons x xs)
  | p x = case dfilter p xs of
            n :=> xs' -> Succ n :=> (Cons x xs')
  | otherwise = dfilter p xs

readFin :: String -> DPair Proxy Fin
readFin "Z"     = Proxy :=> Zero
readFin ('S':s) = case readFin s of
  Proxy :=> n -> Proxy :=> Succ n
readFin _       = error "readFin: invalid parse"

-- unpack :: DPair Proxy f -> f a
-- unpack (Proxy :=> fa) = fa

class ShowTag tag where
  showTag :: tag a -> String

instance Show a => ShowTag (Vect a) where
  showTag = show

instance ShowTag Fin where
  showTag = show

instance ShowTag Proxy where
  showTag = show

instance (ShowTag tag, ShowTag f) => Show (DPair tag f) where
  show (t :=> f) = showTag t ++ " :=> " ++ showTag f