August 17, 2016

Solving custom operations in KnownNat constraints

In my previous post I discussed a solver plugin for KnownNat constraints, and with regards to user-defined type-level operations, I said:

i.e. it cannot solve constraints involving subtraction (-) or user-specified type-level operations on type-level naturals […] For user-defined type-level natural operations we are currently out of luck: unlike for the standard operations in GHC.TypeLits, we cannot encode the corresponding _dictionary functions_ beforehand.

well… it turns our we do not have to know these corresponding dictionary functions beforehand. So, I’m hereby announcing version 0.2 of the ghc-typelits-knownnat plugin, which can now also solve KnownNat constraints over types consisting of:

  • Subtractions (GHC.TypeLits.-)
  • User-defined type-level functions

Supporting user-defined operations

So what is the “trick” for handling user-defined operations? Well, in my previous post, we defined a class, and corresponding instance for every type-level operation. For example, for addition (GHC.TypeLits.+), we defined:

And for multiplication (GHC.TypeLits.*), we defined:

However, what we would want, is a single type class for functions of a certain arity, and subsequently define multiple instances for this single class. We can then export these type-classes, and developers can add an instance for their own type-level operations, and the solver plugin can then just lookup these instances.

Using some singletons trickery we can define such a type class as:

As it says in the comments, the first argument of this class is a type-level Symbol corresponding to the fully qualified name of the type-level operation. We need to do this, because, unlike normal type constructors (.i.e. Maybe), type families cannot be partially applied. This means we cannot write a class and corresponding instance of the form:

So, instead, for the first argument of the KnownNat2, we use a Symbol that corresponds to the name of the type-level operation. The solver plugin can then use the name of type-level operation to find the corresponding KnownNat2 instance.

Now, again due to the restriction on the partial application of type families, the associated type family KnownNatF2 cannot be of kind:

Instead, we must use a defunctionalised form of our type-level operations, which are provided by the singletons package:

Where the difference is that we use ~> (tilde-right_angle) instead of -> (dash-right_angle).

We can now define our addition and multiplication instances as:

And subtraction as:

which gets an extra constraint that KnownNat (a - b) only holds when b <= a.

Adding operations to the solver

So now that we have a type-class for constraint-level arithmetic, what steps should a developer take so that her type-level functions are supported by the ghc-typelits-knownnat solver? We will give a short example.


Enable some language extensions


Import the required modules


Define the type-level operation

One restriction is that such a type-level operation must have at least two equations. This restriction is due GHC treating single-equation type families as type synonyms, which are expanded at the Core level.

That is, had we written our Max operation as a single-equation operation:

then a KnownNat (Max x y) constraint would show up as KnownNat (If (x <=? y) y x) inside the solver plugin. And, consequently, the solver wouldn’t be able to look up the KnownNat2 instance of Max.


Use Template Haskell to generate the defunctionalised form of the type-level operation:

This will create the following definitions:

where we need MaxSym0.


And finally specify the KnownNat2 instance:

where we use the nameToSymbol (exported by GHC.TypeLits.KnownNat) function to converts a Template Haskell Name to a Symbol.

Version 1.0?

The ghc-typelits-knownnat solver plugin is now at version 0.2; and it supports:

  • All the type-level arithmetic functions of GHC.TypeLits
  • User-defined type-level operations

Which might make you wonder: if it basically supports all type-level operations on Nat, why isn’t this version 1.0?

Well, I probably should have called it 1.0, and perhaps I will call it that in a next bugfix release. However, there are still some aspects that would be nice to add/fix:

  • Add a KnownBool and KnownOrdering class and add support for the comparison operators of GHC.TypeLits.
  • Find a way to index the KnownNat classes that is less error-prone than a Symbol corresponding to the fully qualified name of the type-level operation.

An FPGA design house delivering "right the first time" solutions.

Design and realisation by:
Comyoo | creatieve studio


Capitool 10
7521 PL Enschede
+31 (0)85 8000 380

CoC: 66440483
VAT: NL856554558B01