diff --git a/src/Language/Haskell/Liquid/Bare/DataType.hs b/src/Language/Haskell/Liquid/Bare/DataType.hs
index 03f01eec3a..44ea1db40e 100644
--- a/src/Language/Haskell/Liquid/Bare/DataType.hs
+++ b/src/Language/Haskell/Liquid/Bare/DataType.hs
@@ -73,11 +73,15 @@ makeDataConChecker = F.testSymbol . F.symbol
 --   equivalent to `head` and `tail`.
 --------------------------------------------------------------------------------
 makeDataConSelector :: Maybe Bare.DataConMap -> Ghc.DataCon -> Int -> F.Symbol
-makeDataConSelector dmMb d i = M.lookupDefault def (F.symbol d, i) dm
-  where 
-    dm                       = Mb.fromMaybe M.empty dmMb 
+makeDataConSelector dmMb d i
+  | Just ithField <- ithFieldMb = F.symbol (Ghc.flSelector ithField)
+  | otherwise = M.lookupDefault def (F.symbol d, i) dm
+  where
+    fields = Ghc.dataConFieldLabels d
+    ithFieldMb = Misc.getNth (i - 1) fields
+    dm                       = Mb.fromMaybe M.empty dmMb
     def                      = makeDataConSelector' d i
- 
+
 
 makeDataConSelector' :: Ghc.DataCon -> Int -> F.Symbol
 makeDataConSelector' d i
