[ianlancetaylor]

I don't think there is any lack of clarity about your List example; that is clearly forbidden. The example that is less clear is the one that generates a million types and then stops.

A similar issue arises in C++; the C++ standard says that there is an implementation defined limit on the total depth of recursive instantiations. Perhaps Go should do something similar.

[zbobet2012]

C++'s method is certainly a practical way to limit expansion on inductively defined data types. I think a better way would be to construct a type system _opposite_ of most constructed today (which focus on the ability to express problems) and instead intentionally limit the types we are able to construct to those with "easy to use" and computationally efficient properties.

Consider this sample. We want to be able to define inductive types such as `List(T)`, but not `InfiniteList(T)` or `BigArray(T)`. While `BigArray(T)` is an interesting construct (it's effectively a dependent type)* it jumps past the "can I keep it in my head" smell test for me. As soon as a I have to reason deeply about what a type constructor does it just doesn't feel like Go to me.

So we want to be able to construct types which are inductive but can only calculate a single type. List{T} calculates one type, BigArray calculates _n_ types, and InfiniteList calculates an infinite number of types.

* In Idris one would write something like:

  data BigArray : (n : Nat) -> (l : List m) -> Type where
      Z l : Vect Z v
      n l : Vect n l