Add BitPack instance for Index 0

[kleinreact]

This PR gets rid of the additional 1 <= n constraint for the BitPack instance of Index n, which aligns clash-the-compiler's thoughts on Index 0 with BitPack (Index 0).

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.

Requires:

• Add CLog with well-defined zero case ghc-typelits-extra#57
• Bump typelit plugins #3061

Still TODO:

• Add this fact to the typelits plugins.
• 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.

[DigitalBrains1]

This isn't a full review yet; I'll wait until you have it working.

But browsing a bit I did notice you expanded the scope of the PR a lot. You've removed a lot of Index n, 1 <= n constraints even if they don't involve BitPack. If you want to address different cases of Index bounds as well, I think it's better treated in a new PR because it'll require some good thought.

For instance, you're removing the 1 <= n from the resetGlitchFilter functions, but now it is just completely broken:

>>> printX $ sampleN 10 $ unsafeFromReset $ resetGlitchFilter d2 systemClockGen resetGen
[True,True,True,True,True,False,False,False,False,False]
>>> printX $ sampleN 10 $ unsafeFromReset $ resetGlitchFilter d0 systemClockGen resetGen
[True,True,True,True,undefined,undefined,undefined,undefined,undefined,undefined]

[kleinreact]

But browsing a bit I did notice you expanded the scope of the PR a lot. You've removed a lot of Index n, 1 <= n constraints even if they don't involve BitPack. If you want to address different cases of Index bounds as well, I think it's better treated in a new PR because it'll require some good thought.

Thanks for the quick feedback. I primarily was interested in observing which code may change and just wanted to get some feedback from CI. Unfortunately, there won't be any reasonable feedback without also hiding the warnings currently blocking #3061.

I'll definitely have a closer look on all the introduced changes again.

[DigitalBrains1]

I have some comments but have not yet finished the review, please bear with me.

[DigitalBrains1]

Thanks for all the work needed to get rid of these pesky constraints!

I have a few comments where I think the difference between Index 1 and Index 0 needs to be considered.

Also, in the first reply in this PR, Martijn wrote:

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)".

I think the PR cover letter would be improved with that consideration included.

[DigitalBrains1]

Oops, I really did not expect my git to choose your branch to push to when I executed the command

$ git push -u origin peter/add-bitpack-for-index-zero

It probably had something to do with a gaffe in setting up that branch, sorry.

Anyway, on peter/add-bitpack-for-index-zero I added a commit to have maybeNumConvert @_ @(Index 0) always emit Nothing as I suggested above. This seems a much better result than always having it return XException. I'd like to suggest integrating the contents of that commit in this PR.

I added a [skip ci] commit to prevent a costly GitLab CI pipeline, but if I subsequently screw up this branch and restore it, the CI will run for this branch anyway. Sorry, wasted electrons, I salute thee.

[edit]
Ooh, actually, I suspect GitLab CI will not run, only GitHub CI. The revert to the original commit was probably quick enough to put everything in order before the earlier push had a chance to trigger a run. Saved electrons, you may do a useful job later on, I salute thee.
[/edit]

[martijnbastiaan]

I think this is right, though I do feel nervous about making this change. It's right on that border where it's seemingly easy to make a change, but also easy to mess up.

.. so what are we waiting for! ✔️

[kleinreact]

@DigitalBrains1 Are you also satisfied with the updates regarding your requested changes then?

[DigitalBrains1]

Well, almost! I am satisfied with the changes. But I noticed a few last things. First of all, your rebase didn't completely work out: you forgot a 1 <= n! I'd also like to suggest some small changes to the changelog entries.

Note: that is you forgot a 1 <= n. It is not you forgot a 1 <= n!, which holds for all natural numbers 😉.

[martijnbastiaan]

I'm sorry to restart the discussion again, but I got on the wrong track in the NumConvert discussion. I thought we concluded:

• Writing functions / classes that accept Index 0 as an argument is 👍
• Writing functions / classes that return Index 0 is 👎

The logic being that accepting Index 0 is okay, because there is no universe in which a function like that can be called anyway (without using bottom). Conversely, returning Index 0 is not okay, because there is no way you can faithfully implement this (i.e., without using bottom).

And it looks like we've found real issues for Counter and NumConvert if we would violate those rules, but for BitPack we're now doing it anyway.

Am I misunderstanding this discussion so badly, or are we making a mistake here?

