Does Not Work!

src/Language/Haskell/Liquid/Bare.hs

@@ -326,7 +326,8 @@ makeGhcSpec0 cfg src lmap mspecsNoCls = do
     lSpec0   = makeLiftedSpec0 cfg src embs lmap mySpec0 
     embs     = makeEmbeds          src env ((name, mySpec0) : M.toList iSpecs0)
     dm       = Bare.tcDataConMap tycEnv0
-    (dg0, datacons, tycEnv0) = makeTycEnv0   cfg name env embs mySpec2 iSpecs2 
+    (dg0, datacons, tycEnv0') = makeTycEnv0   cfg name env embs mySpec2 iSpecs2
+    tycEnv0  = Bare.qualifyExpand env name rtEnv l [] tycEnv0' where l = F.dummyPos "expand-tycEnv0"
     -- extract name and specs
     env      = Bare.makeEnv cfg src lmap mspecsNoCls
     (mySpec0NoCls, iSpecs0) = splitSpecs name src mspecsNoCls
@@ -753,7 +754,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)]
@@ -1075,7 +1076,7 @@ makeTycEnv0 cfg myName env embs mySpec iSpecs = (diag0 <> diag1, datacons, Bare.
   })
   where
     (tcDds, dcs)   = conTys
-    (diag0, conTys) = withDiagnostics $ Bare.makeConTypes myName env specs 
+    (diag0, conTys) = (withDiagnostics $ Bare.makeConTypes myName env specs)
     specs         = (myName, mySpec) : M.toList iSpecs
     tcs           = Misc.snd3 <$> tcDds 
     tyi           = Bare.qualifyTopDummy env myName (makeTyConInfo embs fiTcs tycons)

src/Language/Haskell/Liquid/Bare/DataType.hs

@@ -42,7 +42,7 @@ import           Language.Haskell.Liquid.WiredIn
 
 import qualified Language.Haskell.Liquid.Measure        as Ms
 import qualified Language.Haskell.Liquid.Bare.Types     as Bare  
-import qualified Language.Haskell.Liquid.Bare.Resolve   as Bare 
+import qualified Language.Haskell.Liquid.Bare.Resolve   as Bare
 import           Text.Printf                     (printf)
 import Text.PrettyPrint ((<+>))
 
@@ -73,11 +73,14 @@ 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
@@ -412,7 +415,7 @@ left' es = Just (Left es)
 --   instead of the unlifted versions.
 
 canonizeDecls :: Bare.Env -> ModName -> [DataDecl] -> Bare.Lookup [DataDecl]
-canonizeDecls env name ds = do
+canonizeDecls env name ds = seq (F.tracepp "" ds) $ do
   kds <- forM ds $ \d -> do
            k <- dataDeclKey env name d 
            return (fmap (, d) k)
@@ -590,7 +593,7 @@ ofBDataCtorTc env name l l' tc αs ps πs _ctor@(DataCtor _c as _ xts res) c' =
     ts'           = Bare.ofBareType env name l (Just ps) <$> ts
     res'          = Bare.ofBareType env name l (Just ps) <$> res
     t0'           = dataConResultTy c' αs t0 res'
