Have `forall n . KnownNat n` but gives type mismatch error for a vector on successive recursion

Clash Help
1

Hi, I am trying to write a simple 8-bit ripple carry adder in Clash as shown in the code below which doesn’t work atm.

As per my understanding, forall n. KnownNat n puts the type-constraints saying that n is known at compile time, which is true for all values of n. So, shouldn’t the rippleCarryAdder as bs cout work just fine? The call should have n-1 size which should be valid as per the constraints.

Is my understanding correct? What am I missing here?

Thanks in advance :pray:

rippleCarryAdder :: forall n . KnownNat n => Vec n Bit -> Vec n Bit -> Bit -> (Vec n Bit, Bit)
rippleCarryAdder Nil Nil cin = (Nil, cin)
rippleCarryAdder (as :< a) (bs :< b) cin =
  let 
    (y, cout) = fullAdder a b cin 
    (ys, cfinal) = rippleCarryAdder as bs cout
  in 
    (ys :< y, cfinal)


-- 8 bit rippple carry adder
topEntity:: Vec 8 Bit -> Vec 8 Bit -> Bit -> (Vec 8 Bit, Bit)
topEntity= rippleCarryAdder

clashi> :r
[1 of 1] Compiling EightBitAdder    ( EightBitAdder.hs, interpreted )

EightBitAdder.hs:28:19: error:
    • Couldn't match type ‘n’ with ‘n0 + 1’
      Expected: Vec n Bit
        Actual: Vec (n0 + 1) Bit
      ‘n’ is a rigid type variable bound by
        the type signature for:
          rippleCarryAdder :: forall (n :: Nat).
                              KnownNat n =>
                              Vec n Bit -> Vec n Bit -> Bit -> (Vec n Bit, Bit)
        at EightBitAdder.hs:26:1-94
    • In the pattern: as :< a
      In an equation for ‘rippleCarryAdder’:
          rippleCarryAdder (as :< a) (bs :< b) cin
            = let
                (y, cout) = fullAdder a b cin
                (ys, cfinal) = rippleCarryAdder as bs cout
              in (ys :< y, cfinal)
    • Relevant bindings include
        rippleCarryAdder :: Vec n Bit
                            -> Vec n Bit -> Bit -> (Vec n Bit, Bit)
          (bound at EightBitAdder.hs:27:1)
   |
28 | rippleCarryAdder (as :< a) (bs :< b) cin =
   |                   ^^^^^^^
Failed, no modules loaded.
2

This is a bug and was fixed in this PR, Here is the original issue if you are interested in the background. But it appears the fix didn’t take.

So you are indeed correct that it should work. For a workaround you can define your function like so:

rippleCarryAdder :: forall n . KnownNat n => Vec n Bit -> Vec n Bit -> Bit -> (Vec n Bit, Bit)
rippleCarryAdder ass bss cins = go (reverse ass) (reverse bss) cins
  where
    go :: forall n . KnownNat n => Vec n Bit -> Vec n Bit -> Bit -> (Vec n Bit, Bit)
    go Nil Nil cin = (Nil, cin)
    go (Cons a as) (Cons b bs) cin =
      let
        (y, cout) = fullAdder a b cin
        (ys, cfinal) = go as bs cout
      in
        (ys :< y, cfinal)

mapAccumR fits a ripple carry adder like glove though:

fullAdder :: Bit -> (Bit, Bit) -> (Bit, Bit)
...

rippleCarryAdder :: forall n . KnownNat n => Vec n Bit -> Vec n Bit -> Bit -> (Bit, Vec n Bit)
rippleCarryAdder as bs cin = mapAccumR fullAdder cin (zip as bs)
2 Likes
3

Thank you very much :pray: