dtypefold.hs

```haskell
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StarIsType #-}

import Clash.Prelude

-- import Data.Singletons.Prelude
import Data.Singletons (TyFun, Apply)
import Data.Proxy
import Data.Kind

-- Helper function to remove one bit
truncate1 :: KnownNat x => Unsigned (x+1) -> Unsigned x
truncate1 input = truncateB input

data TypeGen (x :: Nat) (n :: Nat) (f :: TyFun Nat *) :: *
type instance Apply (TypeGen x n) l =
    Unsigned (x-l)

stage :: KnownNat x
      => 1 <= x
      => ()
      -> Unsigned x
      -> Unsigned (x-1)
stage _ input =
    truncate1 input



pl :: forall x n
    . KnownNat x
   => KnownNat n
   => 1 <= x
   => (1+n) <= x
   => Unsigned x
   -> Unsigned (x-n)
pl input =
    dfold
        (Proxy :: Proxy (TypeGen x d))
        go
        input
        (repeat ())
    where
        go :: forall l x. SystemClockResetEnable
           => KnownNat x
           => 1 <= x
           -- I think this is needed because (x-(l+1)) can not be negative
           => (1+l) <= x
           -- Number of previous folds
           => SNat l
           -- Input to each element in the circuit
           -> ()
           -- Input from previous element
           -> Unsigned (x-l)
           -- Output from this element
           -> Unsigned (x-(l+1))
        go (l@SNat) allInputs prevStage =
            stage allInputs prevStage
```

simple_dtypefold.hs:41:9: error:
    * Could not deduce: ((1 + l) <=? x) ~ 'True
        arising from a use of `go'
      from the context: (KnownNat x, KnownNat n, 1 <= x, (1 + n) <= x)
        bound by the type signature for:
                   pl :: forall (x :: Nat) (n :: Nat).
                         (KnownNat x, KnownNat n, 1 <= x, (1 + n) <= x) =>
                         Unsigned x -> Unsigned (x - n)
        at simple_dtypefold.hs:(31,1)-(37,20)
    * In the second argument of `dfold', namely `go'
      In the expression:
        dfold (Proxy :: Proxy (TypeGen x d)) go input (repeat ())
      In an equation for `pl':
          pl input
            = dfold (Proxy :: Proxy (TypeGen x d)) go input (repeat ())
            where
                go ::
                  forall l x.
                  SystemClockResetEnable =>
                  KnownNat x =>
                  1 <= x =>
                  (1 + l) <= x =>
                  SNat l -> () -> Unsigned (x - l) -> Unsigned (x - (l + 1))
                go (l@SNat) allInputs prevStage = stage allInputs prevStage
    * Relevant bindings include
        input :: Unsigned x (bound at simple_dtypefold.hs:38:4)
        pl :: Unsigned x -> Unsigned (x - n)
          (bound at simple_dtypefold.hs:38:1)
   |
41 |         go
   |         ^^