Add negative test for ucsd-progsys#1904

Fizzixnerd · Jan 6, 2022 · 8aaceac · 8aaceac
1 parent 9f2076b
commit 8aaceac
Showing 1 changed file with 12 additions and 0 deletions.
diff --git a/tests/datacon/neg/AutoliftedFields.hs b/tests/datacon/neg/AutoliftedFields.hs
@@ -0,0 +1,12 @@
+{-@ LIQUID "--exact-data-cons" @-}
+
+module AutoliftedFields where
+
+{-@ type Nat = { v : Int | v >= 0 } @-}
+type Nat = Int
+
+data T = T { getT :: Nat }
+
+{-@ f :: { t : T | getT t <= 0 } -> Nat @-}
+f :: T -> Nat
+f (T x) = x