module Data.Vector.Vinyl.Default.Implication where
import Data.Constraint
import Data.Vector.Vinyl.Default.Internal
import Data.Vinyl.Core (Rec(..))
import Data.Vinyl.Functor (Identity(..))
import Data.Vector.Vinyl.TypeLevel (ListAll)
import qualified Data.Vector.Generic.Mutable as GM
import qualified Data.Vector.Generic as G
listAllVector :: Rec proxy rs
-> ListAll rs HasDefaultVector :- G.Vector Vector (Rec Identity rs)
listAllVector RNil = Sub Dict
listAllVector (_ :& rs) = Sub $ case listAllVector rs of
Sub Dict -> Dict
listAllMVector :: Rec proxy rs
-> ListAll rs HasDefaultVector :- GM.MVector MVector (Rec Identity rs)
listAllMVector RNil = Sub Dict
listAllMVector (_ :& rs) = Sub $ case listAllMVector rs of
Sub Dict -> Dict