clash-compiler
clash-compiler copied to clipboard
Published
20 hours ago •
clash-lang
clash-lang
Type-directed recursion fails to synthesize
In the following minimalized example, sumSucc is recursive over the type-level index ns (via a little indirection in the KnownNats typeclass). Even though the types completely drive the recursion, i.e. for any monomorpic type (like the Sum [Index 16] in my topEntity) it is fully unrollable, CLaSH (as of 28b678ec174758584015434dbfa5d699348488ae) still complains about it at synthesis time. Note that in the version below, I've even tried making the structure of sumSucc more explicit by writing go to pattern-match only on the type-driven singleton argument.
Full code with no external dependencies:
{-# LANGUAGE GADTs, DataKinds, TypeFamilyDependencies, EmptyCase #-}
module TopMain where
import Clash.Prelude
import Data.Proxy
import Data.Maybe (fromMaybe)
import Data.Kind (Type)
data Sum (ts :: [Type]) where
Here :: a -> Sum (a : ts)
There :: Sum ts -> Sum (a : ts)
data SNats :: [Nat] -> Type where
SNatsNil :: SNats '[]
SNatsCons :: (KnownNat n) => SNats ns -> SNats (n : ns)
class KnownNats (ns :: [Nat]) where
type Indices ns = (res :: [Type]) | res -> ns
knownNats :: SNats ns
instance KnownNats '[] where
type Indices '[] = '[]
knownNats = SNatsNil
instance (KnownNat n, KnownNats ns) => KnownNats (n : ns) where
type Indices (n : ns) = Index n : Indices ns
knownNats = SNatsCons knownNats
sumSucc :: (KnownNats ns) => Sum (Indices ns) -> Maybe (Sum (Indices ns))
sumSucc = go knownNats
where
go :: forall ks. SNats ks -> Sum (Indices ks) -> Maybe (Sum (Indices ks))
go SNatsNil = const Nothing
go (SNatsCons k) = \x -> case x of
Here x | x == maxBound -> There <$> next k
| otherwise -> Just $ Here $ succ x
There y -> There <$> go k y
next :: forall ks. SNats ks -> Maybe (Sum (Indices ks))
next (SNatsCons _) = Just $ Here 0
next SNatsNil = Nothing
{-# NOINLINE topEntity #-}
{-# ANN topEntity
(Synthesize
{ t_name = "MAIN"
, t_inputs =
[ PortName "CLK_25MHZ"
, PortName "RESET"
]
, t_output = PortName "COUNTER"
}) #-}
topEntity
:: Clock System Source
-> Reset System Asynchronous
-> Signal System (Index 16)
topEntity = exposeClockReset board
where
board = the <$> r
where
r = register (Here 0) $ fromMaybe (Here 0) . sumSucc <$> r
the :: Sum '[a] -> a
the (Here x) = x
Full error message from :verilog:
GHC: Parsing and optimising modules took: 0.45356967s
GHC: Loading external modules from interface files took: 0.154657024s
GHC: Parsing annotations took: 0.001118169s
GHC+Clash: Loading modules cumulatively took 0.787791599s
Clash: Parsing and compiling primitives took 1.593121757s
Clash: Compiling TopMain.topEntity
Clash.Normalize.Transformations(370): InlineNonRep: c$TopMain.topEntity_r7487489 already inlined 100 times in:TopMain.topEntity8214565720324357756
Type of the subject is: Clash.Signal.Internal.Signal
(Clash.Signal.Internal.Dom "system" 10000)
(TopMain.Sum
(GHC.Types.:
(GHC.Prim.TYPE GHC.Types.LiftedRep)
(Clash.Sized.Internal.Index.Index 16)
(GHC.Types.[]
(GHC.Prim.TYPE GHC.Types.LiftedRep))))
Function TopMain.topEntity8214565720324357756 will not reach a normal form, and compilation might fail.
Run with '-fclash-inline-limit=N' to increase the inlining limit to N.
Clash.Normalize.Transformations(370): InlineNonRep: c$TopMain.topEntity_r7487489 already inlined 100 times in:TopMain.topEntity8214565720324357756
Type of the subject is: Clash.Signal.Internal.Signal
(Clash.Signal.Internal.Dom "system" 10000)
(TopMain.Sum
(GHC.Types.:
(GHC.Prim.TYPE GHC.Types.LiftedRep)
(Clash.Sized.Internal.Index.Index 16)
(GHC.Types.[]
(GHC.Prim.TYPE GHC.Types.LiftedRep))))
Function TopMain.topEntity8214565720324357756 will not reach a normal form, and compilation might fail.
Run with '-fclash-inline-limit=N' to increase the inlining limit to N.
Clash.Normalize.Transformations(370): InlineNonRep: c$TopMain.topEntity_r7487489 already inlined 100 times in:TopMain.topEntity8214565720324357756
Type of the subject is: Clash.Signal.Internal.Signal
(Clash.Signal.Internal.Dom "system" 10000)
(TopMain.Sum
(GHC.Types.:
(GHC.Prim.TYPE GHC.Types.LiftedRep)
(Clash.Sized.Internal.Index.Index 16)
(GHC.Types.[]
(GHC.Prim.TYPE GHC.Types.LiftedRep))))
Function TopMain.topEntity8214565720324357756 will not reach a normal form, and compilation might fail.
Run with '-fclash-inline-limit=N' to increase the inlining limit to N.
*** Exception: Clash.Normalize(232): Callgraph after normalisation contains following recursive components: c$TopMain.topEntity_r7487489 :: Clash.Signal.Internal.Clock
(Clash.Signal.Internal.Dom "system" 10000)
Clash.Signal.Internal.Source
-> Clash.Signal.Internal.Reset
(Clash.Signal.Internal.Dom "system" 10000)
Clash.Signal.Internal.Asynchronous
-> Clash.Signal.Internal.Signal
(Clash.Signal.Internal.Dom "system" 10000)
(TopMain.Sum
(GHC.Types.:
(GHC.Prim.TYPE GHC.Types.LiftedRep)
(Clash.Sized.Internal.Index.Index 16)
(GHC.Types.[]
(GHC.Prim.TYPE
GHC.Types.LiftedRep))))λ(clk6989586621679607093 :: Clash.Signal.Internal.Clock
(Clash.Signal.Internal.Dom
"system"
10000)
Clash.Signal.Internal.Source) ->
λ(rst6989586621679607094 :: Clash.Signal.Internal.Reset
(Clash.Signal.Internal.Dom "system" 10000)
Clash.Signal.Internal.Asynchronous) ->
letrec
i8286623314362312377 :: Clash.Sized.Internal.Index.Index 16
= Clash.Sized.Internal.Index.fromInteger# @16
TopMain.$s$WSNatsCons18214565720324383378
0
in letrec
i18286623314362312348 :: TopMain.Sum
(GHC.Types.:
(GHC.Prim.TYPE GHC.Types.LiftedRep)
(Clash.Sized.Internal.Index.Index 16)
(GHC.Types.[]
(GHC.Prim.TYPE GHC.Types.LiftedRep)))
= TopMain.Here8214565720324357753
@(GHC.Types.:
(GHC.Prim.TYPE GHC.Types.LiftedRep)
(Clash.Sized.Internal.Index.Index 16)
(GHC.Types.[] (GHC.Prim.TYPE GHC.Types.LiftedRep)))
@(Clash.Sized.Internal.Index.Index 16)
@(GHC.Types.[] (GHC.Prim.TYPE GHC.Types.LiftedRep))
(_CO_
@(GHC.Prim.~#
(GHC.Types.[] (GHC.Prim.TYPE GHC.Types.LiftedRep))
(GHC.Types.[] (GHC.Prim.TYPE GHC.Types.LiftedRep))
(GHC.Types.:
(GHC.Prim.TYPE GHC.Types.LiftedRep)
(Clash.Sized.Internal.Index.Index 16)
(GHC.Types.[] (GHC.Prim.TYPE GHC.Types.LiftedRep)))
(GHC.Types.:
(GHC.Prim.TYPE GHC.Types.LiftedRep)
(Clash.Sized.Internal.Index.Index 16)
(GHC.Types.[] (GHC.Prim.TYPE GHC.Types.LiftedRep)))))
i8286623314362312377
in Clash.Signal.Internal.register# @(Clash.Signal.Internal.Dom "system" 10000)
@Clash.Signal.Internal.Source
@Clash.Signal.Internal.Asynchronous
@(TopMain.Sum
(GHC.Types.:
(GHC.Prim.TYPE GHC.Types.LiftedRep)
(Clash.Sized.Internal.Index.Index 16)
(GHC.Types.[] (GHC.Prim.TYPE GHC.Types.LiftedRep))))
clk6989586621679607093
rst6989586621679607094
i18286623314362312348
i18286623314362312348
(case (TopMain.sumSucc_$ssumSucc8214565720324383439
(c$TopMain.topEntity_r7487489
clk6989586621679607093
rst6989586621679607094)) of
GHC.Maybe.Nothing3891110078048108568 ->
i18286623314362312348
GHC.Maybe.Just3891110078048108571 (v6989586621679607126 :: TopMain.Sum
(GHC.Types.:
(GHC.Prim.TYPE
GHC.Types.LiftedRep)
(Clash.Sized.Internal.Index.Index
16)
(GHC.Types.[]
(GHC.Prim.TYPE
GHC.Types.LiftedRep)))) ->
v6989586621679607126)
CallStack (from HasCallStack):
error, called at src/Clash/Normalize.hs:232:10 in clash-lib-0.99-LRkIBt00M5U644zIKIZ4Z0:Clash.Normalize
As an experiment, I have hand-specialized sumSucc so that it is not recursive anymore, but it still fails to synthesize:
{-# LANGUAGE GADTs, DataKinds, TypeFamilyDependencies, EmptyCase #-}
module TopMain where
import Clash.Prelude
import Data.Proxy
import Data.Maybe (fromMaybe)
import Data.Kind (Type)
data Sum (ts :: [Type]) where
Here :: a -> Sum (a : ts)
There :: Sum ts -> Sum (a : ts)
data SNats :: [Nat] -> Type where
SNatsNil :: SNats '[]
SNatsCons :: (KnownNat n) => SNats ns -> SNats (n : ns)
knownNats0 :: SNats '[]
knownNats0 = SNatsNil
knownNats1 :: SNats '[16]
knownNats1 = SNatsCons knownNats0
sumSucc1 :: Sum '[Index 16] -> Maybe (Sum '[Index 16])
sumSucc1 = go1 knownNats1
where
go1 :: SNats '[16] -> Sum '[Index 16] -> Maybe (Sum '[Index 16])
go1 (SNatsCons k) = \x -> case x of
Here x | x == maxBound -> There <$> next0 k
| otherwise -> Just $ Here $ succ x
There y -> There <$> go0 k y
go0 :: SNats '[] -> Sum '[] -> Maybe (Sum '[])
go0 SNatsNil = const Nothing
next0 :: SNats '[] -> Maybe (Sum '[])
next0 SNatsNil = Nothing
{-# NOINLINE topEntity #-}
{-# ANN topEntity
(Synthesize
{ t_name = "MAIN"
, t_inputs =
[ PortName "CLK_25MHZ"
, PortName "RESET"
]
, t_output = PortName "COUNTER"
}) #-}
topEntity
:: Clock System Source
-> Reset System Asynchronous
-> Signal System (Index 16)
topEntity = exposeClockReset board
where
board = the <$> r
where
r = register (Here 0) $ fromMaybe (Here 0) . sumSucc1 <$> r
the :: Sum '[a] -> a
the (Here x) = x
This still fails with
Clash.Normalize.Transformations(370): InlineNonRep: c$TopMain.topEntity_r2276353 already inlined 20 times in:TopMain.topEntity8214565720327684458
Type of the subject is: Clash.Signal.Internal.Signal
(Clash.Signal.Internal.Dom "system" 10000)
(TopMain.Sum
(GHC.Types.:
(GHC.Prim.TYPE GHC.Types.LiftedRep)
(Clash.Sized.Internal.Index.Index 16)
(GHC.Types.[]
(GHC.Prim.TYPE GHC.Types.LiftedRep))))
Function TopMain.topEntity8214565720327684458 will not reach a normal form, and compilation might fail.
Run with '-fclash-inline-limit=N' to increase the inlining limit to N.
Clash.Normalize.Transformations(370): InlineNonRep: c$TopMain.topEntity_r2276353 already inlined 20 times in:TopMain.topEntity8214565720327684458
Type of the subject is: Clash.Signal.Internal.Signal
(Clash.Signal.Internal.Dom "system" 10000)
(TopMain.Sum
(GHC.Types.:
(GHC.Prim.TYPE GHC.Types.LiftedRep)
(Clash.Sized.Internal.Index.Index 16)
(GHC.Types.[]
(GHC.Prim.TYPE GHC.Types.LiftedRep))))
Function TopMain.topEntity8214565720327684458 will not reach a normal form, and compilation might fail.
Run with '-fclash-inline-limit=N' to increase the inlining limit to N.
*** Exception: Clash.Normalize(232): Callgraph after normalisation contains following recursive components: c$TopMain.topEntity_r2276353 :: Clash.Signal.Internal.Clock
(Clash.Signal.Internal.Dom "system" 10000)
Clash.Signal.Internal.Source
-> Clash.Signal.Internal.Reset
(Clash.Signal.Internal.Dom "system" 10000)
Clash.Signal.Internal.Asynchronous
-> Clash.Signal.Internal.Signal
(Clash.Signal.Internal.Dom "system" 10000)
(TopMain.Sum
(GHC.Types.:
(GHC.Prim.TYPE GHC.Types.LiftedRep)
(Clash.Sized.Internal.Index.Index 16)
(GHC.Types.[]
(GHC.Prim.TYPE
GHC.Types.LiftedRep))))λ(clk6989586621682922489 :: Clash.Signal.Internal.Clock
(Clash.Signal.Internal.Dom
"system"
10000)
Clash.Signal.Internal.Source) ->
λ(rst6989586621682922490 :: Clash.Signal.Internal.Reset
(Clash.Signal.Internal.Dom "system" 10000)
Clash.Signal.Internal.Asynchronous) ->
letrec
i8286623314365627340 :: Clash.Sized.Internal.Index.Index 16
= Clash.Sized.Internal.Index.fromInteger# @16
TopMain.$s$WSNatsCons18214565720327698680
0
in letrec
i18286623314365627327 :: TopMain.Sum
(GHC.Types.:
(GHC.Prim.TYPE GHC.Types.LiftedRep)
(Clash.Sized.Internal.Index.Index 16)
(GHC.Types.[]
(GHC.Prim.TYPE GHC.Types.LiftedRep)))
= TopMain.Here8214565720327684453
@(GHC.Types.:
(GHC.Prim.TYPE GHC.Types.LiftedRep)
(Clash.Sized.Internal.Index.Index 16)
(GHC.Types.[] (GHC.Prim.TYPE GHC.Types.LiftedRep)))
@(Clash.Sized.Internal.Index.Index 16)
@(GHC.Types.[] (GHC.Prim.TYPE GHC.Types.LiftedRep))
(_CO_
@(GHC.Prim.~#
(GHC.Types.[] (GHC.Prim.TYPE GHC.Types.LiftedRep))
(GHC.Types.[] (GHC.Prim.TYPE GHC.Types.LiftedRep))
(GHC.Types.:
(GHC.Prim.TYPE GHC.Types.LiftedRep)
(Clash.Sized.Internal.Index.Index 16)
(GHC.Types.[] (GHC.Prim.TYPE GHC.Types.LiftedRep)))
(GHC.Types.:
(GHC.Prim.TYPE GHC.Types.LiftedRep)
(Clash.Sized.Internal.Index.Index 16)
(GHC.Types.[] (GHC.Prim.TYPE GHC.Types.LiftedRep)))))
i8286623314365627340
in Clash.Signal.Internal.register# @(Clash.Signal.Internal.Dom "system" 10000)
@Clash.Signal.Internal.Source
@Clash.Signal.Internal.Asynchronous
@(TopMain.Sum
(GHC.Types.:
(GHC.Prim.TYPE GHC.Types.LiftedRep)
(Clash.Sized.Internal.Index.Index 16)
(GHC.Types.[] (GHC.Prim.TYPE GHC.Types.LiftedRep))))
clk6989586621682922489
rst6989586621682922490
i18286623314365627327
i18286623314365627327
(case (TopMain.sumSucc18214565720327684457
(c$TopMain.topEntity_r2276353
clk6989586621682922489
rst6989586621682922490)) of
GHC.Maybe.Nothing3891110078048108568 ->
i18286623314365627327
GHC.Maybe.Just3891110078048108571 (v6989586621682922520 :: TopMain.Sum
(GHC.Types.:
(GHC.Prim.TYPE
GHC.Types.LiftedRep)
(Clash.Sized.Internal.Index.Index
16)
(GHC.Types.[]
(GHC.Prim.TYPE
GHC.Types.LiftedRep)))) ->
v6989586621682922520)
CallStack (from HasCallStack):
error, called at src/Clash/Normalize.hs:232:10 in clash-lib-0.99-LRkIBt00M5U644zIKIZ4Z0:Clash.Normalize
Even the following fails:
{-# LANGUAGE GADTs, DataKinds #-}
module TopMain where
import Clash.Prelude
import Data.Proxy
import Data.Maybe (fromMaybe)
import Data.Kind (Type)
data Sum (ts :: [Type]) where
Here :: a -> Sum (a : ts)
There :: Sum ts -> Sum (a : ts)
sumSucc1 :: Sum '[Index 16] -> Maybe (Sum '[Index 16])
sumSucc1 = \x -> case x of
Here x | x == maxBound -> Nothing
| otherwise -> Just $ Here $ succ x
There y -> Nothing
{-# NOINLINE topEntity #-}
{-# ANN topEntity
(Synthesize
{ t_name = "MAIN"
, t_inputs =
[ PortName "CLK_25MHZ"
, PortName "RESET"
]
, t_output = PortName "COUNTER"
}) #-}
topEntity
:: Clock System Source
-> Reset System Asynchronous
-> Signal System (Index 16)
topEntity = exposeClockReset board
where
board = the <$> r
where
r = register (Here 0) $ fromMaybe (Here 0) . sumSucc1 <$> r
the :: Sum '[a] -> a
the (Here x) = x
with
Function TopMain.topEntity8214565720324329883 will not reach a normal form, and compilation might fail.
Run with '-fclash-inline-limit=N' to increase the inlining limit to N.
*** Exception: Clash.Normalize(232): Callgraph after normalisation contains following recursive components: c$TopMain.topEntity_r310273 :: Clash.Signal.Internal.Clock
(Clash.Signal.Internal.Dom "system" 10000)
Clash.Signal.Internal.Source
-> Clash.Signal.Internal.Reset
(Clash.Signal.Internal.Dom "system" 10000)
Clash.Signal.Internal.Asynchronous
-> Clash.Signal.Internal.Signal
(Clash.Signal.Internal.Dom "system" 10000)
(TopMain.Sum
(GHC.Types.:
(GHC.Prim.TYPE GHC.Types.LiftedRep)
(Clash.Sized.Internal.Index.Index 16)
(GHC.Types.[]
(GHC.Prim.TYPE
GHC.Types.LiftedRep))))λ(clk6989586621679567657 :: Clash.Signal.Internal.Clock
(Clash.Signal.Internal.Dom
"system"
10000)
Clash.Signal.Internal.Source) ->
λ(rst6989586621679567658 :: Clash.Signal.Internal.Reset
(Clash.Signal.Internal.Dom "system" 10000)
Clash.Signal.Internal.Asynchronous) ->
letrec
i8286623314362272245 :: Clash.Sized.Internal.Index.Index 16
= Clash.Sized.Internal.Index.fromInteger# @16
TopMain.sumSucc28214565720324343829
0
in letrec
i18286623314362272233 :: TopMain.Sum
(GHC.Types.:
(GHC.Prim.TYPE GHC.Types.LiftedRep)
(Clash.Sized.Internal.Index.Index 16)
(GHC.Types.[]
(GHC.Prim.TYPE GHC.Types.LiftedRep)))
= TopMain.Here8214565720324329880
@(GHC.Types.:
(GHC.Prim.TYPE GHC.Types.LiftedRep)
(Clash.Sized.Internal.Index.Index 16)
(GHC.Types.[] (GHC.Prim.TYPE GHC.Types.LiftedRep)))
@(Clash.Sized.Internal.Index.Index 16)
@(GHC.Types.[] (GHC.Prim.TYPE GHC.Types.LiftedRep))
(_CO_
@(GHC.Prim.~#
(GHC.Types.[] (GHC.Prim.TYPE GHC.Types.LiftedRep))
(GHC.Types.[] (GHC.Prim.TYPE GHC.Types.LiftedRep))
(GHC.Types.:
(GHC.Prim.TYPE GHC.Types.LiftedRep)
(Clash.Sized.Internal.Index.Index 16)
(GHC.Types.[] (GHC.Prim.TYPE GHC.Types.LiftedRep)))
(GHC.Types.:
(GHC.Prim.TYPE GHC.Types.LiftedRep)
(Clash.Sized.Internal.Index.Index 16)
(GHC.Types.[] (GHC.Prim.TYPE GHC.Types.LiftedRep)))))
i8286623314362272245
in Clash.Signal.Internal.register# @(Clash.Signal.Internal.Dom "system" 10000)
@Clash.Signal.Internal.Source
@Clash.Signal.Internal.Asynchronous
@(TopMain.Sum
(GHC.Types.:
(GHC.Prim.TYPE GHC.Types.LiftedRep)
(Clash.Sized.Internal.Index.Index 16)
(GHC.Types.[] (GHC.Prim.TYPE GHC.Types.LiftedRep))))
clk6989586621679567657
rst6989586621679567658
i18286623314362272233
i18286623314362272233
(case (TopMain.sumSucc18214565720324329882
(c$TopMain.topEntity_r310273
clk6989586621679567657
rst6989586621679567658)) of
GHC.Maybe.Nothing3891110078048108568 ->
i18286623314362272233
GHC.Maybe.Just3891110078048108571 (v6989586621679567692 :: TopMain.Sum
(GHC.Types.:
(GHC.Prim.TYPE
GHC.Types.LiftedRep)
(Clash.Sized.Internal.Index.Index
16)
(GHC.Types.[]
(GHC.Prim.TYPE
GHC.Types.LiftedRep)))) ->
v6989586621679567692)
CallStack (from HasCallStack):
error, called at src/Clash/Normalize.hs:232:10 in clash-lib-0.99-LRkIBt00M5U644zIKIZ4Z0:Clash.Normalize
but there are no recursive definitions anymore in my simplified code...
The Core generated from the simplified sumSucc1 above:
TopMain.sumSucc2 :: GHC.Natural.Natural
[GblId,
Caf=NoCafRefs,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 100 0}]
TopMain.sumSucc2 = 16
sumSucc1 :: Sum '[Index 16] -> Maybe (Sum '[Index 16])
[GblId,
Arity=1,
Str=<S,1*U>,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True, Guidance=IF_ARGS [30] 180 40}]
sumSucc1
= \ (x_awyS :: Sum '[Index 16]) ->
case x_awyS of {
Here @ a_ay4E @ ts_ay4F co_ay4G x1_awyT ->
case Clash.Sized.Internal.Index.eq#
@ 16
(x1_awyT `cast` (Sub (Nth:1 (Sym co_ay4G)) :: a_ay4E ~R# Index 16))
(Clash.Sized.Internal.Index.maxBound#
@ 16
(TopMain.sumSucc2
`cast` (Sym (GHC.TypeNats.N:SNat[0]
<16>_P) ; Sym (GHC.TypeNats.N:KnownNat[0]) <16>_N
:: GHC.Natural.Natural ~R# KnownNat 16)))
of {
False ->
(GHC.Maybe.Just
@ (Sum '[a_ay4E])
(TopMain.Here
@ '[a_ay4E]
@ a_ay4E
@ '[]
@~ (<'[a_ay4E]>_N :: '[a_ay4E] GHC.Prim.~# '[a_ay4E])
((Clash.Sized.Internal.Index.+#
@ 16
(TopMain.sumSucc2
`cast` (Sym (GHC.TypeNats.N:SNat[0]
<16>_P) ; Sym (GHC.TypeNats.N:KnownNat[0]) <16>_N
:: GHC.Natural.Natural ~R# KnownNat 16))
(x1_awyT `cast` (Sub (Nth:1 (Sym co_ay4G)) :: a_ay4E ~R# Index 16))
(Clash.Sized.Internal.Index.fromInteger#
@ 16
(TopMain.sumSucc2
`cast` (Sym (GHC.TypeNats.N:SNat[0]
<16>_P) ; Sym (GHC.TypeNats.N:KnownNat[0]) <16>_N
:: GHC.Natural.Natural ~R# KnownNat 16))
Clash.Sized.Internal.Index.$fArbitraryIndex1))
`cast` (Sub (Nth:1 co_ay4G) :: Index 16 ~R# a_ay4E))))
`cast` ((Maybe
(Sum ((':) <Type>_N (Nth:1 (Sym co_ay4G)) <'[]>_N)_N)_R)_R
:: Maybe (Sum '[a_ay4E]) ~R# Maybe (Sum '[Index 16]));
True -> GHC.Maybe.Nothing @ (Sum '[Index 16])
};
There @ ts_ay5n @ a_ay5o co_ay5p [Dmd=<L,A>] y_axJQ ->
GHC.Maybe.Nothing @ (Sum '[Index 16])
}
Also, for topEntity:
topEntity [InlPrag=NOINLINE]
:: Clock System 'Source
-> Reset System 'Asynchronous -> Signal System (Index 16)
[GblId,
Arity=2,
Str=<L,U><L,U>,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True, Guidance=IF_ARGS [0 0] 340 0}]
topEntity
= \ (clk_a2l90 :: Clock System 'Source)
(rst_a2l91 :: Reset System 'Asynchronous) ->
Clash.Signal.Internal.mapSignal#
@ (Sum '[Index 16])
@ (Index 16)
@ System
(the @ (Index 16))
(letrec {
r_s2lBu [Occ=LoopBreaker] :: Signal System (Sum '[Index 16])
[LclId]
r_s2lBu
= let {
i_s2lBL :: Index 16
[LclId]
i_s2lBL
= Clash.Sized.Internal.Index.fromInteger#
@ 16
(TopMain.sumSucc2
`cast` (Sym (GHC.TypeNats.N:SNat[0]
<16>_P) ; Sym (GHC.TypeNats.N:KnownNat[0]) <16>_N
:: GHC.Natural.Natural ~R# KnownNat 16))
0 } in
let {
i1_s2lBy :: Sum '[Index 16]
[LclId, Unf=OtherCon []]
i1_s2lBy
= TopMain.Here
@ '[Index 16]
@ (Index 16)
@ '[]
@~ (<'[Index 16]>_N :: '[Index 16] GHC.Prim.~# '[Index 16])
i_s2lBL } in
Clash.Signal.Internal.register#
@ System
@ 'Source
@ 'Asynchronous
@ (Sum '[Index 16])
clk_a2l90
rst_a2l91
i1_s2lBy
i1_s2lBy
(Clash.Signal.Internal.mapSignal#
@ (Sum '[Index 16])
@ (Sum '[Index 16])
@ System
(\ (x_a2l9r :: Sum '[Index 16]) ->
case sumSucc1 x_a2l9r of {
Nothing -> i1_s2lBy;
Just v_a2l9z -> v_a2l9z
})
r_s2lBu); } in
r_s2lBu)
At @expipiplus1's suggestion, I have also tried getting rid of the inductive family Sum by replacing it with just its two member types that are relevant here:
data Sum1 t where
Here1 :: t -> Sum1 t
There1 :: Sum0 -> Sum1 t
data Sum0 where
sumSucc1 :: Sum1 (Index 16) -> Maybe (Sum1 (Index 16))
sumSucc1 = \x -> case x of
Here1 x | x == maxBound -> Nothing
| otherwise -> Just $ Here $ succ x
There1 y -> Nothing
While this version now succeeds in synthesizing Verilog, this gives me no way backward into my original code with the inductively defined Sum family. Also, it is unclear to me what the difference between Sum1 a and Sum '[a] is.
Currently, Clash bails early if it sees a type is recursively defined: https://github.com/clash-lang/clash-compiler/blob/28b678ec174758584015434dbfa5d699348488ae/clash-lib/src/Clash/Netlist/Util.hs#L374-L376
Which means you cannot store recursive types in registers/memory, nor can you have them as inputs/outputs of topEntity (or anything with a Synthesize ANNotation). The exceptions to this rule are Vec and RTree, because they're hard-coded into the compiler: https://github.com/clash-lang/clash-compiler/blob/9b2bb9b300d0ecaace9114fabbfef1ffdd1cfc23/clash-ghc/src-ghc/Clash/GHC/NetlistTypes.hs#L169-L206
Deriving bit-encodings for bounded recursive types is on the TODO list.
Perhaps for now you could do something like:
type family Sum (ts :: [Type]) where
Sum '[] = ()
Sum (t:ts) = Either t (Sum ts)
hereC :: a -> Sum (a:ts)
hereC = Left
hereV :: Sum (a:ts) -> Maybe a
hereV (Left x) = Just x
hereV _ = Nothing
thereC :: Sum ts -> Sum (a:ts)
thereC = Right
thereV :: Sum (a:ts) -> Maybe (Sum ts)
thereV (Right xs) = Just xs
thereV _ = Nothing
and use -XPatternSynonyms to recover some of the pattern matching for Here and There; although that might not be powerful enought for your needs, as pattern synonyms don't introduce coercions to the RHS of the pattern match like GADTs do.