diff --git a/liquid-prelude.cabal b/liquid-prelude.cabal
--- a/liquid-prelude.cabal
+++ b/liquid-prelude.cabal
@@ -1,6 +1,6 @@
 cabal-version:      1.24
 name:               liquid-prelude
-version:            0.8.10.2
+version:            0.9.14.1
 synopsis:           General utility modules for LiquidHaskell
 description:        General utility modules for LiquidHaskell.
 license:            BSD3
@@ -13,7 +13,7 @@
 build-type:         Custom
 
 custom-setup
-  setup-depends: Cabal, base, liquidhaskell
+  setup-depends: Cabal<4, base<5, liquidhaskell-boot
 
 library
   exposed-modules:  Language.Haskell.Liquid.RTick
@@ -25,13 +25,10 @@
                     Language.Haskell.Liquid.Equational
                     Language.Haskell.Liquid.Bag
                     Language.Haskell.Liquid.ProofCombinators
-                    Language.Haskell.Liquid.Synthesize.Error
-                    KMeansHelper
   hs-source-dirs:     src
-  build-depends:      liquid-base          < 5
-                    , bytestring           >= 0.10.0.0 && < 0.11
-                    , containers           >= 0.6.0.0  && < 0.7
-                    , liquidhaskell        >= 0.8.10.2
+  build-depends:      base          < 5
+                    , ghc-prim
+                    , bytestring           >= 0.10.12.1
+                    , containers           >= 0.6.4.1
+                    , liquidhaskell        >= 0.9.14.1
   default-language:   Haskell2010
-  if impl(ghc >= 8.10)
-    ghc-options: -fplugin=LiquidHaskell
diff --git a/src/KMeansHelper.hs b/src/KMeansHelper.hs
deleted file mode 100644
--- a/src/KMeansHelper.hs
+++ /dev/null
@@ -1,78 +0,0 @@
-module KMeansHelper where
-
-import Prelude hiding (zipWith)
-import Data.List (sort, span, minimumBy)
-import Data.Function (on)
-import Data.Ord (comparing)
-import Language.Haskell.Liquid.Prelude (liquidAssert, liquidError)
-
-
--- | Fixed-Length Lists
-
-{-@ type List a N = {v : [a] | (len v) = N} @-}
-
-
--- | N Dimensional Points
-
-{-@ type Point N = List Double N @-}
-
-{-@ type NonEmptyList a = {v : [a] | (len v) > 0} @-}
-
--- | Clustering 
-
-{-@ type Clustering a  = [(NonEmptyList a)] @-}
-
-------------------------------------------------------------------
--- | Grouping By a Predicate -------------------------------------
-------------------------------------------------------------------
-
-{-@ groupBy       :: (a -> a -> Bool) -> [a] -> (Clustering a) @-}
-groupBy _  []     =  []
-groupBy eq (x:xs) =  (x:ys) : groupBy eq zs
-  where (ys,zs)   = span (eq x) xs
-
-------------------------------------------------------------------
--- | Partitioning By a Size --------------------------------------
-------------------------------------------------------------------
-
-{-@ type PosInt = {v: Int | v > 0 } @-}
-
-{-@ partition           :: size:PosInt -> xs:[a] -> (Clustering a) / [len xs] @-}
-
-partition size []       = []
-partition size ys@(_:_) = zs : partition size zs'
-  where
-    zs                  = take size ys
-    zs'                 = drop size ys
-
------------------------------------------------------------------------
--- | Safe Zipping -----------------------------------------------------
------------------------------------------------------------------------
-
-{-@ zipWith :: (a -> b -> c) -> xs:[a] -> (List b (len xs)) -> (List c (len xs)) @-}
-zipWith f (a:as) (b:bs) = f a b : zipWith f as bs
-zipWith _ [] []         = []
-
--- Other cases only for exposition
-zipWith _ (_:_) []      = liquidError "Dead Code"
-zipWith _ [] (_:_)      = liquidError "Dead Code"
-
------------------------------------------------------------------------
--- | "Matrix" Transposition -------------------------------------------
------------------------------------------------------------------------
-
-{-@ type Matrix a Rows Cols  = (List (List a Cols) Rows) @-}
-
-{-@ transpose                :: c:Int -> r:PosInt -> Matrix a r c -> Matrix a c r @-}
-
-transpose                    :: Int -> Int -> [[a]] -> [[a]]
-transpose 0 _ _              = []
-transpose c r ((x:xs) : xss) = (x : map head xss) : transpose (c-1) r (xs : map tail xss)
-
--- Or, with comprehensions
--- transpose c r ((x:xs):xss) = (x : [ xs' | (x':_) <- xss ]) : transpose (c-1) r (xs : [xs' | (_ : xs') <- xss])
-
--- Not needed, just for exposition
-transpose c r ([] : _)       = liquidError "dead code"
-transpose c r []             = liquidError "dead code"
-
diff --git a/src/Language/Haskell/Liquid/Bag.hs b/src/Language/Haskell/Liquid/Bag.hs
--- a/src/Language/Haskell/Liquid/Bag.hs
+++ b/src/Language/Haskell/Liquid/Bag.hs
@@ -1,53 +1,71 @@
+{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}
+
 module Language.Haskell.Liquid.Bag where
 
 import qualified Data.Map      as M
 
