Skip to content
This repository was archived by the owner on Sep 7, 2018. It is now read-only.

unsafeSNat doesn't synthesise #141

Open
cchalmers opened this issue Mar 9, 2018 · 1 comment
Open

unsafeSNat doesn't synthesise #141

cchalmers opened this issue Mar 9, 2018 · 1 comment
Labels

Comments

@cchalmers
Copy link

import Clash.Prelude
import Clash.Promoted.Nat.Unsafe

topEntity :: SystemClockReset => Signal System Bool
topEntity = metronome 4

metronome :: SystemClockReset => Integer -> Signal System Bool
metronome i =
  case unsafeSNat i of
    n@SNat -> (==0) <$> counter n

counter :: SystemClockReset => SNat i -> Signal System (Index i)
counter SNat = go where
  go = register 0 $ fmap (\i -> if i == maxBound then 0 else i+1) go

errors with

<no location info>: error:
    Clash error call:
    Clash.Netlist.BlackBox(116): Forced to evaluate untranslatable type: (Clash.Sized.Internal.Index.fromInteger#
  @(GHC.Types.Any GHC.Types.Nat)
  \$dKnownNat\
  0 :: Clash.Sized.Internal.Index.Index (GHC.Types.Any GHC.Types.Nat))
@christiaanb
Copy link
Member

I think we'll have to wait for -XDependentTypes in GHC in order to support this.

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
Projects
None yet
Development

No branches or pull requests

2 participants