Inconsistent generalizations for [Int] and [Bool]

[rudymatela]

import Test.Extrapolate

-- incorrect property:
prop_lengthZip :: [a] -> [a] -> Bool
prop_lengthZip xs ys = length (zip xs ys) == max (length xs) (length ys)

main :: IO ()
main = do
  check (prop_lengthZip :: [Int] -> [Int] -> Bool)
  putStrLn "\n"
  check (prop_lengthZip :: [()] -> [()] -> Bool)
  putStrLn "\n"
  check (prop_lengthZip :: [Bool] -> [Bool] -> Bool)

For the above program, the output is the following:

*** Failed! Falsifiable (after 2 tests):
[] [0]

Generalization:
xs (_:xs)

Conditional Generalization:
xs ys  when  length xs /= length ys



*** Failed! Falsifiable (after 2 tests):
[] [()]

Generalization:
us (_:us)



*** Failed! Falsifiable (after 2 tests):
[] [False]

Generalization:
ps (_:ps)

Extrapolate is able to produce a conditional generalization involving length of [Int] but not of [Bool] and [()]. Why?

[rudymatela]

@ColinRunciman, thanks for discovering this.

[rudymatela]

I know why now. For the [Bool] case, both the arguments to the property are of [Bool] type. Only the background for the [Bool] and its "sub-type" Bool are included.

Since the background of Int insn't there. There is no (/=) :: Int -> Int -> Bool, hence the missing generalization. If we manually add it the problem is solved:

{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE NoMonomorphismRestriction #-} -- AAARRRRGGHHHH!!!!
import Test.Extrapolate

-- incorrect property:
prop_lengthZip :: [a] -> [a] -> Bool
prop_lengthZip xs ys = length (zip xs ys) == max (length xs) (length ys)

main :: IO ()
main = do
  check (prop_lengthZip :: [Int] -> [Int] -> Bool)
  putStrLn "\n"
  chk (prop_lengthZip :: [()] -> [()] -> Bool)
  putStrLn "\n"
  chk (prop_lengthZip :: [Bool] -> [Bool] -> Bool)
  where
  chk = check `withBackground` [constant "/=" ((/=) :: Int -> Int -> Bool)]

output:

*** Failed! Falsifiable (after 2 tests):
[] [0]

Generalization:
xs (_:xs)

Conditional Generalization:
xs ys  when  length xs /= length ys



*** Failed! Falsifiable (after 2 tests):
[] [()]

Generalization:
us (_:us)

Conditional Generalization:
us vs  when  length us /= length vs



*** Failed! Falsifiable (after 2 tests):
[] [False]

Generalization:
ps (_:ps)

Conditional Generalization:
ps qs  when  length ps /= length qs

Hah!

Maybe what I need to do for a permanent fix is to always include the background of Int and some relevant "core types"?