[thesz]

Have you took a look at Clean the programming language? It has unique types (used for resource management, but less restrictive than linear types) for decades and guess what? They invented special syntax (the "#-notation") which introduce shadowable names much like regular monad syntax does. And code with this syntax is, basically, sequential code most of the time albeit unique types allow for something like "where" clause. You just easily get lost with these handle, handle1, handle2... names.

I do not oppose inferring linear use at core and/or intermediate representation (GRIN allowed for that and more). I just do not see their utility at the high level, in the language that is visible to the user.