diff --git a/src/Language/Haskell/Liquid/Bare.hs b/src/Language/Haskell/Liquid/Bare.hs
index ff96ea4604..bb4a583be2 100644
--- a/src/Language/Haskell/Liquid/Bare.hs
+++ b/src/Language/Haskell/Liquid/Bare.hs
@@ -266,7 +266,7 @@ makeGhcSpec0 cfg src lmap mspecsNoCls = do
     , _gsLSpec  = finalLiftedSpec
                 { impSigs   = makeImports mspecs
                 , expSigs   = [ (F.symbol v, F.sr_sort $ Bare.varSortedReft embs v) | v <- gsReflects refl ]
-                , dataDecls = dataDecls mySpec2 
+                , dataDecls = dataDecls mySpec2
                 , measures  = Ms.measures mySpec
                   -- We want to export measures in a 'LiftedSpec', especially if they are
                   -- required to check termination of some 'liftedSigs' we export. Due to the fact
@@ -752,7 +752,7 @@ makeInlSigs env rtEnv
 
 makeMsrSigs :: Bare.Env -> BareRTEnv -> [(ModName, Ms.BareSpec)] -> [(Ghc.Var, LocSpecType)] 
 makeMsrSigs env rtEnv 
-  = makeLiftedSigs rtEnv (CoreToLogic.inlineSpecType (typeclass (getConfig env)))
+  = makeLiftedSigs rtEnv (CoreToLogic.measureSpecType (typeclass (getConfig env)))
   . makeFromSet "hmeas" Ms.hmeas env 
 
 makeLiftedSigs :: BareRTEnv -> (Ghc.Var -> SpecType) -> [Ghc.Var] -> [(Ghc.Var, LocSpecType)]
@@ -1172,7 +1172,7 @@ makeLiftedSpec name src _env refl sData sig qual myRTE lSpec0 = lSpec0
                        , isLocInFile srcF t
                     ]
   , Ms.axeqs      = gsMyAxioms refl 
-  , Ms.aliases    = F.notracepp "MY-ALIASES" $ M.elems . typeAliases $ myRTE
+  , Ms.aliases    = F.tracepp "MY-ALIASES" $ M.elems . typeAliases $ myRTE
   , Ms.ealiases   = M.elems . exprAliases $ myRTE 
   , Ms.qualifiers = filter (isLocInFile srcF) (gsQualifiers qual)
   }
diff --git a/src/Language/Haskell/Liquid/Bare/DataType.hs b/src/Language/Haskell/Liquid/Bare/DataType.hs
index 03f01eec3a..92b5ed01ac 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
@@ -336,7 +340,7 @@ fieldName d dp x
 
 makeDataFields :: F.TCEmb Ghc.TyCon -> F.FTycon -> [RTyVar] -> [(F.LocSymbol, SpecType)]
                -> [F.DataField]
-makeDataFields tce _c as xts = [ F.DField x (fSort t) | (x, t) <- xts]
+makeDataFields tce _c as xts = F.tracepp "dfields" [ F.DField x (fSort t) | (x, t) <- F.tracepp "xts" xts]
   where
     su    = zip (F.symbol <$> as) [0..]
     fSort = F.substVars su . F.mapFVar (+ (length as)) . RT.rTypeSort tce
diff --git a/src/Language/Haskell/Liquid/Bare/Expand.hs b/src/Language/Haskell/Liquid/Bare/Expand.hs
index af77169b1b..8b9617610f 100644
--- a/src/Language/Haskell/Liquid/Bare/Expand.hs
+++ b/src/Language/Haskell/Liquid/Bare/Expand.hs
@@ -327,7 +327,7 @@ instance Expand Body where
 instance Expand DataCtor where 
   expand rtEnv l c = c
     { dcTheta  = expand rtEnv l (dcTheta c) 
-    , dcFields = [(x, expand rtEnv l t) | (x, t) <- dcFields c ] 
+    , dcFields = F.tracepp "dcFields: postexpand" [(x, expand rtEnv l t) | (x, t) <- F.tracepp "dcFields: preexpand" $ dcFields c ] 
     , dcResult = expand rtEnv l (dcResult c)
     }
  
diff --git a/tests/datacon/neg/AutoliftedFields00.hs b/tests/datacon/neg/AutoliftedFields00.hs
new file mode 100644
index 0000000000..ac90a6bdc8
--- /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 -> { v : Int | v < 0 } @-}
+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..83f98ddfac
--- /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 -> 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