From 8aaceac4b505e12cc88da7afd10eb1e9642112c9 Mon Sep 17 00:00:00 2001 From: Matt Walker Date: Thu, 6 Jan 2022 11:43:35 -0500 Subject: [PATCH] Add negative test for #1904 --- tests/datacon/neg/AutoliftedFields.hs | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100644 tests/datacon/neg/AutoliftedFields.hs diff --git a/tests/datacon/neg/AutoliftedFields.hs b/tests/datacon/neg/AutoliftedFields.hs new file mode 100644 index 0000000000..fa4c5048d8 --- /dev/null +++ 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