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 :: D...

I'm following the official tutorial on Liquid Haskell, and stumbled upon what seems to be a "bug" in it. The following code is present in the tutorial, and Liquid Haskell was supposed to check tha...

I am reading this where I find this: Measures -- In order to allow Haskell functions to appear in refinement types, we need to lift them to the refinement type level. And there are other docu...

I am trying to solve some exercise from LiquidHaskell tutorial. So, I wrote this: data List a = Nil | Cons a (List a) deriving (Show) infixr 5 `Cons` {-@ len :: List a -> Nat @-} len :: List ...

The problem I've been very excited playing with LiquidHaskell, however, I don't know to what extent I need to modify my original Haskell code to meet LiquidHaskell's requirements. Here is a simple ...

I have been playing around with LiquidHaskell and Idris lately and i got a pretty specific question, that i could not find a definitive answer anywhere. Idris is a dependently typed language which...

I have a server in Haskell that responds to Json inputs. The problem is that there are cases where the server will crash because of a partial function, but Liquid Haskell says it is safe. Here's a...

I'm trying to use liquidhaskell on NixOS. I can install the package (liquidhaskell-0.8.2.3), though not the cabal integration, because it requires cabal 1.18-1.25, but I have cabal 2.0.1.0 . I hav...

I am having troubles proving the following law with LiquidHaskell: It is known as (one of) DeMorgan's law, and simply states that the negation of oring two values must be the same as anding the ...