Polymorphism plays a vital role in automating verification in LH. However, thanks to its ubiquity, we often take it for granted, and it can be quite baffling to figure out why verification fails with monomorphic signatures. Let me explain why, using a simple example that has puzzled me and other users several times.

22: 23: module PolymorphicPerplexion where

## A Type for Ordered Lists

Previously we have seen how you can use LH to define a type of lists whose values are in increasing (ok, non-decreasing!) order.

First, we define an `IncList a`

type, with `Emp`

(“empty”)
and `:<`

(“cons”) constructors.

38: data IncList a = Emp 39: | (:<) { hd :: a, tl :: IncList a } 40: 41: infixr 9 :<

Next, we refine the type to specify that each “cons” `:<`

constructor takes as input a `hd`

and a `tl`

which must
be an `IncList a`

of values `v`

each of which is greater
than `hd`

.

50: {-@ data IncList a = Emp 51: | (:<) { hd :: a, tl :: IncList {v:a | hd <= v}} 52: @-}

We can confirm that the above definition ensures that the only
*legal* values are increasingly ordered lists, as LH accepts
the first list below, but rejects the second where the elements
are out of order.

61: legalList :: IncList Int 62: (PolymorphicPerplexion.IncList GHC.Types.Int)legalList = GHC.Types.Int0 :< GHC.Types.Int1 :< GHC.Types.Int2 :< GHC.Types.Int3 :< {VV : forall a . (PolymorphicPerplexion.IncList a) | VV == Emp}Emp 63: 64: illegalList :: IncList Int 65: (PolymorphicPerplexion.IncList GHC.Types.Int)illegalList = GHC.Types.Int0 :< GHC.Types.Int1 :< GHC.Types.Int3 :< GHC.Types.Int2 :< {VV : forall a . (PolymorphicPerplexion.IncList a) | VV == Emp}Emp

## A Polymorphic Insertion Sort

Next, lets write a simple *insertion-sort* function that
takes a plain unordered list of `[a]`

and returns the elements
in increasing order:

76: insertSortP :: (Ord a) => [a] -> IncList a 77: forall a . (GHC.Classes.Ord<[]> a) => [a] -> (PolymorphicPerplexion.IncList a)insertSortP [a]xs = foldr a -> (PolymorphicPerplexion.IncList a) -> (PolymorphicPerplexion.IncList a)insertP {VV : forall a . (PolymorphicPerplexion.IncList a) | VV == Emp}Emp {v : [a] | len v >= 0 && v == xs}xs 78: 79: insertP :: (Ord a) => a -> IncList a -> IncList a 80: forall a . (GHC.Classes.Ord<[]> a) => a -> (PolymorphicPerplexion.IncList a) -> (PolymorphicPerplexion.IncList a)insertP ay Emp = {VV : a | VV == y}y :< {VV : forall a . (PolymorphicPerplexion.IncList a) | VV == Emp}Emp 81: insertP y (x :< xs) 82: | {VV : a | VV == y}y <= {VV : a | VV == x}x = {VV : a | VV == y}y :< {VV : a | VV == x}x :< {v : (PolymorphicPerplexion.IncList {VV : a | x <= VV}) | v == xs}xs 83: | otherwise = {VV : a | VV == x}x :< (PolymorphicPerplexion.IncList a)insertP {VV : a | VV == y}y {v : (PolymorphicPerplexion.IncList {VV : a | x <= VV}) | v == xs}xs

Happily, LH is able to verify the above code without any trouble!
(If that seemed too easy, don’t worry: if you mess up the comparison,
e.g. change the guard to `x <= y`

LH will complain about it.)

## A Monomorphic Insertion Sort

However, lets take the *exact* same code as above *but* change
the type signatures to make the functions *monomorphic*, here,
specialized to `Int`

lists.

99: insertSortM :: [Int] -> IncList Int 100: [GHC.Types.Int] -> (PolymorphicPerplexion.IncList GHC.Types.Int)insertSortM [GHC.Types.Int]xs = foldr GHC.Types.Int -> (PolymorphicPerplexion.IncList GHC.Types.Int) -> (PolymorphicPerplexion.IncList GHC.Types.Int)insertM {VV : forall a . (PolymorphicPerplexion.IncList a) | VV == Emp}Emp {v : [GHC.Types.Int] | len v >= 0 && v == xs}xs 101: 102: insertM :: Int -> IncList Int -> IncList Int 103: GHC.Types.Int -> (PolymorphicPerplexion.IncList GHC.Types.Int) -> (PolymorphicPerplexion.IncList GHC.Types.Int)insertM GHC.Types.Inty Emp = {v : GHC.Types.Int | v == y}y :< {VV : forall a . (PolymorphicPerplexion.IncList a) | VV == Emp}Emp 104: insertM y (x :< xs) 105: | {v : GHC.Types.Int | v == y}y <= {v : GHC.Types.Int | v == x}x = {v : GHC.Types.Int | v == y}y :< {v : GHC.Types.Int | v == x}x :< {v : (PolymorphicPerplexion.IncList {v : GHC.Types.Int | x <= v}) | v == xs}xs 106: | otherwise = {v : GHC.Types.Int | v == x}x :< (PolymorphicPerplexion.IncList GHC.Types.Int)insertM {v : GHC.Types.Int | v == y}y {v : (PolymorphicPerplexion.IncList {v : GHC.Types.Int | x <= v}) | v == xs}xs