-{-@ embed   Data.Map.Map as Map_t                                         @-}
-
-{-@ measure Map_default :: Int -> Bag a                                   @-}
-{-@ measure Map_union   :: Bag a -> Bag a -> Bag a                        @-}
-{-@ measure Map_select  :: Data.Map.Map k v -> k -> v                     @-}
-{-@ measure Map_store   :: Data.Map.Map k v -> k -> v -> Data.Map.Map k v @-}
-{-@ measure bagSize     :: Bag k -> Int                                   @-}
+{-@ embed   Bag as Bag_t                             @-}
+{-@ measure bagSize       :: Bag a -> Int            @-}
 
 -- if I just write measure fromList the measure definition is not imported
 {-@ measure fromList :: [k] -> Bag k
-      fromList ([])   = (Map_default 0)
-      fromList (x:xs) = Map_store (fromList xs) x (1 + (Map_select (fromList xs) x))
+      fromList ([])   = (Bag_empty 0)
+      fromList (x:xs) = Bag_union (fromList xs) (Bag_sng x 1)
 @-}
 
 
-type Bag a = M.Map a Int
+-- TODO newtype doesn't work because LH still expands the definition
+-- https://github.com/ucsd-progsys/liquidhaskell/issues/2332
+data Bag a = Bag { toMap :: M.Map a Int } deriving Eq
 
-{-@ assume empty :: {v:Bag k | v = Map_default 0} @-}
+{-@ assume empty :: {v:Bag k | v = Bag_empty 0} @-}
+{-@ define empty                = (Bag_empty 0) @-}
 empty :: Bag k
-empty = M.empty
-
-{-@ assume bagSize :: b:Bag k -> {i:Nat | i == bagSize b} @-}
-bagSize :: Bag k -> Int 
-bagSize b = sum (M.elems b) 
-
-{-@ fromList :: (Ord k) => xs:[k] -> {v:Bag k | v == fromList xs } @-} 
-fromList :: (Ord k) => [k] -> Bag k 
-fromList []     = empty
-fromList (x:xs) = put x (fromList xs)
+empty = Bag M.empty
 
-{-@ assume get :: (Ord k) => k:k -> b:Bag k -> {v:Nat | v = Map_select b k}  @-}
+{-@ assume get :: (Ord k) => k:k -> b:Bag k -> {v:Nat | v = Bag_count k b}  @-}
+{-@ define get               k      b                    = (Bag_count k b) @-}
 get :: (Ord k) => k -> Bag k -> Int
-get k m = M.findWithDefault 0 k m
+get k b = M.findWithDefault 0 k (toMap b)
 
-{-@ assume put :: (Ord k) => k:k -> b:Bag k -> {v:Bag k | v = Map_store b k (1 + (Map_select b k))} @-}
+{-@ assume put :: (Ord k) => k:k -> b:Bag k -> {v:Bag k | v = Bag_union b (Bag_sng k 1)} @-}
+{-@ define put               k      b                      = (Bag_union b (Bag_sng k 1)) @-}
 put :: (Ord k) => k -> Bag k -> Bag k
