Scoped with extra effects - Polysemy

interpretScopedWith ::
  ∀ extra resource effect r r1 .
  r1 ~ (extra ++ r) =>
  InsertAtIndex 1 '[Scoped resource effect] r1 r (Scoped resource effect : r1) extra =>
  (∀ x . (resource -> Sem r1 x) -> Sem r x) ->
  (∀ m x . resource -> effect m x -> Tactical effect m r1 x) ->
  InterpreterFor (Scoped resource effect) r
interpretScopedWith withResource scopedHandler =
  interpretH' \case
    Weaving (InScope main) s wv ex _ ->
      ex <$> withResource \ resource -> inScope (insertAt @1 @extra (wv (main resource <$ s)))
    _ ->
      error "You're doing it wrong"
  where
    inScope :: InterpreterFor (Scoped resource effect) r1
    inScope =
      interpretH' \case
        Weaving (Run resource act) s wv ex ins ->
          ex <$> runTactics s (raise . inScope . wv) ins (inScope . wv) (scopedHandler resource act)
        _ ->
          error "nested InScope"