title: Syntax for using datatype indexed by Nat
body: <p>The following code tries to refine Clash's <code>Unsigned</code> type family at index <code>4</code> into <code>Digit</code>:</p>
  <pre><code>import Clash.Prelude
  
  {-@ type Digit = {v : Unsigned 4 | v &lt;= 9 } @-}
  type Digit = Unsigned 4
  
  {-@ foo :: Digit -&gt; Digit @-}
  foo = id @Digit
  </code></pre>
  <p>This leads to the following error message:</p>
  <pre><code>The Liquid type
  .
      (Clash.Sized.Internal.Unsigned.Unsigned {4}) -&gt; (Clash.Sized.Internal.Unsigned.Unsigned {4})
  .
  is inconsistent with the Haskell type
  .
      Clash.Sized.Internal.Unsigned.Unsigned 4
  -&gt; 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
  .
  
  </code></pre>
  <p>So it seems the <code>4</code> in <code>Unsigned 4</code> is parsed by LH as something special other than a Haskell type-level <code>Nat</code>. What is the correct syntax to &quot;escape&quot; (or, rather, <em>un-escape?</em>) the <code>4</code> so that it is parsed as part of the type constructor application?</p>