Haskell has infinite and recursive constructs, lazily computed. That’s what makes their type system undecidable. Avail is constructivist in that sense, so immutable structures must be finite (i.e., you can draw them as a dag). For cyclic structures, you have to include mutable “variable” objects as well, but in that case the type of the construct stops at the boundary of the variable. The type of a tuple of variables is a composition of the declared types of the variables, not their current content. This is essential to ensure an object’s type is permanent, and the immutable acyclicity condition ensures everything reachable without hitting a variable contributes to an object’s type.
Haskell has infinite and recursive types but its type system is perfectly decidable, mainly because Haskell's type system is nominal, so cycles are easily detected and dealt with.
