Syntax for using datatype indexed by Nat

Issue

This Content is from Stack Overflow. Question asked by Cactus

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?



Solution

This question is not yet answered, be the first one who answer using the comment. Later the confirmed answer will be published as the solution.

This Question and Answer are collected from stackoverflow and tested by JTuto community, is licensed under the terms of CC BY-SA 2.5. - CC BY-SA 3.0. - CC BY-SA 4.0.

people found this article helpful. What about you?