Remove --exact-data-cons from tests

Author: facundominguez

tests/typed-holes/Example2.hs

@@ -1,12 +1,11 @@
 {-@ LIQUID "--expect-error-containing=Hole Found" @-}
-{-@ LIQUID "--exact-data-cons" @-}
 {-@ LIQUID "--warn-on-term-holes" @-}
 -- Based on https://ucsd-progsys.github.io/liquidhaskell-blog/2016/10/06/structural-induction.lhs/
 
 module Example2 where
     import Prelude hiding ((<>))
     import Language.Haskell.Liquid.ProofCombinators ((===), (***), QED(QED), Proof)
-    
+
     hole = undefined
 
     {-@ reflect empty @-}
@@ -24,7 +23,7 @@ module Example2 where
     leftId x
         =   empty <> x
         === hole
-        === x          
+        === x
         *** QED
 
     {-@ rightId  :: x:[a] -> { (x <> empty) == x } @-}

tests/typed-holes/Example3.hs

@@ -1,5 +1,4 @@
 {-@ LIQUID "--expect-error-containing=Hole Found" @-}
-{-@ LIQUID "--exact-data-cons" @-}
 {-@ LIQUID "--warn-on-term-holes" @-}
 -- Based on paper: Theorem Proving for All: Equational Reasoning in Liquid Haskell (Functional Pearl)
 
@@ -8,7 +7,7 @@ module Example3 where
     import Language.Haskell.Liquid.ProofCombinators ((===), (***), QED(QED), Proof)
 
     hole = undefined
-    
+
     {-@ length :: [a] -> {v:Int | 0 <= v } @-}
     length :: [a] -> Int
     length [] = 0

tests/typed-holes/Example4.hs

@@ -1,5 +1,4 @@
 {-@ LIQUID "--expect-error-containing=Hole Found" @-}
-{-@ LIQUID "--exact-data-cons" @-}
 {-@ LIQUID "--warn-on-term-holes" @-}
 -- Based on paper: Theorem Proving for All: Equational Reasoning in Liquid Haskell (Functional Pearl)
 
@@ -30,11 +29,11 @@ module Example4 where
 
     {-@ reverseApp :: xs:[a] -> ys:[a] -> {zs:[a] | zs == reverse xs ++ ys} @-}
     reverseApp :: [a] -> [a] -> [a]
-    reverseApp [] ys     
+    reverseApp [] ys
         = reverse [] ++ ys
-        === [] ++ ys 
+        === [] ++ ys
         === ys
-    reverseApp (x:xs) ys 
+    reverseApp (x:xs) ys
         = reverse (x:xs) ++ ys
         === (reverse xs ++ [x]) ++ ys
         === (reverse xs ++ [x] ++ ys) ? hole -- I need a lemma here! Can the hole help me?

tests/typed-holes/Example5.hs

@@ -1,5 +1,4 @@
 {-@ LIQUID "--expect-error-containing=Hole Found" @-}
-{-@ LIQUID "--exact-data-cons" @-}
 {-@ LIQUID "--warn-on-term-holes" @-}
 -- Based on paper: Theorem Proving for All: Equational Reasoning in Liquid Haskell (Functional Pearl)
 
@@ -29,7 +28,7 @@ module Example5 where
     (x:xs) ++ ys = x : (xs ++ ys)
     {-@ infixl ++ @-}
     {-@ reflect ++ @-}
-    
+
 
     {-@ flattenApp :: t:Tree -> ns:[Int] -> { v:[Int] | v == flatten t ++ ns } @-}
     flattenApp :: Tree -> [Int] -> [Int]

tests/typed-holes/Example6.hs

@@ -1,5 +1,4 @@
 {-@ LIQUID "--expect-error-containing=Hole Found" @-}
-{-@ LIQUID "--exact-data-cons" @-}
 {-@ LIQUID "--warn-on-term-holes" @-}
 -- Based on paper: Theorem Proving for All: Equational Reasoning in Liquid Haskell (Functional Pearl)
 {-@ infix    :   @-}