Movatterモバイル変換

[0]ホーム
URL:

Skip to content

Navigation Menu

Sign in
Appearance settings

Search code, repositories, users, issues, pull requests...

Provide feedback

We read every piece of feedback, and take your input very seriously.

Saved searches

Use saved searches to filter your results more quickly

 Sign up
Appearance settings

AddBitPack instance forIndex 0#2784

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to ourterms of service andprivacy statement. We’ll occasionally send you account related emails.

Already on GitHub?Sign in to your account

Draft
kleinreact wants to merge1 commit intomaster
base:master
Choose a base branch
Loading
fromadd-bitpack-for-index-zero

Conversation

kleinreact
Copy link
Member

@kleinreactkleinreact commentedAug 7, 2024•
edited
Loading

This PR gets rid of the additional1 <= n constraint for theBitPack instance ofIndex n.

Background:

  • Index 0 andVoid 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 forIndex 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:

Copy link
Member

@martijnbastiaanmartijnbastiaan left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others.Learn more.

Review together with@DigitalBrains1

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

Addthis 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 onIndex 0 withBitPack (Index 0)".

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

Other than that LGTUs.

@DigitalBrains1
Copy link
Member

DigitalBrains1 commentedAug 8, 2024•
edited
Loading

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
Copy link
MemberAuthor

It's because of the newBitSizeIndex 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
Copy link
Member

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

But lets say someone is (accidentally) callingunpack @(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
Copy link
MemberAuthor

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::HiddenClockResetEnableSystem=>SignalSystem (Index0)topEntity=pure$ unpack@(Index0)$ resize (0::BitVector1)

If that description is turned into Verilog withclash, 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 applyingunpack @(Index 0), but that is fine, as there is no outputunpack @(Index 0) can ever produce. Thus, the error is not thatunpack @(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 ofundefined.

@kleinreactkleinreactforce-pushed theadd-bitpack-for-index-zero branch from2714056 to0103c88CompareOctober 4, 2024 15:50
Sign up for freeto join this conversation on GitHub. Already have an account?Sign in to comment
Reviewers

@martijnbastiaanmartijnbastiaanmartijnbastiaan requested changes

@rowanG077rowanG077rowanG077 left review comments

Requested changes must be addressed to merge this pull request.

Assignees
No one assigned
Labels
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

5 participants
@kleinreact@DigitalBrains1@leonschoorl@martijnbastiaan@rowanG077
[8]ページ先頭
©2009-2025 Movatter.jp