plredmond
plredmond
Currently if you want to write a proof with a lot of cases, you have no way of knowing which ones are necessary. The process that I've used is to...
## Repro code Repro7.hs ```haskell {-# LANGUAGE DeriveGeneric #-} module Repro7 where import GHC.Generics (Generic) {-@ data D = D { x::Nat, y::() } @-} data D = D {...
Followup on #1987 which might be of interest to @facundominguez: I've encountered another of these errors caused by name collisions in type aliases. Renaming bindings in the type alias fixes...
Slack thread: https://liquidhaskell.slack.com/archives/C54QAL9RR/p1616392946007000 > ``` > {-@ type Foo N = {n:Int | n == N} @-} > > {-@ type Bar = Foo {n} @-} > ``` > In...
**Problem:** The following snippet of code causes a crash in LH. ```haskell import Control.Arrow (first) {-@ crash :: {x:_ | x == True } @-} crash :: Bool crash =...
Similar to https://github.com/haskell-servant/servant/issues/1085, I needed to write a server which was composed of multiple APIs. I found [Docs » Cookbook » Structuring APIs](https://docs.servant.dev/en/stable/cookbook/structuring-apis/StructuringApis.html) but my APIs were defined as [Docs...
http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1668179472_14471.hs ```haskell {-@ allLeq :: n:Int ~> {x:[a] | len x == n} -> {y:[a] | len y == n} -> Bool @-} allLeq :: Ord a => [a] ->...
This GADT has a phantom type that gets refined (GHC-sense) by its constructor(s). That phantom type has a refinement (LH-sense) in the GADT-signature of its constructor. When we pattern match...
## Summary This change adds a rule to detect functions declared `async` but lacking any of `await`, `async with`, or `async for`. This resolves #9951. ## Test Plan This change...
Resolves #10390 and starts to address #10391 # Changes to the implementation * In the body of the loop over import statements that contain unused bindings, the bindings are partitioned...