search

clash-lang / clash-compiler

Haskell to VHDL/Verilog/SystemVerilog compiler
https://clash-lang.org/
Other
1.43k stars 151 forks source link

Type-directed recursion fails to synthesize #578

Open gergoerdi opened 5 years ago

gergoerdi commented 5 years ago

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
gergoerdi commented 5 years ago

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
gergoerdi commented 5 years ago

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

gergoerdi commented 5 years ago

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])
      }
gergoerdi commented 5 years ago

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)
gergoerdi commented 5 years ago

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.

christiaanb commented 5 years ago

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.

christiaanb commented 5 years ago

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.