aith VS LinearML

As for uses of kinds in general, I'm using them a lot in Aith. Except that, instead of using higher kinds I'm parameterizing my Type to allow for fancier classification then just "this is a type". I'm using kinds for

Aith is another new one.

https://github.com/Superstar64/aith is also an interesting language, with substructural typing. The creator is also in the discord server if you have any questions

In Aith after doing hindley milner type checking, I want to annotate my ast with type annotations for several reasons:

It depends on how powerful you want your macros to be. In aith, my macros are just a compile time lambda calculus. My macros can only generate values or other macros, this limits them to being no more powerful then what you can normally do with functions but it (will when my language is usable) let me write code that I know will be inlined and edsls that compile into fast code. With these limitations I can completely type check macros ahead of time (because they are just like funcitons) and I can also use my kind system to prevent macro types from leaking out into normal ones.

LinearML

LinearML almost fits the bill, but it doesn't have manual memory management. It has a linear type system that is similar to Rust's borrow checker. All values are required to be used exactly once, except for primitives types which can be used multiple times. You can observe a value (similar to Rust's shared reference), but you can't store observed values in records or variants.