[Haskell-cafe] [ANN] ghc-typelits-knownnat-0.2: Solving GHCs KnownNat constraints

Christiaan Baaij christiaan.baaij at gmail.com
Wed Aug 17 13:11:25 UTC 2016


Hi,

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

 >    • Could not deduce (KnownNat (n + 2))
 >        arising from a use of ‘natVal’
 >      from the context: KnownNat n

i.e. where GHC cannot infer a `KnownNat (n+2)` constraint, even though a 
`KnownNat n` constraint is already given.

Enter http://hackage.haskell.org/package/ghc-typelits-knownnat
A type-checker plugin that can automatically derive "complex" KnownNat 
constraints from simpler ones.

To use it, you simply add the

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

pragma to the top of your file.

If you want to know more, you can also check out the corresponding blog 
posts:

http://qbaylogic.com/blog/2016/08/10/solving-knownnat-constraints-plugin.html
http://qbaylogic.com/blog/2016/08/17/solving-knownnat-custom-operations.html

Regards,

Christiaan


More information about the Haskell-Cafe mailing list