August 10, 2016

Solving GHCs KnownNat constraints

If you have ever worked with GHC.TypeLits then you have probably encountered an error that is very similar to:

In our case, the above error originates in the following file:

The problem is that, even though we have a KnownNat n (a type-level natural n which we can reflect to a term-level Integer), GHC cannot infer KnownNat (n+2). You would think that, in 2016, given a natural number n, an advanced compiler such as GHC should surely be able to infer the value corresponding to the natural number n + 2: you simply add 2 to already given n. Sadly, GHC can not do this… and, surely, complaints were made.

A type-checker plugin for solving KnownNat constraints

As I’ve blogged about in another post, GHC supports so-called type-checker plugins since version 7.10.1. Type checker plugins let us extend GHC’s constraint solver, i.e., extend the range of programs GHC can type check.

So, given that GHC 7.10.1 was released on March 27 2015, surely somebody must have already written a type-checker plugin that can fix our annoying KnownNat issue, right? Well, even if someone did, such a plugin has never been released on hackage, until today that is: https://hackage.haskell.org/package/ghc-typelits-knownnat

By just adding the following line:

{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}

to our program:

we can finally see that “all is right with the world (of KnownNat)”:

Creating this type-checker plugin

Now, there are probably a multitude of reasons as to why a plugin for solving KnownNat constraints wasn’t build/released before now; one of the likely reasons being that both the GHC API, and type-checker plugins, are somewhat obscure. Then again, I, the author of this post, have written several type-checker plugins, and I am (at least somewhat) familiar with those parts of the GHC API that are involved with constraint solving. So what are the reasons that I didn’t build such a plugin (much) earlier:

  1. To be honest, I was personally never too bothered with typing in the extra KnownNat constraints. That is, until I wanted to simplify the API of one of the libraries that I work on.
  2. I thought it couldn’t be done.

I will now focus on point 2, the reason I thought it couldn’t be done.

Evidence for KnownNat constraints

Basically, what Type checker plugins must do is provide evidence for the constraints GHC wants them to solve; where this evidence takes on the form of EvTerm:

Where, for example, the evidence for a KnownNat 8 constraint, would be encoded by EvLit (EvNum 8). OK, so what’s the problem with EvTerm? Well, let me first explain what we are trying to do:

  • Given e.g. evidence for KnownNat n and KnownNat 2
  • We want to add the two values of the evidence to create evidence for KnownNat (n+2).

And this is where we run into problems: EvTerm does not have a constructor for adding two KnownNat evidence terms. Actually, the more general problem is that it doesn’t allow us to create (arbitrary) Core expressions which will perform the addition. This problem is discussed in more detail at: https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker#Underdiscussion:EmbeddingCoreExprinEvTerm.

So, this made me think that it was simply not possible to create a KnownNat solver given the current (version 8.0.1) state of the GHC API. And then, yesterday (August 9th, 2016), just before bed, after staring for some time at the EvTerm definition, I realised I could use the EvDFunApp constructor to do what I want!

Building a dictionary (function)

As some of you might already know, class constraints in Haskell are translated to so-called dictionaries by GHC. A dictionary is record, where the fields correspond to the methods (and super-classes) of the class. So, e.g. for the Eq class:

GHC creates the following dictionary:

Now, what perhaps fewer people know, is that for instances with class constraints, GHC creates dictionary functions: functions that create dictionaries. i.e. given the instance:

GHC creates a dictionary function:

Now that we know what dictionary functions are, we can come back to the EvDFunApp constructor of EvTerm.
EvDFunApp applies dictionaries to a given dictionary function. That is, where dictionary functions are our evidence-level lambdas, EvDFunApp is our evidence-level application. This means that all we need to do is figure out how to write an instance that gives us our evidence-level arithmetic operations, and we would be in business.

Evidence-level addition

Below follows the code for our specially crafted class, and corresponding instance, so that we get an _evidence-level_ addition operation:

For the above code, GHC will generate the desired _dictionary function_ to do _evidence-level_ addition:

OK, so we can now build a DKnownNatAdd dictionary, however, this only gives us _evidence_ for a KnownNatAdd constraint, but not for a KnownNat constraint. And this is where another lesser-known aspect of GHCs translation of classes comes in:

  • Single method classes are represented by newtype dictionaries in GHC.

And, we can safe cast a newtype to (and from) its underlying representation using coercions.
Looking at the code for our evidence-level addition, we can now see that:

  • KnownNatAdd is nothing more than a newtype wrapper around SNatKn
  • SNatKn is a newtype wrapper around Integer.

And, when we take a look at the (hidden) definition of KnownNat:

we see that KnownNat is, ultimately, also nothing more than a newtype wrapper around Integer. This means we can safely cast our DKnownNatAdd dictionary to the DKnownNat dictionary (the code for these coercions can be found here):

  1. KnownNatAdd a b ~ SNatKn (a + b)
  2. SNatKn (a + b) ~ Integer
  3. Integer ~ SNat (a + b)
  4. SNat (a + b) ~ KnownNat (a + b)

And that’s it:

  1. We have our DKnownNatAdd dictionary function for _evidence-level_ addition.
  2. A way to safely cast a DKnownNatAdd dictionary to a DKnownNat dictionary, the evidence for KnownNat constraints.

Closing thoughts

So now finally, on August 10th 2016, using the ghc-typelits-knownnat type checker plugin, GHC can finally solve “complex” KnownNat constraints from other simple, single variable, KnownNat constraints. So does that mean it can infer all kinds of “complex” KnownNat constraints? Well… no, it can (currently) only infer constraints involving:

  • Type-level natural numbers
  • Type variables
  • Applications of the following type-level operations: +, *, and ^.

i.e. it cannot solve constraints involving subtraction (-) or user-specified type-level operations on type-level naturals, such as:

Where the problem with subtraction is that it is a partial function on natural numbers. Let’s say someone writes:

then we should not just automatically solve the KnownNat (n-4) constraint from the given KnownNat n constraint, because for 0 <= n < 4, n-4 is not a natural number. In this case, we should only automatically infer KnownNat (n-4) when an additional 4 <= n constraint is given:

I think I know how to check for these additional constraints, so a future version of the plugin will automatically solve KnownNat constraints involving subtractions. 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. Perhaps, once arbitrary Core expressions can be used as evidence (discussed here), we can reflect type-level operations to evidence-level operations, and then also automatically solve KnownNat constraints over user-defined type-level operations.

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

Design and realisation by:
Comyoo | creatieve studio

Address


Institutenweg 25A
7521 PH Enschede
+31 (0)85 8000 380
info@qbaylogic.com


CoC: 66440483
VAT: NL856554558B01