-    _cfg          = getConfig env 
+    _cfg          = getConfig env
     (yts, ot)     = qualifyDataCtor (not isGadt) name dLoc (zip xs ts', t0')
     zts           = zipWith (normalizeField c') [1..] (reverse yts)
     usedTvs       = S.fromList (ty_var_value <$> concatMap RT.freeTyVars (t0':ts'))
@@ -734,7 +737,7 @@ unDummy x i | x /= F.dummySymbol = x
             | otherwise          = F.symbol ("_cls_lq" ++ show i)
 
 makeRecordSelectorSigs :: Bare.Env -> ModName -> [Located DataConP] -> [(Ghc.Var, LocSpecType)]
-makeRecordSelectorSigs env name = checkRecordSelectorSigs . concatMap makeOne
+makeRecordSelectorSigs env name l = checkRecordSelectorSigs $ concatMap makeOne l
   where
   makeOne (Loc l l' dcp)
     | Just cls <- maybe_cls
@@ -770,4 +773,4 @@ makeRecordSelectorSigs env name = checkRecordSelectorSigs . concatMap makeOne
       -- FIXME: this is clearly imprecise, but the preds in the DataConP seem
       -- to be malformed. If we leave them in, tests/pos/kmp.hs fails with
       -- a malformed predicate application. Niki, help!!
-      dropPreds = fmap (\(MkUReft r _ps) -> MkUReft r mempty)
+      dropPreds = id -- fmap (\(MkUReft r _ps) -> MkUReft r mempty)

src/Language/Haskell/Liquid/Bare/Expand.hs

@@ -271,7 +271,7 @@ class Expand a where
 -- because the type alias entry inside 'BareRTEnv' mentioned the tuple (\"OneTyAlias\", \"{v:a | oneFunPred v}\") but
 -- the 'snd' element needed to be qualified as well, before trying to expand anything.
 ----------------------------------------------------------------------------------
-qualifyExpand :: (PPrint a, Expand a, Bare.Qualify a)
+qualifyExpand :: (Expand a, Bare.Qualify a)
               => Bare.Env -> ModName -> BareRTEnv -> F.SourcePos -> [F.Symbol] -> a -> a
 ----------------------------------------------------------------------------------
 qualifyExpand env name rtEnv l bs
@@ -382,6 +382,27 @@ expandBareSpec rtEnv l sp = sp
   }
   where f      = expand rtEnv l
 
+expandTycEnv :: BareRTEnv -> F.SourcePos -> Bare.TycEnv -> Bare.TycEnv
+expandTycEnv rtEnv l tycEnv = tycEnv
+  { Bare.tcSelMeasures = expand rtEnv l (Bare.tcSelMeasures tycEnv)
+  , Bare.tcDataCons = expand rtEnv l (Bare.tcDataCons tycEnv) }
+
+instance Expand Bare.TycEnv where
+  expand = expandTycEnv
+
+instance Expand DataConP where
+  expand rtEnv l dcp = dcp
+    { dcpTyArgs = fmap (expand rtEnv l) <$> (dcpTyArgs dcp)
+    , dcpTyRes = expand rtEnv l <$> (dcpTyRes dcp) }
+
+
+expandMeasure :: Expand ty => BareRTEnv -> F.SourcePos -> Measure ty Ghc.DataCon -> Measure ty Ghc.DataCon
+expandMeasure rtEnv l ms = ms
+  { msSort = expand rtEnv l (msSort ms) }
+
+instance Expand ty => Expand (Measure ty Ghc.DataCon) where
+  expand = expandMeasure
+
 expandBareType :: BareRTEnv -> F.SourcePos -> BareType -> BareType 
 expandBareType rtEnv _ = go 
   where

src/Language/Haskell/Liquid/Bare/Measure.hs

@@ -225,12 +225,14 @@ tyConDataName full tc
     vanillaTc  = Ghc.isVanillaAlgTyCon tc
     dcs        = Misc.sortOn F.symbol (Ghc.tyConDataCons tc)
 
+-- IMPORTANT
 dataConDecl :: Ghc.DataCon -> DataCtor
 dataConDecl d     = {- F.notracepp msg $ -} DataCtor dx (F.symbol <$> as) [] xts outT
   where
     isGadt        = not (Ghc.isVanillaDataCon d)
     -- msg           = printf "dataConDecl (gadt = %s)" (show isGadt)
-    xts           = [(Bare.makeDataConSelector Nothing d i, RT.bareOfType t) | (i, t) <- its ]
+    -- THIS TURNS IT INTO NAT'' IN THE DATACONDECL
+    xts           = [(Bare.makeDataConSelector Nothing d i, RT.bareOfTypeNoExpand t) | (i, t) <- its ]
     dx            = F.symbol <$> GM.locNamedThing d
     its           = zip [1..] ts
     (as,_ps,ts,t)  = Ghc.dataConSig d
@@ -296,7 +298,7 @@ bkDataCon permitTC dc nFlds  = (as, ts, (F.dummySymbol, classRFInfo permitTC, t,
   where
     ts                = RT.ofType <$> Misc.takeLast nFlds (map Ghc.irrelevantMult _ts)
     t                 = -- Misc.traceShow ("bkDataConResult" ++ GM.showPpr (dc, _t, _t0)) $
-                          RT.ofType  $ Ghc.mkTyConApp tc tArgs'
+                          RT.ofType $ Ghc.mkTyConApp tc tArgs'
     as                = makeRTVar . RT.rTyVar <$> (αs ++ αs')
     ((αs,αs',_,_,_ts,_t), _t0) = hammer dc
     tArgs'            = take (nArgs - nVars) tArgs ++ (Ghc.mkTyVarTy <$> αs)

src/Language/Haskell/Liquid/Bare/Resolve.hs

@@ -425,7 +425,17 @@ substEnv :: (F.Subable a) => Env -> ModName -> F.SourcePos -> [F.Symbol] -> a ->
 substEnv env name l bs = F.substa (qualifySymbol env name l bs) 
 
 instance Qualify SpecType where 
-  qualify x1 x2 x3 x4 x5 = emapReft (substFreeEnv x1 x2 x3) x4 x5            
+  qualify x1 x2 x3 x4 x5 = emapReft (substFreeEnv x1 x2 x3) x4 x5
+
+instance Qualify TycEnv where
+  qualify env name l bs tycEnv = tycEnv
+    { tcSelMeasures = qualify env name l bs (tcSelMeasures tycEnv)
+    , tcDataCons = qualify env name l bs (tcDataCons tycEnv) }
+
+instance Qualify DataConP where
+  qualify env name n bs dcp = dcp
+    { dcpTyArgs = qualify env name n bs <$> (dcpTyArgs dcp)
+    , dcpTyRes = qualify env name n bs <$> (dcpTyRes dcp) }
 
 instance Qualify BareType where 
   qualify x1 x2 x3 x4 x5 = emapReft (substFreeEnv x1 x2 x3) x4 x5 
@@ -914,7 +924,8 @@ bareTCApp :: (Expandable r)
 bareTCApp r (Loc l _ c) rs ts | Just rhs <- Ghc.synTyConRhs_maybe c
   = if (GM.kindTCArity c < length ts) 
       then Ex.throw err -- error (F.showpp err)
-      else tyApp (RT.subsTyVars_meet su $ RT.ofType rhs) (drop nts ts) rs r
+      -- STOPS EXPANSION of NAT'' to INT
+      else tyApp (RT.subsTyVars_meet su $ RT.ofTypeNoExpand (Ghc.mkTyConTy c)) (drop nts ts) rs r
     where
        tvs = [ v | (v, b) <- zip (GM.tyConTyVarsDef c) (Ghc.tyConBinders c), GM.isAnonBinder b]
        su  = zipWith (\a t -> (RT.rTyVar a, toRSort t, t)) tvs ts

src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs

@@ -94,7 +94,7 @@ measureSpecType allowTC v = go mkT [] [(1::Int)..] t
         | otherwise = exprReft  
     mkT xs          = MkUReft (mkR $ mkEApp f (EVar <$> reverse xs)) mempty
     f               = dummyLoc (symbol v) 
-    t               = ofType (GM.expandVarType v) :: SpecType
+    t               = ofTypeNoExpand (GM.expandVarType v) :: SpecType
     boolRes         =  isBool $ ty_res $ toRTypeRep t 
 
     go f args i (RAllT a t r)    = RAllT a (go f args i t) r 

src/Language/Haskell/Liquid/Types/RefType.hs

@@ -44,7 +44,7 @@ module Language.Haskell.Liquid.Types.RefType (
   , quantifyFreeRTy
 
   -- * RType constructors
-  , ofType, toType, bareOfType
+  , ofType, toType, bareOfType, ofTypeNoExpand, bareOfTypeNoExpand, ofTypeNoExpand', bareOfTypeNoExpand
   , bTyVar, rTyVar, rVar, rApp, gApp, rEx
   , symbolRTyVar, bareRTyVar
   , tyConBTyCon
@@ -1366,29 +1366,70 @@ subvPredicate :: (UsedPVar -> UsedPVar) -> Predicate -> Predicate
 subvPredicate f (Pr pvs) = Pr (f <$> pvs)
 
 --------------------------------------------------------------------------------
-ofType :: Monoid r => Type -> RRType r
+ofTypeNoExpand' :: Monoid r => Type -> RRType r
+--------------------------------------------------------------------------------
+ofTypeNoExpand'      = ofType_ specTyConv
+
+--------------------------------------------------------------------------------
+ofTypeNoExpand :: Monoid r => Type -> RRType r
 --------------------------------------------------------------------------------
-ofType      = ofType_ $ TyConv
+ofTypeNoExpand      = ofTypeNoExpand_ specTyConv
+
+
+specTyConv :: Monoid r => TyConv RTyCon RTyVar r
+specTyConv = TyConv
   { tcFVar  = rVar
   , tcFTVar = rTVar
   , tcFApp  = \c ts -> rApp c ts [] mempty
   , tcFLit  = ofLitType rApp
   }
 
+ofType :: Monoid r => Type -> RRType r
+ofType =  ofType_ specTyConv . expandTypeSynonyms
+
 --------------------------------------------------------------------------------
-bareOfType :: Monoid r => Type -> BRType r
+bareOfTypeNoExpand :: Monoid r => Type -> BRType r
 --------------------------------------------------------------------------------
-bareOfType  = ofType_ $ TyConv
+bareOfTypeNoExpand  = ofTypeNoExpand_ bareTyConv
+
+bareTyConv :: Monoid m => TyConv BTyCon BTyVar m
+bareTyConv = TyConv
   { tcFVar  = (`RVar` mempty) . BTV . symbol
   , tcFTVar = bTVar
   , tcFApp  = \c ts -> bApp c ts [] mempty
   , tcFLit  = ofLitType bApp
   }
 
+bareOfType :: Monoid r => Type -> BRType r
+bareOfType = ofType_ bareTyConv . expandTypeSynonyms
+
+ofTypeNoExpand_ :: Monoid r => TyConv c tv r -> Type -> RType c tv r
+ofTypeNoExpand_ tx = go
+  where
+    go (TyVarTy α)
+      = tcFVar tx α
+    go (FunTy _ _ τ τ')
+      = rFun dummySymbol (go τ) (go τ')
+    go (ForAllTy (Bndr α _) τ)
+      = RAllT (tcFTVar tx α) (go τ) mempty
+    go (TyConApp c τs)
+      -- | Just (αs, τ) <- Ghc.synTyConDefn_maybe c
+      -- = go (substTyWith αs τs τ)
+      | otherwise
+      = tcFApp tx c (go <$> τs) -- [] mempty
+    go (AppTy t1 t2)
+      = RAppTy (go t1) (go t2) mempty
+    go (LitTy x)
+      = tcFLit tx x
+    go (CastTy t _)
+      = go t
+    go (CoercionTy _)
+      = errorstar "Coercion is currently not supported"
+
 --------------------------------------------------------------------------------
 ofType_ :: Monoid r => TyConv c tv r -> Type -> RType c tv r
 --------------------------------------------------------------------------------
-ofType_ tx = go . expandTypeSynonyms
+ofType_ tx = go
   where
     go (TyVarTy α)
       = tcFVar tx α
@@ -1402,7 +1443,7 @@ ofType_ tx = go . expandTypeSynonyms
       | otherwise
       = tcFApp tx c (go <$> τs) -- [] mempty
     go (AppTy t1 t2)
-      = RAppTy (go t1) (ofType_ tx t2) mempty
+      = RAppTy (go t1) (go t2) mempty
     go (LitTy x)
       = tcFLit tx x
     go (CastTy t _)

tests/datacon/pos/AutoliftedFields000.hs

@@ -0,0 +1,23 @@
+{-@ LIQUID "--exact-data-cons" @-}
+
+-- data decl in LH is missing but uses a LH-refined type alias correctly
+
+module AutoliftedFields000 where
+
+{-@ type Nat'' = { v : Int | v >= 0 } @-}
+type Nat'' = Int
+
+data T = T { getT :: Nat'' }
+
+{-@ f :: Int -> Nat'' @-}
+f :: Int -> Nat''
+f = getT . T
+
+g :: Int -> Nat''
+g z = getT (T z)
+
+x :: T
+x = T 0
+
+y :: Nat''
+y = getT x