We propose a calculus for modeling implicit programming that supports first-class and higher-order rules with higher-kinded types. Unlike previous works, we propose a straightforward generalization of the well-established System $F^\omega$ and give a declarative specification of coherent resolution without introducing vexing restrictions. We present the calculus formally and discuss exciting avenues for further research.