{-|
Copyright   : (c) Hisaket VioletRed, 2022
License     : AGPL-3.0-or-later
Maintainer  : hisaket@outlook.jp
Stability   : experimental
-}

module Polysemy.FS.Scoped.Internal.MembersProof where

import Polysemy ( Members, Effect, EffectRow )
import Polysemy.Internal.Union ( membership, ElemOf (There), )
import Polysemy.Internal.Sing ( SList (SEnd, SCons) )

data MembersProof (es :: EffectRow) (r :: EffectRow) where
    EmptyMembersProof :: MembersProof '[] r
    MembersProof :: ElemOf e r -> MembersProof es r -> MembersProof (e ': es) r

membersProof :: Members es r => SList es -> MembersProof es r
membersProof = \case
    SEnd -> EmptyMembersProof
    SCons xs -> MembersProof membership $ membersProof xs

membersProofId :: SList l -> MembersProof l l
membersProofId = \case
    SEnd -> EmptyMembersProof
    SCons xs -> weakenIdMP $ membersProofId xs

weakenIdMP :: MembersProof l l -> MembersProof (e ': l) (e ': l)
weakenIdMP pr = MembersProof membership $ weakenRightMP pr

weakenRightMP :: MembersProof es r -> MembersProof es (e ': r)
weakenRightMP = \case
    EmptyMembersProof -> EmptyMembersProof
    MembersProof pf pfs -> MembersProof (There pf) $ weakenRightMP pfs