Merge pull request #2458 from ucsd-progsys/fd/measure-conflicts

Give precedence to export local measures over imported measures

liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs

@@ -114,7 +114,13 @@ makeTargetSpec cfg localVars lnameEnv lmap targetSrc bareSpec dependencies = do
     toLegacyDep (sm, ls) = (ModName SrcImport (Ghc.moduleName . Ghc.unStableModule $ sm), fromBareSpecLHName $ unsafeFromLiftedSpec ls)
 
     legacyDependencies :: [(ModName, BareSpec)]
-    legacyDependencies = map toLegacyDep . M.toList . getDependencies $ dependencies
+    legacyDependencies =
+      -- Dependencies are sorted lexicographically to make predictable which
+      -- logic names will have preference when exporting conflicting measures.
+      --
+      -- At the moment it is the measure from the last module after sorting.
+      -- But if there is a local conflicting measure, that one is used.
+      L.sortOn fst $ map toLegacyDep $ M.toList $ getDependencies dependencies
 
     -- Assumptions about local functions that are not exported aren't useful for
     -- other modules.
@@ -254,7 +260,9 @@ makeGhcSpec0 cfg ghcTyLookupEnv tcg instEnvs lenv localVars src lmap targetSpec
                     | v <- gsReflects refl
                     ]
                 , dataDecls = Bare.dataDeclSize mySpec $ dataDecls mySpec
-                , measures  = mconcat $ map Ms.measures $ mySpec : map snd dependencySpecs
+                  -- Placing mySpec at the end causes local measures to take precedence over
+                  -- imported measures when their names clash.
+                , measures  = mconcat $ map Ms.measures $ map snd dependencySpecs ++ [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
                   -- that 'lSpec1' doesn't contain the measures that we compute via 'makeHaskellMeasures',

liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs

@@ -524,7 +524,7 @@ collectUnhandledLiftedSpecLogicNames sp =
 collectLiftedSpecLogicNames :: LiftedSpec -> [LHName]
 collectLiftedSpecLogicNames sp =
     map fst (HS.toList $ liftedExpSigs sp) ++
-    map fst (HM.toList $ liftedMeasures sp)
+    map (fst . snd) (HM.toList $ liftedMeasures sp)
 
 -- | Resolves names in the logic namespace
 --

liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs

@@ -86,7 +86,7 @@ import qualified Data.HashMap.Lazy       as Lazy.M
 import qualified Data.HashMap.Strict     as M
 import           Data.HashMap.Strict     (HashMap)
 import           Data.Maybe
-import           Language.Haskell.Liquid.GHC.Misc (fSrcSpan)
+import           Language.Haskell.Liquid.GHC.Misc (dropModuleNames, fSrcSpan)
 import           Language.Haskell.Liquid.Name.LogicNameEnv
 import           Language.Haskell.Liquid.Types.DataDecl
 import           Language.Haskell.Liquid.Types.Errors
@@ -700,8 +700,15 @@ instance Monoid (Spec lname ty) where
 -- Apart from less fields, a 'LiftedSpec' /replaces all instances of lists with sets/, to enforce
 -- duplicate detection and removal on what we serialise on disk.
 data LiftedSpec = LiftedSpec
-  { liftedMeasures   :: HashMap LHName (MeasureV LHName LocBareTypeLHName (F.Located LHName))
-    -- ^ User-defined properties for ADTs
+  { -- | Measures (a.k.a.  user-defined properties for ADTs)
+    --
+    -- The key of the HashMap is the unqualified name of the measure.
+    -- Constructing such a map discards preceding measures with the same name
+    -- as later measures, which makes possible to predict which of a few
+    -- conflicting measures will be exported.
+    --
+    -- Tested in MeasureOverlapC.hs
+    liftedMeasures   :: HashMap F.Symbol (LHName, MeasureV LHName LocBareTypeLHName (F.Located LHName))
   , liftedExpSigs    :: HashSet (LHName, F.Sort)
     -- ^ Exported logic symbols originated from reflecting functions
   , liftedPrivateReflects :: HashSet F.LocSymbol
@@ -939,7 +946,7 @@ toLiftedSpec :: LogicNameEnv -> BareSpecLHName -> LiftedSpec
 toLiftedSpec lenv a = LiftedSpec
   { liftedMeasures   =
       M.fromList
-        [ (n, m)
+        [ (dropModuleNames $ logicNameToSymbol n, (n, m))
         | m <- measures a
         , let n = fromMaybe (panic (Just $ fSrcSpan (msName m)) "cannot find logic name") $
                     F.lookupSEnv (val $ msName m) (lneLHName lenv)
@@ -974,7 +981,7 @@ toLiftedSpec lenv a = LiftedSpec
 -- suitable for 'makeGhcSpec'.
 unsafeFromLiftedSpec :: LiftedSpec -> BareSpecLHName
 unsafeFromLiftedSpec a = Spec
-  { measures   = M.elems . liftedMeasures $ a
+  { measures   = map snd $ M.elems $ liftedMeasures a
   , expSigs    = S.toList . liftedExpSigs $ a
   , asmSigs    = S.toList . liftedAsmSigs $ a
   , asmReflectSigs = mempty

tests/basic/pos/MeasureOverlapA.hs

@@ -0,0 +1,8 @@
+-- | See "MeasureOverlapC".
+module MeasureOverlapA where
+
+{-@
+measure foo :: Bool -> Bool
+  foo False = False
+  foo True = True
+@-}

tests/basic/pos/MeasureOverlapB.hs

@@ -0,0 +1,12 @@
+-- | See "MeasureOverlapC".
+module MeasureOverlapB where
+
+import MeasureOverlapA
+
+{-@
+measure foo :: Bool -> Bool
+  foo False = True
+  foo True = False
+
+@-}
+

tests/basic/pos/MeasureOverlapC.hs

@@ -0,0 +1,13 @@
+-- | Tests that when names overlap, the local one is exported.
+--
+-- In this case, measure @foo@ is defined in both "MeasureOverlapB" and
+-- "MeasureOverlapA". Both definitions are in scope in "MeasureOverlapB",
+-- but "MeasureOverlapB" only exports its local @foo@ measure.
+--
+module MeasureOverlapC where
+
+import MeasureOverlapB
+
+{-@ lemma :: { foo False } @-}
+lemma :: ()
+lemma = ()

tests/basic/pos/MeasureOverlapD.hs

@@ -0,0 +1,6 @@
+-- | See "MeasureOverlapE".
+module MeasureOverlapD where
+
+import MeasureOverlapA
+import MeasureOverlapB
+

tests/basic/pos/MeasureOverlapE.hs

@@ -0,0 +1,14 @@
+-- | Tests that when names overlap, the one from the highest module
+-- lexicographically is exported.
+--
+-- In this case, measure @foo@ is defined in both "MeasureOverlapB" and
+-- "MeasureOverlapA". Both definitions are in scope in "MeasureOverlapD",
+-- but "MeasureOverlapD" only reexports @foo@ from "MeasureOverlapB".
+--
+module MeasureOverlapE where
+
+import MeasureOverlapD
+
+{-@ lemma :: { foo False } @-}
+lemma :: ()
+lemma = ()

tests/tests.cabal

@@ -2261,6 +2261,11 @@ executable basic-pos
                     , Inc04
                     , Infer00
                     , List00
+                    , MeasureOverlapA
+                    , MeasureOverlapB
+                    , MeasureOverlapC
+                    , MeasureOverlapD
+                    , MeasureOverlapE
                     , OpaqueRefl01
                     , OpaqueRefl02
                     , OpaqueRefl03A