module Data.Vinyl.Relation
( (<:)(..)
, (:~:)
, (~=)
) where
import Data.Vinyl.Field
import Data.Vinyl.Lens
import Data.Vinyl.Rec
import Data.Vinyl.Witnesses
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, Rec xs f <: Rec ys f) => Rec xs f <: Rec (y ': ys) f where
cast r = 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