Make GHC apply basic math laws on `KnownNat`

Question

i just discovered the super awesome Haskell library Numeric.LinearAlgebra.Static from the hmatrix package.

Now i implemented a function that shall transform a matrix A to a vector B and another matrix C like this:

    1 2 3
A = 4 5 6
    7 8 9

B = 2 3

C = 5 6
    8 9

the code that i came up with that successfully compiles looks like this:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}

import GHC.TypeLits
import Numeric.LinearAlgebra.Static

f :: (KnownNat (n + 1), KnownNat n, 1 <= n + 1, ((n + 1) - 1) ~ n)
  => Sq (n + 1) -> (R n, Sq n)
f m = (unrow a, b)
    where
        (a, b) = splitRows . snd . splitCols $ m

main :: IO ()
main = print $ f $ (matrix [1, 2, 3, 4, 5, 6, 7, 8, 9] :: Sq 3)

Now this works well, but i hope that i can remove seemingly redundant things like ((n + 1) - 1) ~ n from the type signature.

Is it somehow possible to make GHC accept a signature like f :: Sq (n + 1) -> (R n, Sq n) without anything else? Or at least something like f :: (KnownNat n, 2 <= n) => Sq n -> (R (n - 1), Sq (n - 1))?

Answer 1

There are type checking plugins that can do this. Specifically, ghc-typelits-natnormalise can figure out that ((n + 1) - 1) ~ n and 1 <= n + 1, while ghc-typelits-knownnat can figure out that KnownNat n implies KnownNat (n+1). So, with both packages installed, you can write:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}

import GHC.TypeLits
import Numeric.LinearAlgebra.Static

f :: (KnownNat n) => Sq (n + 1) -> (R n, Sq n)
f m = (unrow a, b)
    where
        (a, b) = splitRows . snd . splitCols $ m

main :: IO ()
main = print $ f $ (matrix [1, 2, 3, 4, 5, 6, 7, 8, 9] :: Sq 3)

The KnownNat n constraint is unavoidable.