Follow Up on Problem with Constraint Solver

[paddytheplaster]

Hi again,

I am still getting problems with the new constraint solver. The following is symptomatic.

* {-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-}
* Could not deduce: CLog 2 4 ~ 2
  ...
  Expected type: Vec (CLog 2 4 + 1) (BitVector 1)
    Actual type: Vec (2 + 1) (BitVector 1)
* In the `xx' field of a record
  In the `xy' field of a record
  In the `xz' field of a record

|
36 | > ... xx = (0b0:>0b0:>0b0:>Nil) ...
|

What is odd is that the bug arises in the presence of a (harmless) top-level constraint of the form

Constraint x y z .. =>

where all arguments are integer literals. If I remove the constraint, the bug disappears.

I also find that I have to overspecify certain kinds of constraints:

• 1 <= (CLog 2 d + CLog 2 n + 1)

If I specify the following the simplifier can't detect the previous constraint is true.

• 0 <= CLog 2 d + CLog 2 n

Paddy

[rowanG077]

I can't reproduce this.

import Clash.Prelude

f :: (KnownNat n, CLog 2 n ~ 2) => Unsigned n -> Unsigned n
f = id

Running in clashi:

*Main> :l Test.hs
[1 of 1] Compiling Main             ( Test.hs, interpreted )
Ok, one module loaded.
*Main> f (0 :: Unsigned 2)

<interactive>:14:1: error:
    • Couldn't match type ‘CLog 2 2’ with ‘2’ arising from a use of ‘f’
    • In the expression: f (0 :: Unsigned 2)
      In an equation for ‘it’: it = f (0 :: Unsigned 2)
*Main> f (0 :: Unsigned 3)
0
*Main> f (0 :: Unsigned 4)
0
*Main> f (0 :: Unsigned 5)

<interactive>:17:1: error:
    • Couldn't match type ‘CLog 2 5’ with ‘2’ arising from a use of ‘f’
    • In the expression: f (0 :: Unsigned 5)
      In an equation for ‘it’: it = f (0 :: Unsigned 5)
*Main>

Can you make a reproducible example? I don't think you should manually import the solver plugins as Clash should handle that for you.

[paddytheplaster]

Hi Rowan,

Three things.

o The explicit constraint didn't have variables in it.
o When I removed the constraint, the error disappeared.
o The constraint was much more complex and it triggered the error.

I'll try and isolate the error but this is not east. (Spent quite some time on this already.) Without the plugins I get other errors.

Regards,

Paddy