-put k m = M.insert k (1 + get k m) m
+put k b = Bag (M.insert k (1 + get k b) (toMap b))
 
-{-@ assume union :: (Ord k) => m1:Bag k -> m2:Bag k -> {v:Bag k | v = Map_union m1 m2} @-}
+{-@ assume union :: (Ord k) => a:Bag k -> b:Bag k -> {v:Bag k | v = Bag_union a b} @-}
+{-@ define union               a          b                      = (Bag_union a b) @-}
 union :: (Ord k) => Bag k -> Bag k -> Bag k
-union m1 m2 = M.union m1 m2
+union b1 b2 = Bag (M.unionWith (+) (toMap b1) (toMap b2))
 
-{-@ thm_emp :: x:k -> xs:Bag k ->  { Language.Haskell.Liquid.Bag.empty /= put x xs }  @-}
-thm_emp :: (Ord k) => k -> Bag k -> ()  
+{-@ assume unionMax :: (Ord k) => a:Bag k -> b:Bag k -> {v:Bag k | v = Bag_union_max a b} @-}
+{-@ define unionMax               a          b                      = (Bag_union_max a b) @-}
+unionMax :: (Ord k) => Bag k -> Bag k -> Bag k
+unionMax b1 b2 = Bag (M.unionWith max (toMap b1) (toMap b2))
+
+{-@ assume interMin :: (Ord k) => a:Bag k -> b:Bag k -> {v:Bag k | v = Bag_inter_min a b} @-}
+{-@ define interMin               a          b                      = (Bag_inter_min a b) @-}
+interMin :: (Ord k) => Bag k -> Bag k -> Bag k
+interMin b1 b2 = Bag (M.intersectionWith min (toMap b1) (toMap b2))
+
+{-@ assume sub :: (Ord k) => a:Bag k -> b:Bag k -> {v:Bool | v = Bag_sub a b} @-}
+{-@ define sub               a          b                     = (Bag_sub a b) @-}
+sub :: (Ord k) => Bag k -> Bag k -> Bool
+sub b1 b2 = M.isSubmapOfBy (<=) (toMap b1) (toMap b2)
+
+{-@ fromList :: (Ord k) => xs:[k] -> {v:Bag k | v == fromList xs } @-}
+fromList :: (Ord k) => [k] -> Bag k
+fromList []     = empty
+fromList (x:xs) = put x (fromList xs)
+
+{-@ assume bagSize :: b:Bag k -> {i:Nat | i == bagSize b} @-}
+bagSize :: Bag k -> Int
+bagSize b = sum (M.elems (toMap b))
+
+{-@ thm_emp :: x:k -> xs:Bag k -> { empty /= put x xs } @-}
+thm_emp :: (Ord k) => k -> Bag k -> ()
 thm_emp x xs = const () (get x xs)
 
-{-@ assume thm_size :: xs:[k] ->  { bagSize (fromList xs) == len xs }  @-}
-thm_size :: (Ord k) => [k] -> ()  
-thm_size _ = () 
+{-@ assume thm_size :: xs:[k] -> { bagSize (fromList xs) == len xs } @-}
+thm_size :: (Ord k) => [k] -> ()
+thm_size _ = ()
diff --git a/src/Language/Haskell/Liquid/Equational.hs b/src/Language/Haskell/Liquid/Equational.hs
--- a/src/Language/Haskell/Liquid/Equational.hs
+++ b/src/Language/Haskell/Liquid/Equational.hs
@@ -1,4 +1,5 @@
-module Language.Haskell.Liquid.Equational where 
+{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}
+module Language.Haskell.Liquid.Equational where
 
 -------------------------------------------------------------------------------
 -- | Proof is just unit
@@ -7,34 +8,34 @@
 type Proof = ()
 
 -------------------------------------------------------------------------------
--- | Casting expressions to Proof using the "postfix" `*** QED` 
+-- | Casting expressions to Proof using the "postfix" `*** QED`
 -------------------------------------------------------------------------------
 
