`@noinline` interacts badly with auto-quantification

[axch]

Example:

@noinline
def foo {n} (x:Float) (xs:n=>Float) : Float =
  x + sum xs

foo 1.0 [2.0, 3.0]
> Compiler bug!
> Please report this at github.com/google-research/dex-lang/issues
>
> Not a type of runtime-representable data: (Ix (Fin <embedded-simp-atom  v#1  :  Nat >))
> CallStack (from HasCallStack):
>   error, called at src/lib/Simplify.hs:165:23 in dex-0.1.0.0-Gi9B8TxRbicLQnuTnmjlXJ:Simplify

Expected to compute 6.0.

Methinks what happened was that Dex inferred that n=>Float structurally requires Ix n, and constructed the definition

@noinline
def foo {n} (x:Float) [Ix n] (xs:n=>Float) : Float =
  x + sum xs

but this definition violates an unwritten constraint of @noinline, which is that all the arguments on which it specializes must occur before the ones that remain. We should either lift that restriction, or teach auto-quantification to hoist the constraints it infers as high as they can go, and hope that they end up early enough in the binder chain as a result.

[axch]

Offline, @dougalm says "The right thing to do is to lift the ordering constraint on @noinline. We need to do that if we want to deploy it more widely anyway. But I haven't put any thought into how hard it will be."