Except this version doesn’t compile. I’m not sure that it’s possible to get it to compile: type-level Idris is actually a _subset_ of Idris and pattern-matching

Except this version doesn’t compile. I’m not sure that it’s possible to get it to compile: type-level Idris is actually a _subset_ of Idris and pattern-matching non-ADTs is half-broken on the type level. You can also observe this problem in this simplified example: f : Char -> Type f '0' = Int f _ = Char g : (c : Char) -> (f c) g '0' = 0 g c = c