Incompleteness with a top-level higher-order function

[octalsrc]

Hello, I'm exploring what I can or can't do with higher-order functions. Is there a straightforward way to get the following failing example to typecheck?

It seems that defining a higher-order function at the top level, vs. in a where-clause, changes what can be proven about it.

I used liquidhaskell-9.10.1 for these examples.

First, a working example

The following example typechecks. compareSelf is a function that takes another function as its first argument.

{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}

module HigherOrder where

{-@ example1 :: Int -> { v:Bool | v } @-}
example1 :: Int -> Bool
example1 a = compareSelf (==) a
  where
    compareSelf f x = f x x

The example1 function returns True if its Int argument is equal to itself. Of course this is always the case, and Liquid Haskell agrees.

**** LIQUID: SAFE (1 constraints checked) **************************************

The failing example

This example is identical to the first, except that I moved compareSelf out of the where-clause and into a top-level definition.

{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}

module HigherOrder where

compareSelf :: (Int -> Int -> Bool) -> Int -> Bool
compareSelf f x = f x x

{-@ example2 :: Int -> { v:Bool | v } @-}
example2 :: Int -> Bool
example2 a = compareSelf (==) a

This change causes Liquid Haskell to return UNSAFE.

**** LIQUID: UNSAFE ************************************************************
src/HigherOrder.hs:10:1: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : GHC.Types.Bool
    .
    is not a subtype of the required type
      VV : {VV##365 : GHC.Types.Bool | VV##365}
    .
    Constraint id 1
   |
10 | example2 a = compareSelf (==) a
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Annotation did not fix it

I tried adding a refinement annotation to compareSelf, and noticed that this required me to use the --higherorder flag.

{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}

{-@ LIQUID "--higherorder" @-}

module HigherOrder where

{-@ compareSelf :: f:(Int -> Int -> Bool) -> x:Int -> {v:Bool | v <=> f x x} @-}
compareSelf :: (Int -> Int -> Bool) -> Int -> Bool
compareSelf f x = f x x

{-@ example2 :: Int -> { v:Bool | v } @-}
example2 :: Int -> Bool
example2 a = compareSelf (==) a

Adding this annotation changed an inferred type, but did not fix the UNSAFE result.

**** LIQUID: UNSAFE ************************************************************
src/HigherOrder.hs:13:1: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : {v : GHC.Types.Bool | (v <=> lq_anf$##7205759403792801025##d1VL a##aSX a##aSX)
                                 && v == HigherOrder.compareSelf lq_anf$##7205759403792801025##d1VL a##aSX}
    .
    is not a subtype of the required type
      VV : {VV##357 : GHC.Types.Bool | VV##357}
    .
    in the context
      a##aSX : GHC.Types.Int
    Constraint id 1
   |
13 | example2 a = compareSelf (==) a
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Is there an extra annotation or flag I can use to make this example typecheck? Or should I generally avoid defining higher-order functions at top-level?

Thanks!

[facundominguez]

Removing the type signature of compareSelf or giving it a polimorphic type also makes verification succeed.

compareSelf :: (a -> a -> b) -> a -> b

The error says

    The inferred type
      VV : {v : GHC.Types.Bool | (v <=> lq_anf$##7205759403792800974##d1UW a##aDn a##aDn)
                                 && v == Test.compareSelf lq_anf$##7205759403792800974##d1UW a##aDn}
    .
    is not a subtype of the required type
      VV : {VV##523 : GHC.Types.Bool | VV##523}

Using --save the dump to .fq.prettified is a bit more clear:

  lhs {VV : bool | [(VV <=> (GHC.Classes.$61$$61$ a a));
                    (VV = (Test.compareSelf GHC.Classes.$61$$61$ a))]}
  rhs {VV : bool | [VV]}

where $61$$61$ stands for an encoded form of ==.

I'm guessing there is a bug here where GHC.Classes.== is not being understood as equality in the logic.

[octalsrc]

Ah, I did not think to remove the main type signature.

It seems that the == operator is not needed to trigger this bug. Here is an example that doesn't use ==.

{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}

{-@ LIQUID "--higherorder" @-}

module HigherOrder where

{-@ boolEq :: a:Bool -> b:Bool -> { v:Bool | v <=> ((a && b) || (not a && not b)) } @-}
boolEq :: Bool -> Bool -> Bool
boolEq a b = (a && b) || (not a && not b)

-- This example successfully typechecks.
{-@ example1 :: Bool -> { v:Bool | v } @-}
example1 :: Bool -> Bool
example1 a = cself boolEq a
  where
    -- This function is identical to 'compareSelf'.
    cself f x = f x x

{-@ compareSelf :: f:(Bool -> Bool -> Bool) -> x:Bool -> {v:Bool | v <=> f x x} @-}
compareSelf :: (Bool -> Bool -> Bool) -> Bool -> Bool
compareSelf f x = f x x

-- This example fails to typecheck.  It can be made to typecheck by
-- removing the type signature and refinement annotation from the
-- 'compareSelf' definition.
{-@ example2 :: Bool -> { v:Bool | v } @-}
example2 :: Bool -> Bool
example2 a = compareSelf boolEq a

Just as with the previous example, example2 fails to typecheck:

**** LIQUID: UNSAFE ************************************************************
src/HigherOrder.hs:31:1: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : {v : GHC.Types.Bool | (v <=> HigherOrder.boolEq a##aSs a##aSs)
                                 && v == HigherOrder.compareSelf HigherOrder.boolEq a##aSs}
    .
    is not a subtype of the required type
      VV : {VV##413 : GHC.Types.Bool | VV##413}
    .
    in the context
      a##aSs : GHC.Types.Bool
    Constraint id 2
   |
31 | example2 a = compareSelf boolEq a
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

As you suggested, if I remove the type signature and refinement annotation on compareSelf, then example2 does typecheck.

[octalsrc]

Here's an example in which removing the type signature does not help. It's the same as the previous example, except that I use not in the higher-order function (compareNotSelf), preventing it from having a fully polymorphic type.

{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}

-- Required for the signatures of 'compareNotSelf'.
{-# LANGUAGE RankNTypes #-}
{-@ LIQUID "--higherorder" @-}

module HigherOrder where

-- Try any combination of the signatures for 'compareNotSelf': no
-- signature, only normal type, only refinement type, or both
-- signatures.  Note that the normal type requires RankNTypes, and the
-- refinement type requires the "--higherorder" flag.

{-@ compareNotSelf :: forall a. f:(Bool -> Bool -> a) -> x:Bool -> { v:a | v == f (not x) (not x) } @-}
compareNotSelf :: forall a. (Bool -> Bool -> a) -> Bool -> a
compareNotSelf f x = f (not x) (not x)

-- Examples that use (==)

{-@ example1a :: Bool -> { v:Bool | v } @-}
example1a :: Bool -> Bool
example1a a =
  compareNotSelf (==) a

{-@ example1b :: Bool -> { v:Bool | v } @-}
example1b :: Bool -> Bool
example1b a =
  cnself (==) a
  where
    -- 'cnself' is identical to 'compareNotSelf'
    cnself f x = f (not x) (not x)

-- Examples that do not use (==)

{-@ boolEq :: b1:Bool -> b2:Bool -> { v:Bool | v <=> ((b1 && b2) || (not b1 && not b2)) } @-}
boolEq :: Bool -> Bool -> Bool
boolEq b1 b2 =
  (b1 && b2) || (not b1 && not b2)

{-@ example2a :: Bool -> { v:Bool | v } @-}
example2a :: Bool -> Bool
example2a a =
  compareNotSelf boolEq a

{-@ example2b :: Bool -> { v:Bool | v } @-}
example2b :: Bool -> Bool
example2b a =
  cnself boolEq a
  where
    cnself f x = f (not x) (not x)

Here, example1a and example2a do not typecheck, with or without the type signature on compareNotSelf.

On the other hand, example1b and example2b, which replace compareNotSelf with an identical where definition, do typecheck.

With compareNotSelf type signature:

**** LIQUID: UNSAFE ************************************************************
src/HigherOrder.hs:22:1: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : {v : GHC.Types.Bool | v == HigherOrder.compareNotSelf lq_anf$##7205759403792801353##d213 a##aVx
                                 && v == lq_anf$##7205759403792801353##d213 (not a##aVx) (not a##aVx)}
    .
    is not a subtype of the required type
      VV : {VV##516 : GHC.Types.Bool | VV##516}
    .
    in the context
      a##aVx : GHC.Types.Bool
    Constraint id 1
   |
22 | example1a a =
   | ^^^^^^^^^^^^^...

src/HigherOrder.hs:42:1: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : {v : GHC.Types.Bool | v == HigherOrder.boolEq (not a##aVE) (not a##aVE)
                                 && v == HigherOrder.compareNotSelf HigherOrder.boolEq a##aVE}
    .
    is not a subtype of the required type
      VV : {VV##572 : GHC.Types.Bool | VV##572}
    .
    in the context
      a##aVE : GHC.Types.Bool
    Constraint id 9
   |
42 | example2a a =
   | ^^^^^^^^^^^^^...

Without compareNotSelf type signature:

**** LIQUID: UNSAFE ************************************************************
src/HigherOrder.hs:22:1: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : {v : GHC.Types.Bool | v == HigherOrder.compareNotSelf lq_anf$##7205759403792801355##d215 a##aVx}
    .
    is not a subtype of the required type
      VV : {VV##524 : GHC.Types.Bool | VV##524}
    .
    in the context
      a##aVx : GHC.Types.Bool
    Constraint id 1
   |
22 | example1a a =
   | ^^^^^^^^^^^^^...

src/HigherOrder.hs:42:1: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : {v : GHC.Types.Bool | v == HigherOrder.compareNotSelf HigherOrder.boolEq a##aVE}
    .
    is not a subtype of the required type
      VV : {VV##580 : GHC.Types.Bool | VV##580}
    .
    in the context
      a##aVE : GHC.Types.Bool
    Constraint id 9
   |
42 | example2a a =
   | ^^^^^^^^^^^^^...

[AlecsFerra]

The issue is the monomorphic signature, polymorphic variables not only carry types but also refinement information, I think you need abstract refinements