From 00540a716ae5ad609e730616bfb2d0d4eb0abf54 Mon Sep 17 00:00:00 2001
From: Yiyun Liu <liuyiyun@terpmail.umd.edu>
Date: Sun, 9 Feb 2020 14:28:48 -0500
Subject: [PATCH] update submodule with elimEta fix

---
 liquid-fixpoint                                   |  2 +-
 .../Haskell/Liquid/Constraint/ToFixpoint.hs       |  2 +-
 tests/neg/T1601.hs                                | 15 +++++++++++++++
 tests/pos/T1560.hs                                |  1 -
 tests/pos/T1560B.hs                               |  1 -
 5 files changed, 17 insertions(+), 4 deletions(-)
 create mode 100644 tests/neg/T1601.hs

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