I think OP wants transitive exhaustiveness checks while supporting partial base functions. My suggestion: Must you have partial functions? Maybe you can model

I think OP wants transitive exhaustiveness checks while supporting partial base functions. My suggestion: Must you have partial functions? Maybe you can model your data more tightly? If your conditions are too complex, maybe you could decompose them? A big reason I like ADTs with concise syntax is to model data with nearly¹ no room for invalid or useless data. Then all¹ functions are total and matches are checked for exhaustiveness. A nice matching syntax on top makes mistakes easy to spot. Not sure how to help with formal verification or exhaustiveness on partial functions. ¹ I don't model everything absolutely precisely, but deviations are more of an exception rather than the rule. Then they can be made apparent and reasoned about.