Verifying type families for termination and correctness

Interesting question! I’m having difficulties to define what termination even means for type families. Let’s try to work out what is needed to solve this. Please correct me if you think any of the following is not accurate.

In first approximation, a type family is a function f :: Type -> ... -> Type. Let us forget that we are actually dealing with types and abstract to f :: t -> ... -> t.

Next question is, what primitives are available to build f?

• We certainly have recursion, otherwise the question of termination would be trivial. But it is not a full untyped or simply-typed lambda calculus, because there is no currying or partial application in type families, right? At least GHC currently does not support this.
• There is no type of type families. In other words, no higher-rank families. data FamilyKind = Kind | Kind :->: FamilyKind Note: No FamilyKind on the LHS of the arrow.
• We have a context of known type names in scope, which we can regard as elements of t. Moreover, type family declarations can be mutually recursive.
• We have pattern matching on values of t, at least to some extent. We can certainly match on known primitive types names like Int.
• Type families are partial in general. Would you consider a properly partial type family as terminating?

So we have something like a simply-typed lambda calculus, with recursion, (partial) pattern matching and variables, but only application, no lambda abstraction. The Dec type in Template Haskell might give hints where I have over-simplified.

Finally, in our hypothetical universe of type families t -> ... -> t, what counts as termination? I suppose we need a reduction relation similarly to what we have in lambda calculus and say a type family terminates when variable-free terms have a normal form.

All in all, when you ask for type family termination tools, you should look for tools that can prove normalization in lambda calculi. I don’t know whether the absence of lambda abstraction makes this problem any easier.