diff --git a/liquid-fixpoint b/liquid-fixpoint index 12409e8fb2..772b7721ed 160000 --- a/liquid-fixpoint +++ b/liquid-fixpoint @@ -1 +1 @@ -Subproject commit 12409e8fb299205b75bbcc26bf6fe600e364daf7 +Subproject commit 772b7721edce35c81598881e587d0a683527063a diff --git a/src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs b/src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs index bf26ce94c3..5b9e110854 100644 --- a/src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs +++ b/src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs @@ -47,7 +47,7 @@ fixConfig tgt cfg = def , FC.ginteractive = ginteractive cfg , FC.noslice = noslice cfg , FC.rewriteAxioms = Config.allowPLE cfg - , FC.etaElim = not (exactDC cfg) && extensionality cfg -- SEE: https://github.com/ucsd-progsys/liquidhaskell/issues/1601 + , FC.etaElim = not (exactDC cfg) -- && extensionality cfg -- SEE: https://github.com/ucsd-progsys/liquidhaskell/issues/1601 , FC.extensionality = extensionality cfg } diff --git a/tests/neg/T1601.hs b/tests/neg/T1601.hs new file mode 100644 index 0000000000..ce3ae685e2 --- /dev/null +++ b/tests/neg/T1601.hs @@ -0,0 +1,15 @@ +{-@ LIQUID "--reflect" @-} +{-@ LIQUID "--ple" @-} +{-@ reflect g @-} +g :: b -> c -> c +g y z = z +{-@ reflect f @-} +f :: a -> b -> b +f x y = g (g x y) y + +k :: a -> b -> b +k _ b = b + +{-@ fgeq :: x:a -> {f x == g x} @-} +fgeq :: a -> b -> () +fgeq _ _ = () diff --git a/tests/pos/T1560.hs b/tests/pos/T1560.hs index 9d0005daf6..c704abc8c0 100644 --- a/tests/pos/T1560.hs +++ b/tests/pos/T1560.hs @@ -1,6 +1,5 @@ {-@ LIQUID "--ple" @-} {-@ LIQUID "--reflection" @-} -{-@ LIQUID "--extensionality" @-} module T1560 where diff --git a/tests/pos/T1560B.hs b/tests/pos/T1560B.hs index 700ae3c4ad..7c21b7fe66 100644 --- a/tests/pos/T1560B.hs +++ b/tests/pos/T1560B.hs @@ -1,6 +1,5 @@ {-@ LIQUID "--ple" @-} {-@ LIQUID "--reflection" @-} -{-@ LIQUID "--extensionality" @-} module T1560 where