More tests for ucsd-progsys#1904

tests/datacon/neg/AutoliftedFields.hs → tests/datacon/neg/AutoliftedFields00.hs

@@ -1,6 +1,8 @@
 {-@ LIQUID "--exact-data-cons" @-}
 
-module AutoliftedFields where
+-- data decl in LH is missing and uses a LH-refined type alias incorrectly
+
+module AutoliftedFields00 where
 
 {-@ type Nat = { v : Int | v >= 0 } @-}
 type Nat = Int

tests/datacon/neg/AutoliftedFields01.hs

@@ -0,0 +1,15 @@
+{-@ LIQUID "--exact-data-cons" @-}
+
+-- data decl in LH and Haskell do not match and the LH one is not a subtype
+
+module AutoliftedFields01 where
+
+{-@ type Nat = { v : Int | v >= 0 } @-}
+type Nat = Int
+
+{-@ data T = T { getT :: Float } @-}
+data T = T { getT :: Nat }
+
+{-@ f :: { t : T | getT t >= 1 } -> Nat @-}
+f :: T -> Nat
+f (T x) = x

tests/datacon/pos/AutoliftedFields.hs → tests/datacon/pos/AutoliftedFields00.hs

@@ -1,6 +1,8 @@
 {-@ LIQUID "--exact-data-cons" @-}
 
-module AutoliftedFields where
+-- data decl in LH is missing but uses a LH-refined type alias correctly
+
+module AutoliftedFields00 where
 
 {-@ type Nat = { v : Int | v >= 0 } @-}
 type Nat = Int

tests/datacon/pos/AutoliftedFields01.hs

@@ -0,0 +1,16 @@
+{-@ LIQUID "--exact-data-cons" @-}
+
+-- data decl in LH and Haskell give different names to the fields, but use them
+-- in valid ways.
+
+module AutoliftedFields01 where
+
+{-@ type Nat = { v : Int | v >= 0 } @-}
+type Nat = Int
+
+{-@ data T = T { getMyT :: Nat } @-}
+data T = T { getT :: Nat }
+
+{-@ f :: { t : T | getT t == getMyT t } -> Nat @-}
+f :: T -> Nat
+f (T x) = x

tests/datacon/pos/AutoliftedFields02.hs

@@ -0,0 +1,15 @@
+{-@ LIQUID "--exact-data-cons" @-}
+
+-- data decl in LH and Haskell do not match but the LH is a subtype
+
+module AutoliftedFields02 where
+
+{-@ type Nat = { v : Int | v >= 0 } @-}
+type Nat = Int
+
+{-@ data T = T { getT :: Nat } @-}
+data T = T { getT :: Int }
+
+{-@ f :: { t : T | getT t >= 0 } -> Nat @-}
+f :: T -> Nat
+f (T x) = x