[zetalemur]

> GHC'ss linear types don't give you uniqueness types in the same way rust does

Why, though?

Is it because GHC's linear types are a superset of Rust's linear types? I guess that could rule out some features the compiler is able to prove (or not).

[platz]

GHC models linearity differently. Rust puts linearity on the types, GHC puts linearity on the arrows. https://i.imgur.com/s0Mxhcr_d.webp?maxwidth=640&shape=thumb&...

[senorsmile]

Is Idris 2's linearity the same as Haskell's in this respect?

[platz]

yes