Edit: Not saying that I'm against pragmatic choices, to be clear. But I can't shake the feeling that the same issues that showed there is a need for 1 <= n on some classes, will show up for the others but we simply haven't come up with a counter example yet.

[kleinreact]

First of all, your rebase didn't completely work out: you forgot a 1 <= n! I'd also like to suggest some small changes to the changelog entries.

Nice catch. Thanks for the hint. I applied your suggestions.

• Writing functions / classes that accept Index 0 as an argument is 👍
• Writing functions / classes that return Index 0 is 👎

I totally agree. Isn't this exactly what has been implemented by this PR?

[DigitalBrains1]

unpack 0 :: Index 0

returns an Index 0. It's basically the core of this PR: dropping the 1 <= n on BitPack.

Well, it doesn't actually return a value. It returns Index 0. But it bottoms.

[martijnbastiaan]

I thought I'd run it through clashi to be sure. On master:

clashi> unpack 0 :: Index 0
<interactive>:1:1: error: [GHC-64725]
    • Cannot satisfy: 1 <= 0
    • In the expression: unpack 0 :: Index 0
      In an equation for ‘it’: it = unpack 0 :: Index 0

On this branch:

clashi> unpack 0 :: Index 0
*** Exception: X: Clash.Sized.Index: result 0 is out of bounds: <empty range>
CallStack (from HasCallStack):
  errorX, called at src/Clash/Sized/Internal/Index.hs:317:13 in clash-prelude-1.9.0-inplace:Clash.Sized.Internal.Index
  fromInteger_INLINE, called at src/Clash/Sized/Internal/Index.hs:190:20 in clash-prelude-1.9.0-inplace:Clash.Sized.Internal.Index

So on master I get a type error and on this branch a run time error. I.e., we increase the number of places where we can conjure up Void (according to the type signatures). This is not what we want, right? Or is there a pragmatic reason for ignoring the rules of thumb for this class?

[kleinreact]

unpack 0 :: Index 0

is an unfortunate coincidence, because BitVector 0 and Index 0 require both zero wires for being represented in HDL. Remember that our goal here is to correctly reflect the BitSize of Index (cf. the Background section in the description of the PR).

Hence, yes, in the context of REPL simulation you can create a bogous value of Index 0, which won't exist according to the theory and, thus, never will end up in HDL, but appears as undefined in simulation. However, if you are able to create some Index 0, causing an error in simulation, then your Haskell-to-Hardware model must be broken too.

I consider it the same as

topEntity :: Int -> ()
topEntity = undefined

creating an error in simulation, while still describing and being generated to be perfectly valid HDL.

[DigitalBrains1]

However, if you are able to create some Index 0, causing an error in simulation, then your Haskell-to-Hardware model must be broken too.

Could you please elaborate what you mean? Are you saying the Clash user shouldn't have done that? That would not really be a strong argument to allow it. We want to minimise user surprises, and if that means imposing a few unnecessary 1 <= n so the user doesn't accidentally forget a fully load bearing 1 <= n in the type signature of their own function, then that could be the pragmatically correct solution. We don't want to hand people a foot gun and when it goes off say to them "but what you're doing is mathematically unsound, you should have studied mathematics more".

[kleinreact]

Could you please elaborate what you mean?

I say that it is impossible to create any wrong hardware this way, because the Clash model still protects you from breaking things after HDL generation. The only case, where you can observe a difference is in simulation, if returning an Index 0 as part of your top entity result and trying to read that result after simulating. In any other case, lazy evaluation protects you from the obvious, e.g. as the following won't cause any problems, neither in simulation nor in HDL:

topEntity :: HiddenClockResetEnable System => Signal System Bool -> Signal System Bool
topEntity = mealy (\i b -> (if b then i + 1 else i, b)) (undefined :: Index 0)

clashi> sampleN @System 3 $ topEntity $ fromList [True, False, True]
[True,False,True]

In other words, we only give the user a foot gun for the specific case, where he wants to read some Index 0 as a simulation result, which is perfectly fine to lead to an exception, because that means that the simulation test is already set up in a wrong way.

The current situation however, instead imposing that 1 <= n constraint, completely forbids the user to generate that nice and perfectly valid HDL, which is causing all the problems we see with these constraints in our projects regularly.

[DigitalBrains1]

