[Feature] Add refinement hole-fits. Fixes #59

[Tritlo]

By adding refinement hole-fits, we get exponentially more valid fits for any candidate, by enabling fits with additional holes (and those holes are then fit with everything in scope). This might help with more complex programs. Due to #65, and the fact that using refinement-hole fits is a lot more likely to generate non-trivial loops can make refinement fits freeze-up more often. After #66 was fixed we could run it properly, and it gives good results, e.g.:

module SimpleRefinement where

f :: [Int] -> Int
f = foldr (-) 1

-- We want foldl (+) 2 here

prop_isSumPlus2 :: [Int] -> Bool
prop_isSumPlus2 xs = f xs == sum xs + 2

two :: Int
two = 2

main :: IO ()
main = putStrLn "hello, world"

---- EXPECTED ----
-- diff --git a/tests/cases/SimpleRefinement.hs b/tests/cases/SimpleRefinement.hs
-- --- a/tests/cases/SimpleRefinement.hs
-- +++ b/tests/cases/SimpleRefinement.hs
-- @@ -4,1 +4,1 @@ f = foldr (-) 1
-- -f = foldr (-) 1
-- +f = (foldl (+) two)
---- END EXPECTED ----

which I think is pretty neat!

[Tritlo]

I've been able to test it a bit, and the test works great. So I think the refinement hole fits work well, when there aren't any infinite loops to be avoided.