module Data.Vinyl.Relation
( (<:)(..)
, (:~:)
, (~=)
, rIso
) where
import Data.Vinyl.Field
import Data.Vinyl.Lens
import Data.Vinyl.Rec
import Data.Vinyl.Witnesses
import Control.Monad.Identity
import GHC.Prim (Constraint)
class (IsSubtype r1 r2) => r1 <: r2 where
cast :: r1 -> r2
type family IsSubtype r1 r2 :: Constraint
type instance IsSubtype (Rec ss f) (Rec ts f) = ISubset ts ss
type r1 :~: r2 = (r1 <: r2, r2 <: r1)
(~=) :: (Eq a, a :~: b) => a -> b -> Bool
x ~= y = x == (cast y)
instance Rec xs f <: Rec '[] f where
cast _ = RNil
instance (y ~ (sy ::: t), IElem y xs, PlainRec xs <: PlainRec ys) => PlainRec xs <: PlainRec (y ': ys) where
cast r = Identity (rGet field r) :& cast r
where field = lookupField (implicitly :: Elem y xs) r
lookupField :: Elem x xs -> Rec xs f -> x
lookupField Here (_ :& _) = Field
lookupField (There p) (_ :& xs) = lookupField p xs
rIso :: (r1 :~: r2) => Iso' r1 r2
rIso = iso cast cast