Merge pull request #1607 from ucsd-progsys/T1604

fix for #T1604

Author: nikivazou

src/Language/Haskell/Liquid/Bare.hs

@@ -442,6 +442,7 @@ makeSpecRefl cfg src menv specs env name sig tycEnv = SpRefl
     rflSyms      = S.fromList (getReflects specs)
     sigVars      = F.notracepp "SIGVARS" $ (fst3 <$> xtes)            -- reflects
                                         ++ (fst  <$> gsAsmSigs sig)   -- assumes
+                                        ++ (fst  <$> gsRefSigs sig)
                                       -- ++ (fst  <$> gsTySigs  sig)   -- measures 
 
     lmap         = Bare.reLMap env
@@ -462,11 +463,12 @@ getReflects  = fmap val . S.toList . S.unions . fmap (names . snd) . M.toList
 ------------------------------------------------------------------------------------------
 addReflSigs :: GhcSpecRefl -> GhcSpecSig -> GhcSpecSig
 ------------------------------------------------------------------------------------------
-addReflSigs refl sig = sig { gsAsmSigs = reflSigs ++ filter notReflected (gsAsmSigs sig) }
+addReflSigs refl sig = sig { gsRefSigs = reflSigs, gsAsmSigs = wreflSigs ++ filter notReflected (gsAsmSigs sig) }
   where 
-    reflSigs        = [ (x, t) | (x, t, _) <- gsHAxioms refl ]   
-    reflected       = fst <$> reflSigs
-    notReflected xt = (fst xt) `notElem` reflected
+    (wreflSigs, reflSigs)   = L.partition ((`elem` gsWiredReft refl) . fst) 
+                                 [ (x, t) | (x, t, _) <- gsHAxioms refl ]   
+    reflected       = fst <$> (wreflSigs ++ reflSigs)
+    notReflected xt = fst xt `notElem` reflected
 
 makeAutoInst :: Bare.Env -> ModName -> Ms.BareSpec -> M.HashMap Ghc.Var (Maybe Int)
 makeAutoInst env name spec = Misc.hashMapMapKeys (Bare.lookupGhcVar env name "Var") (Ms.autois spec)
