Syntax for using datatype indexed by Nat


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
is inconsistent with the Haskell component

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?


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?