Inconsistent Constraint Parsing

[paddytheplaster]

The code below compiles fine.

However, the constraint checker will fail if your remove some redundant parentheses in the constraints of the function f. The commented line below has the parentheses removed. If you uncomment that line and remove the next line, you'll get an error.

Regards,

Paddy

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

> module Example where

> import Clash.Prelude

> type ExampleSize r n = n*(2^r-1) + 2^(r+1) - r * 2^r - 2

> g :: forall (r :: Nat) (i :: Nat) (s :: Nat) (a :: Nat)
>    .  (KnownNat a, KnownNat i, KnownNat r, KnownNat s, 1 <= a, (i+1)*a+r<=s)
>   => SNat r -> SNat i -> BitVector s -> BitVector a
> g r i v = undefined

> f :: forall (n :: Nat) (r :: Nat) (i :: Nat)
>   .  ( KnownNat n, KnownNat r, KnownNat i, r <= n
>      -- , (i+1)*(n-r)+n*(2^r-1)+2^(r+1)-r*2^r-2
>      , (i+1)*(n-r)+(n*(2^r-1)+2^(r+1)-r*2^r)-2
>          <= ((((n*((2^n)-1))+(2^(n+1)))-(n*(2^n)))-2)
>      )
>   => SNat n -> SNat r -> SNat i -> BitVector (ExampleSize n n) -> BitVector (n-r)
> f n r i v = undefined
>     where x :: BitVector (n-r)
>           x = g (SNat @(ExampleSize r n)) i v

[christiaanb]

Interesting.... but nigh impossible to debug in a short time...

[christiaanb]

I think it's a result of what constraints arise from the subtraction, e.g. when you have:

(a + b) - c

Then during solving it will want to know that c <= (a + b) because we're dealing with natural numbers. But when we write:

a + (b - c)

It will only want to know that c <= b. And I think what's happening here is the one case the current solver is smart enough that the inequality holds, but in the other case it isn't smart enough. And thus the way you put the parenthesis matters, which is somewhat disappointing and unexpected.

[paddytheplaster]

Thanks.

I didn't make up this constraint as it was output by Clash when my (then) current constraints weren't tight enough. I then added the suggested constraint and could then simplify the constraints to one single constraint and simplified the example. This surprised me as the constraint had lots of subtractions. Eg. what about the term n-r? Personally, I'd find it more useful if additive terms in constraints like x <= (a-b)+(c-d) were simplified to (b <= a,d<=c,x+b+d <= a+c), i.e. as few subtractions and parentheses as possible. Another advantage is that now terms may cancel. E.g. x <= (a-b) + (c-a) simplifies to (b<=a,c<=a,x<=c-b) simplifies to (b <= a,c <= a,b<=c,b+x<=c) simplifies to (b <= a, c <= a, b+x <= c).

Regards,

Paddy

[paddytheplaster]

Consider the following.

> module Example where

> import Clash.Prelude

> f :: forall (d :: Nat) (i :: Nat)
>   .  (KnownNat d,KnownNat i,1<=d)
>   => SNat d -> SNat i -> Bool
> f d i
>     -- The two compareSNat calls are each others complements
>     -- EDIT (Because they're in the scope of `1<=d`):
>     -- we can only get (SNatLE,SNatGT) or (SNatGT,SNatLE).
>   = case ( compareSNat (SNat @(d-1)) (SNat @i)
>          , compareSNat (SNat @(i+2)) (SNat @d) ) of
>       -- You get an error if you comment out the 1st and 2nd line
>       -- and uncomment 3rd and 4th next line
>       (SNatLE,SNatGT) -> g1 d i
>       (SNatGT,SNatLE) -> g2 d i
>       -- (SNatLE,_     ) -> g1 d i
>       -- (SNatGT,_     ) -> g2 d i

> g1 :: forall (d :: Nat) (i :: Nat) .  (1<=d,d<=i+1) => SNat d -> SNat i -> Bool
> g1 _ _ = True

> g2 :: forall (d :: Nat) (i :: Nat) .  (1<=d,i+2<=d) => SNat d -> SNat i -> Bool
> g2 _ _ = False

EDIT: The constraint in the previous is equivalent to i+2<=d.

The problem disappears if you write the following for the first compareSNat.

compareSNat (SNat @d) (SNat @(i+1))

Regards,

Paddy

I think it's a result of what constraints arise from the subtraction, e.g. when you have:

(a + b) - c

Then during solving it will want to know that c <= (a + b) because we're dealing with natural numbers. But when we write:

a + (b - c)

It will only want to know that c <= b. And I think what's happening here is the one case the current solver is smart enough that the inequality holds, but in the other case it isn't smart enough. And thus the way you put the parenthesis matters, which is somewhat disappointing and unexpected.

[paddytheplaster]

Consider the following.

> module Example where

> import Clash.Prelude

> f :: forall (d :: Nat) (i :: Nat)
>   .  (KnownNat d,KnownNat i,1<=d)
>   => SNat d -> SNat i -> Bool
> f d i
>     -- The two compareSNat calls are each others complements
>     -- EDIT (Because they're in the scope of `1<=d`):
>     -- we can only get (SNatLE,SNatGT) or (SNatGT,SNatLE).
>   = case ( compareSNat (SNat @(d-1)) (SNat @i)
>          , compareSNat (SNat @(i+2)) (SNat @d) ) of
>       -- You get an error if you comment out the 1st and 2nd line
>       -- and uncomment 3rd and 4th next line
>       (SNatLE,SNatGT) -> g1 d i
>       (SNatGT,SNatLE) -> g2 d i
>       -- (SNatLE,_     ) -> g1 d i
>       -- (SNatGT,_     ) -> g2 d i

> g1 :: forall (d :: Nat) (i :: Nat) .  (1<=d,d<=i+1) => SNat d -> SNat i -> Bool
> g1 _ _ = True

> g2 :: forall (d :: Nat) (i :: Nat) .  (1<=d,i+2<=d) => SNat d -> SNat i -> Bool
> g2 _ _ = False

EDIT: The constraint in the previous is equivalent to i+2<=d.

The problem disappears if you write the following for the first compareSNat.

compareSNat (SNat @d) (SNat @(i+1))

Regards,

Paddy

I think it's a result of what constraints arise from the subtraction, e.g. when you have:

(a + b) - c

Then during solving it will want to know that c <= (a + b) because we're dealing with natural numbers. But when we write:

a + (b - c)

It will only want to know that c <= b. And I think what's happening here is the one case the current solver is smart enough that the inequality holds, but in the other case it isn't smart enough. And thus the way you put the parenthesis matters, which is somewhat disappointing and unexpected.

FWIW The example I gave was to make it easier to understand what's going on and verify the problem (by just commenting/uncommenting). The reason for the bug is that Clash can't infer a simple (IMHO) constraint (that 1 <= d and the negation of the first compareSNat is the same as the constraint of g2). I originally only had one compareSNat and pattern matched on SNatLE and SNatGT only (so not on the pair). This is where I got an error. Since GHC's error messages aren't always so easy to understand it took a long while before I figured out I had to reformulate the negation of the compareSNat and pattern match on pairs.