This is a typechecker plugin for GHC using an SMT solver to resolve constraints on booleans and natural numbers.
Add type-nat-solver to your build-depends list and -fplugin TypeNatSolver to ghc-options.
type-nat-solver
build-depends
-fplugin TypeNatSolver
ghc-options