I just wish we could write simpler compile time type guard kind of things in a more simple way, because when the trait bounds metastasize it can get hard to rea

I just wish we could write simpler compile time type guard kind of things in a more simple way, because when the trait bounds metastasize it can get hard to read these type level programs “Where <<<T as F>::Output as G>::Output as H>::Output: HList<Head = A, Tail = B> + Z type Output = <<<T as F>::Output as G>::Output as H>::Output;” Put some Cons<Cons<Cons<U8, Nil>>>> in there and then realize numbers like U8 (from TypeNum) is itself a nesting of Cons<Cons<Cons< of binaries and it just winds up feeling like you’re looking at a massive nesting of <<<>>> Consequently you can make progress in this area and get it to verify what you want, but the error messages can be massively complicated and divergent from the way the human developer writes their code (because of the “types vs values” difference producing wildly different error messages which are hard to customize) and the implementation can be a massive pain in the ass. Developer experience here is surprising because it’s not “just functions” but rather combinations of functionalities with certain generics and associated types. You want to write a runtime style check but execute it at compile time, but to make that happen requires quite different code (in my experience) All this to say, perhaps making type level comptime rust more simple and functional and readable is ultimately what would enable a lot of these formal analysis projects to provide a good experience for their maintainers and users TLDR, wtb “comptime” Rust! P.S. are we ossified on Pin<&mut Self> Future ? I wish I could tinker with different underlying implementations of async/await but no clue how to get started