Arnaud Spiwack

I don't think it's wise to use an arbitrary encoding. At least not at this time. Maybe non-serialisable algebraic types is the reasonable step forward. And it's forward compatible with...

We could just make `Linearly` be a regular (`Dupable` but not `Movable`) data type. But then we'd have to manage duplication manually, which is a little bit of a pain....

@YellowOnion sorry I'd missed your comment until now. Thank you. If this is the implementation of `Integer`, then indeed the operations are going to be linear. I assume that the...

I wanted to have a look at this today, to understand what's going on better. Here are the array benchmarks today, on my machine (Ryzen something), with the recently released...

So, looking at the benchmark for reads, which reads every element in an array The implementation of the benchmark is the following: ```haskell bReads :: Impls bReads = Impls linear...

Besides the case on `Ur`, the main possible difference is the call to `$wget`. Here is the Core for it ```haskell $wget = \ @a ww eta -> case unsafeEqualityProof...

Allowing `get` to inline doesn't affect timing significantly. The generated Core for the benchmark doesn't look better (I'm not even sure why `$wget` got inlined to be honest): ```haskell Rec...

Honestly it looks like a bug, this is a representation coercion between an unrestricted arrow and a linear arrow. Which I don't think we've programmed (it probably doesn't pass the...

Manually eta-expanding doesn't remove this dubious cast (the outer cast: I've just realise that there is an inner cast too, this one is normal). I'm noticing that calls to `Unsafe.toLinear`,...

I take it back, I somewhat thought that the cast was outside of the `unsafeCoerce`. But it's inside the scope, and it's applying the coercion (`co`) from the unsafe coercion....