Merge pull request #1602 from ucsd-progsys/T1601

ranjitjhala · web-flow · commit 11cc7e31c26d · 2020-02-04T21:20:28.000-08:00
T1601
diff --git a/liquid-fixpoint b/liquid-fixpoint
@@ -1 +1 @@
-Subproject commit 429e6a0e5b60102cc65fd6464efeb5248338c84e
+Subproject commit 12409e8fb299205b75bbcc26bf6fe600e364daf7
diff --git 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)
+  , FC.etaElim          = not (exactDC cfg) && extensionality cfg -- SEE: https://github.com/ucsd-progsys/liquidhaskell/issues/1601
   , FC.extensionality   = extensionality    cfg 
   }
 
diff --git a/tests/pos/T1560.hs b/tests/pos/T1560.hs
@@ -1,5 +1,6 @@
 {-@ LIQUID "--ple"        @-}
 {-@ LIQUID "--reflection" @-}
+{-@ LIQUID "--extensionality" @-}
 
 module T1560 where 
 
@@ -24,4 +25,4 @@ fgeqx x = f x `k` g x `k` ()
 
 {-@ fgeq :: {f = g} @-}
 fgeq :: ()
-fgeq = f `k` g `k` ()
+fgeq = f `k` g `k` ()
diff --git a/tests/pos/T1560B.hs b/tests/pos/T1560B.hs
@@ -1,5 +1,6 @@
 {-@ LIQUID "--ple"        @-}
 {-@ LIQUID "--reflection" @-}
+{-@ LIQUID "--extensionality" @-}
 
 module T1560 where 
 

Original file line number	Diff line number	Diff line change
`@@ -47,7 +47,7 @@ fixConfig tgt cfg = def`
`47`	`47`	`, FC.ginteractive = ginteractive cfg`
`48`	`48`	`, FC.noslice = noslice cfg`
`49`	`49`	`, FC.rewriteAxioms = Config.allowPLE cfg`
`50`		`- , FC.etaElim = not (exactDC cfg)`
	`50`	`+ , FC.etaElim = not (exactDC cfg) && extensionality cfg -- SEE: https://github.com/ucsd-progsys/liquidhaskell/issues/1601`
`51`	`51`	`, FC.extensionality = extensionality cfg`
`52`	`52`	`}`
`53`	`53`