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

Manipulation of constraints that apply to field labels (as opposed to actual types stored in the record).
-}

{-# LANGUAGE 
    ConstraintKinds
  , DataKinds
  , GADTs
  , PolyKinds
  , TypeFamilies
  , TypeOperators
  #-}

{-# OPTIONS_HADDOCK show-extensions #-}

module Data.Vinyl.Utils.Field where

import Data.Proxy
import Data.Vinyl
import GHC.Exts

-- |Assert that all field labels in a given type list satisfy a given constraint.
type family FieldAll (rs :: [k]) (c :: k -> Constraint) :: Constraint where
  FieldAll '[] c = ()
  FieldAll (r ': rs) c = (c r, FieldAll rs c)

-- |A data type that reifies a constraint. Pattern match on the 'DictProxy' constructor to bring the constraint into scope.
data DictProxy c a where
  DictProxy :: c a => DictProxy c a

getProxy :: DictProxy c a -> Proxy a
-- ^Obtain a 'Proxy' from a 'DictProxy', forgetting its constraint.
getProxy DictProxy = Proxy

reifyFieldConstraint :: FieldAll rs c => proxy c -> Rec Proxy rs -> Rec (DictProxy c) rs
-- ^Given a dummy record and a constraint that applies to all field labels, reify the constraint for each field label.
reifyFieldConstraint _ RNil = RNil
reifyFieldConstraint c (Proxy :& ps) = DictProxy :& reifyFieldConstraint c ps