Related to #2, generalize the notion of runtime dependence. Instantiating a built-in type with an unknown value should generate a new dependent type. For example:
def X : record {
n : int;
a : int[n]; // or array(int, n)
};
Would cause all uses of a to also depend on n. I'm not sure if there is a general pattern that can be defined for this or if we need to define special cases for types that can be made dependent.
Related to #2, generalize the notion of runtime dependence. Instantiating a built-in type with an unknown value should generate a new dependent type. For example:
Would cause all uses of
a
to also depend onn
. I'm not sure if there is a general pattern that can be defined for this or if we need to define special cases for types that can be made dependent.