@@ -478,6 +480,7 @@ makeSpecSig :: Config -> ModName -> Bare.ModSpecs -> Bare.Env -> Bare.SigEnv ->
 makeSpecSig cfg name specs env sigEnv tycEnv measEnv cbs = SpSig 
   { gsTySigs   = F.notracepp "gsTySigs"  tySigs 
   , gsAsmSigs  = F.notracepp "gsAsmSigs" asmSigs
+  , gsRefSigs  = [] 
   , gsDicts    = dicts 
   , gsMethods  = if noclasscheck cfg then [] else Bare.makeMethodTypes dicts (Bare.meClasses  measEnv) cbs 
   , gsInSigs   = mempty -- TODO-REBARE :: ![(Var, LocSpecType)]  

src/Language/Haskell/Liquid/Constraint/Init.hs

@@ -79,14 +79,16 @@ initEnv info
        (invs2, f42) <- mapSndM refreshArgs' $ makeAutoDecrDataCons dcsty' (gsAutosize (gsTerm sp)) dcs'
        let f4    = mergeDataConTypes tce (mergeDataConTypes tce f40 (f41 ++ f42)) (filter (isDataConId . fst) f2)
        let tx    = mapFst F.symbol . addRInv ialias . predsUnify sp
-       let bs    = (tx <$> ) <$> [f0 ++ f0' ++ fi, f1 ++ f1', f2, (F.notracepp "assumed" f3) ++ f3', f4, f5]
+       f6       <- (map tx . addPolyInfo') <$> (refreshArgs' $ vals gsRefSigs (gsSig sp))  
+       let bs    = (tx <$> ) <$> [f0 ++ f0' ++ fi, f1 ++ f1', f2, f3 ++ f3', f4, f5]
        modify $ \s -> s { dataConTys = f4 }
        lt1s     <- F.toListSEnv . cgLits <$> get
        let lt2s  = [ (F.symbol x, rTypeSort tce t) | (x, t) <- f1' ]
        let tcb   = mapSnd (rTypeSort tce) <$> concat bs
        let cbs   = giCbs . giSrc $ info
-       let γ0    = measEnv sp (head bs) cbs tcb lt1s lt2s (bs!!3) (bs!!5) hs info
-       γ  <- globalize <$> foldM (+=) γ0 ( [("initEnv", x, y) | (x, y) <- concat $ tail bs])
+       rTrue   <- mapM (mapSndM true) f6 
+       let γ0    = measEnv sp (head bs) cbs tcb lt1s lt2s (f6 ++ bs!!3) (bs!!5) hs info
+       γ  <- globalize <$> foldM (+=) γ0 ( [("initEnv", x, y) | (x, y) <- concat $ (rTrue:tail bs)])
        return γ {invs = is (invs1 ++ invs2)}
   where
     sp           = giSpec info
@@ -239,7 +241,7 @@ recSelectorsTy info = forM topVs $ \v -> (v,) <$> trueTy (varType v)
   where
     topVs        = filter isTop $ giDefVars (giSrc info)
     isTop v      = isExportedVar (giSrc info) v && not (v `S.member` sigVs) &&  isRecordSelector v
-    sigVs        = S.fromList [v | (v,_) <- gsTySigs sp ++ gsAsmSigs sp ++ gsInSigs sp]
+    sigVs        = S.fromList [v | (v,_) <- gsTySigs sp ++ gsAsmSigs sp ++ gsRefSigs sp ++ gsInSigs sp]
     sp           = gsSig . giSpec $ info
 
 
@@ -249,7 +251,7 @@ grtyTop info     = forM topVs $ \v -> (v,) <$> trueTy (varType v)
   where
     topVs        = filter isTop $ giDefVars (giSrc info)
     isTop v      = isExportedVar (giSrc info) v && not (v `S.member` sigVs) && not (isRecordSelector v)
-    sigVs        = S.fromList [v | (v,_) <- gsTySigs sp ++ gsAsmSigs sp ++ gsInSigs sp]
+    sigVs        = S.fromList [v | (v,_) <- gsTySigs sp ++ gsAsmSigs sp ++ gsRefSigs sp ++ gsInSigs sp]
     sp           = gsSig . giSpec $ info
 
 

src/Language/Haskell/Liquid/Constraint/Qualifier.hs

@@ -126,6 +126,7 @@ specBinders :: GhcInfo -> [(Var, LocSpecType)]
 specBinders info = mconcat
   [ gsTySigs  (gsSig  sp)
   , gsAsmSigs (gsSig  sp)
+  , gsRefSigs (gsSig  sp)
   , gsCtors   (gsData sp)
   , if info `hasOpt` scrapeInternals then gsInSigs (gsSig sp) else []
   ]

src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs

@@ -144,8 +144,8 @@ makeSimplify (x, t) = go $ specTypeToResultRef (F.eApps (F.EVar $ F.symbol x) (F
 makeEquations :: GhcSpec -> [F.Equation]
 makeEquations sp = [ F.mkEquation f xts (equationBody (F.EVar f) xArgs e mbT) t
                       | F.Equ f xts e t _ <- axioms 
-                      , let mbT            = M.lookup f sigs
                       , let xArgs          = F.EVar . fst <$> xts
+                      , let mbT            = if null xArgs then Nothing else M.lookup f sigs
                    ]
   where
     axioms       = gsMyAxioms refl ++ gsImpAxioms refl 

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

@@ -94,6 +94,7 @@ data GhcSpecQual = SpQual
 data GhcSpecSig = SpSig 
   { gsTySigs   :: ![(Var, LocSpecType)]           -- ^ Asserted Reftypes
   , gsAsmSigs  :: ![(Var, LocSpecType)]           -- ^ Assumed Reftypes
+  , gsRefSigs  :: ![(Var, LocSpecType)]           -- ^ Reflected Reftypes 
   , gsInSigs   :: ![(Var, LocSpecType)]           -- ^ Auto generated Signatures
   , gsNewTypes :: ![(TyCon, LocSpecType)]         -- ^ Mapping of 'newtype' type constructors with their refined types.
   , gsDicts    :: !(DEnv Var LocSpecType)            -- ^ Refined Classes from Instances 

tests/neg/T1604.hs

@@ -0,0 +1,21 @@
+{-@ LIQUID "--reflection" @-}
+{-@ LIQUID "--ple"        @-}
+
+data Val = V { val :: Int }
+{-@ data Val = V { val :: Int } @-}
+{-@ type ValN N = {v:Val | val v == N} @-}
+
+{-@ reflect ex1 @-}
+{-@ ex1 :: ValN 5 @-}
+ex1 :: Val
+ex1 = V 4
+
+
+{-@ test1 :: {v:Bool | v} @-}
+test1 = val ex1 == 6
+
+{-@ test2 :: () -> {v:() | val ex1 == 6} @-}
+test2 () = ()
+
+{-@ test3 :: () -> {v:() | 1 == 2} @-}
+test3 () = ()