Jonathan Lindegaard Starup
Jonathan Lindegaard Starup
`res and {BLOCK}` does correspond to the input so I don't think that is the error
But I would expect `res and {BLOCK}` to be letbound by EffectBinder phase 🤔 perhaps EffectBinder sees `_ and _` as a simple expression that don't have to be let-bound
this seems okay, i was thinking about the apply nodes where it seeks to binds args
we also shouldnt because of lazy evaluation. but ill take a look once i get back to the computer
#7850 is one solution. another solution is another associated effect
it sounds like holger checks the length dynamically instead of reading it once at the start. that choice also shows up in the effects
you can also make it valid (and more precise) with an associated effect
~Should they not be inside the `mod`?~ Ah I was just about to complain that we don't enforce it - but they do have to be inside the mod
It is definitely a good idea, but it also has downsides (currently). Each call to unifySubset introduces a new type variable. The solver takes exponential time based on the number...
Even though the individual formulas are small, their solution might be very big. The solution for `φ_out` in the first equation is substituted into the next formula, and so on...