Add BitPack instance for Index 0

[kleinreact]

This PR gets rid of the additional 1 <= n constraint for the BitPack instance of Index n.

Background:

• Index 0 and Void are empty types → isomorphic to the empty set
• Index 1 and () are singleton types → isomorphic to a singleton set

Hence, we only need to question ourselves: how many bits do you need to distinguish between different elements of these types / sets? In both cases the answer clearly is: 0. Thus, BitSize (Index 0) = 0.

From another perspective: Clash generates valid HDL for Index 0 and the number of bits required by the generated HDL is zero as well. Hence, there is no reason to hide this fact in the type system for this particular case.

Still TODO:

• Add this fact to the typelits plugins. (WIP: https://github.com/clash-lang/ghc-typelits-extra/tree/add-clog-with-zero)
• Write a changelog entry (see changelog/README.md)
• Check copyright notices are up to date in edited files

[martijnbastiaan]

Review together with @DigitalBrains1

Nice, this would get rid of a lot of unwanted 1 <= n constraints.

Add this fact to the typelits plugins.

I doubt reasoning about type families is in-scope for the plugins, but you might want to take that up with the maintainers :-).

I think we should change the cover letter's motivation to be something along the lines of "this aligns clash-the-compiler's thoughts on Index 0 with BitPack (Index 0)".

A changelog is needed, but that's also in the TODOs.

Other than that LGTUs.

[DigitalBrains1]

It seems to still need something more though:

src/Clash/Explicit/Synchronizer.hs:126:35: error: [GHC-25897]
    • Could not deduce ‘Clash.Sized.Internal.Index.BitSizeIndex
                          (2 ^ addrSize)
                        ~ addrSize’
      from the context: (KnownDomain wdom, KnownDomain rdom, NFDataX a,
                         KnownNat addrSize, 1 <= addrSize)

Full message

src/Clash/Explicit/Synchronizer.hs:126:35: error: [GHC-25897]
    • Could not deduce ‘Clash.Sized.Internal.Index.BitSizeIndex
                          (2 ^ addrSize)
                        ~ addrSize’
      from the context: (KnownDomain wdom, KnownDomain rdom, NFDataX a,
                         KnownNat addrSize, 1 <= addrSize)
        bound by the type signature for:
                   fifoMem :: forall (wdom :: Clash.Signal.Internal.Domain)
                                     (rdom :: Clash.Signal.Internal.Domain) a
                                     (addrSize :: GHC.TypeNats.Nat).
                              (KnownDomain wdom, KnownDomain rdom, NFDataX a, KnownNat addrSize,
                               1 <= addrSize) =>
                              Clock wdom
                              -> Clock rdom
                              -> Enable wdom
                              -> Enable rdom
                              -> Signal wdom Bool
                              -> Signal rdom (BitVector addrSize)
                              -> Signal wdom (BitVector addrSize)
                              -> Signal wdom (Maybe a)
                              -> Signal rdom a
        at src/Clash/Explicit/Synchronizer.hs:(100,1)-(115,18)
      Expected: BitVector addrSize
                -> Clash.Sized.Internal.Index.Index (2 ^ addrSize)
        Actual: BitVector
                  (Clash.Class.BitPack.Internal.BitSize
                     (Clash.Sized.Internal.Index.Index (2 ^ addrSize)))
                -> Clash.Sized.Internal.Index.Index (2 ^ addrSize)
      ‘addrSize’ is a rigid type variable bound by
        the type signature for:
          fifoMem :: forall (wdom :: Clash.Signal.Internal.Domain)
                            (rdom :: Clash.Signal.Internal.Domain) a
                            (addrSize :: GHC.TypeNats.Nat).
                     (KnownDomain wdom, KnownDomain rdom, NFDataX a, KnownNat addrSize,
                      1 <= addrSize) =>
                     Clock wdom
                     -> Clock rdom
                     -> Enable wdom
                     -> Enable rdom
                     -> Signal wdom Bool
                     -> Signal rdom (BitVector addrSize)
                     -> Signal wdom (BitVector addrSize)
                     -> Signal wdom (Maybe a)
                     -> Signal rdom a
        at src/Clash/Explicit/Synchronizer.hs:(100,1)-(115,18)
    • In the first argument of ‘fmap’, namely ‘unpack’
      In the second argument of ‘(<$>)’, namely ‘fmap unpack waddr’
      In the first argument of ‘(<*>)’, namely
        ‘RamWrite <$> fmap unpack waddr’
    • Relevant bindings include
        portB :: Signal wdom (RamOp (2 ^ addrSize) a)
          (bound at src/Clash/Explicit/Synchronizer.hs:125:4)
        waddr :: Signal wdom (BitVector addrSize)
          (bound at src/Clash/Explicit/Synchronizer.hs:116:38)
        raddr :: Signal rdom (BitVector addrSize)
          (bound at src/Clash/Explicit/Synchronizer.hs:116:32)
        fifoMem :: Clock wdom
                   -> Clock rdom
                   -> Enable wdom
                   -> Enable rdom
                   -> Signal wdom Bool
                   -> Signal rdom (BitVector addrSize)
                   -> Signal wdom (BitVector addrSize)
                   -> Signal wdom (Maybe a)
                   -> Signal rdom a
          (bound at src/Clash/Explicit/Synchronizer.hs:116:1)
    |
126 |                (RamWrite <$> fmap unpack waddr <*> fmap fromJustX wdataM)
    |                                   ^^^^^^

Experienced with GHC 9.6.6.

[edit]
This also happens on CI with multiple (perhaps all? Didn't check) GHC versions.
[/edit]

[kleinreact]

It's because of the new BitSizeIndex type family introduced and can be fixed by teaching the typelits plugins about it's properties in particular. Unfortunately, I also don't know about any better solution at the moment. I tried several other things to help the type checker in acting in any smarter way, but that's the best solution I could find.

[leonschoorl]

I understand the desire to get rid of that 1 <= n constraint in a polymorphic setting.

But lets say someone is (accidentally) calling unpack @(Index 0).
This PR changes this from a compile time error to a run time error.
Which feels to me like a step in the wrong direction.

[kleinreact]

This PR changes this from a compile time error to a run time error.

I don't think that this is the right way to look at it. Consider the following example:

topEntity ::
  HiddenClockResetEnable System =>
  Signal System (Index 0)
topEntity = pure $ unpack @(Index 0) $ resize (0 :: BitVector 1)

If that description is turned into Verilog with clash, without the changes of this PR, then the example produces a compile time error. However, it produces perfectly valid Verilog after the fixes introduced by this PR.

I agree that the user might end up with a run time error in simulation, if trying to inspect what comes out of applying unpack @(Index 0), but that is fine, as there is no output unpack @(Index 0) can ever produce. Thus, the error is not that unpack @(Index 0) now is a valid object, which can be created at runtime, but more that the user tries to get something out of it, which just is not possible.

Note that the type system never was intended to prevent us from this, in the same way as it cannot prevent us from ever having a look at the contents of undefined.