The language is quite interesting https://github.com/Morgan-Stanley/hobbes#evaluation: e. g. anonymous variants, isorecursive types.