Andrew Martin

Thanks! That totally makes sense. Now that you point that out, I'm not sure why I even expected that `sendAll` would be thread-safe. I'll try to PR some documentation warning...

This is also a problem for me, and I do not know how to fix it either.

Just dumping some thoughts here since this is the only real discussion of this question that I can find. What about sidestepping the variance issue entirely by only allowing type...

> I'm pretty sure just adding that new subtyping rule you showed is enough. I don't think that just the subtyping rule is enough because I didn't add anything that...

This is very much a non sequitur, but I started thinking about this again yesterday and started wondering about how the covariant-type-constructors-only world implied by a rule like ``` Ψ...

I'm writing this down mostly for my own sake so that I don't forget it. From an [earlier comment](https://github.com/ollef/Bidirectional/issues/5#issuecomment-646658821): > One way to simplify the algorithm of "Sound and Complete..."...

I just ran into the same issue that @not-napoleon described. The fact that closing indices breaks `/_cat/shards` is a problem for us, and it means that we essentially cannot ever...

The CircleCI logs say: ``` > tests/pos/abs.hs:5:1: error: > Liquid Type Mismatch > . > The inferred type > VV : GHC.Types.Int > . > is not a subtype of...

Ah, that makes sense. Yeah, it seems like it would be good to just get rid of `autosize`. I didn't even realize that the structural checker existed. Perhaps, if you...

As: indexArray# :: forall a. x:_ -> {v:Nat | v < len x } -> a It still errors with Unknown variable `MySpec.indexArray#`