Default rules deliberately accept any kind.
Good. But you need a comment in TcSimplify.try_group. With mb_subst we see
-- Make sure the kinds match too; hence this call to tcMatchTy -- E.g. suppose the only constraint was (Typeable k (a::k))
It's very useful that kind-check is there, because we *also* want to reject the ill-kinded attempt (Eq ). Worth saying so!
Better "The types in a 'default' decl can have varying kinds; see Note [Extended defaults]" in TcEnv"
Oh, thanks. T10971b should pass, that's just intended so I don't mess something up. However, T10971a should fail; the main I put in by accident is preventing that. I'll remove it in a bit.