I agree (and I said) that it's a challenge for type inference. While part of me likes the idea of reducing syntactic weight by using constraints, I probably agree that it's not a good idea in this case. The reason I went in to this example is to illustrate that there is nothing magical about arrays or vectors that inherently requires them to be homogeneous in all situations, and that there is nothing magical about indexing syntax, that indices need to be disjoint (but not necessarily drawn from Nat) and discriminators need to be disjoint (but not necessarily drawn from a Sort defined implicitly by the datatype definition).
So I'm mainly trying to tease out the conceptual distinctions here as a way to start looking at what other kinds of discriminators are possible. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
