[Haskell-cafe] Polymorphic equality in LiquidHaskell

[Henning Thielemann]

I want to assert statically assert equality of polymorphic parameters 
using LiquidHaskell. See for instance the following simplified Array type 
containing an array shape and for demonstration purposes only a single 
element:


data Array sh a = Array {shape :: sh, element :: a}

{-@
lift2 ::
    (Eq sh) =>
    (a -> b -> c) ->
    arrA : Array sh a ->
    {arrB : Array sh b | shape arrA == shape arrB} ->
    Array sh c
@-}
lift2 ::
    (Eq sh) => (a -> b -> c) -> Array sh a -> Array sh b -> Array sh c
lift2 f (Array sha a) (Array shb b) =
    if sha == shb
       then Array sha $ f a b
       else error "shapes mismatch"


Running liquidhaskell yields

Illegal type specification
...
Sort Error in Refinement: {arrB : (Example.Equality.Array sh##a31s b##a31u) | 
Example.Equality.shape arrA == Example.Equality.shape arrB}
     Unbound symbol Example.Equality.shape


I think the Haskell function (==) is not automatically lifted to 
LiquidHaskell's logic language. Is there another way to assert a kind of 
equality in LiquidHaskell?