Thanks. The Shen language takes this to its logical conclusion (pun intended) and implements a fully Turing complete type system. Types are specified with sequents which are essentially Prolog relations using a slightly different notation.[1]
IIRC the type checker is literally a Prolog.