diff --git a/tests/basic/neg/GADTFields00.hs b/tests/basic/neg/GADTFields00.hs
new file mode 100644
index 0000000000..f0863b4b2d
--- /dev/null
+++ b/tests/basic/neg/GADTFields00.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE GADTs #-}
+
+{-@ LIQUID "--exact-data-cons" @-}
+
+-- With a refinement type embedded and then used wrongly
+
+module GADTFields00 where
+
+{-@
+data T where
+  T :: { getT :: Int, getT' :: { v:Int | v >= 0 } } -> T
+ @-}
+data T where
+  T :: { getT :: Int, getT' :: Int } -> T
+
+{-@ f :: T -> { v:Int | v < 0} @-}
+f :: T -> Int
+f = getT'
+
+main :: IO ()
+main = print (getT' (T 5 6))
diff --git a/tests/basic/neg/GADTFields01.hs b/tests/basic/neg/GADTFields01.hs
new file mode 100644
index 0000000000..e2a882a10b
--- /dev/null
+++ b/tests/basic/neg/GADTFields01.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE GADTs #-}
+
+{-@ LIQUID "--exact-data-cons" @-}
+
+-- With a refinement type embedded in a function using a fieldname, but with a
+-- bad type
+
+module GADTFields01 where
+
+{-@
+data T where
+  T :: { getT :: Int, getT' :: Int } -> T 
+ @-}
+data T where
+  T :: { getT :: Int, getT' :: Int } -> T
+
+{-@ f :: { v:T | getT' v < 0 } -> { x:Int | x >= 0 } @-}
+f :: T -> Int
+f = getT'
+
+main :: IO ()
+main = print (getT' (T 5 6))
diff --git a/tests/basic/neg/GADTFields02.hs b/tests/basic/neg/GADTFields02.hs
new file mode 100644
index 0000000000..4ec0a8b63b
--- /dev/null
+++ b/tests/basic/neg/GADTFields02.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE GADTs #-}
+
+{-@ LIQUID "--exact-data-cons" @-}
+
+-- With a refinement type embedded in a function using a fieldname, but with a
+-- bad type
+
+module GADTFields02 where
+
+{-@
+data T where
+  T :: { getT :: Int, getT' :: { v:Int | v >= 0 } } -> T 
+ @-}
+data T where
+  T :: { getT :: Int, getT' :: Int } -> T
+
+{-@ f :: { v:T | getT' v < 0 } -> { x:Int | x >= 0 } @-}
+f :: T -> Int
+f = getT'
+
+main :: IO ()
+main = print (getT' (T 5 6))
diff --git a/tests/basic/neg/GADTFields03.hs b/tests/basic/neg/GADTFields03.hs
new file mode 100644
index 0000000000..54c9dc252a
--- /dev/null
+++ b/tests/basic/neg/GADTFields03.hs
@@ -0,0 +1,32 @@
+{-# LANGUAGE GADTs #-}
+
+{-@ LIQUID "--exact-data-cons" @-}
+
+-- With a refinement type embedded in a function using a fieldname, but with a
+-- bad type
+
+module GADTFields03 where
+
+{-@
+data T a where
+  T :: { getT :: Int, getT' :: { v:Int | v >= 0 } } -> T Int
+  S :: { getT :: Int, getS :: Float } -> T Int
+ @-}
+data T a where
+  T :: { getT :: Int, getT' :: Int } -> T Int
+  S :: { getT :: Int, getS :: Float } -> T Int
+
+{-@
+measure isT
+isT :: T Int -> Bool
+@-}
+isT :: T Int -> Bool
+isT (T _ _) = True
+isT _ = False
+
+{-@ f :: { v: T Int | isT v && getS v >= 0  } -> Float @-}
+f :: T Int -> Float
+f = getS
+
+main :: IO ()
+main = print (f (S 5 0.1))
diff --git a/tests/basic/neg/GADTFields04.hs b/tests/basic/neg/GADTFields04.hs
new file mode 100644
index 0000000000..37faa8a745
--- /dev/null
+++ b/tests/basic/neg/GADTFields04.hs
@@ -0,0 +1,25 @@
+{-# LANGUAGE GADTs #-}
+
+{-@ LIQUID "--exact-data-cons" @-}
+
+-- With shared field names
+
+module GADTFields04 where
+
+{-@
+data T a where
+  T :: { getT :: Int, getT' :: { v:Int | v >= 0 } } -> T Int
+  S :: { getT :: Int, getS :: String } -> T Int
+ @-}
+data T a where
+  T :: { getT :: Int, getT' :: Int } -> T Int
+  S :: { getT :: Int, getS :: String } -> T Int
+
+{-@ f :: { v:T Int | getT v >= 0 } -> { x: Int | x >= 0 } @-}
+f :: T Int -> Int
+f = getT
+
+main :: IO ()
+main = do
+  print (f (T 5 6))
+  print (f (S 3 ""))
diff --git a/tests/basic/pos/GADTFields00.hs b/tests/basic/pos/GADTFields00.hs
new file mode 100644
index 0000000000..3972197e4c
--- /dev/null
+++ b/tests/basic/pos/GADTFields00.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE GADTs #-}
+
+{-@ LIQUID "--exact-data-cons" @-}
+
+-- Basic syntax checking
+
+module GADTFields00 where
+
+{-@
+data T where
+  T :: { getT :: Int } -> T
+ @-}
+data T where
+  T :: { getT :: Int } -> T
+
+main :: IO ()
+main = print ()
diff --git a/tests/basic/pos/GADTFields01.hs b/tests/basic/pos/GADTFields01.hs
new file mode 100644
index 0000000000..ce984e4cd1
--- /dev/null
+++ b/tests/basic/pos/GADTFields01.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE GADTs #-}
+
+{-@ LIQUID "--exact-data-cons" @-}
+
+-- With a refinement type embedded
+
+module GADTFields01 where
+
+{-@
+data T where
+  T :: { getT :: Int, getT' :: { v:Int | v >= 0 } } -> T
+ @-}
+data T where
+  T :: { getT :: Int, getT' :: Int } -> T
+
+main :: IO ()
+main = print ()
diff --git a/tests/basic/pos/GADTFields02.hs b/tests/basic/pos/GADTFields02.hs
new file mode 100644
index 0000000000..133faa9681
--- /dev/null
+++ b/tests/basic/pos/GADTFields02.hs
@@ -0,0 +1,26 @@
+{-# LANGUAGE GADTs #-}
+
+{-@ LIQUID "--exact-data-cons" @-}
+{-@ LIQUID "--reflection" @-}
+
+-- With shared field names
+
+module GADTFields02 where
+
+{-@
+data T a where
+  T :: { getT :: Int, getT' :: { v:Int | v >= 0 } } -> T Int
+  S :: { getT :: Int, getS :: String } -> T Int
+ @-}
+data T a where
+  T :: { getT :: Int, getT' :: Int } -> T Int
+  S :: { getT :: Int, getS :: String } -> T Int
+
+{-@ f :: { v:T Int | getT v >= 0 } -> { x: Int | x >= 0 } @-}
+f :: T Int -> Int
+f = getT
+
+main :: IO ()
+main = do
+  print (f (T 5 6))
+  print (f (S 3 ""))
diff --git a/tests/datacon/neg/AutoliftedFields00.hs b/tests/datacon/neg/AutoliftedFields00.hs
new file mode 100644
index 0000000000..06974bfc85
--- /dev/null
+++ b/tests/datacon/neg/AutoliftedFields00.hs
@@ -0,0 +1,14 @@
+{-@ LIQUID "--exact-data-cons" @-}
+
+-- 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
+
+data T = T { getT :: Nat }
+
+{-@ f :: { t : T | getT t <= 0 } -> Nat @-}
+f :: T -> Nat
+f (T x) = x
diff --git a/tests/datacon/neg/AutoliftedFields01.hs b/tests/datacon/neg/AutoliftedFields01.hs
new file mode 100644
index 0000000000..73522d5ba8
--- /dev/null
+++ b/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
diff --git a/tests/datacon/pos/AutoliftedFields00.hs b/tests/datacon/pos/AutoliftedFields00.hs
new file mode 100644
index 0000000000..7b215a6d76
--- /dev/null
+++ b/tests/datacon/pos/AutoliftedFields00.hs
@@ -0,0 +1,14 @@
+{-@ LIQUID "--exact-data-cons" @-}
+
+-- 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
+
+data T = T { getT :: Nat }
+
+{-@ f :: { t : T | getT t >= 1 } -> Nat @-}
+f :: T -> Nat
+f (T x) = x
diff --git a/tests/datacon/pos/AutoliftedFields01.hs b/tests/datacon/pos/AutoliftedFields01.hs
new file mode 100644
index 0000000000..59fe08bbca
--- /dev/null
+++ b/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
diff --git a/tests/datacon/pos/AutoliftedFields02.hs b/tests/datacon/pos/AutoliftedFields02.hs
new file mode 100644
index 0000000000..994df82d8f
--- /dev/null
+++ b/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 -> Nat @-}
+f :: T -> Nat
+f (T x) = x