My attempt at using Purescript Run to Solve "Data Types a la Carte"'s Original Problem. This doesn't work

01-Value.purs

module Free.RunBased.Value (main, value, example_value) where

import Prelude
import Effect (Effect)
import Effect.Console (log)
import Run (Run, extract)

value :: forall r. Int -> Run r Int
value i = pure i

example_value :: forall r. Run r Int
example_value = value 5

main :: Effect Unit
main = do
  log $ show $ extract example_value

02-Add.purs

module Free.RunBased.Add
  (
  -- main
  -- ,
  AddF
  , ADD --, add
  -- , example_add
  , addAlgebra
  ) where

import Prelude hiding (add)
import Effect (Effect)
import Effect.Console (log)
import Data.Functor.Variant (VariantF, FProxy, inj, on, case_)
import Data.Symbol (SProxy(..))
import Type.Row (type (+))
import Free.RunBased.Value (value)
import Run (Run, lift, interpret, send)

-- Data stuff
data AddF e = AddF e e

derive instance af :: Functor AddF

-- Variant Stuff
type ADD r = (add :: FProxy AddF | r)

_add :: SProxy "add"
_add = SProxy

-- 1) Compiler says the type signature for this function is:
add :: forall r
     . Run (ADD + r)
    -> Run (ADD + r)
    -> Run (ADD + r) (Run (ADD + r) Int)
add x y = lift _add (AddF x y)
-- But this means the output type is another Run
-- which screws up my expectation for "interpret"

-- Eval stuff
addAlgebra :: forall r
            . (VariantF r Int -> Int)
           -> (VariantF (ADD + r) Int -> Int)
addAlgebra = on _add \(AddF x y) -> x + y

-- Examples
main :: Effect Unit
main = do
  -- 2) What should "?notSure" be?
  (i :: Int) <- interpret ?notSure (add (value 5) (value 6))
  log $ show i