[tathougies]

Avail does not seem to have dependent types. The term 'dependent type' is overused. It means that the type system must allow the compile-time type of an expression to depend on the run-time value. This is not totally decidable. Most type systems, including advanced ones, such as Haskell's, do not have this property. Avail seems no different.

[markvangulik]

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.

[tome]

> Haskell has infinite and recursive constructs, lazily computed. That’s what makes their type system undecidable.

Haskell (98) has infinite and recursive constructs and its type system is not undecidable.

[tathougies]

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.