Liquid Haskell can't recognize the inaccessible pattern, where bound names are forced to be equal via types.

InaccessiblePattern.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}

module InaccessiblePattern where

type Proof = ()

{-@
measure eqWrapped :: a -> a -> Bool
@-}

{-@
type EqW a X Y = {_:EqWrapped a | eqWrapped X Y}
@-}

{-@
data EqWrapped :: * -> * where
  EqWrapped :: x:a -> y:a -> {_:Proof | x = y} -> EqW a {x} {y}
@-}
data EqWrapped :: * -> * where
  EqWrapped :: a -> a -> Proof -> EqWrapped a

-- eq -> eqWrapped
{-@
wrap :: x:a -> y:a -> {_:Proof | x = y} -> EqW a {x} {y}
@-}
wrap :: a -> a -> Proof -> EqWrapped a
wrap = EqWrapped

-- eqWrapped -> eq
{-@
unwrap :: x:a -> y:a -> EqW a {x} {y} -> {x = y}
@-}
unwrap :: a -> a -> EqWrapped a -> Proof
unwrap x y ew@(EqWrapped x_ y_ e) = e

InaccessiblePattern.md

Liquid Haskell is missing the Inaccessible Pattern

The above code does not typecheck with Liquid Haskell, throwing a liquid type mismatch on the e in the definition of unwrap:

    Liquid Type Mismatch
    .
    The inferred type
      VV : {v : () | x_ == y_
                     && v == e}
    .
    is not a subtype of the required type
      VV : {VV : () | x == y}
    .
    in the context
      x_ : a
       
      y_ : a
       
      e : {e : () | x_ == y_}
       
      x : a
       
      y : a
   |
32 | unwrap x y ew@(EqWrapped x_ y_ e) = e
   |                                     ^

The problem here is that the type ew :: EqW a {x} {y} requires that x = x_ and y = y_. However, LH doesn't aknowledge this, and assumes x_ and y_ are totally independent. This yields the error where the inferred type of e contains the refinement x_ = y_, but this isn't enough to convince LH that x = y which is the desired refinement.

In dependently typed languages like Agda and Coq (some degree of dependent types are required for this situation to arise), you can indicate that a name binding is redundant due to forced equality enforced by types by using an _ (or in the case of agda, a . prefix aka the dot pattern).

It turns out that this is not actually an issue with LH. If the above code did typecheck, it would allow, for example, the following unsound case.

You could define

{-@ ew0 :: EqW Int 0 0 @-}
ew0 :: EqWrapped Int
ew0 = EqWrapped 0 0 ()

{-@ ew1 :: EqW Int 1 1 @-}
ew1 :: EqWrapped Int
ew1 = EqWrapped 1 1 ()

{-@ ew1' :: EqW Int 0 0 @-}
ew1' :: EqWrapped Int
ew1' = ew1 `withProof` ew0

withProof :: a -> b -> a
withProof x y = x

and then call

bad = unwrap 0 0 ew1'

with a EqWrap object that was built using a different x and y.
In the definition of ew1', which is ew1 withProof ew0, the term that ew1' is equal to is ew1, but the predicate that provides EqW Int 0 0 comes from ew0. So if you unwrap ew1', you don’t get an EqWrapped corresponding to 1 = 1 like you might expect.

This example was provided by @rjhala.