Being forced to write bogus 1 <= n constraints is frutrating, but chasing XExceptions is also no fun at all. Being able to unpack into an Index 0 might make the following code suddenly error which would have been prevented by a 1 <= n constraint, which would cause the attempt to fail type checking instead, a much more manageable error than suddenly cropping up XExceptions.

shouldInit :: Index n -> Bool
shouldInit 0 = True
shouldInit _ = False

(The idea is you iterate over all elements of something and you need something to fire whenever you restarted the iteration).

The only case, where you can observe a difference is in simulation, if returning an Index 0 as part of your top entity result and trying to read that result after simulating.

That doesn't sound correct. For one, my function above returns a Bool yet it suddenly causes XExceptions if handed a counter produced by unpack. Furthermore, simulation is not limited to the top entity, so the top entity is not special in simulation. Finally, you can use traceSignal to look at inner signals.

[kleinreact]

Are we going to merge this now or not?

My patience already reached its limits, noting that this PR already is open for more than 1.5 years now. If you still wanna discuss your concerns, then please do so in week one or two after opening the PR and not 1.5 years later.

[DigitalBrains1]

The delay is absolutely not due to the reviewers, which you seem to imply. I'm sorry you're fed up with it, but I'm also sorry you seem to lay blame for that on people who were not the cause.

What has changed is that the review pointed out several issues with just removing 1 <= n in several cases. This has changed how Martijn is assessing the desirability of the change. I currently don't have a strong conviction, but today I tried to get clear why earlier you were absolutely adamant that functions should never return a void type, yet unpack doing exactly that is merely an unfortunate coincidence. I'm trying to reason about how surprising this can be to users who did not study mathematics, and whether merging the PR is actually a net benefit to users. Because that final point is my primary concern.

It definitely would be an enormous shame and enormous waste of work if this were not merged, I will grant you that. It'd suck big time. But if the PR is not an improvement for our users when all things are considered, that could still be the best outcome.

[christiaanb]

We have introduced XExceptions in the past #2563 in order to get rid of 1 <= n constraints. I don't see why we should not make the same decision this time, i.e. to err in favor of removing a 1 <= n constraint at the cost of introducing an XException.

[DigitalBrains1]

That PR seems to use clashCompileError, not XException. That's a major difference!

Should we perhaps make unpack @(Index 0) also return ErrorCall instead of XException? That would still be a lot more lenient than the other PR. The other PR merely turned a type-checking error into an error when generating HDL. It still errors, just at a later time.

[christiaanb]

The PR still introduced a run-time exception by dropping a 1 <= n constraint, so it’s not that much different. And the reason why that PR uses clashCompileError is because generating HDL for sum Nil would actually be bad, which is why we couldn’t get by with a simple errorX

[DigitalBrains1]

The PR still introduced a run-time exception by dropping a 1 <= n constraint, so it’s not that much different.

What we do in this PR creates the opportunity for users to write code that causes XExceptions they might not expect. Could you show me an instance of the other PR where we could generate HDL, but the Haskell simulation now gives extra XExceptions? Only then would I say they are not that much different.

Because the way I see it, the other PR only either

• creates opportunities to write correct, fully working code that could not be written before, or
• does not generate HDL, which means the Clash design is not a valid Clash design and really what it does in simulation is pretty irrelevant.

(Of course it's not fully irrelevant, because you might want to use the functions merely in simulation, outside your design itself. But it's a completely different story than this. I'm not saying we're wrong to merge this PR, I just think the other PR is no argument either in favour of or against this PR, it's just a different situation that has no bearing on this PR.)

[edit]
Nit pick: sum Nil = 0, you probably meant maximum from Foldable or something like that. But I understand what you meant.
[/edit]

[kleinreact]

The delay is absolutely not due to the reviewers, which you seem to imply.

There never was any intention that would imply such allegation.

I am just tiered of running into similar appearing discussions over and over again with individual opinions about the "dos and don'ts" swapping back and forth all the time. My question simply was about "What do you like to see as the outcome?", because if we don't even agree on the outcome, then it doesn't make any sense to further put effort into changing the code.

I opened this PR, because multiple users at QBayLogic reported to be restricted by the 1 <= n constraints for no real reason, which I also could confirm and see independently in the projects I worked on.

I first want confirmation now, whether maintainers agree with this update or not, where agreement also means for me to not raise any further arguments against the update, which is merely counter-productive.

Before agreeing on the outcome, I don't see why I should put any more effort into further touching this PR.

[christiaanb]

I agree @kleinreact i will merge this PR