Cannot parse `GHC.Types.:`

https://github.com/ucsd-progsys/liquidhaskell/blob/7d623adaf36cbd43f597387cada60bd1e3f019a6/docs/blog/2014-02-11-the-advantage-of-measures.lhs#L338-L346

---

There is no way to refer to list contructor : inside specifications, as : is reserved for typing variables and expressions. This makes it impossible to prove semi-advanced programs based on lists.

I think there should be a way to refer to GHC.Types.: in specifications, or a canonical way to define aliases for strange names that cannot be parsed.

---

I have made numerous attempts at bypassing this issue, to no avail.

• (xs:[a] -> x:a -> b<p xs> -> b<p (GHC.Types.: x xs)>) has undefined symbol GHC.Types.
• (xs:[a] -> x:a -> b<p xs> -> b<p (x:xs)>) has cast error, because x (a a) cannot be converted to the type of xs (a [a])
• (xs:[a] -> x:a -> b<p xs> -> b<p (cons x xs)>) seems to work (with cons = (:) being reflected) until you realize the inference cannot prove anything useful about cons. Something as trivial as this fails verification:

{-@ prop_cons :: x:a -> xs:[a] -> {xxs:[a] | xxs == (cons x xs)} @-}
prop_cons x xs = x:xs -- Fails

More generally, it is possible to prove that insertionSort and quickSort generate ordered permutations of their inputs, but not when using foldr, or a generalized foldr' that supports a ghost variable. The initial quote above cannot be made to work.

---

If you are curious, here is my attempt:

{-# LANGUAGE NoMonomorphismRestriction #-}

module PuttingThingsInOrder () where

import Prelude hiding (break)
import qualified Language.Haskell.Liquid.Bag as B
import Language.Haskell.Liquid.Prelude (liquidAssert)

{-@ measure elems @-}
elems :: (Ord a) => [a] -> B.Bag a
elems []     = B.empty
elems (x:xs) = B.put x (elems xs)

{-@ predicate Perm X Y = elems X == elems Y @-}
{-@ type IncrList a = [a]<{\xi xj -> xi <= xj}> @-}
{-@ type SortedList a Xs = {ys:IncrList a | Perm ys Xs} @-}

{-@ reflect cons @-}
cons :: a -> [a] -> [a]
cons x xs = x : xs

-- All the properties fail

{-@ prop_cons :: x:a -> xs:[a] -> {b:Bool | b} @-}
prop_cons x xs = cons x xs == x:xs

{-@ prop_cons2 :: x:a -> xs:[a] -> {xxs:[a] | xxs == (cons x xs)} @-}
prop_cons2 x xs = x:xs

{-@ prop_elems_cons :: x:a -> xs:[a] -> {b:Bool | b} @-}
prop_elems_cons x xs = elems (cons x xs) == B.put x (elems xs)

{-@ prop_elems_cons2 :: x:a -> xs:[a] -> {b:Bool | b} @-}
prop_elems_cons2 x xs = elems (cons x xs) == elems (x:xs)

{-@ prop_elems_put :: x:a -> xs:[a] -> {b:Bool | b} @-}
prop_elems_put x xs = elems (cons x xs) == B.put x (elems xs)

{-@ insert :: (Ord a) => x:a -> xs:IncrList a -> ys:{ys:IncrList a | elems ys == B.put x (elems xs)} @-}
-- FAILS: {-@ insert :: (Ord a) => x:a -> xs:IncrList a -> SortedList a (cons x xs) @-}
insert y []     = [y]
insert y (x:xs)
  | y <= x      = y : x : xs
  | otherwise   = x : insert y xs

{-@
foldr' :: forall <p :: [a] -> b -> Bool>.
          (xs:[a] -> x:a -> b<p xs> -> b<p (cons x xs)>)
       -> b<p []>
       -> ys:[a]
       -> b<p ys>
@-}
foldr' :: ([a] -> a -> b -> b) -> b -> [a] -> b
foldr' f z []     = z
foldr' f z (x:xs) = f xs x (foldr' f z xs)

{-@ ghostInsert :: (Ord a) => xs:[a] -> y:a -> ys:SortedList a xs -> SortedList a (cons y ys) @-}
ghostInsert :: Ord a => [a] -> a -> [a] -> [a]
ghostInsert xs y ys = insert y ys

{-@ insertSort :: (Ord a) => xs:[a] -> SortedList a xs @-}
insertSort :: Ord a => [a] -> [a]
insertSort xs  = foldr' ghostInsert [] xs

cc @facundominguez follow-up from previous discussion