Syntax for using datatype indexed by Nat

The following code tries to refine Clash's Unsigned type family at index 4 into Digit:

import Clash.Prelude

{-@ type Digit = {v : Unsigned 4 | v <= 9 } @-}
type Digit = Unsigned 4

{-@ foo :: Digit -> Digit @-}
foo = id @Digit

This leads to the following error message:

The Liquid type
.
    (Clash.Sized.Internal.Unsigned.Unsigned {4}) -> (Clash.Sized.Internal.Unsigned.Unsigned {4})
.
is inconsistent with the Haskell type
.
    Clash.Sized.Internal.Unsigned.Unsigned 4
-> Clash.Sized.Internal.Unsigned.Unsigned 4
.
defined at src/HelloClash.hs:11:1-3
.
Specifically, the Liquid component
.
    {4}
.
is inconsistent with the Haskell component
.
    GHC.Types.Int
.

So it seems the 4 in Unsigned 4 is parsed by LH as something special other than a Haskell type-level Nat. What is the correct syntax to "escape" (or, rather, un-escape?) the 4 so that it is parsed as part of the type constructor application?

Recommended topics

Hot tags