Sebastian Ertel

In the following code, LH loses Type Applications and then complains that the types do not match: (Sorry for pasting the code, but I had problems retrieving a permanent link...

Refined GADTs with deriving confuse the type checker

1

The following GADT type checks just fine: ``` {-@ LIQUID "--exact-data-cons" @-} {-@ LIQUID "--prune-unsorted" @-} {-# LANGUAGE NoOverloadedLists #-} {-# LANGUAGE NoOverloadedStrings, DataKinds, KindSignatures, TypeApplications, GADTs #-} module Base...

Unbound symbol is$GHC.Types.[] for pattern match on empty list

9

Hi LiquidHaskellers, I really like the idea of LH and would like to use it but I’m stuck on an error. Please excuse me if this error is only due...

More precise parser error

1

When the parser encounters a type that is unknown, it fails with the following error: ``` expected: {""} ``` It would be extremely helpful if the parser would at the...

Infinite loop

3

Dear @cpitclaudel , We are trying out Koika to run part of an operating system on an FPGA. In a test case (a.k.a. `Example`) we are using `tc_compute` and `interpret_action`...

Hi, Is there any possibility to access the location information for a type? I'm doing roughly the following: ``` fn_entity .get_type().unwrap() .get_argument_types().unwrap() .into_iter() .for_each(|t:Type| { // get location information for...

Nix flake suppport and CI

3

Dear SSProvers, this PR adds the following: - support loading `SSProve` via Nix flakes - additional CI jobs: - to test the added Nix flake - to test the CI...