使用 Nat 索引的数据类型的语法

Question

以下代码尝试将Unsigned索引处的 Clash 类型族细化4为Digit：

import Clash.Prelude

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

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

这会导致以下错误消息：

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
.

因此 LH 似乎将4inUnsigned 4解析为除 Haskell 类型级别之外的特殊内容Nat。“转义”（或者更确切地说，取消转义？）的正确语法是什么，4以便将其解析为类型构造函数应用程序的一部分？