{-|
Module      : Data.Vinyl.Utils.Proxy
Copyright   : (c) Marcin Mrotek, 2014
License     : BSD3
Maintainer  : marcin.jan.mrotek@gmail.com

Create a dummy record parametrized by 'Proxy', for the purpose of guiding code generation through pattern matching.
-}

{-# LANGUAGE
    DataKinds
  , GADTs
  , PolyKinds
  , RankNTypes
  , TypeOperators
  #-}

module Data.Vinyl.Utils.Proxy 
  ( module Data.Vinyl.Utils.Proxy
  , Proxy (..)
  ) where

import Data.Proxy
import Data.Vinyl

-- |Create a dummy record parametrized by 'Proxy'. The class is named 'Record' to signify that every possible type list is its instance.
class Record (rs :: [k]) where
  proxyRecord :: Rec Proxy rs

instance Record '[] where
  proxyRecord = RNil

instance Record rs => Record (r ': rs) where
  proxyRecord = Proxy :& proxyRecord

recPure :: forall (f :: k -> *) (rs :: [k]). Record rs => (forall (a :: k). f a) -> Rec f rs
recPure = recPure' proxyRecord

recPure' :: forall (f :: k -> *) (rs :: [k]). Rec Proxy rs -> (forall (a :: k). f a) -> Rec f rs
recPure' RNil _ = RNil
recPure' (Proxy :& ps) a = a :& recPure' ps a