I had been trying to figure out how to get \ involved, and this is the way. Thanks! It does require that all inputs come before all outputs, which might not be true for constructors:

data T a where

  MkT :: forall b a. b -> T a

Here, `b` is an output while `a` would be an input. And in many cases constructors designed with visible type application in mind will want to put existentials ("outputs") before universals ("inputs"). If we ever did the C <inputs> \ <outputs> in the future, I suppose we could just say that such constructors will have their type variables reordered, perhaps issuing a warning if someone writes a mis-ordered constructor.

In any case, I'm glad that this discussion has changed your mind about accepting this proposal.

Thanks,

Richard