The difference between regular languages and "type system languages" (at least well designed ones) is that the latter are decidable. In that sense another types

The difference between regular languages and "type system languages" (at least well designed ones) is that the latter are decidable. In that sense another typesystem lang for the typesystem lang would still be a decidable one. The most generic one I know of is Idris. It uses some heuristics to make some functions decidable that in theory should not be.