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
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.