My thoughts here are based on this section of the generics draft: > We would like to understand better if it is feasible to allow any valid function body as a

My thoughts here are based on this section of the generics draft: > We would like to understand better if it is feasible to allow any valid function body as a contract body. A generic function to compute a type is _very much_ in the realm of both refinement and dependent types. The BigArray example (as mentioned in a sister thread) is just a dependent type. > The hard part is defining precisely which generic function bodies are allowed by a given contract body. .. We are most uncertain about exactly what to allow in contract bodies, to make them as easy to read and write for users while still being sure the compiler can enforce them as limits on the implementation. That is, we are unsure about the exact algorithm to deduce the properties required for type-checking a generic function from a corresponding contract. My proposal/goal here is to define a type system, or set of constructors which has nice, formally provable limits on what can be constructed. Those constructs should be both easy to grasp _and_ computationally simple. As you say _general_ refinement types are not suited for a compiler focused on speed; however, a subset can very well be.