Another issue is that in real world types in fast programs usually can't be expressed and auto checked by a simple type system without mental/runtime overhead.

Another issue is that in real world types in fast programs usually can't be expressed and auto checked by a simple type system without mental/runtime overhead. For example, in many GPU kernels each thread visits patterns like (ax+b)%k, how do you ensure no data race in this example? The result depends on the coprimality between a and k. You will still need to check this at runtime and creating affine_mod_view for each access patterns like this would be overkill.