module Data.Vector.Vinyl.Default.NonEmpty.Polymorphic.Implication where
import Data.Constraint
import Data.Vector.Vinyl.Default.NonEmpty.Polymorphic.Internal
import Data.Vinyl.Core (Rec(..))
import Data.Vinyl.Functor (Identity(..))
import Data.Vinyl.TypeLevel (RecAll)
import qualified Data.Vector.Generic.Mutable as GM
import qualified Data.Vector.Generic as G
listAllVector :: (rs ~ (a ': as))
=> Rec f rs
-> RecAll f rs HasDefaultVector :- G.Vector Vector (Rec f rs)
listAllVector (_ :& RNil) = Sub Dict
listAllVector (_ :& rs@(_ :& _)) = Sub $ case listAllVector rs of
Sub Dict -> Dict
listAllMVector :: (rs ~ (a ': as))
=> Rec f rs
-> RecAll f rs HasDefaultVector :- GM.MVector MVector (Rec f rs)
listAllMVector (_ :& RNil) = Sub Dict
listAllMVector (_ :& rs@(_ :& _)) = Sub $ case listAllMVector rs of
Sub Dict -> Dict
listAllMVector' :: (rs ~ (a ': as))
=> proxy1 f
-> Rec proxy2 rs
-> RecAll f rs HasDefaultVector :- GM.MVector MVector (Rec f rs)
listAllMVector' _ (_ :& RNil) = Sub Dict
listAllMVector' p (_ :& rs@(_ :& _)) = Sub $ case listAllMVector' p rs of
Sub Dict -> Dict