Huh? Now LH appears to be unhappy with the code! How is this possible?

Lets look at the type error:

114: /Users/rjhala/PerplexingPolymorphicProperties.lhs:80:27-38: Error: Liquid Type Mismatch 115: 116: 80 | | otherwise = x :< insertM y xs 117: ^^^^^^^^^^^^ 118: Inferred type 119: VV : Int 120: 121: not a subtype of Required type 122: VV : {VV : Int | x <= VV} 123: 124: In Context 125: x : Int

LH *expects* that since we’re using the “cons” operator `:<`

the “tail”
value `insertM y xs`

must contain values `VV`

that are greater than the
“head” `x`

. The error says that, LH cannot prove this requirement of
*actual* list `insertM y xs`

.

Hmm, well thats a puzzler. Two questions that should come to mind.

*Why*does the above fact hold in the first place?*How*is LH able to deduce this fact with the*polymorphic*signature but not the monomorphic one?

Lets ponder the first question: why *is* every element
of `insert y xs`

in fact larger than `x`

? For three reasons:

every element in

`xs`

is larger than`x`

, as the list`x :< xs`

was ordered,`y`

is larger than`x`

as established by the`otherwise`

and cruciallythe elements returned by

`insert y xs`

are either`y`

or from`xs`

!

Now onto the second question: how *does* LH verify the polymorphic code,
but not the monomorphic one? The reason is the fact (c)! LH is a *modular*
verifier, meaning that the *only* information that it has about the behavior
of `insert`

at a call-site is the information captured in the (refinement)
*type specification* for `insert`

. The *polymorphic* signature:

156: insertP :: (Ord a) => a -> IncList a -> IncList a

via *parametricity*, implicitly states fact (c). That is, if at a call-site
`insertP y xs`

we pass in a value that is greater an `x`

and a list of values
greater than `x`

then via *polymorphic instantiation* at the call-site, LH
infers that the returned value must also be a list of elements greater than `x`

!

However, the *monomorphic* signature

167: insertM :: Int -> IncList Int -> IncList Int

offers no such insight. It simply says the function takes in an `Int`

and another
ordered list of `Int`

and returns another ordered list, whose actual elements could
be arbitrary `Int`

. Specifically, at the call-site `insertP y xs`

LH has no way to
conclude the the returned elements are indeed greater than `x`

and hence rejects
the monomorphic code.

## Perplexity

While parametricity is all very nice, and LH’s polymorphic instanatiation is very
clever and useful, it can also be quite mysterious. For example, q curious user
Oisín pointed out
that while the code below is *rejected* that if you *uncomment* the type signature
for `go`

then it is *accepted* by LH!

187: insertSortP' :: (Ord a) => [a] -> IncList a 188: forall a . (GHC.Classes.Ord<[]> a) => [a] -> (PolymorphicPerplexion.IncList a)insertSortP' = (PolymorphicPerplexion.IncList a)foldr a -> (PolymorphicPerplexion.IncList a) -> (PolymorphicPerplexion.IncList a)go {VV : forall a . (PolymorphicPerplexion.IncList a) | VV == Emp}Emp 189: where 190: -- go :: (Ord a) => a -> IncList a -> IncList a 191: a -> (PolymorphicPerplexion.IncList a) -> (PolymorphicPerplexion.IncList a)go ay Emp = {VV : a | VV == y}y :< {VV : forall a . (PolymorphicPerplexion.IncList a) | VV == Emp}Emp 192: go y (x :< xs) 193: | {VV : a | VV == y}y <= {VV : a | VV == x}x = {VV : a | VV == y}y :< {VV : a | VV == x}x :< {v : (PolymorphicPerplexion.IncList {VV : a | x <= VV}) | v == xs}xs 194: | otherwise = {VV : a | VV == x}x :< (PolymorphicPerplexion.IncList a)go {VV : a | VV == y}y {v : (PolymorphicPerplexion.IncList {VV : a | x <= VV}) | v == xs}xs

This is thoroughly perplexing, but again, is explained by the absence of
parametricity. When we *remove* the type signature, GHC defaults to giving
`go`

a *monomorphic* signature where the `a`

is not universally quantified,
and which roughly captures the same specification as the monomorphic `insertM`

above causing verification to fail!

Restoring the signature provides LH with the polymorphic specification,
which can be instantiated at the call-site to recover the fact `(c)`

that is crucial for verification.

## Moral

I hope that example illustrates two points.

First, *parametric polymorphism* lets type specifications
say a lot more than they immediately let on: so do write
polymorphic signatures whenever possible.

Second, on a less happy note, *explaining* why fancy type
checkers fail remains a vexing problem, whose difficulty
is compounded by increasing the cleverness of the type
system.

We’d love to hear any ideas you might have to solve the explanation problem!