Yes to almost all of that. The proposal process has exhausted me, but I suppose I will write it again, since your questions there serve as excellent section headings :).

> Do you think the feature is not going to be very useful in a practical setting?

Yes. For one example, you cannot write anything like `malloc :: Word -> LinearPtr Void`. With, `malloc :: Word -o Ptr Void`, since Word is not duplicable, `Ptr Void` would be. The "solution" is to CPS everything, which is pointed out in the paper and they say it's OK cause some big honking monad can take care of that, but I don't buy it, and I don't believe in "zomg all the effects" monads either.

Haskell is supposed to lead they way with type system features, but I think we are the ignorant followers on this one (At least Go outsourced generics!!). There's so much that can be learned from Rust, and yet I don't think this feature learns those lessons. In particular, anyone that spent any time with Rust would realize that borrowing / borrow checking is super important for making something actually usable.

Unfortunately, regions/lifetimes are far less studied theoretically! So the first step would be not making some linear proposal that cherry-picks theory to make for an easier implementation, but go back to the ivory tower and figure out what the hell this borrow checking is and how to understand it better.

> Do you fear people are going to use it all over the place in libraries and make life harder for their users?

Yes, it is a fact that lot of Haskell users are magpies driven by boredom with the rest of the industry. That's certainly how I was when starting Haskell! I think there is a tendency to be attracted to shiny new features and have fun with them, which is fine itself. But this will lead to a bunch of PRs to all the core libraries, which is understandable too, since no feature works except for at scale.

However, if this proves to be a bad feature as I fear, then we will be left with a bunch of newly-complicated core libraries on this debt-end route. And no language ecosystem I know I think has a good story for deprecating and cleaning up failed experiments in a timely matter. I think we are just too small and disorganized a community to risk our ecosystem like this.

> Is there something wrong with this feature in a theoretically basis. Does it need more thought?

Yes, I think linear types should be a separate kind, like runtime reps. Right now there is just a linear arrow with normal types. If you recall the relationship between --> in the language and |- in the meta language, it feels to me that the meta language has no kept up.

I really do believe more in affine types, but think linearity is useful for fixing Rust's Drop to be a dual to Copy and Clone (Types are linear by default, you can right a designated destructor (like Clone) for RAII, or furthermore (in some cases) use a built-in special no-opt destructor (like Copy).

https://arxiv.org/abs/1803.02796 is a paper from the OCaml community that I think is on much better footing.

> Do you think the implementation is broken or not finished? Does it need more work?

No. I haven't looked at the implementation but this doesn't worry me as much. I think the features were chosen to make an implementation without even more effort tractable---I'm sympathetic as it's enough work as it is and I do commend Tweag for marshaling the resources for our commons at this scale even though I do not agree with what is actually being done. Cleaning up GHC is easier than cleaning up the library ecosystem, and in this case a smaller implementation helps.