Internal error: unknown normalized binder

[gergoerdi]

Clash fails on the following self-contained source file:

{-# LANGUAGE BlockArguments, TupleSections, LambdaCase, GADTs, RequiredTypeArguments #-}
module Sudoku where

import Clash.Prelude hiding (print, Const)
import Clash.Annotations.TH
import Clash.Class.Counter
import Protocols
import qualified Protocols.Df as Df
import Data.Word
import Data.Maybe

data a :- b
    = Const b
    | Varying (a -> b)
    deriving (Functor)
infixr 0 :-

type Transition s i o = i :- (s, o, Bool)

type FormatTransition s i o = s -> Transition (Maybe s) i (Maybe o)

mapState :: (s -> s') -> Transition s i o -> Transition s' i o
mapState f = fmap \(s, y, consume) -> (f s, y, consume)

countSuccChecked :: (Counter a) => a -> Maybe a
countSuccChecked = countSucc . Just

data Formatter s where
    SingleStep :: (Word8 :- (Maybe Word8, Bool)) -> Formatter ()
    Loop :: Formatter s -> Formatter s
    Rep :: (1 <= n) => SNat n -> Formatter s -> Formatter (s, Index n)

start :: Formatter s -> s
start = \case
    SingleStep{} -> ()
    Loop fmt -> start fmt
    Rep SNat fmt -> (start fmt, 0)

transition :: Formatter s -> FormatTransition s Word8 Word8
transition = \case
    SingleStep f -> \_ ->
        fmap (\(y, c) -> (Nothing, y, c)) f
    Loop fmt ->
        mapState (Just . fromMaybe (start fmt)) . transition fmt
    Rep SNat fmt -> \(s, i) ->
        let continue s' = Just (s', i)
            repeat = (start fmt,) <$> countSuccChecked i
        in mapState (maybe repeat continue) $ transition fmt s

print :: Formatter ()
print = SingleStep $ Varying \x -> (Just x, True)

infix 7 *:

(*:) :: forall n -> (KnownNat n, 1 <= n) => Formatter a -> Formatter (a, Index n)
n *: fmt = Rep (SNat @n) fmt

{-# INLINE format #-}
format :: (HiddenClockResetEnable dom, NFDataX s) => Formatter s -> Circuit (Df dom Word8) (Df dom Word8)
format fmt = Df.compander (Just $ start fmt, True) \(s, ready) x -> case step s of
    Const (s', y, consume) -> ((s', ready && not consume), y, False)
    Varying f
        | ready, (s', y, consume) <- f x -> ((s', not consume), y, False)
        | otherwise -> ((s, True), Nothing, True)
  where
    step = \case
        Nothing -> Varying \_ -> (Nothing, Nothing, True)
        Just s -> transition fmt s

board :: (HiddenClockResetEnable dom) => Circuit (Df dom Word8) (Df dom Word8)
board = format (Loop $ 3 *: print)

topEntity
    :: "CLK_100MHZ" ::: Clock System
    -> "RESET"      ::: Reset System
    -> ( "IN_DATA"    ::: Signal System (Df.Data Word8)
       , "OUT_ACK"    ::: Signal System Ack
       )
    -> ( "IN_ACK"   ::: Signal System Ack
       , "OUT_DATA" ::: Signal System (Df.Data Word8)
       )
topEntity clk rst = withClockResetEnable clk rst enableGen $
    toSignals board

makeTopEntity 'topEntity

