The main problem with levity polymorphism in a binding position is that it's impossible to do codegen since the calling convention depending on the instantiation of the runtime representation variable. From the paper, we have the following rejected example code:

bTwice :: ∀ (r :: RuntimeRep) (a :: TYPE r). Bool → a → (a → a) → a

However, if you are able to inline the function, this problem disappears. You would need a guarantee stronger than what the INLINE pragma provides though since the INLINE pragma still allows the function to be fed as an argument to a higher-order function. I'll refer to a hypothetical new pragma as INLINE MANDATE. This pragma causes a compile-time error to be admitted if the function is ever used in a way that would cause it to not be inlined. Now bTwice would be writeable:

{-# INLINE MANDATE #-}
bTwice :: ∀ (r :: RuntimeRep) (a :: TYPE r). Bool → a → (a → a) → a

The function definition would be provide in the .hi file just as it would be for a function marked as INLINE, but unlike the INLINE counterpart, there would be no generated code for this function, since generating the code would be impossible.

I have several uses for this in mind. I often want a levity-polymorphic variant ST. With INLINE MANDATE, I still wouldn't get do notation, but I could write:

-- This newtype is already allowed today
newtype STL s (a :: TYPE r) = STL (State# s -> (# s, a #) #)

intA, intB, intC :: STL s Int#
wordA, wordB :: Int# -> STL s Word#

{-# INLINE MANDATE #-}
(>>=.) :: STL s a -> (a -> STL s b) -> STL s b
STL a >>=. g = STL (\s0 -> case a s0 of
    (# s1, v #) -> case g v of
      STL f -> f s1

myFunc :: STL s Word#
myFunc =
  intA >>=. \a ->
  intB >>=. \b -> 
  intC >>=. \c -> 
  wordA a >>=. \wa -> 
  wordB b >>=. \wb ->
  ... -- do something with the data

I would appreciate any feedback on this. If there's something that makes this fundamentally impossible, that would be good to know. Or if other people feel like this would be useful, that would be good to know as well.