-data QED = QED 
+data QED = QED
 
 infixl 2 ***
 (***) :: a -> QED -> Proof
-_ *** QED = () 
+_ *** QED = ()
 
 -------------------------------------------------------------------------------
--- | Equational Reasoning operators 
--- | The `eq` operator is inlined in the logic, so can be used in reflected 
--- | functions while ignoring the equality steps. 
+-- | Equational Reasoning operators
+-- | The `eq` operator is inlined in the logic, so can be used in reflected
+-- | functions while ignoring the equality steps.
 -------------------------------------------------------------------------------
 
-infixl 3 ==., `eq` 
+infixl 3 ==., `eq`
 
 
 {-@ (==.) :: x:a -> y:{a | x == y} -> {v:a | v == y && v == x} @-}
-(==.) :: a -> a -> a 
-_ ==. x = x 
-{-# INLINE (==.) #-} 
+(==.) :: a -> a -> a
+_ ==. x = x
+{-# INLINE (==.) #-}
 
 
 {-@ eq :: x:a -> y:{a | x == y} -> {v:a | v == y && v == x} @-}
-eq :: a -> a -> a 
-_ `eq` x = x 
-{-# INLINE eq #-} 
+eq :: a -> a -> a
+_ `eq` x = x
+{-# INLINE eq #-}
 
 -------------------------------------------------------------------------------
 -- | Explanations
@@ -43,13 +44,13 @@
 infixl 3 ?
 
 {-@ (?) :: forall a b <pa :: a -> Bool>. a<pa> -> b -> a<pa> @-}
-(?) :: a -> b -> a 
-x ? _ = x 
-{-# INLINE (?)   #-} 
+(?) :: a -> b -> a
+x ? _ = x
+{-# INLINE (?)   #-}
 
 -------------------------------------------------------------------------------
--- | Using proofs as theorems 
+-- | Using proofs as theorems
 -------------------------------------------------------------------------------
 
-withTheorem :: a -> Proof -> a 
-withTheorem z _ = z 
+withTheorem :: a -> Proof -> a
+withTheorem z _ = z
diff --git a/src/Language/Haskell/Liquid/Foreign.hs b/src/Language/Haskell/Liquid/Foreign.hs
--- a/src/Language/Haskell/Liquid/Foreign.hs
+++ b/src/Language/Haskell/Liquid/Foreign.hs
@@ -1,3 +1,4 @@
+{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}
 {-# OPTIONS_GHC -fno-warn-unused-imports #-}
 {-# LANGUAGE MagicHash #-}
 
@@ -34,7 +35,7 @@
 cSizeInt = fromIntegral
 
 
-{-@ assume mkPtr :: x:GHC.Prim.Addr# -> {v: (Ptr b) | ((plen v) = (addrLen x) && ((plen v) >= 0)) } @-}
+{-@ assume mkPtr :: x:Addr# -> {v: (Ptr b) | ((plen v) = (addrLen x) && ((plen v) >= 0)) } @-}
 mkPtr   :: Addr# -> Ptr b
 mkPtr = undefined -- Ptr x
 
diff --git a/src/Language/Haskell/Liquid/List.hs b/src/Language/Haskell/Liquid/List.hs
--- a/src/Language/Haskell/Liquid/List.hs
+++ b/src/Language/Haskell/Liquid/List.hs
@@ -1,3 +1,4 @@
+{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}
 module Language.Haskell.Liquid.List (transpose) where
 
 {-@ lazy transpose @-}
diff --git a/src/Language/Haskell/Liquid/Prelude.hs b/src/Language/Haskell/Liquid/Prelude.hs
--- a/src/Language/Haskell/Liquid/Prelude.hs
+++ b/src/Language/Haskell/Liquid/Prelude.hs
@@ -1,3 +1,4 @@
+{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}
 {-# LANGUAGE MagicHash      #-}
 
 module Language.Haskell.Liquid.Prelude where
@@ -126,17 +127,25 @@
 
 -----------------------------------------------------------------------------------------------
 
-{-@ safeZipWith :: (a -> b -> c) -> xs : [a] -> ys:{v:[b] | len v = len xs} 
+{-@ safeZipWith :: (a -> b -> c) -> xs : [a] -> ys:{v:[b] | len v = len xs}
                 -> {v : [c] | len v = len xs } @-}
 safeZipWith :: (a->b->c) -> [a]->[b]->[c]
 safeZipWith f (a:as) (b:bs) = f a b : safeZipWith f as bs
 safeZipWith _ []     []     = []
 safeZipWith _ _ _ = error "safeZipWith: cannot happen!"
 
-{-@ (==>) :: p:Bool -> q:Bool -> {v:Bool | v <=> (p =>  q)} @-}
+{-@ (==>) :: p:Bool -> q:Bool -> {v:Bool | v <=> (p => q)} @-}
 infixr 8 ==>
 (==>) :: Bool -> Bool -> Bool
 False ==> False = True
 False ==> True  = True
 True  ==> True  = True
 True  ==> False = False
+
+{-@ (<=>) :: p:Bool -> q:Bool -> {v:Bool | v <=> (p <=> q)} @-}
+infixr 8 <=>
+(<=>) :: Bool -> Bool -> Bool
+False <=> False = True
+False <=> True  = False
+True  <=> True  = True
+True  <=> False = False
diff --git a/src/Language/Haskell/Liquid/ProofCombinators.hs b/src/Language/Haskell/Liquid/ProofCombinators.hs
--- a/src/Language/Haskell/Liquid/ProofCombinators.hs
+++ b/src/Language/Haskell/Liquid/ProofCombinators.hs
@@ -1,3 +1,4 @@
+{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE TypeFamilies          #-}
@@ -9,7 +10,7 @@
 
   -- * Proof is just a () alias
   Proof
-  , toProof 
+  , toProof
 
   -- * Proof constructors
   , trivial, unreachable, (***), QED(..)
@@ -20,19 +21,21 @@
   -- * These two operators check all intermediate equalities
   , (===) -- proof of equality is implicit eg. x === y
   , (=<=) -- proof of equality is implicit eg. x <= y
-  , (=>=)  -- proof of equality is implicit eg. x =>= y 
+  , (=>=)  -- proof of equality is implicit eg. x =>= y
 
   -- * This operator does not check intermediate equalities
-  , (==.) 
+  , (==.)
 
   -- Uncheck operator used only for proof debugging
   , (==!) -- x ==! y always succeeds
 
   -- * Combining Proofs
   , (&&&)
-  , withProof 
-  , impossible 
+  , withProof
+  , impossible
 
+  -- * PLE-specific
+  , pleUnfold
 
 ) where
 
@@ -72,8 +75,10 @@
 
 data QED = Admit | QED
 
-{-@ measure isAdmit :: QED -> Bool @-}
-{-@ Admit :: {v:QED | isAdmit v } @-}
+{-@ measure isAdmit @-}
+isAdmit :: QED -> Bool
+isAdmit Admit = True
+isAdmit QED   = False
 
 
 -------------------------------------------------------------------------------
@@ -110,20 +115,44 @@
 _ =>= y  = y
 
 -------------------------------------------------------------------------------
--- | `?` is basically Haskell's $ and is used for the right precedence
--- | `?` lets you "add" some fact into a proof term
+-- | @e ? lemma@ lets you use the type of @lemma@ when checking that @e@ haskell
+-- has some expected refinement type.
+--
+-- Schematically, @?@ allows to use @q x@ to check that @e@ satisfies @p x e@
+-- in the following function.
+--
+-- > f :: x:t0 -> {v:t1 | p x v}
+-- > f x = e ? lemma x
+-- >   where
+-- >     lemma :: y:t0 -> { q y }
+-- >     lemma = ...
+--
+-- While @?@ is defined as Haskell's 'const', @?@ is optimized by Liquid
+-- Haskell. The 'const' function, on the other hand, would incur some extra
+-- verification overhead because Liquid Haskell needs to go through the trouble
+-- of checking that @const e lemma@ is actually @e@.
+--
+-- === At a lower level
+--
+-- Liquid Haskell treats @e ? lemma@ as
+--
+-- > let fresh0 = e
+-- >  in let fresh1 = lemma
+-- >      in fresh0
+--
+-- Which makes the @fresh1@ binding available in the environment of whatever
+-- constraints arise in the inner occurrence of @fresh0@.
 -------------------------------------------------------------------------------
 
 infixl 3 ?
 
-{-@ (?) :: forall a b <pa :: a -> Bool, pb :: b -> Bool>. a<pa> -> b<pb> -> a<pa> @-}
-(?) :: a -> b -> a 
-x ? _ = x 
-{-# INLINE (?)   #-} 
+(?) :: a -> b -> a
+x ? _ = x
+{-# INLINE (?)   #-}
 
 -------------------------------------------------------------------------------
 -- | Assumed equality
--- 	`x ==! y `
+--      `x ==! y `
 --   returns the admitted proof certificate that result value is equals x and y
 -------------------------------------------------------------------------------
 
@@ -135,9 +164,9 @@
 
 -- | To summarize:
 --
--- 	- (==!) is *only* for proof debugging
---	- (===) does not require explicit proof term
--- 	- (?)   lets you insert "lemmas" as other `Proof` values
+--      - (==!) is *only* for proof debugging
+--      - (===) does not require explicit proof term
+--      - (?)   lets you insert "lemmas" as other `Proof` values
 
 -------------------------------------------------------------------------------
 -- | * Unchecked Proof Certificates -------------------------------------------
@@ -146,15 +175,13 @@
 -- | The above operators check each intermediate proof step.
 --   The operator `==.` below accepts an optional proof term
 --   argument, but does not check intermediate steps.
---   TODO: What is it USEFUL FOR?
+--   So, using `==.` the proofs are faster, but the error messages worse.
 
 infixl 3 ==.
 
-{-# DEPRECATED (==.) "Use (===) instead" #-}
-
-{-# INLINE (==.) #-} 
-(==.) :: a -> a -> a 
-_ ==. x = x 
+{-# INLINE (==.) #-}
+(==.) :: a -> a -> a
+_ ==. x = x
 
 -------------------------------------------------------------------------------
 -- | * Combining Proof Certificates -------------------------------------------
@@ -164,7 +191,8 @@
 x &&& _ = x
 
 
-{-@ withProof :: x:a -> b -> {v:a | v = x} @-}
+{-@        withProof :: x:a -> b -> {v:a | v = x} @-}
+{-@ define withProof    x      y            = (x) @-}
 withProof :: a -> b -> a
 withProof x _ = x
 
@@ -173,11 +201,23 @@
 impossible _ = undefined
 
 -------------------------------------------------------------------------------
--- | Convenient Syntax for Inductive Propositions 
+-- | Convenient Syntax for Inductive Propositions
 -------------------------------------------------------------------------------
 
 {-@ measure prop :: a -> b           @-}
 {-@ type Prop E = {v:_ | prop v = E} @-}
 
+-- New syntax for "inductive propositions", aka indexed types, it
+-- should be used in place of `Prop` that is kept for backward
+-- compatibility.
+{-@ type Ix typ E = {v:typ | prop v = E} @-}
 
+-------------------------------------------------------------------------------
+-- PLE-specific
+-------------------------------------------------------------------------------
 
+-- | Forces PLE to unfold a function application if the body of the function
+-- starts with an application of @pleUnfold@.
+{-@ reflect pleUnfold @-}
+pleUnfold :: a -> a
+pleUnfold x = x
diff --git a/src/Language/Haskell/Liquid/RTick.hs b/src/Language/Haskell/Liquid/RTick.hs
--- a/src/Language/Haskell/Liquid/RTick.hs
+++ b/src/Language/Haskell/Liquid/RTick.hs
@@ -1,3 +1,4 @@
+{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}
 
 --
 -- Liquidate your assets: reasoning about resource usage in Liquid Haskell.
diff --git a/src/Language/Haskell/Liquid/RTick/Combinators.hs b/src/Language/Haskell/Liquid/RTick/Combinators.hs
--- a/src/Language/Haskell/Liquid/RTick/Combinators.hs
+++ b/src/Language/Haskell/Liquid/RTick/Combinators.hs
@@ -1,3 +1,4 @@
+{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}
 
 --
 -- Liquidate your assets: reasoning about resource usage in Liquid Haskell.
diff --git a/src/Language/Haskell/Liquid/String.hs b/src/Language/Haskell/Liquid/String.hs
--- a/src/Language/Haskell/Liquid/String.hs
+++ b/src/Language/Haskell/Liquid/String.hs
@@ -1,4 +1,5 @@
--- Support for Strings for SMT 
+{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}
+-- Support for Strings for SMT
 
 {-# LANGUAGE OverloadedStrings   #-}
 
@@ -9,7 +10,7 @@
 
 {-@ embed SMTString as Str @-}
 
-data SMTString = S BS.ByteString 
+data SMTString = S BS.ByteString
   deriving (Eq, Show)
 
 {-@ invariant {s:SMTString | 0 <= stringLen s } @-}
@@ -24,7 +25,7 @@
 
 ----------------------------------
 
-{-@ assume concatString :: x:SMTString -> y:SMTString 
+{-@ assume concatString :: x:SMTString -> y:SMTString
                  -> {v:SMTString | v == concatString x y && stringLen v == stringLen x + stringLen y } @-}
 concatString :: SMTString -> SMTString -> SMTString
 concatString (S s1) (S s2) = S (s1 `BS.append` s2)
@@ -33,30 +34,30 @@
 stringEmp :: SMTString
 stringEmp = S (BS.empty)
 
-stringLen :: SMTString -> Int  
+stringLen :: SMTString -> Int
 {-@ assume stringLen :: x:SMTString -> {v:Nat | v == stringLen x} @-}
-stringLen (S s) = BS.length s 
+stringLen (S s) = BS.length s
 
 
 {-@ assume subString  :: s:SMTString -> offset:Int -> ln:Int -> {v:SMTString | v == subString s offset ln } @-}
-subString :: SMTString -> Int -> Int -> SMTString 
-subString (S s) o l = S (BS.take l $ BS.drop o s) 
+subString :: SMTString -> Int -> Int -> SMTString
+subString (S s) o l = S (BS.take l $ BS.drop o s)
 
 
-{-@ assume takeString :: i:Nat -> xs:{SMTString | i <= stringLen xs } -> {v:SMTString | stringLen v == i && v == takeString i xs } @-} 
+{-@ assume takeString :: i:Nat -> xs:{SMTString | i <= stringLen xs } -> {v:SMTString | stringLen v == i && v == takeString i xs } @-}
 takeString :: Int -> SMTString -> SMTString
 takeString i (S s) = S (BS.take i s)
 
-{-@ assume dropString :: i:Nat -> xs:{SMTString | i <= stringLen xs } -> {v:SMTString | stringLen v == stringLen xs - i && v == dropString i xs } @-} 
+{-@ assume dropString :: i:Nat -> xs:{SMTString | i <= stringLen xs } -> {v:SMTString | stringLen v == stringLen xs - i && v == dropString i xs } @-}
 dropString :: Int -> SMTString -> SMTString
 dropString i (S s) = S (BS.drop i s)
 
 
 {-@ assume fromString :: i:String -> {o:SMTString | i == o && o == fromString i} @-}
 fromString :: String -> SMTString
-fromString = S . ST.fromString 
+fromString = S . ST.fromString
 
 
-{-@ assume isNullString :: i:SMTString -> {b:Bool | b <=> stringLen i == 0 } @-} 
-isNullString :: SMTString -> Bool 
-isNullString (S s) = BS.length s == 0 
+{-@ assume isNullString :: i:SMTString -> {b:Bool | b <=> stringLen i == 0 } @-}
+isNullString :: SMTString -> Bool
+isNullString (S s) = BS.length s == 0
diff --git a/src/Language/Haskell/Liquid/Synthesize/Error.hs b/src/Language/Haskell/Liquid/Synthesize/Error.hs
deleted file mode 100644
--- a/src/Language/Haskell/Liquid/Synthesize/Error.hs
+++ /dev/null
@@ -1,5 +0,0 @@
-module Language.Haskell.Liquid.Synthesize.Error where 
-
-{-@ err :: { v: Int | false } -> a @-}
-err :: Int -> a
-err s = undefined