[kustosz]

This feature is a bit of a misnomer, as it immediately brings up discussions about category theory. That being said, the idea behind it is pretty simple, yet powerful. Our typechecker will be able to track the shape of data on a deeper level than usual types. Basically will be tracking the exact constructors used to construct data, not just types – something that is a huge pain in most existing typed languages. If you for example take Haskell, you can have a data type with multiple different constructors, and even though you may be certain that some of those are impossible to occur at some points in your program, it is difficult to express that certainty on typelevel – other than repacking to a different datatype, with less constructors, which then need to be named differently and need repacking even if you're just calling a function that expects a wider range of constructors, and thus is definitely safe. However, due to the amount of work with more foundational layers of the language, we've had to postpone implementing this feature until further down the line. It is coming at some point for sure, though :)

[tentaTherapist]

That sounds like a horribly leaky abstraction if you mean that you're literally going to statically track the call stack to attempt to verify invariants. Hopefully it's just a misunderstanding on my part.

[thecity2]

This sounds a bit like Idris with its dependent types.