Fix weird behaviour when dealing with datatypes following an invariant

[rudymatela]

{-# LANGUAGE TemplateHaskell #-}
import Test.Extrapolate

newtype Nat = Nat Int deriving (Eq, Show, Ord)

deriveListable ''Nat
deriveGeneralizable ''Nat

-- incorrect property:
prop_lengthTake :: Nat -> [Int] -> Bool
prop_lengthTake (Nat n) xs = length (take n xs) == n

main :: IO ()
main = do
  check prop_lengthTake

The output for the above program is:

*** Failed! Falsifiable (after 3 tests):
(Nat 1) []

Conditional Generalization:
n _  when  n < (Nat 0)

The conditional generalization is correct. However it is only correct for data values that do not follow the data invariant of Nat.

Thanks to @ColinRunciman for discovering this.

[rudymatela]

Maybe this could be solved by adding yet another function to the Generalizable typeclass?

class Generalizable a where
  ...
  valid :: a -> Bool
  valid = True

instance Generalizable Nat where
  ...
  valid (Nat n) = n >= 0