Constraint 'n <= i' Does not Imply '(i+1) > n'

[paddytheplaster]

Greetings.

I can't convince the type checker that 'n <= i' implies '(i + 1) > n'. (The 'OPTIONS' in the following may be omitted.)

   module Ex where
   import Clash.Prelude

   {-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-}
   {-# OPTIONS -fconstraint-solver-iterations=0 #-}

   g :: forall (i :: Nat) (n :: Nat) . (CmpNat (i+1) n ~ 'GT) => SNat i -> SNat n -> Bool
   g _ _ = True
   g' :: forall (i::Nat) (n::Nat) . (KnownNat i, KnownNat i,n <= i) => SNat i -> SNat n -> Bool
   g' = g

      * Could not deduce: CmpNat (i + 1) n ~ 'GT
          arising from a use of `g'
        from the context: (KnownNat i, n <= i)

[rowanG077]

Unfortunately the type checker is not a mathematician that can prove all these things. The extra solvers Clash uses are able to solve quite a few additional things compared to normal GHC but the case you present here is unfortunately not one of them since it doesn't know what CmpNat is.

I would advice to try and rewrite constraints such as CmpNat in terms of <= since that is most likely to be able to be solved.

Oh and you don't need to manually enable the solver so this line is redundant:

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

[paddytheplaster]

Thanks Rowan. Unfortunately, some Clash functions such as 'select' are expressed using 'CmpNat'. This is what triggered the entire example...

module Ex where

import Clash.Prelude

-- Express the equivalent of a simple 'take n . drop f' with 'select'.
-- I'm starting without any knowledge about the length of the input vector
-- because that's what my context requires. The example is deliberately
-- contrived. My actual example is more complex and requires 'select'.
sel0 :: forall (f :: Nat) (n :: Nat) (l :: Nat) a
     . (KnownNat f,KnownNat n,KnownNat l) => SNat f -> SNat n -> Vec l a -> Vec n a
sel0 f n as = case compareSNat f (SNat @l) of SNatLE -> sel1 f n as

sel1 :: forall (f :: Nat) (n :: Nat) (l :: Nat) a
     .  (KnownNat f,KnownNat l,f <= l) => SNat f -> SNat n -> Vec l a -> Vec n a
sel1 f n as = sel2 @f @n @(l-f) f n as

sel2 :: forall (f :: Nat) (n :: Nat) (i :: Nat) a
     . ( KnownNat i ) => SNat f -> SNat n -> Vec (f+i) a -> Vec n a
sel2 f n as = case compareSNat n (SNat @i) of SNatLE -> sel3 f n as

sel3 :: forall (f :: Nat) (n :: Nat) (i :: Nat) a
     . n <= i => SNat f -> SNat n -> Vec (f+i) a -> Vec n a
sel3 f n as = select f d1 n as

Is there a way to convince the type checker to go from 'sel0' to 'select'?

Regards,

Paddy

[rowanG077]

Well I don't know if you can directly convince the type checker. But you can make a function that given a constraint of the form n <= m you gain a proof of the CmpNat (m + 1) n ~ 'GT constraint. You basically sidestep the type checker and tell it "Trust me I know this is always true". It's possible there are already functions that convert the constraints like this but I couldn't find them.

import Data.Kind (Type)
import Data.Constraint (Dict(..), (:-)( Sub ))
import Unsafe.Coerce (unsafeCoerce)

leToCmpNatGtProof
  :: forall (n :: Nat)
            (m :: Nat)
   . (n <= m) :- (CmpNat (m + 1) n ~ 'GT)
leToCmpNatGtProof = Sub axiom
  where
    axiom :: (n <= m) => Dict (CmpNat (m + 1) n ~ 'GT)
    axiom = unsafeCoerce (Dict :: Dict (a ~ a))

leToCmpNatGt
  :: forall (n :: Nat)
            (m :: Nat)
            (r :: Type)
   . n <= m
  => (CmpNat (m + 1) n ~ 'GT => r)
  -> r
leToCmpNatGt r = case leToCmpNatGtProof @n @m of { Sub Dict -> r }

g :: forall (i :: Nat) (n :: Nat) . (CmpNat (i+1) n ~ 'GT) => SNat i -> SNat n -> Bool
g _ _ = True

g' :: forall (i::Nat) (n::Nat) . (KnownNat i, KnownNat i,n <= i) => SNat i -> SNat n -> Bool
g' = leToCmpNatGt @n @i g

You can make similar cases for doing it the other way around or with other CmpNat results. It's wonky and dangerous since if you manually make a proof that's not actually true bad things may happen.

Another way to achieve what you want is to implement this step in the type checker plugin clash uses (https://github.com/clash-lang/ghc-typelits-extra) and make a pull request. But I'm not sure whether we even want to implement this there.

[paddytheplaster]

Hi Rowan,

Thanks very much. That's very useful.

FWIW If it takes this much effort to convince the type checker wouldn't it be much better to avoid using 'CmpNat' in the API of functions defined in general purpose libraries such as 'Clash.Sized.Vector'?

Thanks again,

Paddy

[rowanG077]

I don't know the reason why it was chosen for select. I had never even heard of/used CmpNat before this post. GHC.TypeLits does mention that <=? might go away in the future in favor of CmpNat and you should prefer it to <=?.

I guess the API of Clash was written before this though. But any of the core maintainers can probably answer that question.

[paddytheplaster]

Hi Rowan,

Interesting that they're thinking of getting rid of '<=?' because expressing things with 'CmpNat' will require many more keystrokes and will result in constraint which are more difficult to parse for the human eye.

Thanks again,

Paddy

[christiaanb]

Automated reasoning about CmpNat is going to be much more annoying than automated reasoning about <=, so I'll actively try to prevent that CmpNat will subsume <= in the future.

With regards to select, we could change the type signature so that it says:

select :: (s * n) <= (i + s + 1) => SNat f -> SNat s -> SNat n -> Vec (f + i) a -> Vec n a 

instead of

select :: CmpNat (i + s) (s * n) ~ 'GT => SNat f -> SNat s -> SNat n -> Vec (f + i) a -> Vec n a 

[paddytheplaster]

Thanks Christiaan.

I welcome the proposed signature of 'select'.

Regards,

Paddy

[rowanG077]

Options for migration would be either to make a new select function with the constraint changed and a deprecation message for the old select. Or have a very ugly constraint where it's fine for the user to satisfy either the CmpNat constraint or the <=? constraint. With the new signature we can still warn for deprecation but it would be a false positive for people who are using <=?.