> Any type system with dependent types (`where` in Passerine) is undecidable, meaning error reporting for these types has to be moved to runtime. Maybe I am mi

> Any type system with dependent types (`where` in Passerine) is undecidable, meaning error reporting for these types has to be moved to runtime. Maybe I am misunderstanding you, but this is very confusing. Most dependently-typed languages do in fact check types at compile time: the undecidability problem usually implies a compromise that “correct” programs will be incorrectly rejected (the compiler gives up earlier than it needs to) instead of letting the type-checker get stuck in an infinite loop. But it does not mean type-checking is simply moved to runtime! I am sincerely confused where you got this idea, which makes me wonder if I misunderstood you.