Total Type Families
A total type family feels quite comfortable. By total here, I mean a type family whose equations cover all the possible cases and which is guaranteed to terminate. That is, a total type family is properly a function on types. Those other dependently typed languages have functions on types, and they seem to work nicely. I am completely unbothered by total type families.
Non-covering Type Families (are strange)
> A non-covering type family is a type family whose patterns do not cover the whole space.