I don't see how that mechanism provides subtyping (which typeclasses do)? Last I checked Haskell's structures weren't structurally typed.

You could do it like in Agda,

    data ApplicativeI f = 
      AI { pure      :: forall a. a -> f a
         , ap        :: forall a b. f (a -> b) -> f a -> f b
         , _FunctorI :: FunctorI f }

    data MonadI m = 
      AI { bind          :: forall a b. (a -> m b) -> m a -> m b
         , _ApplicativeI :: ApplicativeI m }

    return :: _MonadI m -> a -> m a
    return (MonadI { _ApplicativeI = ApplicativeI { pure = fn } }) = fn

Almost, but that's not extensible: I can't declare some new typeclass Foo and then declare that every x s.t. Monad x is also Foo x without editing the definition of Monad.

Instead of providing an instance declaration you provide a value of MonadI f -> FooI f.

Exactly, and then that function is "proof" of the relationship.

Personally I wouldn't want to do the instance plumbing by hand.