with the following error message:

    Clash error call:
    Internal error: unknown normalized binder:
    
      Sudoku.start[3996] :: GHC.Tuple.Unit[3746994889972252672]
    CallStack (from HasCallStack):
      error, called at src/Clash/Netlist.hs:716:20 in clash-lib-1.9.0-0ad9e06dffc4266f94889468bcd322ac15e502a35080fee76189434bc4c3b152:Clash.Netlist
      mkFunApp, called at src/Clash/Netlist.hs:417:20 in clash-lib-1.9.0-0ad9e06dffc4266f94889468bcd322ac15e502a35080fee76189434bc4c3b152:Clash.Netlist
      mkDeclarations', called at src/Clash/Netlist.hs:403:18 in clash-lib-1.9.0-0ad9e06dffc4266f94889468bcd322ac15e502a35080fee76189434bc4c3b152:Clash.Netlist
      mkDeclarations, called at src/Clash/Netlist.hs:278:40 in clash-lib-1.9.0-0ad9e06dffc4266f94889468bcd322ac15e502a35080fee76189434bc4c3b152:Clash.Netlist
      genComponentT, called at src/Clash/Netlist.hs:241:41 in clash-lib-1.9.0-0ad9e06dffc4266f94889468bcd322ac15e502a35080fee76189434bc4c3b152:Clash.Netlist
      genComponent, called at src/Clash/Netlist.hs:119:9 in clash-lib-1.9.0-0ad9e06dffc4266f94889468bcd322ac15e502a35080fee76189434bc4c3b152:Clash.Netlist

[gergoerdi]

This alternative formulation seems to work, with the s hidden behind an existential:

{-# LANGUAGE BlockArguments, TupleSections, LambdaCase, GADTs, RequiredTypeArguments #-}
{-# LANGUAGE DeriveFunctor #-}
module Sudoku where

import Clash.Prelude hiding (print, Const)
import Clash.Annotations.TH
import Clash.Class.Counter
import Protocols
import qualified Protocols.Df as Df
import Data.Word
import Data.Maybe

data a :- b
    = Const b
    | Varying (a -> b)
    deriving (Functor)
infixr 0 :-

type Transition s i o = i :- (s, o, Bool)

type FormatTransition s i o = s -> Transition (Maybe s) i (Maybe o)

mapState :: (s -> s') -> Transition s i o -> Transition s' i o
mapState f = fmap \(s, y, consume) -> (f s, y, consume)

countSuccChecked :: (Counter a) => a -> Maybe a
countSuccChecked = countSucc . Just

data Formatter where
    MkFormatter :: (NFDataX s) => s -> FormatTransition s Word8 Word8 -> Formatter

print :: Formatter
print = MkFormatter () $ \() -> Varying \x -> (Nothing, Just x, True)

loop :: Formatter -> Formatter
loop (MkFormatter start transition) = MkFormatter start $ mapState (Just . fromMaybe start) . transition

(*:) :: forall n -> (KnownNat n, 1 <= n) => Formatter -> Formatter
n *: MkFormatter start transition = MkFormatter (start, (0 :: Index n)) \(s, i) ->
    let continue s' = Just (s', i)
        repeat = (start,) <$> countSuccChecked i
    in mapState (maybe repeat continue) $ transition s

infix 7 *:

format :: (HiddenClockResetEnable dom) => Formatter -> Circuit (Df dom Word8) (Df dom Word8)
format (MkFormatter start transition) = Df.compander (Just start, True) \(s, ready) x -> case step s of
    Const (s', y, consume) -> ((s', ready && not consume), y, False)
    Varying f
      | ready, (s', y, consume) <- f x -> ((s', not consume), y, False)
      | otherwise -> ((s, True), Nothing, True)
  where
    step = \case
        Nothing -> Varying \_ -> (Nothing, Nothing, True)
        Just s -> transition s

board :: (HiddenClockResetEnable dom) => Circuit (Df dom Word8) (Df dom Word8)
board = format (loop $ 3 *: print)

topEntity
    :: "CLK_100MHZ" ::: Clock System
    -> "RESET"      ::: Reset System
    -> ( "IN_DATA"    ::: Signal System (Df.Data Word8)
       , "OUT_ACK"    ::: Signal System Ack
       )
    -> ( "IN_ACK"   ::: Signal System Ack
       , "OUT_DATA" ::: Signal System (Df.Data Word8)
       )
topEntity clk rst = withClockResetEnable clk rst enableGen $
    toSignals board

makeTopEntity 'topEntity