Troels Henriksen

I have a suggestion for Futhark.Internalise.Refinement: instead of adding `#[unsafe]` to the things it can prove, *reject* the program if it cannot prove everything safe (possibly involving migrating checks to...

> Why? Because our goal for now is to figure out when and how verification fails, which is easier when it does not happen silently. Long term, it is my...

I also strongly recommend keeping things in SoP form as much as possible. Constructing source language expressions is a sign you're on the wrong track.

The problem here is that the size of the `#just` constructor in the first branch (0) is also simply taken to be the size of the second branch. We do...

That's an interesting perspective that I had not considered. I don't think we ever clarified the rules for which sizes are witnessed by a sum type.

Yes, there is a real bug that will need to be fixed, regardless of what we decide with witnesses. Your intuition of sum type witnesses being the intersection of the...

`script output` would be equivalent to wrapping the entry point a function that does the rewriting. That is already possible. This would be a useful feature, but I don't think...

You can use `#[noinline]` inside the wrapper. (And in the future, we'll inline less aggressively.)

There is currently no way to use those in Futhark. We've been reluctant to support them since they don't exist for all our targets. It's definitely something it would be...

Yes, but while we already have a mechanism for target-dependent code generation of parallel constructs, we don't have a notion of target-dependent primitive types, so the engineering effort is somewhat...