liquidhaskell-boot 0.9.12.2 → 0.9.12.2.1

raw patch · 44 files changed

+1451/−1032 lines, 44 filesdep ~liquid-fixpointPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: liquid-fixpoint

API changes (from Hackage documentation)

Files

• liquidhaskell-boot.cabal +4/−4
• src-ghc/Liquid/GHC/API.hs +15/−2
• src-ghc/Liquid/GHC/API/Extra.hs +78/−0
• src/Language/Haskell/Liquid/Bare.hs +88/−49
• src/Language/Haskell/Liquid/Bare/Axiom.hs +5/−1
• src/Language/Haskell/Liquid/Bare/Check.hs +114/−39
• src/Language/Haskell/Liquid/Bare/Elaborate.hs +1/−3
• src/Language/Haskell/Liquid/Bare/Expand.hs +125/−91
• src/Language/Haskell/Liquid/Bare/Measure.hs +1/−1
• src/Language/Haskell/Liquid/Bare/Misc.hs +8/−5
• src/Language/Haskell/Liquid/Bare/Plugged.hs +3/−1
• src/Language/Haskell/Liquid/Bare/Resolve.hs +1/−1
• src/Language/Haskell/Liquid/Bare/Typeclass.hs +1/−1
• src/Language/Haskell/Liquid/Constraint/Env.hs +1/−1
• src/Language/Haskell/Liquid/Constraint/Generate.hs +100/−3
• src/Language/Haskell/Liquid/Constraint/Qualifier.hs +24/−6
• src/Language/Haskell/Liquid/Constraint/Relational.hs +6/−6
• src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs +29/−100
• src/Language/Haskell/Liquid/GHC/Interface.hs +0/−16
• src/Language/Haskell/Liquid/GHC/Plugin.hs +35/−22
• src/Language/Haskell/Liquid/GHC/TypeRep.hs +0/−5
• src/Language/Haskell/Liquid/LHNameResolution.hs +409/−253
• src/Language/Haskell/Liquid/Liquid.hs +15/−13
• src/Language/Haskell/Liquid/Measure.hs +2/−2
• src/Language/Haskell/Liquid/Misc.hs +3/−0
• src/Language/Haskell/Liquid/Name/LogicNameEnv.hs +3/−2
• src/Language/Haskell/Liquid/Parse.hs +36/−31
• src/Language/Haskell/Liquid/Transforms/ANF.hs +7/−7
• src/Language/Haskell/Liquid/Transforms/InlineAux.hs +1/−1
• src/Language/Haskell/Liquid/Types/Errors.hs +78/−9
• src/Language/Haskell/Liquid/Types/Names.hs +57/−6
• src/Language/Haskell/Liquid/Types/PredType.hs +1/−1
• src/Language/Haskell/Liquid/Types/PrettyPrint.hs +6/−0
• src/Language/Haskell/Liquid/Types/RType.hs +9/−3
• src/Language/Haskell/Liquid/Types/RefType.hs +37/−18
• src/Language/Haskell/Liquid/Types/Specs.hs +27/−20
• src/Language/Haskell/Liquid/Types/Types.hs +13/−8
• src/Language/Haskell/Liquid/UX/Annotate.hs +3/−3
• src/Language/Haskell/Liquid/UX/CmdLine.hs +73/−262
• src/Language/Haskell/Liquid/UX/Config.hs +6/−15
• src/Language/Haskell/Liquid/UX/Errors.hs +8/−8
• src/Language/Haskell/Liquid/UX/QuasiQuoter.hs +6/−5
• src/Language/Haskell/Liquid/WiredIn.hs +6/−1
• tests/Parser.hs +6/−7

@@ -1,6 +1,6 @@ cabal-version:      2.4 name:               liquidhaskell-boot-version:            0.9.12.2+version:            0.9.12.2.1 synopsis:           Liquid Types for Haskell description:        This package provides a plugin to verify Haskell programs.                     But most likely you should be using the [liquidhaskell package](https://hackage.haskell.org/package/liquidhaskell)@@ -122,7 +122,7 @@   hs-source-dirs:     src src-ghc src-ghc-9.10    build-depends:      base                 >= 4.11.1.0 && < 5-                    , Diff                 >= 0.3 && < 0.6+                    , Diff                 >= 0.3 && < 1.1                     , array                     , aeson                     , binary@@ -142,9 +142,9 @@                     , gitrev                     , hashable             >= 1.3 && < 1.6                     , hscolour             >= 1.22-                    , liquid-fixpoint      == 0.9.6.3.3+                    , liquid-fixpoint      == 0.9.6.3.5                     , mtl                  >= 2.1-                    , optparse-applicative < 0.19+                    , optparse-applicative < 0.20                     , githash                     , megaparsec           >= 8                     , pretty               >= 1.1

@@ -206,6 +206,7 @@     , liftedTypeKindTyConName     , listTyCon     , listTyConName+    , zonkAnyTyCon     , naturalTy     , nilDataCon     , stringTy@@ -403,6 +404,7 @@     , newTyConInstRhs     , piResultTys     , splitAppTys+    , splitForAllForAllTyBinders     , splitFunTy_maybe     , splitFunTys     , splitTyConApp@@ -476,7 +478,12 @@ import GHC.Core.Opt.OccurAnal         as Ghc     ( occurAnalysePgm ) import GHC.Core.TyCo.FVs              as Ghc (tyCoVarsOfCo, tyCoVarsOfType)-import GHC.Driver.Backend             as Ghc (interpreterBackend)+import GHC.Driver.Backend             as Ghc (backendName, interpreterBackend)+import GHC.Driver.Backend.Internal    as Ghc (BackendName(NoBackend))+import GHC.Driver.DynFlags            as Ghc+    ( DumpFlag(Opt_D_dump_timings)+    , dopt_set+    ) import GHC.Driver.Env                 as Ghc     ( HscEnv(hsc_NC, hsc_unit_env, hsc_dflags, hsc_plugins)     , Hsc@@ -826,7 +833,13 @@     , withBinBuffer     ) import GHC.Utils.Error                as Ghc (pprLocMsgEnvelope, withTiming)-import GHC.Utils.Logger               as Ghc (Logger(logFlags), putLogMsg)+import GHC.Utils.Logger               as Ghc+    ( LogFlags+    , Logger(logFlags)+    , putLogMsg+    , log_set_dopt+    , updateLogFlags+    ) import GHC.Utils.Outputable           as Ghc hiding ((<>)) import GHC.Utils.Panic                as Ghc (panic, throwGhcException, throwGhcExceptionIO) import GHC.Utils.Misc                 as Ghc (lengthAtLeast)

@@ -24,8 +24,14 @@   , thisPackage   , tyConRealArity   , untick+  , withTimingWallClock   ) where +import Control.Monad+import Control.Monad.IO.Class+import GHC.Conc (getAllocationCounter)+import Debug.Trace+import GHC.Clock (getMonotonicTimeNSec) import           Liquid.GHC.API.StableModule      as StableModule import GHC hiding (modInfoLookupName) import Data.Data (Data, gmapQr, gmapT)@@ -51,7 +57,10 @@ import GHC.Types.SrcLoc               as Ghc import GHC.Types.Unique               (getUnique, hasKey) +import GHC.Utils.Error                as Ghc+import GHC.Utils.Logger               as Ghc import GHC.Utils.Outputable           as Ghc hiding ((<>))+import qualified GHC.Utils.Outputable as Ghc  import GHC.Unit.Module @@ -263,3 +272,72 @@  minus_RDR :: RdrName minus_RDR = nameRdrName minusName++-- | A version of 'withTiming' that uses wall clock time instead of CPU time.+--+-- This version is copied and modified from GHC's 'GHC.Utils.Error.withTiming'+withTimingWallClock :: MonadIO m+           => Logger+           -> SDoc         -- ^ The name of the phase+           -> (a -> ())    -- ^ A function to force the result+                           -- (often either @const ()@ or 'rnf')+           -> m a          -- ^ The body of the phase to be timed+           -> m a+withTimingWallClock logger what force_result action =+    if logVerbAtLeast logger 2 || logHasDumpFlag logger Opt_D_dump_timings+    then do when printTimingsNotDumpToFile $ liftIO $+              logInfo logger $ withPprStyle defaultUserStyle $+                text "***" <+> what Ghc.<> colon+            let ctx = log_default_user_context (logFlags logger)+            alloc0 <- liftIO getAllocationCounter+            !start <- liftIO getMonotonicTimeNSec+            eventBegins ctx what+            recordAllocs alloc0+            !r <- action+            () <- pure $ force_result r+            eventEnds ctx what+            !end <- liftIO getMonotonicTimeNSec+            alloc1 <- liftIO getAllocationCounter+            recordAllocs alloc1+            -- recall that allocation counter counts down+            let alloc = alloc0 - alloc1+                time = (end - start) `div` 1000000++            when (logVerbAtLeast logger 2 && printTimingsNotDumpToFile)+                $ liftIO $ logInfo logger $ withPprStyle defaultUserStyle+                    (text "!!!" <+> what Ghc.<> colon <+> text "finished in"+                     <+> word64 time+                     <+> text "milliseconds"+                     Ghc.<> comma+                     <+> text "allocated"+                     <+> doublePrec 3 (realToFrac alloc / 1024 / 1024)+                     <+> text "megabytes")++            liftIO $ putDumpFileMaybe logger Opt_D_dump_timings "" FormatText+                    $ text $ showSDocOneLine ctx+                    $ hsep [ what Ghc.<> colon+                           , text "alloc=" Ghc.<> ppr alloc+                           , text "time=" Ghc.<> word64 time+                           ]+            pure r+     else action++    where -- Avoid both printing to console and dumping to a file (#20316).+          printTimingsNotDumpToFile =+            not (log_dump_to_file (logFlags logger))++          recordAllocs alloc =+            liftIO $ traceMarkerIO $ "GHC:allocs:" ++ show alloc++          eventBegins ctx w = do+            let doc = eventBeginsDoc ctx w+            liftIO $ traceMarkerIO doc+            liftIO $ traceEventIO doc++          eventEnds ctx w = do+            let doc = eventEndsDoc ctx w+            liftIO $ traceMarkerIO doc+            liftIO $ traceEventIO doc++          eventBeginsDoc ctx w = showSDocOneLine ctx $ text "GHC:started:" <+> w+          eventEndsDoc   ctx w = showSDocOneLine ctx $ text "GHC:finished:" <+> w

@@ -93,17 +93,18 @@                -> TargetDependencies                -> Ghc.TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec)) makeTargetSpec cfg localVars lnameEnv lmap targetSrc bareSpec dependencies = do-  let targDiagnostics     = Bare.checkTargetSrc cfg targetSrc+  let targDiagnostics     = Bare.checkTargetSrc cfg bareSpec targetSrc   let depsDiagnostics     = mapM (Bare.checkBareSpec . snd) legacyDependencies   let bareSpecDiagnostics = Bare.checkBareSpec bareSpec-  case targDiagnostics >> depsDiagnostics >> bareSpecDiagnostics of-   Left d | noErrors d -> secondPhase (allWarnings d)+  let stratDiagnostics   = Bare.checkStratTys bareSpec targetSrc+  case targDiagnostics >> depsDiagnostics >> bareSpecDiagnostics >> stratDiagnostics of+   Left d | noErrors d -> secondPhase [] (allWarnings d)    Left d              -> return $ Left d-   Right ()            -> secondPhase mempty+   Right stratNames   -> secondPhase stratNames mempty   where-    secondPhase :: [Warning] -> Ghc.TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))-    secondPhase phaseOneWarns = do-      diagOrSpec <- makeGhcSpec cfg lnameEnv localVars (fromTargetSrc targetSrc) lmap bareSpec legacyDependencies+    secondPhase :: [Ghc.Name] -> [Warning] -> Ghc.TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))+    secondPhase stratNames phaseOneWarns = do+      diagOrSpec <- makeGhcSpec stratNames cfg lnameEnv localVars (fromTargetSrc targetSrc) lmap bareSpec legacyDependencies       case diagOrSpec of         Left d -> return $ Left d         Right (warns, ghcSpec) -> do@@ -144,7 +145,8 @@ -- | @makeGhcSpec@ invokes @makeGhcSpec0@ to construct the @GhcSpec@ and then --   validates it using @checkGhcSpec@. --------------------------------------------------------------------------------------makeGhcSpec :: Config+makeGhcSpec :: [Ghc.Name]+            -> Config             -> LogicNameEnv             -> Bare.LocalVars             -> GhcSrc@@ -153,12 +155,12 @@             -> [(ModName, Ms.BareSpec)]             -> Ghc.TcRn (Either Diagnostics ([Warning], GhcSpec)) --------------------------------------------------------------------------------------makeGhcSpec cfg lenv localVars src lmap targetSpec dependencySpecs = do+makeGhcSpec stratNames cfg lenv localVars src lmap bareSpec dependencySpecs = do   ghcTyLookupEnv <- Bare.makeGHCTyLookupEnv (_giCbs src)   tcg <- Ghc.getGblEnv   instEnvs <- Ghc.tcGetInstEnvs-  (dg0, sp) <- makeGhcSpec0 cfg ghcTyLookupEnv tcg instEnvs lenv localVars src lmap targetSpec dependencySpecs-  let diagnostics = Bare.checkTargetSpec (targetSpec : map snd dependencySpecs)+  (dg0, sp) <- makeGhcSpec0 stratNames cfg ghcTyLookupEnv tcg instEnvs lenv localVars src lmap bareSpec dependencySpecs+  let diagnostics = Bare.checkTargetSpec (bareSpec : map snd dependencySpecs)                                          (toTargetSrc src)                                          (ghcSpecEnv sp)                                          (_giCbs src)@@ -195,7 +197,8 @@ --   lets us use aliases inside data-constructor definitions. ------------------------------------------------------------------------------------- makeGhcSpec0-  :: Config+  :: [Ghc.Name]+  -> Config   -> Bare.GHCTyLookupEnv   -> Ghc.TcGblEnv   -> Ghc.InstEnvs@@ -206,20 +209,24 @@   -> Ms.BareSpec   -> [(ModName, Ms.BareSpec)]   -> Ghc.TcRn (Diagnostics, GhcSpec)-makeGhcSpec0 cfg ghcTyLookupEnv tcg instEnvs lenv localVars src lmap targetSpec dependencySpecs = do+makeGhcSpec0 stratNames cfg ghcTyLookupEnv tcg instEnvs lenv localVars src lmap bareSpec dependencySpecs = do   globalRdrEnv <- Ghc.tcg_rdr_env <$> Ghc.getGblEnv   -- build up environments   tycEnv <- makeTycEnv1 env (tycEnv0, datacons) coreToLg simplifier   let tyi      = Bare.tcTyConMap   tycEnv   let sigEnv   = makeSigEnv  embs tyi (_gsExports src) rtEnv+  -- This spec is used to add lifted measures.   let lSpec1   = makeLiftedSpec1 cfg src tycEnv lmap mySpec1+  -- 'mySpec' and 'specs' contain the result of the first lifting stages, see [NOTE]: REFLECT-IMPORTS+  -- and the expanded aliases obtained using 'rtEnv'. 'myRTE' is a filtered 'rtEnv' used at the final+  -- lifting.   let mySpec   = mySpec2 <> lSpec1   let specs    = M.insert name mySpec iSpecs2-  let myRTE    = myRTEnv       src env sigEnv rtEnv+  let myRTE    = myRTEnv src env sigEnv rtEnv   -- NB: we first compute a measure environment w/o the opaque reflections, so that we can bootstrap   -- the signature `sig`. Then we'll add the opaque reflections before we compute `sData` and al.   let (dg1, measEnv0) = withDiagnostics $ makeMeasEnv      env tycEnv sigEnv       specs-  let (dg2, (specInstances, sig)) = withDiagnostics $ makeSpecSig cfg name mySpec iSpecs2 env sigEnv tycEnv measEnv0 (_giCbs src)+  let (dg2, (specInstances, sig)) = withDiagnostics $ makeSpecSig stratNames cfg name mySpec iSpecs2 env sigEnv tycEnv measEnv0 (_giCbs src)   elaboratedSig <-     if allowTC then Bare.makeClassAuxTypes (elaborateSpecType coreToLg simplifier) datacons instMethods                               >>= elaborateSig sig@@ -282,15 +289,34 @@                   -- Preserve rinstances.                 , asmReflectSigs = Ms.asmReflectSigs mySpec                 , reflects = Ms.reflects mySpec0-                , cmeasures  = mconcat $ map Ms.cmeasures $ map snd dependencySpecs ++ [targetSpec]-                , embeds = Ms.embeds targetSpec+                , cmeasures  = mconcat $ map Ms.cmeasures $ map snd dependencySpecs ++ [bareSpec]+                , embeds = Ms.embeds bareSpec                 , privateReflects = mconcat $ map (privateReflects . snd) mspecs-                , defines = Ms.defines targetSpec+                , defines = Ms.defines bareSpec                 , usedDataCons = usedDcs+                  -- Placing the @bareSpec@ at the end causes local aliases+                  -- to take precedence over imported ones when their names clash.+                  -- Alternatively, the last among @dependencySpecs@ (which is+                  -- ordered lexcographically) is picked.+                  -- See @tests/name/pos/ImportedTypeAlias.hs@+                , aliases = M.elems $ M.fromList $+                    [ (lhNameToUnqualifiedSymbol (val . rtName $ rt) , rt)+                    | rt <- concat $+                        map (aliases . snd) dependencySpecs +++                        [expandedAliasesOf myRTE typeAliases $ aliases bareSpec]+                    ]+                , ealiases = M.elems $ M.fromList $+                    [ (lhNameToUnqualifiedSymbol (val . rtName $ rt) , rt)+                    | rt <- concat $+                        map (ealiases . snd) dependencySpecs +++                        [expandedAliasesOf myRTE exprAliases $ ealiases mySpec1']+                    ]                 }     })   where     thisModule = Ghc.tcg_mod tcg+    expandedAliasesOf myRTE fld = Mb.mapMaybe ((`M.lookup` fld myRTE) . val . rtName)+     -- typeclass elaboration      coreToLg ce =@@ -322,24 +348,30 @@     simplifier :: Ghc.CoreExpr -> Ghc.TcRn Ghc.CoreExpr     simplifier = pure -- no simplification     allowTC  = typeclass cfg+    -- Specs with type and expression aliases expanded.     mySpec2  = Bare.expand rtEnv (F.dummyPos "expand-mySpec2") mySpec1     iSpecs2  = Bare.expand rtEnv (F.dummyPos "expand-iSpecs2") (M.fromList dependencySpecs)-    rtEnv    = Bare.makeRTEnv env name mySpec1 dependencySpecs lmap+    -- Environment for alias lookup and expansion.+    rtEnv    = Bare.makeRTEnv lenv name mySpec1' dependencySpecs     mspecs   = (name, mySpec0) : dependencySpecs+    -- mySpec0 adds typeclass methods to the bare spec.     (mySpec0, instMethods)  = if allowTC-                              then Bare.compileClasses src env (name, targetSpec) dependencySpecs-                              else (targetSpec, [])+                              then Bare.compileClasses src env (name, bareSpec) dependencySpecs+                              else (bareSpec, [])+    mySpec1' = addDefinesToExprAliases env lmap mySpec1+    -- Ready for alias expansion.     mySpec1  = mySpec0 <> lSpec0+    -- This spec just has the 'ealiases' (with Haskell inlines) and 'dataDecls' fields.     lSpec0   = makeLiftedSpec0 cfg src embs lmap mySpec0     embs     = makeEmbeds          src ghcTyLookupEnv (mySpec0 : map snd dependencySpecs)     dm       = Bare.tcDataConMap tycEnv0     (dg0, datacons, tycEnv0) = makeTycEnv0   cfg name env embs mySpec2 iSpecs2-    env      = Bare.makeEnv cfg ghcTyLookupEnv dataConIds tcg instEnvs localVars src lmap ((name, targetSpec) : dependencySpecs)+    env      = Bare.makeEnv cfg ghcTyLookupEnv dataConIds tcg instEnvs localVars src lmap ((name, bareSpec) : dependencySpecs)     -- check barespecs     name     = F.notracepp ("ALL-SPECS" ++ zzz) $ _giTargetMod  src     zzz      = F.showpp (fst <$> mspecs) -    usedDcs  = collectAllDataCons (_giCbs src) $ targetSpec : map snd dependencySpecs+    usedDcs  = collectAllDataCons (_giCbs src) $ bareSpec : map snd dependencySpecs     dataConIds =       [ Ghc.dataConWorkId dc       | lhn <- S.toList usedDcs@@ -428,6 +460,19 @@     where       symTc = Mb.maybeToList . either (const Nothing) Just . Bare.lookupGhcTyConLHName env +-- | See [NOTE:EXPRESSION-ALIASES]+addDefinesToExprAliases :: Bare.Env -> LogicMap -> Ms.BareSpec -> Ms.BareSpec+addDefinesToExprAliases env lmap mySpec =+  mySpec {+    Ms.ealiases = Ms.ealiases mySpec +++      if typeclass (getConfig env) then []+      -- lmap expansion happens during elaboration+      -- this clearly breaks things if a signature+      -- contains lmap functions but never gets+      -- elaborated+      else [ e | (_, xl) <- M.toList (lmSymDefs lmap), let e = lmapEAlias xl ]+    }+ -------------------------------------------------------------------------------- -- | [NOTE]: REFLECT-IMPORTS --@@ -454,7 +499,8 @@ -- This is because we need the inlines to build the @BareRTEnv@ which then -- does the alias @expand@ business, that in turn, lets us build the DataConP, -- i.e. the refined datatypes and their associate selectors, projectors etc,--- that are needed for subsequent stages of the lifting.+-- that are needed for subsequent stages of the lifting. Here is relevant to+-- [NOTE:EXPRESSION-ALIASES]. -------------------------------------------------------------------------------- makeLiftedSpec0 :: Config -> GhcSrc -> F.TCEmb Ghc.TyCon -> LogicMap -> Ms.BareSpec                 -> Ms.BareSpec@@ -819,10 +865,10 @@   -----------------------------------------------------------------------------------------makeSpecSig :: Config -> ModName -> Ms.BareSpec -> Bare.ModSpecs -> Bare.Env -> Bare.SigEnv -> Bare.TycEnv -> Bare.MeasEnv -> [Ghc.CoreBind]+makeSpecSig :: [Ghc.Name] -> Config -> ModName -> Ms.BareSpec -> Bare.ModSpecs -> Bare.Env -> Bare.SigEnv -> Bare.TycEnv -> Bare.MeasEnv -> [Ghc.CoreBind]             -> Bare.Lookup ([RInstance LocBareType], GhcSpecSig) -----------------------------------------------------------------------------------------makeSpecSig cfg name mySpec specs env sigEnv tycEnv measEnv cbs = do+makeSpecSig stratNames cfg name mySpec specs env sigEnv tycEnv measEnv cbs = do   mySigs     <- makeTySigs  env sigEnv name mySpec   aSigs      <- F.notracepp ("makeSpecSig aSigs " ++ F.showpp name) $ makeAsmSigs env sigEnv name allSpecs   let asmSigs =  Bare.tcSelVars tycEnv ++ aSigs@@ -837,6 +883,7 @@   asmRel     <-  makeRelation env name sigEnv (Ms.asmRel mySpec)   return (instances, SpSig     { gsTySigs   = tySigs+    , gsStratCtos = stratNames     , gsAsmSigs  = asmSigs     , gsAsmReflects = bimap getVar getVar <$> concatMap (asmReflectSigs . snd) allSpecs     , gsRefSigs  = []@@ -1373,7 +1420,6 @@                        , isLocInFile srcF t                     ]   , Ms.axeqs      = gsMyAxioms refl-  , Ms.aliases    = F.notracepp "MY-ALIASES" $ M.elems . typeAliases $ myRTE   , Ms.ealiases   = M.elems . exprAliases $ myRTE   , Ms.qualifiers = filter (isLocInFile srcF) (gsQualifiers qual)   }@@ -1386,7 +1432,6 @@     xbs           = toBare <$> reflTySigs     reflTySigs    = [(x, t) | (x,t,_) <- gsHAxioms refl]     reflVars      = S.fromList (fst <$> reflTySigs)-    -- myAliases fld = M.elems . fld $ myRTE     srcF          = _giTarget src      isLocalName = \case@@ -1418,42 +1463,36 @@   ----------------------------------------------------------------------------------- | @myRTEnv@ slices out the part of RTEnv that was generated by aliases defined---   in the _target_ file, "cooks" the aliases (by conversion to SpecType), and---   then saves them back as BareType.+-- | @myRTEnv@ "cooks" the type aliases by converting them to SpecType and then+--   back to BareType. -------------------------------------------------------------------------------- myRTEnv :: GhcSrc -> Bare.Env -> Bare.SigEnv -> BareRTEnv -> BareRTEnv-myRTEnv src env sigEnv rtEnv = mkRTE tAs' eAs+myRTEnv src env sigEnv rtEnv = rtEnv { typeAliases = M.fromList [ (aName a, a) | a <- tAs' ] }   where-    tAs'                     = normalizeBareAlias env sigEnv name <$> tAs-    tAs                      = myAliases typeAliases-    eAs                      = myAliases exprAliases-    myAliases fld            = filter (isLocInFile srcF) . M.elems . fld $ rtEnv-    srcF                     = _giTarget    src-    name                     = _giTargetMod src--mkRTE :: [Located (RTAlias x a)] -> [Located (RTAlias F.Symbol F.Expr)] -> RTEnv x a-mkRTE tAs eAs   = RTE-  { typeAliases = M.fromList [ (aName a, a) | a <- tAs ]-  , exprAliases = M.fromList [ (aName a, a) | a <- eAs ]-  }-  where aName   = rtName . F.val+    tAs'  = normalizeBareAlias env sigEnv modName <$> tAs+    tAs   = M.elems . typeAliases $ rtEnv+    modName  = _giTargetMod src+    aName = F.val . rtName -normalizeBareAlias :: Bare.Env -> Bare.SigEnv -> ModName -> Located BareRTAlias-                   -> Located BareRTAlias-normalizeBareAlias env sigEnv name lx = fixRTA <$> lx+-- | Prepare an alias for constraint checking by /fixing/ its body and type argument names.+normalizeBareAlias :: Bare.Env -> Bare.SigEnv -> ModName -> BareRTAlias+                   -> BareRTAlias+normalizeBareAlias env sigEnv name a = fixRTA a   where     fixRTA  :: BareRTAlias -> BareRTAlias     fixRTA  = mapRTAVars fixArg . fmap fixBody +    -- | Uses GHC to assign arguments a unique symbol by lifting them as local 'Type' variables and back.     fixArg  :: Symbol -> Symbol     fixArg  = F.symbol . GM.symbolTyVar +    -- | Completely /cooks/ the body of a type alias by conversion to 'SpecType'+    -- and back. At this point they have been expanded already.     fixBody :: BareType -> BareType     fixBody = Bare.specToBare             . F.val             . Bare.cookSpecType env sigEnv name Bare.RawTV-            . F.atLoc lx+            . F.atLoc (rtName a)   withDiagnostics :: (Monoid a) => Bare.Lookup a -> (Diagnostics, a)

@@ -45,6 +45,7 @@ import Data.Function (on) import qualified Data.Map as Map import qualified Data.HashMap.Strict as M+import System.IO.Unsafe (unsafePerformIO)  findDuplicatePair :: Ord k => (a -> k) -> [a] -> Maybe (a, a) findDuplicatePair key xs =@@ -113,8 +114,11 @@   else     Ex.throw $ mkError actual $       show qPretended ++ " and " ++ show qActual ++ " should have the same type. But " ++-      "types " ++ F.showpp pretendedTy ++ " and " ++ F.showpp actualTy  ++ " do not match."+      "types\n\n" ++ showType pretendedTy ++ "\n\n and\n\n" ++ showType actualTy  ++ "\n\ndo not match."   where+    showType = Ghc.showPpr+      (unsafePerformIO $ Ghc.reflectGhc Ghc.getDynFlags $ gtleSession $ reTyLookupEnv env)+     at = val $ strengthenSpecWithMeasure sig env actualV pretended{val=qPretended}      -- Get the Ghc.Var's of the actual and pretended function names

@@ -3,16 +3,18 @@ {-# LANGUAGE TupleSections       #-} {-# LANGUAGE RecordWildCards     #-} {-# LANGUAGE OverloadedStrings   #-}+{-# LANGUAGE DeriveTraversable   #-}+ {-# OPTIONS_GHC -Wno-x-partial #-}  module Language.Haskell.Liquid.Bare.Check   ( checkTargetSpec   , checkBareSpec   , checkTargetSrc+  , checkStratTys   , tyCompat   ) where - import           Language.Haskell.Liquid.Constraint.ToFixpoint  import           Liquid.GHC.API                   as Ghc hiding ( Located@@ -34,6 +36,7 @@ import qualified Language.Fixpoint.Misc                    as Misc import           Language.Fixpoint.SortCheck               (ElabM, checkSorted, checkSortedReftFull, checkSortFull) import qualified Language.Fixpoint.Types                   as F+import qualified Language.Fixpoint.Types.Config            as FC import qualified Language.Haskell.Liquid.GHC.Misc          as GM import           Language.Haskell.Liquid.GHC.Play          (getNonPositivesTyCon) import           Language.Haskell.Liquid.Misc              (condNull, thd5, foldMapM)@@ -53,29 +56,103 @@ import qualified Language.Haskell.Liquid.Bare.Types        as Bare import qualified Language.Haskell.Liquid.Bare.Resolve      as Bare import           Language.Haskell.Liquid.UX.Config-import Language.Fixpoint.Types.Config (ElabFlags (ElabFlags), solverFlags)-+-- import Language.Fixpoint.Types.Config (ElabFlags (ElabFlags))  ---------------------------------------------------------------------------------------------- -- | Checking TargetSrc ------------------------------------------------------------------------ -----------------------------------------------------------------------------------------------checkTargetSrc :: Config -> TargetSrc -> Either Diagnostics ()-checkTargetSrc cfg spec+checkTargetSrc :: Config -> BareSpec -> TargetSrc -> Either Diagnostics ()+checkTargetSrc cfg bare spec   |  nopositivity cfg   || nopositives == emptyDiagnostics   = Right ()   | otherwise   = Left nopositives-  where nopositives = checkPositives (gsTcs spec)+  where nopositives = checkPositives bare $ gsTcs spec +isStratifiedTyCon :: BareSpec -> TyCon -> Bool+isStratifiedTyCon bs tc = Ghc.tyConName tc `elem` sn+  where sn = mapMaybe (getLHGHCName . F.val) $ S.toList $ stratified bs -checkPositives :: [TyCon] -> Diagnostics-checkPositives tys = mkDiagnostics [] $ mkNonPosError (getNonPositivesTyCon tys)+checkPositives :: BareSpec -> [TyCon] -> Diagnostics+checkPositives bare tys = mkDiagnostics []+                        $ mkNonPosError+                        $ filter (not . isStratifiedTyCon bare . fst)+                        $ getNonPositivesTyCon tys  mkNonPosError :: [(TyCon, [DataCon])]  -> [Error] mkNonPosError tcs = [ ErrPosTyCon (getSrcSpan tc) (pprint tc) (pprint dc <+> ":" <+> pprint (dataConRepType dc))                     | (tc, dc:_) <- tcs] +--------------------------------------------------+-- | Checking that stratified ctors are present --+--------------------------------------------------++--- | Like 'Either' but the 'Semigroup' instance combines the failure+--- | values.+data Validation e a+  = Failure e+  | Success a+  deriving (Show, Eq, Functor, Foldable, Traversable)++instance (Semigroup e, Semigroup a) => Semigroup (Validation e a) where+  Failure e1 <> Failure e2 = Failure (e1 <> e2)+  Failure e  <> _          = Failure e+  _          <> Failure e  = Failure e+  Success x  <> Success y  = Success (x <> y)++instance (Semigroup e, Monoid a) => Monoid (Validation e a) where+  mempty = Success mempty+  mappend = (<>)++valToEither :: Validation e a -> Either e a+valToEither (Failure e) = Left e+valToEither (Success x) = Right x++-- | Check that all stratified types have their constructors+-- defined with refinement type signatures in the BareSpec.+--+-- Yields the names of the data constructors of the stratified types.+checkStratTys :: BareSpec -> TargetSrc -> Either Diagnostics [Name]+checkStratTys bare spec =+  valToEither+  $ foldMap (checkStratTy bare)+  $ mapMaybe (traverse (findTyCon (gsTcs spec)))+  $ S.toList $ stratified bare++-- | Find the TyCon corresponding to the given LHName in the given list of TyCons+findTyCon :: [TyCon] -> LHName -> Maybe TyCon+findTyCon tcs nm = do+  c <- getLHGHCName nm+  L.find ((== c) . Ghc.tyConName) tcs++-- | Check that the given TyCon is an ADT and that all its constructors+-- have refinements in the BareSpec.+checkStratTy :: BareSpec -> Located TyCon -> Validation Diagnostics [Name]+checkStratTy spec ltycon =+  case tyConDataCons_maybe (val ltycon) of+    Just ctors -> foldMap (checkStratCtor ltycon spec) ctors+    Nothing    -> Failure $ mkDiagnostics mempty [ err ]+  where+    pos = GM.sourcePos2SrcSpan (loc ltycon) (locE ltycon)+    err = ErrStratNotAdt pos (pprint (Ghc.tyConName $ val ltycon))++-- | Check that the given DataCon has a refinement type signature in the BareSpec.+--+-- Yields the names of the data constructors that are stratified.+checkStratCtor :: Located TyCon -> BareSpec -> DataCon -> Validation Diagnostics [Name]+checkStratCtor ltycon spec datacon+  | hasRefinementTypeSignature datacon (map (val . fst) $ sigs spec)+  = Success [ dataConName datacon ]+  | otherwise = Failure $ mkDiagnostics mempty [ err ]+  where+    pos = GM.sourcePos2SrcSpan (loc ltycon) (locE ltycon)+    err = ErrStratNotRefCtor pos (pprint $ dataConName datacon) (pprint $ Ghc.tyConName $ val ltycon)+    hasRefinementTypeSignature :: DataCon -> [LHName] -> Bool+    hasRefinementTypeSignature dc lns =+      dataConName dc `elem` mapMaybe getLHGHCName lns++ ---------------------------------------------------------------------------------------------- -- | Checking BareSpec ------------------------------------------------------------------------ ----------------------------------------------------------------------------------------------@@ -166,8 +243,8 @@                      -- TODO-REBARE ++ checkQualifiers env                                       (gsQualifiers (gsQual sp))                      <> checkDuplicate                                            (gsAsmSigs    (gsSig tsp))                      <> checkDupIntersect                                         (gsTySigs (gsSig tsp)) (gsAsmSigs (gsSig tsp))-                     <> checkRTAliases "Type Alias" env            tAliases-                     <> checkRTAliases "Pred Alias" env            eAliases+                     <> checkRTAliases "Type Alias" env myTAliases+                     <> checkRTAliases "Pred Alias" env myPAliases                      -- ++ _checkDuplicateFieldNames                   (gsDconsP sp)                      -- NV TODO: allow instances of refined classes to be refined                      -- but make sure that all the specs are checked.@@ -179,10 +256,11 @@                           then mempty                           else checkConstructorRefinement (gsTySigs $ gsSig tsp) -    _rClasses         = concatMap Ms.classes specs-    _rInsts           = concatMap Ms.rinstance specs-    tAliases          = concat [Ms.aliases sp  | sp <- specs]-    eAliases          = concat [Ms.ealiases sp | sp <- specs]+    _rClasses        = concatMap Ms.classes specs+    _rInsts          = concatMap Ms.rinstance specs+    -- Duplicate alias (definition) is checked within the bare spec only.+    myTAliases       = Ms.aliases (head specs)+    myPAliases       = Ms.ealiases (head specs)     emb              = gsTcEmbeds (gsName tsp)     tcEnv            = gsTyconEnv (gsName tsp)     ms               = gsMeasures (gsData tsp)@@ -194,9 +272,11 @@     noPrune          = not (pruneFlag tsp)     txCtors ts       = [(v, fmap (fmap (fmap (F.filterUnMatched temps))) t) | (v, t) <- ts]     temps            = F.makeTemplates $ gsUnsorted $ gsData tsp-    ef               = maybe (ElabFlags False) solverFlags $ smtsolver $ getConfig tsp-    -- env'             = L.foldl' (\e (x, s) -> insertSEnv x (RR s mempty) e) env wiredSortedSyms+    ef               = mkElabFlags (smtsolver $ getConfig tsp) +mkElabFlags :: Maybe FC.SMTSolver -> FC.ElabFlags+mkElabFlags Nothing    = FC.ElabFlags False False+mkElabFlags (Just slv) = FC.mkElabFlags slv False   -- | Tests that the returned refinement type of data constructors has predicate @True@ or @prop v == e@.@@ -222,11 +302,7 @@     validRef (F.Reft (_, F.PTrue))                       = True     -- Prop foo from ProofCombinators-    validRef (F.Reft (v, F.PAtom F.Eq (F.EApp (F.EVar n) (F.EVar v')) _))-      | n == "Language.Haskell.Liquid.ProofCombinators.prop"-      , v == v'-      = True-    validRef _ = False+    validRef n = isJust $ getPropIndex n      isCtorName x = case idDetails x of       DataConWorkId _ -> True@@ -267,7 +343,7 @@     vtes           = [ (x, (t, es)) | (x, t) <- gsTySigs sig, let es = M.lookup x vExprs]     vExprs         = M.fromList  [ (x, es) | (x, _, es) <- gsTexprs sig ] -    checkVisitor  :: ElabFlags -> CoreVisitor (F.SEnv F.SortedReft) Diagnostics+    checkVisitor  :: FC.ElabFlags -> CoreVisitor (F.SEnv F.SortedReft) Diagnostics     checkVisitor ef = CoreVisitor                        { envF  = \env v     -> F.insertSEnv (F.symbol v) (vSort v) env                        , bindF = \env acc v -> runReader (errs env v) ef <> acc@@ -305,7 +381,7 @@                                                        $+$   msg)                                  (pprint (tcpCon tcp)) -    go :: ElabFlags -> TyConP -> Maybe ((F.Symbol -> F.Expr, TyConP), Doc)+    go :: FC.ElabFlags -> TyConP -> Maybe ((F.Symbol -> F.Expr, TyConP), Doc)     go ef tcp = case tcpSizeFun tcp of                Nothing                   -> Nothing                Just f | isWiredInLenFn f -> Nothing -- Skip the check.@@ -326,7 +402,8 @@          -> F.SEnv F.SortedReft          -> (Maybe Var, LocSpecType)          -> ElabM Diagnostics-checkInv allowHO bsc emb tcEnv env (_, t) = checkTy allowHO bsc err emb tcEnv env t+checkInv allowHO bsc emb tcEnv env (_, t) =+  checkTy allowHO bsc err emb tcEnv env t   where     err              = ErrInvt (GM.sourcePosSrcSpan $ loc t) (val t) @@ -363,7 +440,7 @@   -- FIXME: Should _ be removed if it isn't used?-checkRTAliases :: String -> t -> [Located (RTAlias s a)] -> Diagnostics+checkRTAliases :: String -> t -> [RTAlias s a] -> Diagnostics checkRTAliases msg _ as = err1s   where     err1s               = checkDuplicateRTAlias msg as@@ -377,7 +454,8 @@           -> F.SEnv F.SortedReft           -> (v, LocSpecType)           -> ElabM Diagnostics-checkBind allowHO bsc s emb tcEnv env (v, t) = checkTy allowHO bsc msg emb tcEnv env t+checkBind allowHO bsc s emb tcEnv env (v, t) =+  checkTy allowHO bsc msg emb tcEnv env t   where     msg                      = ErrTySpec (GM.fSrcSpan t) (Just s) (pprint v) (val t) @@ -399,10 +477,10 @@     -- mkErr   = uncurry (\ e d -> ErrTermSpec (GM.sourcePosSrcSpan l) (pprint v) (text "ill-sorted" ) e t d)     -- mkErr'  = uncurry (\ e d -> ErrTermSpec (GM.sourcePosSrcSpan l) (pprint v) (text "non-numeric") e t d) -    go :: ElabFlags -> [F.Located F.Expr] -> Maybe (F.Expr, Doc)+    go :: FC.ElabFlags -> [F.Located F.Expr] -> Maybe (F.Expr, Doc)     go ef     = L.foldl' (\err e -> err <|> (val e,) <$> runReader (checkSorted (F.srcSpan e) env' (val e)) ef)     Nothing -    go' :: ElabFlags -> [F.Located F.Expr] -> Maybe (F.Expr, Doc)+    go' :: FC.ElabFlags -> [F.Located F.Expr] -> Maybe (F.Expr, Doc)     go' ef    = L.foldl' (\err e -> err <|> (val e,) <$> runReader (checkSorted (F.srcSpan e) env' (cmpZero e)) ef) Nothing      env'    = F.sr_sort <$> L.foldl' (\e (x,s) -> F.insertSEnv x s e) env xts@@ -456,15 +534,15 @@     xts' = F.notracepp "XTS" $ filter (not . (`elem` cls) . fst) xts     cls  = F.notracepp "CLS" cms -checkDuplicateRTAlias :: String -> [Located (RTAlias s a)] -> Diagnostics+checkDuplicateRTAlias :: String -> [RTAlias s a] -> Diagnostics checkDuplicateRTAlias s tas = mkDiagnostics mempty (map mkError dups)   where-    mkError xs@(x:_)          = ErrDupAlias (GM.fSrcSpan x)-                                          (text s)-                                          (pprint . rtName . val $ x)-                                          (GM.fSrcSpan <$> xs)-    mkError []                = panic Nothing "mkError: called on empty list"-    dups                    = [z | z@(_:_:_) <- groupDuplicatesOn (rtName . val) tas]+    mkError xs@(x:_) = ErrDupAlias (GM.fSrcSpan $ rtName x)+                                   (text s)+                                   (pprint $ rtName x)+                                   (GM.fSrcSpan . rtName <$> xs)+    mkError []       = panic Nothing "mkError: called on empty list"+    dups             = [z | z@(_:_:_) <- groupDuplicatesOn (lhNameToUnqualifiedSymbol . val . rtName) tas]  groupDuplicatesOn :: Ord b => (a -> b) -> [a] -> [[a]] groupDuplicatesOn f = L.groupBy ((==) `on` f) . L.sortOn f@@ -604,7 +682,7 @@     mkPEnv _             = []     pvType' p          = Misc.safeHead (showpp p ++ " not in env of " ++ showpp rt) [pvType q | q <- penv, pname p == pname q] -+-- TODO remove the unused UReft arg checkReft                    :: (PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable (RTProp RTyCon RTyVar (UReft r)))                              => F.SrcSpan -> F.SEnv F.SortedReft -> F.TCEmb TyCon -> Maybe (RRType (UReft r)) -> UReft r -> ElabM (Maybe Doc) checkReft _  _   _   Nothing  _ = pure Nothing -- TODO:RPropP/Ref case, not sure how to check these yet.@@ -777,6 +855,3 @@                                       (pprint (val (msName m)))                                       (pprint ((dataConTyCon . ctor . head . msEqns) m))                                       (GM.fSrcSpan <$> (m:ms)))---

@@ -556,6 +556,7 @@   rename F.FInt             = F.FInt   rename F.FReal            = F.FReal   rename F.FNum             = F.FNum+  rename (F.FNatNum n)      = F.FNatNum n   rename F.FFrac            = F.FFrac   rename (   F.FObj s     ) = F.FObj (f s)   rename t'@(F.FVar _     ) = t'@@ -704,9 +705,6 @@     RApp RTyCon { rtc_tc = tc } ts _ _ -> mkHsTyConApp       (getRdrName tc)       [ specTypeToLHsType t | t <- ts, notExprArg t ]-     where-      notExprArg (RExprArg _) = False-      notExprArg _            = True     RAllE _ tin tout -> nlHsFunTy (specTypeToLHsType tin) (specTypeToLHsType tout)     REx _ tin tout -> nlHsFunTy (specTypeToLHsType tin) (specTypeToLHsType tout)     RAppTy _ (RExprArg _) _ ->

@@ -28,11 +28,13 @@ import Data.Maybe  import           Control.Monad+import           Control.Monad.Identity import           Control.Monad.State import           Data.Bifunctor (second) import           Data.Functor ((<&>)) import qualified Control.Exception         as Ex import qualified Data.HashMap.Strict       as M+import qualified Data.HashSet              as HS import qualified Data.Char                 as Char import qualified Data.List                 as L import qualified Text.PrettyPrint.HughesPJ as PJ@@ -51,8 +53,10 @@ import           Language.Haskell.Liquid.Types.RTypeOp import           Language.Haskell.Liquid.Types.Specs import           Language.Haskell.Liquid.Types.Types+import           Language.Haskell.Liquid.LHNameResolution (symbolToLHName) import qualified Language.Haskell.Liquid.Misc          as Misc import qualified Language.Haskell.Liquid.Measure       as Ms+import           Language.Haskell.Liquid.Name.LogicNameEnv (LogicNameEnv(..)) import qualified Language.Haskell.Liquid.Bare.Resolve  as Bare import qualified Language.Haskell.Liquid.Bare.Types    as Bare import qualified Language.Haskell.Liquid.Bare.Plugged  as Bare@@ -64,40 +68,53 @@ --   that is, the below needs to be called *before* we use `Expand.expand` -------------------------------------------------------------------------------- makeRTEnv-  :: Bare.Env+  :: LogicNameEnv   -> ModName   -> Ms.BareSpec   -> [(ModName, Ms.BareSpec)]-  -> LogicMap   -> BareRTEnv ---------------------------------------------------------------------------------makeRTEnv env modName mySpec dependencySpecs lmap+makeRTEnv lenv modName mySpec dependencySpecs           = renameRTArgs $ makeRTAliases tAs $ makeREAliases eAs   where-    tAs   = [ t | (_, s)  <- specs, t <- Ms.aliases  s ]-    eAs   = [ e | (_m, s)  <- specs, e <- Ms.ealiases s ]-         ++ if typeclass (getConfig env) then []-                                              -- lmap expansion happens during elaboration-                                              -- this clearly breaks things if a signature-                                              -- contains lmap functions but never gets-                                              -- elaborated-              else [ e | (_, xl) <- M.toList (lmSymDefs lmap)-                                  , let e    = lmapEAlias xl             ]+    tAs     = concatMap (Ms.aliases . snd) specs+    eAs     = concatMap (getLHNameExprAliases . snd) specs     specs = (modName, mySpec) : dependencySpecs +    -- | 'Symbol's are temporarily converted to 'LHName's in expression alias+    -- bodies to use the same lookup and expansion procedure for both+    -- kinds of aliases. Implemented as an specialization of+    -- 'toBareSpecLHName' for the expression aliases field.+    getLHNameExprAliases:: Ms.BareSpec -> [RTAlias F.Symbol (ExprV LHName)]+    getLHNameExprAliases = runIdentity . go++    go :: Ms.BareSpec -> Identity [RTAlias F.Symbol (ExprV LHName)]+    go = mapM (emapRTAlias (\e -> emapExprVM (symToLHName . (++ e)))) . ealiases++    symToLHName = symbolToLHName "makeRTEnv" lenv unhandledNames+    unhandledNames = HS.fromList $ map fst $ expSigs mySpec+ -- | We apply @renameRTArgs@ *after* expanding each alias-definition, to --   ensure that the substitutions work properly (i.e. don't miss expressions --   hidden inside @RExprArg@ or as strange type parameters. renameRTArgs :: BareRTEnv -> BareRTEnv renameRTArgs rte = RTE-  { typeAliases = M.map (fmap (renameTys . renameVV . renameRTVArgs)) (typeAliases rte)-  , exprAliases = M.map (fmap                         renameRTVArgs) (exprAliases rte)+  { typeAliases = M.map (renameTys . renameVV . renameRTVArgs) (typeAliases rte)+  , exprAliases = M.map renameRTVArgs (exprAliases rte)   } -makeREAliases :: [Located (RTAlias F.Symbol F.Expr)] -> BareRTEnv+-- | Recursively expands expression aliases by unfolding the definitions of all+--   inner aliases and adds them to the environment.+--   Innermost aliases are unfolded and added first, and an error is thrown if+--   cyclic dependencies are detected.+makeREAliases :: [RTAlias F.Symbol (F.ExprV LHName)] -> BareRTEnv makeREAliases = graphExpand buildExprEdges f mempty   where-    f rtEnv xt = setREAlias rtEnv (expandLoc rtEnv xt)+    f rtEnv xt = setREAlias rtEnv (expand rtEnv (F.loc . rtName $ xt) (lhNametoSymbol xt))+    -- Expression aliases 'LHName's are transformed back to 'Symbol's for the+    -- actual expansion to take place and to be stored in the environment.+    lhNametoSymbol :: RTAlias F.Symbol (F.ExprV LHName) -> RTAlias F.Symbol Expr+    lhNametoSymbol xt = (fmap $ fmap lhNameToResolvedSymbol) xt   -- | @renameTys@ ensures that @RTAlias@ type parameters have distinct names@@ -106,7 +123,7 @@ renameTys rt = rt { rtTArgs = ys, rtBody = sbts (rtBody rt) (zip xs ys) }   where     xs    = rtTArgs rt-    ys    = (`F.suffixSymbol` rtName rt) <$> xs+    ys    = (`F.suffixSymbol` (lhNameToUnqualifiedSymbol . val . rtName $ rt)) <$> xs     sbts  = foldl (flip subt)  @@ -126,65 +143,78 @@     oldArgs      = rtVArgs rt     rtArg x i    = F.suffixSymbol x (F.intSymbol "rta" i) -makeRTAliases :: [Located (RTAlias F.Symbol BareType)] -> BareRTEnv -> BareRTEnv+-- | Recursively expands type aliases by unfolding the definitions of all inner+--   aliases and adds them to the environment.+--   Innermost aliases are unfolded and added first, and an error is thrown if+--   cyclic dependencies are detected.+--   Note that when called from 'makeRTEnv', the input environment contains only+--   expanded expression aliases.+makeRTAliases :: [RTAlias F.Symbol BareType] -> BareRTEnv -> BareRTEnv makeRTAliases lxts rte = graphExpand buildTypeEdges f rte lxts   where-    f rtEnv xt         = setRTAlias rtEnv (expandLoc rtEnv xt)+    f rtEnv xt = setRTAlias rtEnv (expand rtEnv (F.loc . rtName $ xt) xt)  -------------------------------------------------------------------------------------------------------------- +-- | Builds a directed graph of aliases, checks for cyclic dependencies,+--   reorders them so that inner aliases are processed first, and folds over+--   the graph to add each expanded node to the environment. graphExpand :: (PPrint t)-            => (AliasTable x t -> t -> [F.Symbol])         -- ^ dependencies-            -> (thing -> Located (RTAlias x t) -> thing) -- ^ update+            => (AliasTable x t -> t -> [LHName])         -- ^ dependencies+            -> (thing -> RTAlias x t -> thing) -- ^ update             -> thing                                     -- ^ initial-            -> [Located (RTAlias x t)]                   -- ^ vertices+            -> [RTAlias x t]                   -- ^ vertices             -> thing                                     -- ^ final graphExpand buildEdges expBody env lxts            = L.foldl' expBody env (genExpandOrder table' graph)   where-    -- xts    = val <$> lxts     table  = buildAliasTable lxts     graph  = buildAliasGraph (buildEdges table) lxts     table' = checkCyclicAliases table graph -setRTAlias :: RTEnv x t -> Located (RTAlias x t) -> RTEnv x t+-- | Inserts a type alias into the environment.+setRTAlias :: RTEnv x t -> RTAlias x t -> RTEnv x t setRTAlias env a = env { typeAliases =  M.insert n a (typeAliases env) }   where-    n            = rtName (val a)+    n            = val . rtName $ a -setREAlias :: RTEnv x t -> Located (RTAlias F.Symbol F.Expr) -> RTEnv x t+-- | Inserts an expression alias into the environment.+setREAlias :: RTEnv x t -> RTAlias F.Symbol F.Expr -> RTEnv x t setREAlias env a = env { exprAliases = M.insert n a (exprAliases env) }   where-    n            = rtName (val a)--+    n            = val . rtName $ a  ---------------------------------------------------------------------------------type AliasTable x t = M.HashMap F.Symbol (Located (RTAlias x t)) -buildAliasTable :: [Located (RTAlias x t)] -> AliasTable x t-buildAliasTable = M.fromList . map (\rta -> (rtName (val rta), rta))+type AliasTable x t = M.HashMap LHName (RTAlias x t) -fromAliasSymbol :: AliasTable x t -> F.Symbol -> Located (RTAlias x t)-fromAliasSymbol table sym-  = fromMaybe err (M.lookup sym table)+buildAliasTable :: [RTAlias x t] -> AliasTable x t+buildAliasTable = M.fromList . map (\rta -> (val . rtName $ rta, rta))++fromAliasLHName :: AliasTable x t -> LHName -> RTAlias x t+fromAliasLHName table lhname+  = fromMaybe err (M.lookup lhname table)   where-    err = panic Nothing ("fromAliasSymbol: Dangling alias symbol: " ++ show sym)+    err = panic Nothing ("fromAliasLHName: Dangling alias name: " ++ show lhname) +-- | An adjacency list of nodes representing a directed graph.+--   Used to detect cyclic alias dependencies and to order the expansion+--   of aliases. type Graph t = [Node t]+-- | A node described by a label, a key, and a list of connected nodes,+--   all parameterized by the same type. This type is used to represent+--   aliases nested within other aliases. type Node  t = (t, t, [t]) -buildAliasGraph :: (PPrint t) => (t -> [F.Symbol]) -> [Located (RTAlias x t)]-                -> Graph F.Symbol-buildAliasGraph buildEdges = map (buildAliasNode buildEdges)--buildAliasNode :: (PPrint t) => (t -> [F.Symbol]) -> Located (RTAlias x t)-               -> Node F.Symbol-buildAliasNode f la = (rtName a, rtName a, f (rtBody a))+buildAliasGraph :: (PPrint t) => (t -> [LHName]) -> [RTAlias x t]+                -> Graph LHName+buildAliasGraph buildEdges = map (buildNode buildEdges)   where-    a               = val la+    buildNode :: (PPrint t) => (t -> [LHName]) -> RTAlias x t+               -> Node LHName+    buildNode f a = (val . rtName $ a, val . rtName $ a, f (rtBody a)) -checkCyclicAliases :: AliasTable x t -> Graph F.Symbol -> AliasTable x t+checkCyclicAliases :: AliasTable x t -> Graph LHName -> AliasTable x t checkCyclicAliases table graph   = case mapMaybe go (stronglyConnComp graph) of       []   -> table@@ -193,34 +223,32 @@       go (CyclicSCC vs) = Just vs       go (AcyclicSCC _) = Nothing -cycleAliasErr :: AliasTable x t -> [F.Symbol] -> Error-cycleAliasErr _ []          = panic Nothing "checkCyclicAliases: No type aliases in reported cycle"-cycleAliasErr t symList@(rta:_) = ErrAliasCycle { pos    = fst (locate rta)-                                                , acycle = map locate symList }+cycleAliasErr :: AliasTable x t -> [LHName] -> Error+cycleAliasErr _ []          = panic Nothing "checkCyclicAliases: No aliases in reported cycle"+cycleAliasErr t nameList@(name:_) = ErrAliasCycle { pos    = fst (locate name)+                                                , acycle = map locate nameList }   where-    locate sym = ( GM.fSrcSpan $ fromAliasSymbol t sym-                 , pprint sym )-+    locate n = ( GM.fSrcSpan . rtName $ fromAliasLHName t n+                 , pprint n ) -genExpandOrder :: AliasTable x t -> Graph F.Symbol -> [Located (RTAlias x t)]+-- | Orders aliases so that nested ones are processed first.+genExpandOrder :: AliasTable x t -> Graph LHName -> [RTAlias x t] genExpandOrder table graph-  = map (fromAliasSymbol table) symOrder+  = map (fromAliasLHName table) nameOrder   where     (digraph, lookupVertex, _)       = graphFromEdges graph-    symOrder+    nameOrder       = map (Misc.fst3 . lookupVertex) $ reverse $ topSort digraph  -------------------------------------------------------------------------------- -ordNub :: Ord a => [a] -> [a]-ordNub = map head . L.group . L.sort--buildTypeEdges :: AliasTable x t -> BareType -> [F.Symbol]-buildTypeEdges table = ordNub . go+-- | Gathers all constructor names within a the body of a type alias+--   that match a key from the type 'AliasTable'.+buildTypeEdges :: AliasTable x t -> BareType -> [LHName]+buildTypeEdges table = Misc.ordNub . go   where-    -- go :: t -> [Symbol]-    go (RApp c ts rs _) = go_alias (getLHNameSymbol $ val $ btc_tc c) ++ concatMap go ts ++ concatMap go (mapMaybe go_ref rs)+    go (RApp c ts rs _) = go_alias (val $ btc_tc c) ++ concatMap go ts ++ concatMap go (mapMaybe go_ref rs)     go (RFun _ _ t1 t2 _) = go t1 ++ go t2     go (RAppTy t1 t2 _) = go t1 ++ go t2     go (RAllE _ t1 t2)  = go t1 ++ go t2@@ -235,10 +263,11 @@     go_ref (RProp _ (RHole _)) = Nothing     go_ref (RProp  _ t) = Just t -buildExprEdges :: M.HashMap F.Symbol a -> F.Expr -> [F.Symbol]-buildExprEdges table  = ordNub . go+-- | Gathers all variable names within the body of an expression alias+--   that match a key from the expression 'AliasTable'.+buildExprEdges :: AliasTable x t -> F.ExprV LHName -> [LHName]+buildExprEdges table  = Misc.ordNub . go   where-    go :: F.Expr -> [F.Symbol]     go (EApp e1 e2)   = go e1 ++ go e2     go (ENeg e)       = go e     go (EBin _ e1 e2) = go e1 ++ go e2@@ -254,13 +283,13 @@     go (PIff p q)      = go p ++ go q     go (PAll _ p)      = go p     go (ELam _ e)      = go e+    go (ELet _ e1 e2)  = go e1 ++ go e2     go (ECoerc _ _ e)  = go e     go (PAtom _ e1 e2) = go e1 ++ go e2     go (ETApp e _)     = go e     go (ETAbs e _)     = go e     go (PKVar _ _)     = []     go (PExist _ e)    = go e-    go (PGrad _ _ _ e) = go e     go_alias f         = [f | M.member f table ]  @@ -398,11 +427,11 @@     go t@RExprArg{}      = t     goRef (RProp ss t)   = RProp (map (expand rtEnv l <$>) ss) (go t) -lookupRTEnv :: BTyCon -> BareRTEnv -> Maybe (Located BareRTAlias)-lookupRTEnv c rtEnv = M.lookup (getLHNameSymbol $ val $ btc_tc c) (typeAliases rtEnv)+lookupRTEnv :: BTyCon -> BareRTEnv -> Maybe BareRTAlias+lookupRTEnv c rtEnv = M.lookup (val $ btc_tc c) (typeAliases rtEnv) -expandRTAliasApp :: F.SourcePos -> Located BareRTAlias -> [BareType] -> RReft -> BareType-expandRTAliasApp l (Loc la _ rta) args r = case isOK of+expandRTAliasApp :: F.SourcePos -> BareRTAlias -> [BareType] -> RReft -> BareType+expandRTAliasApp l rta@(RTA {rtName = Loc la _ _}) args r = case isOK of   Just e     -> Ex.throw e   Nothing    -> F.subst esu . (`RT.strengthen` r) . RT.subsTyVarsMeet tsu $ rtBody rta   where@@ -466,8 +495,9 @@ ---------------------------------------------------------------------------------------- cookSpecType :: Bare.Env -> Bare.SigEnv -> ModName -> Bare.PlugTV Ghc.Var -> LocBareType              -> LocSpecType-cookSpecType env sigEnv name x bt-         = either Ex.throw id (cookSpecTypeE env sigEnv name x bt)+cookSpecType env sigEnv name x bt =+  either Ex.throw id $+  cookSpecTypeE env sigEnv name x bt   where     _msg = "cookSpecType: " ++ GM.showPpr (z, Ghc.varType <$> z)     z    = Bare.plugSrc x@@ -480,7 +510,8 @@ cookSpecTypeE env sigEnv name@(ModName _ _) x bt   = fmap f . bareSpecType env $ bareExpandType rtEnv bt   where-    f = (if doplug || not allowTC then plugHoles allowTC sigEnv name x else id)+    f :: LocSpecType -> LocSpecType+    f =   (if doplug || not allowTC then plugHoles allowTC sigEnv name x else id)         . fmap (RT.addTyConInfo embs tyi)         . Bare.txRefSort tyi embs         . fmap txExpToBind -- What does this function DO@@ -510,7 +541,7 @@ generalizeWith _             t = RT.generalize t  generalizeVar :: Ghc.Var -> SpecType -> SpecType-generalizeVar v t = mkUnivs (zip as (repeat mempty)) [] t+generalizeVar v t = mkUnivs [(a, mempty) | a <- as] [] t   where     as            = filter isGen (RT.freeTyVars t)     (vas,_)       = Ghc.splitForAllTyCoVars (GM.expandVarType v)@@ -529,21 +560,24 @@ specExpandType = expandLoc  bareSpecType :: Bare.Env -> LocBareType -> Bare.Lookup LocSpecType-bareSpecType env bt = case Bare.ofBareTypeE env (F.loc bt) Nothing (val bt) of-  Left e  -> Left e-  Right t -> Right (F.atLoc bt t)+bareSpecType env bt =+  case Bare.ofBareTypeE env (F.loc bt) Nothing (val bt) of+    Left e  -> Left e+    Right t -> Right (F.atLoc bt t)  maybePlug :: Bool -> Bare.SigEnv -> ModName -> Bare.PlugTV Ghc.Var -> LocSpecType -> LocSpecType-maybePlug allowTC sigEnv name kx = case Bare.plugSrc kx of-                             Nothing -> id-                             Just _  -> plugHoles allowTC sigEnv name kx+maybePlug allowTC sigEnv name kx =+  case Bare.plugSrc kx of+    Nothing -> id+    Just _  -> plugHoles allowTC sigEnv name kx  plugHoles :: Bool -> Bare.SigEnv -> ModName -> Bare.PlugTV Ghc.Var -> LocSpecType -> LocSpecType-plugHoles allowTC sigEnv name = Bare.makePluggedSig allowTC name embs tyi exports+plugHoles allowTC sigEnv name =+  Bare.makePluggedSig allowTC name embs tyi exports   where-    embs              = Bare.sigEmbs     sigEnv-    tyi               = Bare.sigTyRTyMap sigEnv-    exports           = Bare.sigExports  sigEnv+    embs    = Bare.sigEmbs     sigEnv+    tyi     = Bare.sigTyRTyMap sigEnv+    exports = Bare.sigExports  sigEnv  {- [NOTE:Cooking-SpecType]     A @SpecType@ is _raw_ when it is obtained directly from a @BareType@, i.e.@@ -610,6 +644,7 @@     go (PAll xs p)      = PAll xs    (go p)     go (PExist xs p)    = PExist xs  (go p)     go (ELam xt e)      = ELam xt    (go e)+    go (ELet x e1 e2)   = ELet x     (go e1) (go e2)     go (ECoerc a t e)   = ECoerc a t (go e)     go (ETApp e s)      = ETApp      (go e) s     go (ETAbs e s)      = ETAbs      (go e) s@@ -618,7 +653,6 @@     go (PIff    e1 e2)  = PIff       (go e1) (go e2)     go (PAtom b e1 e2)  = PAtom b    (go e1) (go e2)     go (EIte  p e1 e2)  = EIte (go p)(go e1) (go e2)-    go (PGrad k su i e) = PGrad k su i (go e)     go e@(PKVar _ _)    = e     go e@(ESym _)       = e     go e@(ECon _)       = e@@ -637,7 +671,7 @@     Just re -> expandApp l   re       es'     Nothing -> F.eApps       (EVar f) es'   where-    eAs     = exprAliases rtEnv+    eAs     = M.mapKeys lhNameToResolvedSymbol $ exprAliases rtEnv     mBody   = M.lookup f eAs `mplus` M.lookup (GM.dropModuleUnique f) eAs     es'     = expandExpr rtEnv l <$> es     _f0     = GM.dropModuleNamesAndUnique f@@ -647,18 +681,17 @@ -------------------------------------------------------------------------------- -- | Expand Alias Application -------------------------------------------------- ---------------------------------------------------------------------------------expandApp :: F.Subable ty => F.SourcePos -> Located (RTAlias F.Symbol ty) -> [Expr] -> ty-expandApp l lre es+expandApp :: F.Subable ty => F.SourcePos -> RTAlias F.Symbol ty -> [Expr] -> ty+expandApp l re es   | Just su <- args = F.subst su (rtBody re)   | otherwise       = Ex.throw err   where-    re              = F.val lre     args            = F.mkSubst <$> Misc.zipMaybe (rtVArgs re) es     err             :: UserError     err             = ErrAliasApp sp alias sp' msg     sp              = GM.sourcePosSrcSpan l     alias           = pprint           (rtName re)-    sp'             = GM.fSrcSpan lre -- sourcePosSrcSpan (rtPos re)+    sp'             = GM.fSrcSpan . rtName $ re     msg             =  "expects" PJ.<+> pprint (length $ rtVArgs re)                    PJ.<+> "arguments but it is given"                    PJ.<+> pprint (length es)@@ -669,7 +702,8 @@ ------------------------------------------------------------------------------- txExpToBind   :: SpecType -> SpecType --------------------------------------------------------------------------------txExpToBind t = evalState (expToBindT t) (ExSt 0 M.empty πs)+txExpToBind t =+  evalState (expToBindT t) (ExSt 0 M.empty πs)   where     πs        = M.fromList [(pname p, p) | p <- ty_preds $ toRTypeRep t ] 

@@ -402,7 +402,7 @@         concat (tycDCons `Mb.mapMaybe` (dataDecls spec ++ newtyDecls spec))     getFromDataCtor decl = S.fromList $       map lhNameToResolvedSymbol $ val (dcName decl) : (fst <$> dcFields decl)-    getAliases spec = S.fromList $ rtName . val <$> Ms.ealiases spec+    getAliases spec = S.fromList $ lhNameToUnqualifiedSymbol . val . rtName <$> Ms.ealiases spec  -- Get the set of `DataCon`s (DCs) needed for the reflection of a given list of variables, -- and which are not already present in the logic

@@ -108,7 +108,8 @@ -- Renaming Type Variables in Haskell Signatures ------------------------------ ------------------------------------------------------------------------------- runMapTyVars :: Bool -> Type -> SpecType -> (PJ.Doc -> PJ.Doc -> Error) -> Either Error MapTyVarST-runMapTyVars allowTC τ t err = execStateT (mapTyVars allowTC τ t) (MTVST [] err)+runMapTyVars allowTC τ t err =+  execStateT (mapTyVars allowTC τ t) (MTVST [] err)  data MapTyVarST = MTVST   { vmap   :: [(Var, RTyVar)]@@ -141,8 +142,8 @@ mapTyVars _ _ (RExprArg _)   = return () mapTyVars allowTC (AppTy τ τ') (RAppTy t t' _)-  = do  mapTyVars allowTC τ t-        mapTyVars allowTC τ' t'+  = do mapTyVars allowTC τ t+       mapTyVars allowTC τ' t' mapTyVars _ _ (RHole _)   = return () mapTyVars _ k _ | isKind k@@ -154,8 +155,10 @@        throwError (err (F.pprint hsT) (F.pprint lqT))  isKind :: Kind -> Bool-isKind = isTYPEorCONSTRAINT -- TODO:GHC-863 isStarKind k --  typeKind k-+isKind k = isTYPEorCONSTRAINT k -- TODO:GHC-863 isStarKind k --  typeKind k+          || case k of+                TyVarTy kk -> varType kk == Ghc.liftedTypeKind+                _ -> False  mapTyRVar :: MonadError Error m           => Var -> RTyVar -> MapTyVarST -> m MapTyVarST

@@ -282,7 +282,9 @@     -- zipWithDefM: if ts and ts' have different length then the liquid and haskell types are different.     -- keep different types for now, as a pretty error message will be created at Bare.Check     go (RApp _ ts _ _)  (RApp c ts' p r)-      | length ts == length ts'            = RApp c     (Misc.zipWithDef go ts $ Bare.matchKindArgs ts ts') p r+    -- Removing length check because Haskell types can contain kinds which is safe based on the comment above +    --   | length ts == length ts'            +      = RApp c     (Misc.zipWithDef go ts $ Bare.matchKindArgs ts ts') p r     go hsT lqT                             = Ex.throw (err (F.pprint hsT) (F.pprint lqT))      -- otherwise                          = Ex.throw err

@@ -188,7 +188,7 @@  -- | @lookupLocalVar@ takes as input the list of "global" (top-level) vars --   that also match the name @lx@; we then pick the "closest" definition.---   See tests/names/LocalSpec.hs for a motivating example.+--   See tests/names/pos/LocalSpec.hs for a motivating example.  lookupLocalVar :: F.Loc a => LocalVars -> LocSymbol -> [a] -> Maybe (Either a Ghc.Var) lookupLocalVar localVars lx gvs = findNearest lxn kvs

@@ -348,7 +348,7 @@         ptys    = [(F.vv (Just i), classRFInfo True, pty, mempty) | (i,pty) <- zip [0,1..] isPredSpecTys]         fullSig =           mkArrow-            (zip isRTvs (repeat mempty))+            [(bRTV, mempty) | bRTV <- isRTvs]             []             ptys .           subst (zip clsTvs isSpecTys) $

@@ -113,7 +113,7 @@ lookupREnv x rE = msum $ M.lookup x <$> renvMaps rE  memberREnv :: F.Symbol -> REnv -> Bool-memberREnv x rE = or   $ M.member x <$> renvMaps rE+memberREnv x rE = any (M.member x) (renvMaps rE)  globalREnv :: REnv -> REnv globalREnv (REnv gM lM) = REnv gM' M.empty

@@ -7,6 +7,7 @@ {-# LANGUAGE MultiParamTypeClasses     #-} {-# LANGUAGE OverloadedStrings         #-} {-# LANGUAGE ImplicitParams            #-}+{-# LANGUAGE NamedFieldPuns            #-}  {-# OPTIONS_GHC -Wno-orphans #-} {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}@@ -28,8 +29,9 @@ import qualified Language.Haskell.Liquid.GHC.SpanStack         as Sp import qualified Language.Haskell.Liquid.GHC.Misc              as GM -- ( isInternal, collectArguments, tickSrcSpan, showPpr ) import Text.PrettyPrint.HughesPJ ( text )-import           Control.Monad ( foldM, forM, forM_, when, void )+import           Control.Monad ( foldM, forM, forM_, when, void, unless) import           Control.Monad.State+import           Data.Bifunctor                                (first) import           Data.Maybe                                    (fromMaybe, isJust, mapMaybe) import           Data.Either.Extra                             (eitherToMaybe) import qualified Data.HashMap.Strict                           as M@@ -67,7 +69,7 @@ import           Language.Haskell.Liquid.Bare.DataType (dataConMap, makeDataConChecker) import Language.Haskell.Liquid.UX.Config     ( HasConfig(getConfig),-      Config(typeclass, gradual, checkDerived, extensionality,+      Config(typeclass, checkDerived, extensionality,              nopolyinfer, noADT, dependantCase, exactDC, rankNTypes),       patternFlag,       higherOrderFlag )@@ -86,7 +88,6 @@ consAct γ cfg info = do   let sSpc = gsSig . giSpec $ info   let gSrc = giSrc info-  when (gradual cfg) (mapM_ (addW . WfC γ . val . snd) (gsTySigs sSpc ++ gsAsmSigs sSpc))   γ' <- foldM (consCBTop cfg info) γ (giCbs gSrc)   -- Relational Checking: the following only runs when the list of relational specs is not empty   (ψ, γ'') <- foldM (consAssmRel cfg info) ([], γ') (gsAsmRel sSpc ++ gsRelation sSpc)@@ -97,11 +98,107 @@   hws <- gets hsWfs   fcs <- concat <$> mapM (splitC (typeclass (getConfig info))) hcs   fws <- concat <$> mapM splitW hws+  checkStratCtors γ sSpc   modify $ \st -> st { fEnv     = fEnv    st `mappend` feEnv (fenv γ)                      , cgLits   = litEnv   γ                      , cgConsts = cgConsts st `mappend` constEnv γ                      , fixCs    = fcs                      , fixWfs   = fws }+++---------------------------------+-- | Checking stratified ctors --+---------------------------------+type FExpr = F.ExprV F.Symbol+type Ctors = S.HashSet F.Symbol++checkStratCtors :: CGEnv -> GhcSpecSig -> CG ()+checkStratCtors env sSpc = do+  let ctors = S.fromList $ M.keys $ F.seBinds $ constEnv env+  let ctorRefinements = filter (isStrat . fst) $ gsTySigs sSpc+  forM_ ctorRefinements $ uncurry $ checkCtor ctors+  where+    -- (Alecs): For some reason it can't see that they are the same+    -- GHC name, probably is due to some worker wrapper shenannigans+    hack = occNameString . nameOccName+    isStrat nm = hack (varName nm) `elem` map hack (gsStratCtos sSpc)++uncurryPi :: SpecType -> ([SpecType], SpecType)+uncurryPi (RFun _ _ dom cod _) = first (dom :) $ uncurryPi cod+uncurryPi rest                 = ([], rest)++getTyConName :: SpecType -> Name+getTyConName a = Ghc.tyConName $ rtc_tc $ rt_tycon a++checkCtor :: Ctors -> Var -> LocSpecType -> CG ()+checkCtor ctors name typ = do+  let loc = GM.fSrcSpan $ F.loc typ+  let (args, ret) = uncurryPi $ val typ+  -- The constuctor that we want not to appear negatively+  let tyName = getTyConName ret+  -- Its index information+  retIdx <- case getPropIndex $ ur_reft $ rt_reft ret of+    Just idx -> pure idx+    Nothing  -> uError $ ErrStratNotPropRet loc (pprint tyName) (pprint name) (F.pprint ret)+  -- For every argument of the constructor we check that all the+  -- self-refernce are refined by a "smaller" `prop` annotation+  forM_ args $ checkNg ctors loc name tyName retIdx++checkNg :: Ctors -> SrcSpan -> Var -> Name -> FExpr -> SpecType -> CG ()+checkNg ctors loc ctorName tyName retIdx = go+  where+    go :: SpecType -> CG ()+    go RVar {} = pure ()+    go RAllT { rt_ty } = go rt_ty+    go RAllP { rt_ty } = go rt_ty+    go RFun { rt_in, rt_out } = do+      go rt_in+      go rt_out+    go r@RApp { rt_tycon = RTyCon { rtc_tc }, rt_args, rt_reft } = do+      if Ghc.tyConName rtc_tc == tyName then do+          case getPropIndex $ ur_reft rt_reft of+            (Just arg) -> do+              -- We compare index information The occurrence is safe+              -- iff the index of the return type is strictly bigger+              -- than the one in negative position+              unless (isStructurallySmaller ctors arg retIdx) $ do+                uError $ ErrStratIdxNotSmall loc+                  (pprint tyName) (pprint ctorName) (F.pprint retIdx) (F.pprint arg)+            -- We don't have index information for both so we bail+            _ -> uError $ ErrStratOccProp loc (pprint tyName) (pprint ctorName) (F.pprint r)+      else do+        forM_ rt_args go+    go _ = lift $ impossible (Just loc) "checkNg unexpected type"+++isStructurallySmaller :: Ctors -> FExpr -> FExpr -> Bool+isStructurallySmaller ctors l r+  -- Congruence rule+  | (F.EVar nl, argsl) <- F.splitEAppThroughECst l+  , (F.EVar nr, argsr) <- F.splitEAppThroughECst r+  , nl == nr+  , length argsl == length argsr+  , nl `elem` ctors+  = lexOrder ctors argsl argsr+  | otherwise = isSubterm ctors l r && l /= r++lexOrder :: Ctors -> [F.ExprV F.Symbol] -> [F.ExprV F.Symbol] -> Bool+lexOrder _     []     []            = False+lexOrder ctors (l:ls) (r:rs)+  | isStructurallySmaller ctors l r = True+  | l == r                          = lexOrder ctors ls rs+  | otherwise                       = False+lexOrder _ _ _ = errorP "" "lexOrder: different length lists"++isSubterm :: Ctors -> FExpr -> FExpr -> Bool+isSubterm ctors l r | l == r+                   = True+                  -- Congruence rule+                  | (F.EVar nm, args) <- F.splitEAppThroughECst r+                  , nm `elem` ctors+                  = any (isSubterm ctors l) args+                  | otherwise+                  = False  -------------------------------------------------------------------------------- -- | Ensure that the instance type is a subtype of the class type --------------

@@ -9,7 +9,7 @@   where  import           Prelude hiding (error)-import           Data.List                (delete, nub)+import           Data.List                (delete, nub, partition) import           Data.Maybe               (isJust, catMaybes, fromMaybe, isNothing) import qualified Data.HashSet        as S import qualified Data.HashMap.Strict as M@@ -18,6 +18,7 @@  import           Language.Fixpoint.Types                  hiding (panic, mkQual) import qualified Language.Fixpoint.Types.Config as FC+import           Language.Fixpoint.Misc                  (fst3) import           Language.Fixpoint.SortCheck import           Language.Haskell.Liquid.Types.RefType import           Language.Haskell.Liquid.GHC.Misc         (getSourcePos)@@ -31,7 +32,7 @@ import           Language.Haskell.Liquid.Types.Specs import           Language.Haskell.Liquid.Types.Types import           Language.Haskell.Liquid.UX.Config-import Language.Fixpoint.Types.Config (ElabFlags)+import           Language.Fixpoint.Types.Config (ElabFlags)   --------------------------------------------------------------------------------@@ -39,10 +40,16 @@ -------------------------------------------------------------------------------- giQuals info lEnv   =  notracepp ("GI-QUALS: " ++ showpp lEnv)-  $  condNull (useSpcQuals info) (gsQualifiers . gsQual . giSpec $ info)+  $  currentSpec+  ++ condNull (useSpcQuals info) otherSpecs   ++ condNull (useSigQuals info) (sigQualifiers  info lEnv)   ++ condNull (useAlsQuals info) (alsQualifiers  info lEnv)+  where+    (currentSpec, otherSpecs) = partition isQualifierFromCurrentModule (gsQualifiers . gsQual . giSpec $ info)+    isQualifierFromCurrentModule qual =+      fst3 (sourcePosElts (qPos qual)) == giTarget (giSrc info) + -- -------------------------------------------------------------------------------- -- qualifiers :: GhcInfo -> SEnv Sort -> [Qualifier] -- --------------------------------------------------------------------------------@@ -84,10 +91,22 @@         , validQual lEnv q     ]     where-      ef  = maybe (FC.ElabFlags False) FC.solverFlags . smtsolver . getConfig $ info+      ef  = elabFlag info       k   = maxQualParams info       tce = gsTcEmbeds . gsName . giSpec $ info +elabFlag :: (HasConfig t) => t -> FC.ElabFlags+elabFlag info = FC.ElabFlags setBag False+  where+      setBag = maybe False elabSetBag . smtsolver . getConfig $ info+      elabSetBag :: FC.SMTSolver -> Bool+      elabSetBag FC.Z3    = True+      elabSetBag FC.Z3mem = True+      elabSetBag _        = False++++ validQual :: SEnv Sort -> Qualifier -> Bool validQual lEnv q = isJust $ checkSortExpr (srcSpan q) env (qBody q)   where@@ -107,7 +126,7 @@         , length (qParams q) <= k + 1     ]     where-      ef  = maybe (FC.ElabFlags False) FC.solverFlags . smtsolver . getConfig $ info+      ef  = elabFlag info       k   = maxQualParams info       tce = gsTcEmbeds . gsName . giSpec $ info @@ -180,7 +199,6 @@   = [ mkQ' v so pa  | let (RR so (Reft (v, ra))) = rTypeSortedReft tce rrt                    , pa                        <- conjuncts ra                    , not $ isHole    pa-                   , not $ isGradual pa                    , notracepp ("refTopQuals: " ++ showpp pa)                      $ isNothing $ runReader (checkSorted (srcSpan l) (insertSEnv v so γ') pa) ef     ]

@@ -559,13 +559,13 @@     γ'' <- γ' += ("consRelSub Base R", rr, t2)     let cstr = F.subst (F.mkSubst [(resL, F.EVar rl), (resR, F.EVar rr)]) $ F.PImp p1 p2     entl γ'' (traceWhenLoud ("consRelSub Base cstr " ++ F.showpp cstr) cstr) "consRelSub Base"-consRelSub _ t1@(RHole _) t2@(RHole _) _ _ = F.panic $ "consRelSub is undefined for RHole " ++ show (t1, t2)+consRelSub _ t1@(RHole _)    t2@(RHole _)    _ _ = F.panic $ "consRelSub is undefined for RHole "    ++ show (t1, t2) consRelSub _ t1@(RExprArg _) t2@(RExprArg _) _ _ = F.panic $ "consRelSub is undefined for RExprArg " ++ show (t1, t2)-consRelSub _ t1@REx {} t2@REx {} _ _ = F.panic $ "consRelSub is undefined for REx " ++ show (t1, t2)-consRelSub _ t1@RAllE {} t2@RAllE {} _ _ = F.panic $ "consRelSub is undefined for RAllE " ++ show (t1, t2)-consRelSub _ t1@RRTy {} t2@RRTy {} _ _ = F.panic $ "consRelSub is undefined for RRTy " ++ show (t1, t2)-consRelSub _ t1@RAllP {} t2@RAllP {} _ _ = F.panic $ "consRelSub is undefined for RAllP " ++ show (t1, t2)-consRelSub _ t1@RAllT {} t2@RAllT {} _ _ = F.panic $ "consRelSub is undefined for RAllT " ++ show (t1, t2)+consRelSub _ t1@REx {}       t2@REx {}       _ _ = F.panic $ "consRelSub is undefined for REx "      ++ show (t1, t2)+consRelSub _ t1@RAllE {}     t2@RAllE {}     _ _ = F.panic $ "consRelSub is undefined for RAllE "    ++ show (t1, t2)+consRelSub _ t1@RRTy {}      t2@RRTy {}      _ _ = F.panic $ "consRelSub is undefined for RRTy "     ++ show (t1, t2)+consRelSub _ t1@RAllP {}     t2@RAllP {}     _ _ = F.panic $ "consRelSub is undefined for RAllP "    ++ show (t1, t2)+consRelSub _ t1@RAllT {}     t2@RAllT {}     _ _ = F.panic $ "consRelSub is undefined for RAllT "    ++ show (t1, t2) consRelSub _ t1 t2 _ _ =  F.panic $ "consRelSub is undefined for different types " ++ show (t1, t2)  --------------------------------------------------------------

@@ -27,11 +27,9 @@ import           Language.Haskell.Liquid.UX.Config import           Language.Haskell.Liquid.UX.DiffCheck (coreDefs, coreDeps, dependsOn, Def(..)) import qualified Language.Haskell.Liquid.GHC.Misc  as GM -- (simplesymbol)-import qualified Data.List                         as L import qualified Data.HashMap.Strict               as M import qualified Data.HashSet                      as S -- import           Language.Fixpoint.Misc-import qualified Language.Haskell.Liquid.Misc      as Misc  import           Language.Haskell.Liquid.Types.Errors import           Language.Haskell.Liquid.Types.RType@@ -41,37 +39,33 @@  fixConfig :: FilePath -> Config -> FC.Config fixConfig tgt cfg = def-  { FC.solver                   = Mb.fromJust (smtsolver cfg)-  , FC.linear                   = linear            cfg-  , FC.eliminate                = eliminate         cfg-  , FC.nonLinCuts               = not (higherOrderFlag cfg) -- eliminate cfg /= FC.All-  , FC.save                     = saveQuery         cfg-  , FC.srcFile                  = tgt-  , FC.cores                    = cores             cfg-  , FC.minPartSize              = minPartSize       cfg-  , FC.maxPartSize              = maxPartSize       cfg-  , FC.elimStats                = elimStats         cfg-  , FC.elimBound                = elimBound         cfg-  , FC.allowHO                  = higherOrderFlag   cfg-  , FC.allowHOqs                = higherorderqs     cfg-  , FC.smtTimeout               = smtTimeout        cfg-  , FC.stringTheory             = stringTheory      cfg-  , FC.gradual                  = gradual           cfg-  , FC.ginteractive             = ginteractive       cfg-  , FC.noslice                  = noslice           cfg-  , FC.rewriteAxioms            = allowPLE   cfg-  , FC.pleWithUndecidedGuards   = pleWithUndecidedGuards cfg-  , FC.etabeta                  = etabeta    cfg-  , FC.localRewrites            = dependantCase cfg-  , FC.etaElim                  = not (exactDC cfg) && extensionality cfg -- SEE: https://github.com/ucsd-progsys/liquidhaskell/issues/1601-  , FC.extensionality           = extensionality    cfg-  , FC.interpreter              = interpreter    cfg-  , FC.oldPLE                   = oldPLE cfg-  , FC.rwTerminationCheck       = rwTerminationCheck cfg-  , FC.noLazyPLE                = noLazyPLE cfg-  , FC.fuel                     = fuel      cfg-  , FC.noEnvironmentReduction   = not (environmentReduction cfg)-  , FC.inlineANFBindings        = inlineANFBindings cfg+  { FC.solver         = Mb.fromJust (smtsolver cfg)+  , FC.linear         = linear            cfg+  , FC.eliminate      = eliminate         cfg+  , FC.nonLinCuts     = not (higherOrderFlag cfg) -- eliminate cfg /= FC.All+  , FC.save           = saveQuery         cfg+  , FC.srcFile        = tgt+  , FC.cores          = cores             cfg+  , FC.minPartSize    = minPartSize       cfg+  , FC.maxPartSize    = maxPartSize       cfg+  , FC.elimStats      = elimStats         cfg+  , FC.elimBound      = elimBound         cfg+  , FC.allowHO        = higherOrderFlag   cfg+  , FC.allowHOqs      = higherorderqs     cfg+  , FC.smtTimeout     = smtTimeout        cfg+  , FC.noStringTheory = not (stringTheory cfg)+  , FC.noslice        = noslice           cfg+  , FC.rewriteAxioms  = allowPLE   cfg+  , FC.pleUndecGuards = pleWithUndecidedGuards cfg+  , FC.etabeta        = etabeta    cfg+  , FC.localRewrites  = dependantCase cfg+  , FC.etaElim        = not (exactDC cfg) && extensionality cfg -- SEE: https://github.com/ucsd-progsys/liquidhaskell/issues/1601+  , FC.extensionality = extensionality    cfg+  , FC.interpreter    = interpreter    cfg+  , FC.rwTermination  = rwTerminationCheck cfg+  , FC.fuel           = fuel      cfg+  , FC.noEnvReduction = not (environmentReduction cfg)+  , FC.inlineANFBinds = inlineANFBindings cfg   }  cgInfoFInfo :: TargetInfo -> CGInfo -> IO (F.FInfo Cinfo)@@ -80,11 +74,10 @@ targetFInfo :: TargetInfo -> CGInfo -> F.FInfo Cinfo targetFInfo info cgi = mappend (mempty { F.ae = ax, F.lrws = localRewrites cgi }) fi   where-    fi               = F.fi cs ws bs ls consts ks qs bi aHO aHOqs es mempty adts ebs+    fi               = F.fi cs ws bs ls consts ks qs bi aHO aHOqs es mempty adts     cs               = fixCs    cgi     ws               = fixWfs   cgi     bs               = binds    cgi-    ebs              = ebinds   cgi     ls               = fEnv     cgi     consts           = cgConsts cgi     ks               = kuts     cgi@@ -104,10 +97,7 @@            (doExpand sp cfg <$> fcs)            (makeRewrites info <$> fcs)   where-    eqs      = if oldPLE cfg-                then makeEquations (typeclass cfg) sp ++ map (uncurry $ specTypeEq emb) xts-                else axioms-    emb      = gsTcEmbeds (gsName sp)+    eqs      = axioms     cfg      = getConfig  info     sp       = giSpec     info     axioms   = gsMyAxioms refl ++ gsImpAxioms refl@@ -213,17 +203,6 @@ -- 3. Don't create `define` for the ctor.  -- Unfortunately 3 breaks a bunch of tests... -specTypeEq :: F.TCEmb TyCon -> Var -> SpecType -> F.Equation-specTypeEq emb f t = F.mkEquation (F.symbol f) xts body tOut-  where-    xts            = Misc.safeZipWithError "specTypeEq" xs (RT.rTypeSort emb <$> ts)-    body           = specTypeToResultRef bExp t-    tOut           = RT.rTypeSort emb (ty_res tRep)-    tRep           = toRTypeRep t-    xs             = ty_binds tRep-    ts             = ty_args  tRep-    bExp           = F.eApps (F.eVar f) (F.EVar <$> xs)- makeSimplify :: (Var, SpecType) -> [F.Rewrite] makeSimplify (var, t)   | not (GM.isDataConId var)@@ -265,56 +244,6 @@      fromEVar (F.EVar x) = x     fromEVar _ = impossible Nothing "makeSimplify.fromEVar"--makeEquations :: Bool -> TargetSpec -> [F.Equation]-makeEquations allowTC sp = [ F.mkEquation f xts (equationBody allowTC (F.EVar f) xArgs e mbT) t-                      | F.Equ f xts e t _ <- axioms-                      , let xArgs          = F.EVar . fst <$> xts-                      , let mbT            = if null xArgs then Nothing else M.lookup f sigs-                   ]-  where-    axioms       = gsMyAxioms refl ++ gsImpAxioms refl-    refl         = gsRefl sp-    sigs         = M.fromList [ (GM.simplesymbol v, t) | (v, t) <- gsTySigs (gsSig sp) ]--equationBody :: Bool -> F.Expr -> [F.Expr] -> F.Expr -> Maybe LocSpecType -> F.Expr-equationBody allowTC f xArgs e mbT-  | Just t <- mbT = F.pAnd [eBody, rBody t]-  | otherwise     = eBody-  where-    eBody         = F.PAtom F.Eq (F.eApps f xArgs) e-    rBody t       = specTypeToLogic allowTC xArgs (F.eApps f xArgs) (val t)---- NV Move this to types?--- sound but imprecise approximation of a type in the logic-specTypeToLogic :: Bool -> [F.Expr] -> F.Expr -> SpecType -> F.Expr-specTypeToLogic allowTC es expr st-  | ok        = F.subst su (F.PImp (F.pAnd args) res)-  | otherwise = F.PTrue-  where-    res       = specTypeToResultRef expr st-    args      = zipWith mkExpr (mkReft <$> ts) es-    mkReft t  =  toReft $ Mb.fromMaybe mempty (stripRTypeBase t)-    mkExpr (F.Reft (v, ev)) e = F.subst1 ev (v, e)---    ok      = okLen && okClass && okArgs-    okLen   = length xs == length xs-    okClass = all (isTauto . snd) cls-    okArgs  = all okArg ts--    okArg (RVar _ _) = True-    okArg t@RApp{}   = isTauto (t{rt_reft = mempty})-    okArg _          = False---    su           = F.mkSubst $ zip xs es-    (cls, nocls) = L.partition ((if allowTC then isEmbeddedClass else isClassType).snd) $ zip (ty_binds trep) (ty_args trep)-                 :: ([(F.Symbol, SpecType)], [(F.Symbol, SpecType)])-    (xs, ts)     = unzip nocls :: ([F.Symbol], [SpecType])--    trep = toRTypeRep st-  specTypeToResultRef :: F.Expr -> SpecType -> F.Expr specTypeToResultRef e t

@@ -33,7 +33,6 @@   , modSummaryHsFile   , makeFamInstEnv   , clearSpec-  , checkFilePragmas   , lookupTyThing   , updLiftedSpec   ) where@@ -50,7 +49,6 @@                                                                ) import qualified Liquid.GHC.API as Ghc -import Control.Exception import Control.Monad import Control.Monad.Trans.Maybe @@ -61,7 +59,6 @@  import Text.PrettyPrint.HughesPJ        hiding (first, (<>)) import Language.Fixpoint.Types          hiding (err, panic, Error, Result, Expr)-import qualified Language.Fixpoint.Misc as Misc import Language.Haskell.Liquid.GHC.Misc import Language.Haskell.Liquid.GHC.Types (MGIModGuts(..)) import Language.Haskell.Liquid.GHC.Play@@ -151,19 +148,6 @@       "modSummaryHsFile: missing .hs file for " ++       showPpr (ms_mod modSummary))     (ml_hs_file $ ms_location modSummary)--checkFilePragmas :: [Located String] -> IO ()-checkFilePragmas = Misc.applyNonNull (return ()) throw . mapMaybe err-  where-    err pragma-      | check (val pragma) = Just (ErrFilePragma $ fSrcSpan pragma :: Error)-      | otherwise          = Nothing-    check pragma           = any (`isPrefixOf` pragma) bad-    bad =-      [ "-i", "--idirs"-      , "-g", "--ghc-option"-      , "--c-files", "--cfiles"-      ]  -------------------------------------------------------------------------------- -- | Family instance information

@@ -110,7 +110,7 @@   , pluginRecompile       = purePlugin   }   where-    liquidPlugin :: (MonadIO m) => [CommandLineOption] -> a -> (Config -> m a) -> m a+    liquidPlugin :: MonadIO m => [CommandLineOption] -> a -> (Config -> m a) -> m a     liquidPlugin opts def go = do         cfg <- liftIO $ LH.getOpts opts         if skipModule cfg then return def else go cfg@@ -123,17 +123,24 @@     typecheckPlugin opts summary gblEnv = liquidPlugin opts gblEnv $ \cfg ->       typecheckPluginGo cfg summary gblEnv -    -- Unfortunately, we can't make Haddock run the LH plugin, because the former-    -- does mangle the '.hi' files, causing annotations to not be persisted in the-    -- 'ExternalPackageState' and/or 'HomePackageTable'. For this reason we disable-    -- the plugin altogether if the module is being compiled with Haddock.-    -- See also: https://github.com/ucsd-progsys/liquidhaskell/issues/1727-    -- for a post-mortem.     typecheckPluginGo cfg summary gblEnv = do-      logger <- getLogger-      dynFlags <- getDynFlags-      withTiming logger (text "LiquidHaskell" <+> brackets (ppr $ ms_mod_name summary)) (const ()) $ do-        if gopt Opt_Haddock dynFlags+      logger0 <- getLogger+      let logger = updateLogFlags logger0 (maybeDDumpTimings cfg)+      GHC.withTiming+        logger (text "LiquidHaskellCPU" <+> brackets (ppr $ ms_mod_name summary)) (const ()) $+        GHC.withTimingWallClock+          logger (text "LiquidHaskell" <+> brackets (ppr $ ms_mod_name summary)) (const ()) $ do+        dynFlags <- getDynFlags+        -- Haddock runs the LH plugin, but it does not expose the annotations of dependencies.+        -- This makes verification fail, so for now, we disable the plugin when haddock runs it.+        --+        -- Detecting if Haddock is running the plugin is not obvious enough. We+        -- try to see for now if Haddock comments are being collected and if the+        -- noBackend is set.+        --+        -- See https://gitlab.haskell.org/ghc/ghc/-/issues/26761+        -- and https://github.com/ucsd-progsys/liquidhaskell/issues/2188+        if gopt Opt_Haddock dynFlags && GHC.backendName (backend dynFlags) == GHC.NoBackend           then do             -- Warn the user             let msg     = PJ.vcat [ PJ.text "LH can't be run with Haddock."@@ -155,6 +162,13 @@               Right newGblEnv' ->                 pure newGblEnv' +    -- We instruct LH to collect timings instead of doing it directly to GHC+    -- This helps work around https://github.com/haskell/cabal/issues/11116+    maybeDDumpTimings :: Config -> LogFlags -> LogFlags+    maybeDDumpTimings cfg =+      if ddumpTimings cfg then log_set_dopt Opt_D_dump_timings+      else id+ -------------------------------------------------------------------------------- -- | Inter-phase communication ------------------------------------------------- --------------------------------------------------------------------------------@@ -300,7 +314,7 @@  liquidCheckModule :: Config -> ModSummary -> TcGblEnv -> [BPspec] -> TcM (Either LiquidCheckException TcGblEnv) liquidCheckModule cfg0 ms tcg specs = do-  withPragmas cfg0 thisFile pragmas $ \cfg -> do+  withPragmas cfg0 pragmas $ \cfg -> do     pipelineData <- do       env <- getTopEnv       session <- Session <$> liftIO (newIORef env)@@ -308,7 +322,6 @@     liquidLib <- setGblEnv tcg $ liquidHaskellCheckWithConfig cfg pipelineData ms     traverse (serialiseSpec tcg) liquidLib   where-    thisFile = LH.modSummaryHsFile ms     pragmas = [ s | Pragma s <- specs ]  mkPipelineData :: (GhcMonad m) => ModSummary -> TcGblEnv -> [BPspec] -> m PipelineData@@ -412,10 +425,10 @@       out <- liftIO $ LH.checkTargetInfo pmrTargetInfo        let bareSpec = lhInputSpec lhContext-          file = LH.modSummaryHsFile $ lhModuleSummary lhContext -      withPragmas (lhGlobalCfg lhContext) file (Ms.pragmas bareSpec) $ \moduleCfg ->  do+      withPragmas (lhGlobalCfg lhContext) (Ms.pragmas bareSpec) $ \moduleCfg ->  do         let filters = getFilters moduleCfg+            file = LH.modSummaryHsFile $ lhModuleSummary lhContext         -- Report the outcome of the checking         LH.reportResult (errorLogger file filters) moduleCfg [giTarget (giSrc pmrTargetInfo)] out         -- If there are unmatched filters or errors, and we are not reporting with@@ -448,11 +461,13 @@ -- | Working with bare & lifted specs ------------------------------------------ -------------------------------------------------------------------------------- +-- | Loads the specs of direct dependencies and /their/ dependencies as well. loadDependencies :: Config -> [Module] -> TcM TargetDependencies loadDependencies currentModuleConfig mods = do   hscEnv    <- env_top <$> getEnv   results   <- SpecFinder.findRelevantSpecs                  (excludeAutomaticAssumptionsFor currentModuleConfig) hscEnv mods+  -- REVIEW: What does reversing the list accomplishes here?   let deps = TargetDependencies $ foldl' processResult mempty (reverse results)   redundant <- liftIO $ configToRedundantDependencies hscEnv currentModuleConfig @@ -498,14 +513,8 @@   debugLog ("Module ==> " ++ renderModule thisModule)    let bareSpec0       = lhInputSpec-  -- /NOTE/: For the Plugin to work correctly, we shouldn't call 'canonicalizePath', because otherwise-  -- this won't trigger the \"external name resolution\" as part of 'Language.Haskell.Liquid.Bare.Resolve'-  -- (cfr. 'allowExtResolution').-  let file            = LH.modSummaryHsFile lhModuleSummary -  _                   <- liftIO $ LH.checkFilePragmas $ Ms.pragmas bareSpec0--  withPragmas lhGlobalCfg file (Ms.pragmas bareSpec0) $ \moduleCfg -> do+  withPragmas lhGlobalCfg (Ms.pragmas bareSpec0) $ \moduleCfg -> do     dependencies <- loadDependencies moduleCfg lhRelevantModules      debugLog $ "Found " <> show (HM.size $ getDependencies dependencies) <> " dependencies:"@@ -518,6 +527,7 @@     hscEnv <- getTopEnv     let preNormalizedCore = preNormalizeCore moduleCfg modGuts0         modGuts = modGuts0 { mg_binds = preNormalizedCore }+        file = LH.modSummaryHsFile lhModuleSummary     targetSrc  <- liftIO $ makeTargetSrc moduleCfg file modGuts hscEnv     logger <- getLogger @@ -587,6 +597,9 @@     putStrLn "\n*************** Pre-normalized CoreBinds *****************\n"     putStrLn $ unlines $ L.intersperse "" $ map (GHC.showPpr (GHC.hsc_dflags hscEnv)) (mg_binds modGuts)   coreBinds <- anormalize cfg hscEnv modGuts+  when (dumpNormalizedCore cfg) $ do+    putStrLn "\n*************** normalized CoreBinds *****************\n"+    putStrLn $ unlines $ L.intersperse "" $ map (GHC.showPpr (GHC.hsc_dflags hscEnv)) coreBinds    let allTcs      = mgi_tcs mgiModGuts 

@@ -9,8 +9,6 @@ {-# OPTIONS_GHC -Wno-orphans #-}  module Language.Haskell.Liquid.GHC.TypeRep (-  mkTyArg, -   showTy   ) where @@ -19,9 +17,6 @@ import           Language.Fixpoint.Types (symbol)  -- e368f3265b80aeb337fbac3f6a70ee54ab14edfd--mkTyArg :: TyVar -> TyVarBinder-mkTyArg v = Bndr v Required  instance Eq Type where   t1 == t2 = eqType' t1 t2

@@ -9,7 +9,7 @@ -- entities remains work in progress. -- -- Haskell entities include all functions that LH might reflect, or types that--- might be referred in refinment types, type aliases or other annotations.+-- might be referred in refinement types, type aliases or other annotations. -- -- Logic entities include the names of reflected functions, inlined functions, -- uninterpreted functions, predefined functions, local bindings, reflected data@@ -23,16 +23,15 @@ -- * Next the names of Haskell entities are resolved by 'resolveLHNames'. --   For now, this pass doesn't change the type of the names. -- * Next the names of logic entities are resolved. This pass produces---   a 'BareSpecLHName', where 'Symbol's are replaced with 'LHName'. At---   the moment most LHNames are just wrappers over the symbols. As name---   resolution is implemented for logic names, the wrappers will be---   replaced with the actual result of name resolution.+--   a 'BareSpecLHName', where 'Symbol's are replaced with 'LHName'. ----- 'BareSpecLHName' has a bijection to 'BareSpec' via a 'LogicNameEnv'+-- 'BareSpecLHName' has an approximate bijection to 'BareSpec' via a 'LogicNameEnv' -- which allows to convert 'LHName' to an unambiguous form of 'Symbol' -- and back. The bijection is implemented with the functions 'toBareSpecLHName' -- and 'fromBareSpecLHName'. This allows to use liquid-fixpoint functions -- unmodified as they will continue to operate on (now unambiguous) Symbols.+-- The bijection is approximate because in the roundtrip the representation of+-- LHName's might change. -- -- At the same time, the 'BareSpecLHName' form is kept to serialize and to -- resolve names of modules that import the specs.@@ -53,6 +52,7 @@   , exprArg   , fromBareSpecLHName   , toBareSpecLHName+  , symbolToLHName   , LogicNameEnv(..)   ) where @@ -63,19 +63,20 @@ import           Language.Haskell.Liquid.Types.RType import           Language.Haskell.Liquid.Types.RTypeOp +import           Control.Monad.Except (ExceptT, runExceptT, throwError) import           Control.Monad ((<=<), mplus, unless, void) import           Control.Monad.Identity import           Control.Monad.State.Strict-import           Data.Bifunctor (first)+import           Data.Bifunctor (first, second) import qualified Data.Char                               as Char import           Data.Coerce (coerce)-import           Data.Data (Data, gmapT)-import           Data.Generics (extT)+import           Data.Data (Data, gmapM)+import           Data.Generics (extM)   import qualified Data.HashSet                            as HS import qualified Data.HashMap.Strict                     as HM-import           Data.List (find, isSuffixOf, nubBy)+import           Data.List (find, isSuffixOf, nubBy, partition) import           Data.List.Extra (dropEnd) import qualified Data.Map as Map import           Data.Maybe (fromMaybe, listToMaybe, mapMaybe, maybeToList)@@ -85,6 +86,7 @@ import           Language.Fixpoint.Types as F hiding (Error, panic) import qualified Language.Haskell.Liquid.Bare.Resolve as Resolve import           Language.Haskell.Liquid.Bare.Types (LocalVars(lvNames), LocalVarDetails(lvdLclEnv))+import           Language.Fixpoint.Misc as Misc import           Language.Haskell.Liquid.Name.LogicNameEnv import qualified Language.Haskell.Liquid.Types.DataDecl as DataDecl import           Language.Haskell.Liquid.Types.Errors (TError(ErrDupNames, ErrResolve), panic)@@ -98,36 +100,58 @@  -- | Collects type aliases from the current module and its dependencies. ----- It doesn't matter at the moment in which module a type alias is defined.--- Type alias names cannot be qualified at the moment, and therefore their--- names identify them uniquely.+-- By construction, type alises from transitive dependencies are neglected (see 'moduleAliases').+-- We do so because all type aliases in scope are added to the 'LiftedSpec' later.+-- Aliases with the same unqualified name coexist during name resolution,+-- as long as we have a means to disambiguate (namely, by qualifing the import).+-- In this case, when building the 'LiftedSpec' we carry only the first such alias according+-- to lexicographic order. collectTypeAliases-  :: GHC.Module+  :: GHC.ImportedMods+  -> GHC.Module   -> BareSpecParsed   -> TargetDependencies-  -> HM.HashMap Symbol (GHC.Module, RTAlias Symbol ())-collectTypeAliases m spec deps =-    let bsAliases = [ (rtName a, (m, void a)) | a <- map val (aliases spec) ]-        depAliases =-          [ (rtName a, (GHC.unStableModule sm, void a))+  -> InScopeEnv (RTAlias Symbol ())+collectTypeAliases impMods thisModule spec deps =+    let bsAliases = mkAliasEnv thisModule impMods (thisModule, bsNames)+        bsNames = [ (val . rtName $ rta, void rta) | rta <- aliases spec]+        depAliases = map (mkAliasEnv thisModule impMods) $+          [ (m, depNames)           | (sm, lspec) <- HM.toList (getDependencies deps)-          , a <- map val (HS.toList $ liftedAliases lspec)+          , let m = GHC.unStableModule sm+          , let depNames = [ (val . rtName $ rta , void rta)+                           | rta <- HS.toList $ liftedAliases lspec+                           ]           ]      in-        HM.fromList $ bsAliases ++ depAliases+        unionAliasEnvs $ bsAliases : depAliases -collectExprAliases-  :: BareSpecParsed-  -> TargetDependencies-  -> HS.HashSet Symbol-collectExprAliases spec deps =-    let bsAliases = HS.fromList $ map (rtName . val) (ealiases spec)-        depAliases =-          [ HS.map (rtName . val) $ liftedEaliases lspec-          | (_, lspec) <- HM.toList (getDependencies deps)-          ]-     in-        HS.unions $ bsAliases : depAliases+--------------------------------------------------------------------------------+-- | [NOTE:EXPRESSION-ALIASES]:+--+-- In a lifted spec, expression aliases include fully unfolded predicate,+-- inline, and define annotations. By contrast, a bare spec’s expression+-- aliases include only predicate aliases. This is because symbols from these+-- three kinds of annotations are unfolded uniformly in logical expressions+-- during spec lifting.+--+-- Inlines and defines are converted to expression aliases via 'lmapEalias',+-- which assigns them a 'GeneratedLogicName'. This allows us to distinguish+-- them from predicate aliases, which should be the only 'LogicName's among+-- expression aliases.+--+-- Here, we collect the symbols of inlines and defines from expression aliases+-- to identify their uses when resolving logic variable names.+-- This should be redundant when these aliases are resolved via the+-- logic environments and a dedicated lifted field for inlines is added.+--------------------------------------------------------------------------------+collectInlinesAndDefines:: TargetDependencies -> HS.HashSet Symbol+collectInlinesAndDefines deps = HS.unions+  [ HS.map lhNameToResolvedSymbol depInlinesAndDefines+  | (_, lspec) <- HM.toList (getDependencies deps)+  , let exprAliases = HS.map (val . rtName) $ liftedEaliases lspec+        depInlinesAndDefines = HS.filter (not . isResolvedLogicName) exprAliases+   ]  -- | Converts occurrences of LHNUnresolved to LHNResolved using the provided -- type aliases and GlobalRdrEnv.@@ -140,59 +164,66 @@   -> BareSpecParsed   -> TargetDependencies   -> Either [Error] (BareSpec, LogicNameEnv, LogicMap)-resolveLHNames cfg thisModule localVars impMods globalRdrEnv bareSpec0 dependencies = do-    let ((bs, logicNameEnv, lmap2), ro) =-          flip runState RenameOutput {roErrors = [], roUsedNames = [], roUsedDataCons = mempty} $ do-            -- A generic traversal that resolves names of Haskell entities-            sp1 <- mapMLocLHNames (\l -> (<$ l) <$> resolveLHName l) $-                     fixExpressionArgsOfTypeAliases taliases bareSpec0-            -- Data decls contain fieldnames that introduce measures with the-            -- same names. We resolved them before constructing the logic-            -- environment.-            dataDecls <- mapM (mapDataDeclFieldNamesM resolveFieldLogicName) (dataDecls sp1)-            let sp2 = sp1 {dataDecls}+resolveLHNames cfg thisModule localVars impMods globalRdrEnv bareSpec0 dependencies =+  flip evalState RenameOutput { roErrors = [], roUsedNames = [], roUsedDataCons = mempty } $+    runExceptT $ do+      -- Prepare type aliases for resolution.+      sp0 <- lift $ fixExpressionArgsOfTypeAliases taliases $ resolveBoundVarsInTypeAliases bareSpec0 -            es0 <- gets roErrors-            if null es0 then do+      checkErrors -              -- Now we do a second traversal to resolve logic names-              let (inScopeEnv, logicNameEnv0, privateReflectNames, unhandledNames) =-                    makeLogicEnvs impMods thisModule sp2 dependencies-              -- Add resolved local defines to the logic map-                  lmap1 =-                    lmap <> mkLogicMap (HM.fromList $-                                         (\(k , v) ->-                                             let k' = lhNameToResolvedSymbol <$> k in-                                             (F.val k', (val <$> v) { lmVar = k' }))-                                         <$> defines sp2)-              sp3 <- fromBareSpecLHName <$>-                       resolveLogicNames-                         cfg-                         inScopeEnv-                         globalRdrEnv-                         unhandledNames-                         lmap1-                         localVars-                         logicNameEnv0-                         privateReflectNames-                         allEaliases-                         sp2-              dcs <- gets roUsedDataCons-              return (sp3 {usedDataCons = dcs} , logicNameEnv0, lmap1)-            else-              return ( error "resolveLHNames: invalid spec"-                     , error "resolveLHNames: invalid logic environment"-                     , error "resolveLHNames: invalid logic map")-        logicNameEnv' = extendLogicNameEnv logicNameEnv (roUsedNames ro)-    if null (roErrors ro) then-      Right (bs, logicNameEnv', lmap2)-    else-      Left (roErrors ro)+      -- First resolution pass: A generic traversal that resolves names+      -- of Haskell entities and type alias binders.+      sp1 <- lift $ mapMLocLHNames (\l -> (<$ l) <$> resolveLHName l) sp0++      -- Data decls contain fieldnames that introduce measures with the+      -- same names. We resolve them before constructing the logic+      -- environments.+      dataDecls <- lift $ mapM (mapDataDeclFieldNamesM resolveFieldLogicName) (dataDecls sp1)+      let sp2 = sp1 {dataDecls}++      checkErrors++      -- Second resolution pass: a traversal to resolve logic names using the following+      -- lookup environments.+      let (inScopeEnv, logicNameEnv0, privateReflectNames) =+            makeLogicEnvs impMods thisModule sp2 dependencies++          -- Add resolved local defines to the logic map.+          lmap1 = lmap <> mkLogicMap (HM.fromList $+                   [ (F.val $ lhNameToResolvedSymbol <$> k,+                      (val <$> v) { lmVar = lhNameToResolvedSymbol <$> k })+                   | (k,v) <- defines sp2 ])+      sp3 <- lift $ fromBareSpecLHName <$>+                  resolveLogicNames+                    cfg+                    thisModule+                    inScopeEnv+                    globalRdrEnv+                    lmap1+                    localVars+                    logicNameEnv0+                    privateReflectNames+                    depsInlinesAndDefines+                    sp2++      checkErrors++      dcs <- gets roUsedDataCons+      return (sp3 { usedDataCons = dcs }, logicNameEnv0, lmap1)   where-    taliases = collectTypeAliases thisModule bareSpec0 dependencies-    allEaliases = collectExprAliases bareSpec0 dependencies+    -- Early exit name resolution if errors are found and pass them to the output.+    checkErrors :: ExceptT [Error] (StateT RenameOutput Identity) ()+    checkErrors = do+      es <- gets roErrors+      unless (null es) (throwError es) -    -- add defines from dependencies to the logical map+    -- We collect type aliases before resolving names so we have a means to disambiguate+    -- imported and local ones (according to their resolution status).+    taliases = collectTypeAliases impMods thisModule bareSpec0 dependencies+    depsInlinesAndDefines = collectInlinesAndDefines dependencies++    -- Add defines from dependencies to the logical map.     lmap =         (LH.listLMap <>) $         mconcat $@@ -207,7 +238,7 @@      resolveLHName lname =       case val lname of-        LHNUnresolved LHTcName s+        LHNUnresolved (LHTcName lcl) s           | isTuple s ->             pure $ LHNResolved (LHRGHC $ GHC.tupleTyConName GHC.BoxedTuple (tupleArity s)) s           | isList s ->@@ -215,24 +246,35 @@           | s == "*" ->             pure $ LHNResolved (LHRGHC GHC.liftedTypeKindTyConName) s           | otherwise ->-            case HM.lookup s taliases of-              Just (m, _) -> pure $ LHNResolved (LHRLogic $ LogicName s m Nothing) s-              Nothing -> lookupGRELHName LHTcName lname s listToMaybe+            case resolveTypeAlias taliases s of+              -- Priority is given to aliases defined in the current module,+              -- so name occurrences are resolved using them, disregarding+              -- any imported aliases with the same name.+              -- This allows the user to shadow imported aliases.+              FoundTypeAliases { tarLocallyDefined = [(m, _, _)] } ->+                pure $ makeLogicLHName (LH.dropModuleNames s) m Nothing+              FoundTypeAliases { tarImported = [(_, lh, _)]+                               , tarLocallyDefined = []} | lcl == LHAnyModuleNameF ->+                pure lh+              -- If multiple matches are found, report the ambiguous name and return it.+              tar@(FoundTypeAliases { }) -> do addError $ errResolveTypeAlias (s <$ lname) tar+                                               pure $ val lname+              NoSuchTypeAlias alts -> lookupGRELHName alts (LHTcName lcl) lname s listToMaybe         LHNUnresolved ns@(LHVarName lcl) s           | isDataCon s ->-              lookupGRELHName (LHDataConName lcl) lname s listToMaybe+              lookupGRELHName [] (LHDataConName lcl) lname s listToMaybe           | otherwise ->-              lookupGRELHName ns lname s+              lookupGRELHName [] ns lname s                 (fmap (either id GHC.getName) . Resolve.lookupLocalVar localVars (atLoc lname s))         LHNUnresolved LHLogicNameBinder s ->           pure $ makeLogicLHName s thisModule Nothing         n@(LHNUnresolved LHLogicName _) ->           -- This one will be resolved by resolveLogicNames           pure n-        LHNUnresolved ns s -> lookupGRELHName ns lname s listToMaybe-        n -> pure n+        LHNUnresolved ns@(LHDataConName _) s -> lookupGRELHName [] ns lname s listToMaybe+        n@LHNResolved { } -> pure n -    lookupGRELHName ns lname s localNameLookup =+    lookupGRELHName alts ns lname s localNameLookup =       case maybeDropImported ns $ GHC.lookupGRE globalRdrEnv (mkLookupGRE ns s) of         [e] -> do           let n = GHC.greName e@@ -247,6 +289,7 @@               addError                 (ErrDupNames                    (LH.fSrcSpan lname)+                   "variable"                    (pprint s)                    (map (PJ.text . GHC.showPprUnsafe) es)                 )@@ -257,7 +300,7 @@               pure $ LHNResolved (LHRGHC n') s             Nothing -> do               addError-                (errResolve (nameSpaceKind ns) "Cannot resolve name" (s <$ lname))+                (errResolve alts (nameSpaceKind ns) "Cannot resolve name" (s <$ lname))               pure $ val lname      maybeDropImported ns es@@ -267,13 +310,14 @@     localNameSpace = \case       LHDataConName lcl -> lcl == LHThisModuleNameF       LHVarName lcl -> lcl == LHThisModuleNameF-      LHTcName -> False+      LHTcName lcl -> lcl == LHThisModuleNameF       LHLogicNameBinder -> False       LHLogicName -> False      nameSpaceKind :: LHNameSpace -> PJ.Doc     nameSpaceKind = \case-      LHTcName -> "type constructor"+      LHTcName LHAnyModuleNameF -> "type constructor"+      LHTcName LHThisModuleNameF -> "locally-defined type constructor"       LHDataConName LHAnyModuleNameF -> "data constructor"       LHDataConName LHThisModuleNameF -> "locally-defined data constructor"       LHVarName LHAnyModuleNameF -> "variable"@@ -293,9 +337,20 @@           else             a -errResolve :: PJ.Doc -> String -> LocSymbol -> Error-errResolve k msg lx = ErrResolve (LH.fSrcSpan lx) k (pprint (val lx)) (PJ.text msg)+errResolve :: [Symbol] -> PJ.Doc -> String -> LocSymbol -> Error+errResolve alts k msg ls =+  ErrResolve+    (LH.fSrcSpan ls)+    k+    (pprint $ val ls)+    (if null alts then+        PJ.text msg+      else+        PJ.text msg PJ.$$+        PJ.sep (PJ.text "Maybe you meant one of:" : map pprint alts)+    ) + -- | Produces an LHName from a symbol by looking it in the rdr environment. resolveSymbolToTcName :: GHC.GlobalRdrEnv -> LocSymbol -> Either Error (Located LHName) resolveSymbolToTcName globalRdrEnv lx@@ -306,11 +361,12 @@     | s == "*" =       pure $ LHNResolved (LHRGHC GHC.liftedTypeKindTyConName) s <$ lx     | otherwise =-      case GHC.lookupGRE globalRdrEnv (mkLookupGRE LHTcName s) of+      case GHC.lookupGRE globalRdrEnv (mkLookupGRE (LHTcName LHAnyModuleNameF) s) of         [e] -> Right $ LHNResolved (LHRGHC $ GHC.greName e) s <$ lx-        [] -> Left $ errResolve "type constructor" "Cannot resolve name" lx+        [] -> Left $ errResolve [] "type constructor" "Cannot resolve name" lx         es -> Left $ ErrDupNames                 (LH.fSrcSpan lx)+                "type constructor"                 (pprint s)                 (map (PJ.text . GHC.showPprUnsafe) es)   where@@ -352,7 +408,7 @@   where     mkWhichGREs :: LHNameSpace -> GHC.WhichGREs GHC.GREInfo     mkWhichGREs = \case-      LHTcName -> GHC.SameNameSpace+      LHTcName _ -> GHC.SameNameSpace       LHDataConName _ -> GHC.SameNameSpace       LHVarName _ -> GHC.RelevantGREs         { GHC.includeFieldSelectors = GHC.WantNormal@@ -363,7 +419,7 @@       LHLogicName -> panic Nothing "mkWhichGREs: unexpected namespace LHLogicName"      mkGHCNameSpace = \case-      LHTcName -> GHC.tcName+      LHTcName _ -> GHC.tcName       LHDataConName _ -> GHC.dataName       LHVarName _ -> GHC.Types.Name.Occurrence.varName       LHLogicNameBinder -> panic Nothing "mkGHCNameSpace: unexpected namespace LHLogicNameBinder"@@ -375,11 +431,11 @@ resolveBoundVarsInTypeAliases = updateAliases resolveBoundVars   where     resolveBoundVars boundVars = \case-      LHNUnresolved LHTcName s ->+      LHNUnresolved (LHTcName lcl) s ->         if elem s boundVars then           LHNResolved (LHRLocal s) s         else-          LHNUnresolved LHTcName s+          LHNUnresolved (LHTcName lcl) s       n ->         error $ "resolveLHNames: Unexpected resolved name: " ++ show n @@ -387,8 +443,8 @@     -- arguments of the alias.     updateAliases f spec =        spec-            { aliases = [ Loc sp0 sp1 (a { rtBody = mapLHNames (f args) (rtBody a) })-                        | Loc sp0 sp1 a <- aliases spec+            { aliases = [ a { rtBody = mapLHNames (f args) (rtBody a) }+                        | a <- aliases spec                         , let args = rtTArgs a ++ rtVArgs a                         ]             }@@ -401,44 +457,67 @@ -- > {-@ type Prop E = {v:_ | prop v = E} @-} -- -- the parser builds a type for @Ev (plus n n)@.+-- | @fixExpressionArgsOfTypeAliases taliases spec@ converts types to+-- values when they appear in value positions of type aliases according+-- to @taliases@. --+-- The expression arguments of type aliases are initially parsed as+-- types. This function converts them to expressions.+--+-- For instance, in @Prop (Ev (plus n n))@ where `Prop` is the alias+--+-- > {-@ type Prop E = {v:_ | prop v = E} @-}+--+-- the parser builds a type for @Ev (plus n n)@, making a type+-- constructor of @Ev@ and type variables of @plus@ and @n@. But+-- @Ev@ is really a data constructor, @plus@ is a function, and @n@+-- is a value.  fixExpressionArgsOfTypeAliases-  :: HM.HashMap Symbol (GHC.Module, RTAlias Symbol ())-  -> BareSpecParsed+  :: InScopeEnv (RTAlias Symbol ())   -> BareSpecParsed-fixExpressionArgsOfTypeAliases taliases =-    mapBareTypes go . resolveBoundVarsInTypeAliases+  -> StateT RenameOutput Identity BareSpecParsed+fixExpressionArgsOfTypeAliases taliases = mapMBareTypes go   where-    go :: BareTypeParsed -> BareTypeParsed-    go (RApp c@(BTyCon { btc_tc = Loc _ _ (LHNUnresolved LHTcName s) }) ts rs r)-      | Just (_, rta) <- HM.lookup s taliases =-        RApp c (fixExprArgs (btc_tc c) rta (map go ts)) (map goRef rs) r-    go (RApp c ts rs r) =-        RApp c (map go ts) (map goRef rs) r-    go (RAppTy t1 t2 r)  = RAppTy (go t1) (go t2) r-    go (RFun  x i t1 t2 r) = RFun  x i (go t1) (go t2) r-    go (RAllT a t r)     = RAllT a (go t) r-    go (RAllP a t)       = RAllP a (go t)-    go (RAllE x t1 t2)   = RAllE x (go t1) (go t2)-    go (REx x t1 t2)     = REx   x (go t1) (go t2)-    go (RRTy e r o t)    = RRTy  e r o     (go t)-    go t@RHole{}         = t-    go t@RVar{}          = t-    go t@RExprArg{}      = t-    goRef (RProp ss t)   = RProp ss (go t)+    go :: BareTypeParsed -> StateT RenameOutput Identity BareTypeParsed+    go (RApp c@(BTyCon { btc_tc = lname@(Loc _ _ (LHNUnresolved (LHTcName _) s)) }) ts rs r)+      | tar@(FoundTypeAliases imported local) <- resolveTypeAlias taliases s =+          case (imported, local) of+               -- Local alias definitions get priority over imported ones.+               -- This allows the user to shadow imported aliases.+               (_ ,[(_, _, rta)]) ->+                 RApp <$> pure c <*> fixExprArgs (btc_tc c) rta (mapM go ts) <*> mapM goRef rs <*> pure r+               ([(_, _, rta)] , []) ->+                 RApp <$> pure c <*> fixExprArgs (btc_tc c) rta (mapM go ts) <*> mapM goRef rs <*> pure r+               -- Report ambiguos name and continue traversing.+               _ -> do+                 addError $ errResolveTypeAlias (s <$ lname) tar+                 RApp <$> pure c <*> mapM go ts <*> mapM goRef rs <*> pure r+    go (RApp c ts rs r)    = RApp <$> pure c <*> mapM go ts <*> mapM goRef rs <*> pure r+    go (RAppTy t1 t2 r)    = RAppTy <$> go t1 <*> go t2 <*> pure r+    go (RFun  x i t1 t2 r) = RFun <$> pure x <*> pure i <*> go t1 <*> go t2 <*> pure r+    go (RAllT a t r)       = RAllT <$> pure a <*> go t <*> pure r+    go (RAllP a t)         = RAllP a <$> go t+    go (RAllE x t1 t2)     = RAllE x <$> go t1 <*> go t2+    go (REx x t1 t2)       = REx  x <$> go t1 <*> go t2+    go (RRTy e r o t)      = RRTy  e r o  <$> go t+    go t@RHole{}           = pure t+    go t@RVar{}            = pure t+    go t@RExprArg{}        = pure t+    goRef (RProp ss t)     = RProp ss <$> go t -    fixExprArgs lname rta ts =+    fixExprArgs lname rta mts = do+      ts <- mts       let n = length (rtTArgs rta)           (targs, eargs) = splitAt n ts           msg = "FIX-EXPRESSION-ARG: " ++ showpp (rtName rta)           toExprArg = exprArg (LH.fSourcePos lname) msg-       in targs ++ [ RExprArg $ toExprArg e <$ lname | e <- eargs ]+      pure $ targs ++ [ RExprArg $ toExprArg e <$ lname | e <- eargs ] -mapBareTypes :: (BareTypeParsed -> BareTypeParsed) -> BareSpecParsed -> BareSpecParsed-mapBareTypes f  = go+mapMBareTypes :: forall m a.(Data a, Monad m) => (BareTypeParsed -> m BareTypeParsed) -> a -> m a+mapMBareTypes f  = go   where-    go :: Data a => a -> a-    go = gmapT (go `extT` f)+    go :: forall b. Data b => b -> m b+    go = gmapM (go `extM` f)  -- | exprArg converts a tyVar to an exprVar because parser cannot tell --   this function allows us to treating (parsed) "types" as "value"@@ -448,31 +527,110 @@ --   the string `Prop (Ev (plus n n))` where `Prop` is the alias: --     {-@ type Prop E = {v:_ | prop v = E} @-} --   the parser will chomp in `Ev (plus n n)` as a `BareType` and so---   `exprArg` converts that `BareType` into an `Expr`.+-- | @exprArg@ converts a type to a value.+--   +--   At parse time the arguments of type aliases are all treated as types.+--   This needs fixing before verification because some arguments are+--   meant to be values. Hence, this function to correct the+--   arguments in question. See the documentation of+--   @fixExpressionArgsOfTypeAliases@ for some more context. exprArg :: SourcePos -> String -> BareTypeParsed -> ExprV LocSymbol exprArg l msg = notracepp ("exprArg: " ++ msg) . go   where     go :: BareTypeParsed -> ExprV LocSymbol     go (RExprArg e)     = val e-    go (RVar (BTV x) _)       = EVar x+    go (RVar (BTV x) _) = EVar x     go (RApp x [] [] _) = EVar (getLHNameSymbol <$> btc_tc x)-    go (RApp f ts [] _) = eApps (EVar (getLHNameSymbol <$> btc_tc f)) (go <$> ts)+    go (RApp f ts [] _) = eApps (EVar (renameAmbiguousCtor . getLHNameSymbol <$> btc_tc f)) (go <$> ts)     go (RAppTy t1 t2 _) = EApp (go t1) (go t2)     go z                = panic sp $ Printf.printf "Unexpected expression parameter: %s in %s" (show $ parsedToBareType z) msg     sp                  = Just (LH.sourcePosSrcSpan l) +renameAmbiguousCtor :: Symbol -> Symbol+renameAmbiguousCtor x+  | Just n <- isTyTupleSizedSymbol x = tmTupleSizedSymbol n+  | otherwise = x++-- | A type alias 'lookupInScopeEnv' that distinguishes locally defined names+-- from imported ones based on their resolution status:+-- unresolved names correspond to type aliases defined in the current module,+-- whereas all imported names are expected to be resolved.+resolveTypeAlias+   :: InScopeEnv (RTAlias Symbol a)+   -> Symbol+   -> TypeAliasResolution (RTAlias Symbol a)+resolveTypeAlias taliases s = case lookupInScopeEnv taliases  s of+  Right ns -> let (imported, local) =+                    partition (\(_,lhname,_) -> isResolvedLogicName lhname ) ns+              in FoundTypeAliases imported local+  Left alts -> NoSuchTypeAlias alts++-- | When resolving type aliases we either find matching 'LHName's+-- or similar, but distinct, 'Symbol's.+data TypeAliasResolution a+  = NoSuchTypeAlias [Symbol]+  | FoundTypeAliases+      { tarImported :: [(GHC.Module, LHName, a)]+      , tarLocallyDefined :: [(GHC.Module, LHName, a)]+      }++errResolveTypeAlias :: LocSymbol -> TypeAliasResolution (RTAlias x a) -> Error+errResolveTypeAlias ls (FoundTypeAliases imported local) =+  ErrDupNames (LH.fSrcSpan ls) "type alias" (pprint $ val ls)+    (+      -- Currently, multiple local definitions prevent this error from being raised,+      -- because duplicate names are discarded when constructing the alias environment+      -- for each individual module,+      -- and a local alias always shadows any imported one. Such duplicates are detected+      -- later during validation of the final target spec.+      --+      -- Also, note that collected local type alias names remain unresolved at this stage,+      -- so we must extract their symbol using a function that can safely handle unresolved+      -- names.+      map (\(_, lhn, rta) -> pprint (getLHNameSymbol lhn)+                             PJ.<+>+                             PJ.text "defined in current module at"+                             PJ.<+>+                             pprint  (LH.fSrcSpan . rtName $ rta)+          )+          local+     +++     map (\(m, lhn, rta) -> pprint (lhNameToUnqualifiedSymbol lhn)+                            PJ.<+>+                            PJ.text "imported from module"+                            PJ.<+>+                            PJ.text (GHC.moduleNameString (GHC.moduleName m))+                            PJ.<+>+                            PJ.text "defined at"+                            PJ.<+>+                            pprint (LH.fSrcSpan . rtName $ rta)+         )+         imported+    )+errResolveTypeAlias ls (NoSuchTypeAlias alts) =+  errResolve alts "type alias" "Cannot resolve name" ls++ -- | An environment of names in scope ----- For each symbol we have the aliases with which it is imported and the--- name corresponding to each alias.-type InScopeNonReflectedEnv = SEnv [(GHC.ModuleName, (GHC.Module, LHName))]+-- We construct it using 'mkAliasEnv' and 'unionAliasEnvs' in such a way that each+-- symbol in the environment corresponds to all matching 'LHNames' along with+-- the aliases of the module we import it from.+-- Currently, the parameter is used to include the type alias representation when+-- we 'collectTypeAliases'.+type InScopeEnv a = SEnv [(GHC.ModuleName, (GHC.Module, LHName, a))] --- | Looks the names in scope with the given symbol.--- Returns a list of close but different symbols or a non empty list+type InScopeNonReflectedEnv = InScopeEnv ()++-- | Looks for the 'LHName's in scope with the given symbol,+-- taking possible qualification prefixes into account.+-- Returns a list of close but different symbols or a non-empty list -- with the matched names.-lookupInScopeNonReflectedEnv-  :: InScopeNonReflectedEnv -> Symbol -> Either [Symbol] [(GHC.Module, LHName)]-lookupInScopeNonReflectedEnv env s = do+lookupInScopeEnv+  :: InScopeEnv a -> Symbol -> Either [Symbol] [(GHC.Module, LHName, a)]+lookupInScopeEnv env s = do+    -- The symbol might be qualified or not,+    -- but we use the unqualified symbol for the lookup.     let n = LH.dropModuleNames s     case lookupSEnvWithDistance n env of       Alts closeSyms -> Left closeSyms@@ -486,7 +644,7 @@       if m == "" then n else LH.qualifySymbol m n  -- | Builds an environment of non-reflected names in scope from the module--- aliases for the current module, the spec of the current module, and the specs+-- imports for the current module, the spec of the current module, and the specs -- of the dependencies. -- -- Also returns a LogicNameEnv constructed from the same names.@@ -500,28 +658,16 @@   -> ( InScopeNonReflectedEnv      , LogicNameEnv      , HS.HashSet LocSymbol-     , HS.HashSet Symbol      )-makeLogicEnvs impAvails thisModule spec dependencies =-    let unqualify s =-          if s == LH.qualifySymbol (symbol $ GHC.moduleName thisModule) (LH.dropModuleNames s) then-            LH.dropModuleNames s-          else-            s--        -- Names should be removed from this list as they are supported-        -- by renaming.-        unhandledNames = HS.fromList $-          map unqualify unhandledNamesList ++ map (LH.qualifySymbol (symbol $ GHC.moduleName thisModule)) unhandledNamesList-        unhandledNamesList =-          map (rtName . val) (ealiases spec)-          ++ concatMap (map getLHNameSymbol . snd) unhandledLogicNames-        unhandledLogicNames =-          map (fmap collectUnhandledLiftedSpecLogicNames) dependencyPairs-        logicNames =-          (thisModule, thisModuleNames) :+makeLogicEnvs impMods thisModule spec dependencies =+    let depsLogicNames =           map (fmap collectLiftedSpecLogicNames) dependencyPairs-          ++ unhandledLogicNames+        logicNames =+          (thisModule, thisModuleNames) : depsLogicNames+        nonReflectedNamesWithUnit =+          map+            (second $ map (, ()) . filter isNonReflectedLogicName)+            logicNames         thisModuleNames = concat           [ [ reflectLHName thisModule (val n)             | n <- concat@@ -538,51 +684,70 @@              concatMap DataDecl.dcFields $ concat $              mapMaybe DataDecl.tycDCons $              dataDecls spec+          , [ val (rtName ea) | ea <- ealiases spec ]           ]         privateReflectNames =           mconcat $             privateReflects spec : map (liftedPrivateReflects . snd) dependencyPairs      in-        ( unionAliasEnvs $ map mkAliasEnv logicNames+        ( unionAliasEnvs $ map (mkAliasEnv thisModule impMods) nonReflectedNamesWithUnit         , mkLogicNameEnv (concatMap snd logicNames)         , privateReflectNames-        , unhandledNames         )   where     dependencyPairs = map (first GHC.unStableModule) $ HM.toList $ getDependencies dependencies -    mkAliasEnv (m, lhnames) =-      let aliases = moduleAliases m-       in fromListSEnv-            [ (s, map (,(m, lhname)) aliases)-              -- Note that only non-reflected names go to the InScope environment.-              -- See the local function resolveVarName for more details.-            | lhname@(LHNResolved (LHRLogic (LogicName s _ Nothing)) _) <- lhnames-            ]+    mkLogicNameEnv names =+      LogicNameEnv+        { lneLHName = fromListSEnv [ (lhNameToResolvedSymbol n, n) | n <- names ]+        , lneReflected = GHC.mkNameEnv [(rn, n) | n <- names, Just rn <- [maybeReflectedLHName n]]+        } -    unionAliasEnvs :: [InScopeNonReflectedEnv] -> InScopeNonReflectedEnv-    unionAliasEnvs =-      coerce .-      HM.map (nubBy (\(alias1, (_, n1)) (alias2, (_, n2)) -> alias1 == alias2 && n1 == n2)) .-      foldl' (HM.unionWith (++)) HM.empty .-      coerce @_ @[HM.HashMap Symbol [(GHC.ModuleName, (GHC.Module, LHName))]]+unionAliasEnvs :: forall a. [InScopeEnv a] -> InScopeEnv a+unionAliasEnvs =+    coerce .+    -- We make sure that the module alias and the 'LHName' effectively disambiguate+    -- the occurrence of a symbol. This is because the same name can come from+    -- several imported modules.+    HM.map (nubBy (\(alias1, (_, n1, _)) (alias2, (_, n2, _)) -> alias1 == alias2 && n1 == n2)) .+    foldl' (HM.unionWith (++)) HM.empty .+    coerce @_ @[HM.HashMap Symbol [(GHC.ModuleName, (GHC.Module, LHName, a))]] -    moduleAliases m =-      case Map.lookup m impAvails of-        Just impBys -> concatMap imvAliases $ GHC.importedByUser impBys-        Nothing-          | thisModule == m ->-            -- Aliases for the current module-            [GHC.moduleName m, GHC.mkModuleName ""]-          | otherwise ->-            -- Use the aliases of the unsuffixed module-            concatMap imvAliases $ GHC.importedByUser $-              concat $ maybeToList $ do-                pString <- dropLHAssumptionsSuffix m-                pMod <- findDependency pString-                Map.lookup pMod impAvails+-- | Builds a symbol lookup environment from a list of names associated with the+-- module they were extracted from, adding any import aliases that module may+-- have within the current module (if it was imported directly).+mkAliasEnv:: GHC.Module -> GHC.ImportedMods -> (GHC.Module, [(LHName, a)]) -> InScopeEnv a+mkAliasEnv thisModule impMods (m, lhnames) =+    let aliases = moduleAliases thisModule impMods m+     in fromListSEnv+          -- Note that when building a name environment for the current module+          -- we might process unresolved names here.+          [ (LH.dropModuleNames $ getLHNameSymbol lhname+            , map (,(m, lhname, x)) aliases)+          | (lhname, x) <- lhnames+          ] -    dropLHAssumptionsSuffix m =+-- | Produces the list of aliases a module is imported with.+-- The first parameter holds the reference to the current module.+-- Transitive dependencies get an empty alias list.+moduleAliases :: GHC.Module -> GHC.ImportedMods -> GHC.Module -> [GHC.ModuleName]+moduleAliases thisModule impMods m =+    case Map.lookup m impMods of+      -- Aliases for imported modules.+      Just impBys -> concatMap imvAliases $ GHC.importedByUser impBys+      Nothing+        | thisModule == m ->+          -- Aliases for the current module.+          [GHC.moduleName m, GHC.mkModuleName ""]+        | otherwise ->+          -- For LHAssumptions modules, use the aliases of the unsuffixed module.+          concatMap imvAliases $ GHC.importedByUser $+            concat $ maybeToList $ do+              pString <- dropLHAssumptionsSuffix+              pMod <- findDependency pString+              Map.lookup pMod impMods+  where+    dropLHAssumptionsSuffix =       let mString = GHC.moduleNameString (GHC.moduleName m)           sfx = "_LHAssumptions"        in if isSuffixOf sfx mString then@@ -592,31 +757,22 @@      findDependency ms =       find ((ms ==) . GHC.moduleNameString . GHC.moduleName) $-      Map.keys impAvails+      Map.keys impMods      imvAliases imv       | GHC.imv_qualified imv = [GHC.imv_name imv]       | otherwise = [GHC.imv_name imv, GHC.mkModuleName ""] -    mkLogicNameEnv names =-      LogicNameEnv-        { lneLHName = fromListSEnv [ (lhNameToResolvedSymbol n, n) | n <- names ]-        , lneReflected = GHC.mkNameEnv [(rn, n) | n <- names, Just rn <- [maybeReflectedLHName n]]-        }--{- HLINT ignore collectUnhandledLiftedSpecLogicNames "Use ++" -}-collectUnhandledLiftedSpecLogicNames :: LiftedSpec -> [LHName]-collectUnhandledLiftedSpecLogicNames sp =-    map (makeLocalLHName . LH.dropModuleNames . rtName . val) $ HS.toList $ liftedEaliases sp- collectLiftedSpecLogicNames :: LiftedSpec -> [LHName] collectLiftedSpecLogicNames sp = concat     [ map fst (HS.toList $ liftedExpSigs sp)     , map (val . msName) (HM.elems $ liftedMeasures sp)     , map (val . msName) (HM.elems $ liftedCmeasures sp)+    , map (val . msName) (HS.toList $ liftedOmeasures sp)     , map fst $ concatMap DataDecl.dcFields $ concat $         mapMaybe DataDecl.tycDCons $         HS.toList $ liftedDataDecls sp+    , map  (val . rtName) $ HS.toList $ liftedEaliases sp     ]  -- | Resolves names in the logic namespace@@ -626,9 +782,9 @@ -- the names of data constructors that are found during renaming. resolveLogicNames   :: Config+  -> GHC.Module   -> InScopeNonReflectedEnv   -> GHC.GlobalRdrEnv-  -> HS.HashSet Symbol   -> LogicMap   -> LocalVars   -> LogicNameEnv@@ -636,7 +792,7 @@   -> HS.HashSet Symbol   -> BareSpecParsed   -> State RenameOutput BareSpecLHName-resolveLogicNames cfg env globalRdrEnv unhandledNames lmap0 localVars lnameEnv privateReflectNames allEaliases sp = do+resolveLogicNames cfg thisModule env globalRdrEnv lmap0 localVars lnameEnv privateReflectNames depsInlinesAndDefines sp = do     -- Instance measures must be defined for names of class measures.     -- The names of class measures should be in @env@     imeasures <- mapM (mapMeasureNamesM resolveIMeasLogicName) (imeasures sp)@@ -659,7 +815,7 @@         -- The name is local       | elem s ss = return $ makeLocalLHName s       | otherwise =-        case lookupInScopeNonReflectedEnv env s of+        case lookupInScopeEnv env s of           Left alts ->             -- If names are not in the environment, they must be data constructors,             -- or they must be reflected functions, or they must be in the logicmap.@@ -669,39 +825,33 @@                 | elem s wiredInNames ->                   return $ makeLocalLHName s                 | otherwise -> do-                  unless (HS.member s unhandledNames) $-                    addError (errResolveLogicName ls alts)-                  return $ makeLocalLHName s-          Right [(_, lhname)] ->-            return lhname-          Right names -> do-            addError $-              ErrDupNames-                (LH.fSrcSpan ls)-                (pprint s)-                [ pprint (lhNameToResolvedSymbol n) PJ.<+>-                  PJ.text-                    ("imported from " ++ GHC.moduleNameString (GHC.moduleName m))-                | (m, n) <- names-                ]-            return $ makeLocalLHName s+                    addError $ errResolve alts "logic name" "Cannot resolve name" ls+                    return $ makeLocalLHName s+          Right [(_, lhname, _)] -> pure lhname+          -- In case of multiple matches, we give precedence to locally defined+          -- logic entities for the user to be able to overwrite them.+          -- TODO: When a mechanism allowing to specify explicitly which logic names+          -- are imported is in place, we should cosider notifying the ambiguity directly.+          Right names ->+            case filter ((== thisModule) . logicNameOriginModule . Misc.snd3) names of+              [(_, lhname, _)] -> pure lhname+              _ -> do addError $ errDupInScopeNames ls names+                      return $ makeLocalLHName s       where         s = val ls         wiredInNames =            map fst wiredSortedSyms ++            map (lhNameToResolvedSymbol . fst) (concatMap (DataDecl.dcpTyArgs . val) wiredDataCons)--    errResolveLogicName s alts =-      ErrResolve-        (LH.fSrcSpan s)-        (PJ.text "logic name")-        (pprint $ val s)-        (if null alts then-           PJ.text "Cannot resolve name"-         else-           PJ.text "Cannot resolve name" PJ.$$-           PJ.sep (PJ.text "Maybe you meant one of:" : map pprint alts)-        )+        errDupInScopeNames locSym inScopeNames =+          ErrDupNames+            (LH.fSrcSpan locSym)+            "non-reflected logic entity"+            (pprint (val locSym))+            [ pprint (lhNameToResolvedSymbol n) PJ.<+>+              PJ.text+                ("imported from " ++ GHC.moduleNameString (GHC.moduleName m))+            | (m, n, _) <- inScopeNames+            ]      resolveDataConName ls       | unqualifiedS == ":" = Just $@@ -739,6 +889,7 @@             addError               (ErrDupNames                  (LH.fSrcSpan s)+                 "data constructor"                  (pprint $ val s)                  (map (PJ.text . GHC.showPprUnsafe) es)               )@@ -763,9 +914,8 @@           -> case gres of           [e] -> do             let n = GHC.greName e-            -- TODO: The check for allEaliases should be redundant when-            -- ealiases are put in the logic environments-            if HM.member (symbol n) (lmSymDefs lmap) || HS.member (symbol n) allEaliases then+            -- See [NOTE:EXPRESSION-ALIASES]+            if HM.member (symbol n) (lmSymDefs lmap) || HS.member (symbol n) depsInlinesAndDefines then               Just $ do                 let lhName = makeLogicLHName (symbol $ GHC.getOccString n) (GHC.nameModule n) Nothing                 addName lhName@@ -779,6 +929,7 @@               addError                  (ErrDupNames                    (LH.fSrcSpan s)+                   "variable"                    (pprint $ val s)                    (map (PJ.text . GHC.showPprUnsafe) es)                  )@@ -808,7 +959,7 @@       return c{DataDecl.dcFields}  toBareSpecLHName :: Config -> LogicNameEnv -> BareSpec -> BareSpecLHName-toBareSpecLHName cfg env sp0 = runIdentity $ go sp0+toBareSpecLHName cfg lenv sp0 = runIdentity $ go sp0   where     -- This is implemented with a monadic traversal to reuse the logic     -- that collects the local symbols in scope.@@ -817,19 +968,24 @@       emapSpecM         (bscope cfg)         (const [])-        symbolToLHName-        (emapBareTypeVM (bscope cfg) symbolToLHName)+        symToLHName+        (emapBareTypeVM (bscope cfg) symToLHName)         sp +    symToLHName = symbolToLHName "toBareSpecLHName" lenv unhandledNames+     unhandledNames = HS.fromList $ map fst $ expSigs sp0 -    symbolToLHName :: [Symbol] -> Symbol -> Identity LHName-    symbolToLHName ss s-      | elem s ss = return $ makeLocalLHName s-      | otherwise =-        case lookupSEnv s (lneLHName env) of-          Nothing -> do-            unless (HS.member s unhandledNames) $-              panic Nothing $ "toBareSpecLHName: cannot find " ++ show s-            return $ makeLocalLHName s-          Just lhname -> return lhname+-- | Uses the logic name environment to convert a resolved 'Symbol' to 'LHName'.+-- Symbols not present in the environment correspond to local symbols (e.g.+-- bounded variables) or are explicitly left unhandled.+symbolToLHName :: String -> LogicNameEnv -> HS.HashSet Symbol -> [Symbol] -> Symbol -> Identity LHName+symbolToLHName caller lenv unhandledNames ss s+  | elem s ss = return $ makeLocalLHName s+  | otherwise =+    case lookupSEnv s (lneLHName lenv) of+      Nothing -> do+        unless (HS.member s unhandledNames) $+          panic Nothing $ caller ++ ": cannot find " ++ show s+        return $ makeLocalLHName s+      Just lhname -> return lhname

@@ -12,6 +12,7 @@ import qualified Data.HashSet as S  import           Text.PrettyPrint.HughesPJ import           Control.Monad (when)+import qualified Data.HashMap.Strict as HashMap import qualified Data.Maybe as Mb import qualified Data.List  as L  import qualified Language.Haskell.Liquid.UX.DiffCheck as DC@@ -133,29 +134,30 @@ solveCs cfg tgt cgi info names = do   finfo            <- cgInfoFInfo info cgi   let fcfg          = fixConfig tgt cfg-  F.Result {resStatus=r0, resSolution=sol} <- solve fcfg finfo+  F.Result {resStatus=r0, resSolution=solCuts, resNonCutsSolution=solNonCuts} <- solve fcfg finfo+  let sol           = HashMap.union (HashMap.map F.Delayed solCuts) solNonCuts   let failBs        = gsFail $ gsTerm $ giSpec info   let (r,rf)        = splitFails (S.map val failBs) r0 -  let resErr        = second (applySolution sol . cinfoError) <$> r+  let resErr        = second (applySolution finfo sol . cinfoError) <$> r   -- resModel_        <- fmap (e2u cfg sol) <$> getModels info cfg resErr-  let resModel_     = cidE2u cfg sol <$> resErr-  let resModel'     = resModel_  `addErrors` (e2u cfg sol <$> logErrors cgi)+  let resModel_     = cidE2u cfg <$> resErr+  let resModel'     = resModel_  `addErrors` (e2u cfg <$> logErrors cgi)                                  `addErrors` makeFailErrors (S.toList failBs) rf                                   `addErrors` makeFailUseErrors (S.toList failBs) (giCbs $ giSrc info)-  let lErrors       = applySolution sol <$> logErrors cgi-  let resModel      = resModel' `addErrors` (e2u cfg sol <$> lErrors)-  let out0          = mkOutput cfg resModel sol (annotMap cgi)+  let lErrors       = applySolution finfo sol <$> logErrors cgi+  let resModel      = resModel' `addErrors` (e2u cfg <$> lErrors)+  let out0          = mkOutput cfg resModel finfo sol (annotMap cgi)   return            $ out0 { o_vars    = names    }                            { o_result  = resModel }  -e2u :: Config -> F.FixSolution -> Error -> UserError-e2u cfg s = fmap F.pprint . tidyError cfg s+e2u :: Config -> Error -> UserError+e2u cfg = fmap F.pprint . tidyError cfg -cidE2u :: Config -> F.FixSolution -> (Integer, Error) -> UserError-cidE2u cfg s (subcId, e) =+cidE2u :: Config -> (Integer, Error) -> UserError+cidE2u cfg (subcId, e) =   let e' = attachSubcId e-   in fmap F.pprint (tidyError cfg s e')+   in fmap F.pprint (tidyError cfg e')   where     attachSubcId es@ErrSubType{}      = es { cid = Just subcId }     attachSubcId es@ErrSubTypeModel{} = es { cid = Just subcId }@@ -178,7 +180,7 @@      go :: CoreBind -> [(Var,[Var])]     go (NonRec x e) = [(x, readVars e)] -    go (Rec xes)    = [(x,cls) | x <- map fst xes] where cls = concatMap readVars (snd <$> xes)+    go (Rec xes)    = [(x,cls) | x <- map fst xes] where cls = concatMap (readVars . snd) xes  makeFailErrors :: [F.Located Var] -> [Cinfo] -> [UserError] makeFailErrors bs cis = [ mkError x | x <- bs, notElem (val x) vs ]  

@@ -92,7 +92,7 @@ dataConTypes allowTC  s = (ctorTys, measTys)   where     measTys     = [(msName m, msSort m) | m <- M.elems (measMap s) ++ imeas s]-    ctorTys     = concatMap (makeDataConType allowTC) (notracepp "HOHOH" . snd <$> M.toList (ctorMap s))+    ctorTys     = concatMap (makeDataConType allowTC . notracepp "HOHOH" . snd) (M.toList (ctorMap s))  makeDataConType :: Bool -> [Def (RRType Reft) DataCon] -> [(Var, RRType Reft)] makeDataConType _ []@@ -126,7 +126,7 @@     isWorkerDef def       -- types are missing for arguments, so definition came from a logical measure       -- and it is for the worker datacon-      | any Mb.isNothing (snd <$> binds def)+      | any (Mb.isNothing . snd) (binds def)       = True       | otherwise       = length (binds def) == length (fst $ splitFunTys $ snd $ splitForAllTyCoVars wot)

@@ -346,6 +346,9 @@     getFst     = head . sortOn fst     krvss      = groupList [ (k, (r, v)) | (r, k, v) <- rkvs ] +ordNub :: Ord a => [a] -> [a]+ordNub = map head . L.group . L.sort+ sortOn :: (Ord b) => (a -> b) -> [a] -> [a] sortOn f = L.sortBy (compare `on` f) 

@@ -13,8 +13,9 @@ -- Symbols are expected to have been created by 'lhNameToResolvedSymbol'. -- data LogicNameEnv = LogicNameEnv-       { lneLHName :: SEnv LHName-         -- | Haskell names that have a reflected counterpart+       { -- | A (qualified) symbol map to resolve logic names.+         lneLHName :: SEnv LHName+         -- | Haskell names that have a reflected counterpart.        , lneReflected :: GHC.NameEnv LHName        } 

@@ -241,7 +241,7 @@              b <- locInfixSymbolP              PC _ t2 <- btP              return $ PC sb $ RApp-               (mkBTyCon $ fmap (makeUnresolvedLHName LHTcName) b)+               (mkBTyCon $ fmap (makeUnresolvedLHName (LHTcName LHAnyModuleNameF)) b)                [t1,t2]                []                trueURef@@ -458,9 +458,9 @@ bTyConP :: Parser BTyCon bTyConP   =  (reservedOp "'" >> mkPromotedBTyCon <$> locUpperIdLHNameP (LHDataConName LHAnyModuleNameF))- <|> mkBTyCon <$> locUpperIdLHNameP LHTcName+ <|> mkBTyCon <$> locUpperIdLHNameP (LHTcName LHAnyModuleNameF)  <|> (reserved "*" >>-        return (mkBTyCon (dummyLoc $ makeUnresolvedLHName LHTcName $ symbol ("*" :: String)))+        return (mkBTyCon (dummyLoc $ makeUnresolvedLHName (LHTcName LHAnyModuleNameF) $ symbol ("*" :: String)))      )  <?> "bTyConP" @@ -471,7 +471,7 @@ mkPromotedBTyCon x = BTyCon x False True -- (consSym '\'' <$> x) False True  classBTyConP :: Parser BTyCon-classBTyConP = mkClassBTyCon <$> locUpperIdLHNameP LHTcName+classBTyConP = mkClassBTyCon <$> locUpperIdLHNameP (LHTcName LHAnyModuleNameF)  mkClassBTyCon :: Located LHName -> BTyCon mkClassBTyCon x = BTyCon x True False@@ -770,8 +770,8 @@      -> [RTPropV v BTyCon tv (UReftV v r)]      -> r      -> RTypeV v BTyCon tv (UReftV v r)-bLst (Just t) rs r = RApp (mkBTyCon $ dummyLoc $ makeUnresolvedLHName LHTcName listConName) [t] rs (reftUReft r)-bLst Nothing  rs r = RApp (mkBTyCon $ dummyLoc $ makeUnresolvedLHName LHTcName listConName) []  rs (reftUReft r)+bLst (Just t) rs r = RApp (mkBTyCon $ dummyLoc $ makeUnresolvedLHName (LHTcName LHAnyModuleNameF) listConName) [t] rs (reftUReft r)+bLst Nothing  rs r = RApp (mkBTyCon $ dummyLoc $ makeUnresolvedLHName (LHTcName LHAnyModuleNameF) listConName) []  rs (reftUReft r)  bTup :: [(Maybe Symbol, BareTypeParsed)]      -> [RTPropV LocSymbol BTyCon BTyVar (UReftV LocSymbol (ReftV LocSymbol))]@@ -781,13 +781,13 @@   | isTauto (fmap val r)  = t   | otherwise  = t `strengthenUReft` reftUReft r bTup ts rs r-  | all Mb.isNothing (fst <$> ts) || length ts < 2+  | all (Mb.isNothing . fst) ts || length ts < 2   = RApp-      (mkBTyCon $ dummyLoc $ makeUnresolvedLHName LHTcName $ fromString $ "Tuple" ++ show (length ts))+      (mkBTyCon $ dummyLoc $ makeUnresolvedLHName (LHTcName LHAnyModuleNameF) $ tyTupleSizedSymbol (length ts))       (snd <$> ts) rs (reftUReft r)   | otherwise   = RApp-      (mkBTyCon $ dummyLoc $ makeUnresolvedLHName LHTcName $ fromString $ "Tuple" ++ show (length ts))+      (mkBTyCon $ dummyLoc $ makeUnresolvedLHName (LHTcName LHAnyModuleNameF) $ tyTupleSizedSymbol (length ts))       (mapReft (const trueURef) . snd <$> ts)       rs'       (reftUReft r)@@ -845,7 +845,6 @@     go (PIff p1 p2) = PIff (go p1) (go p2)     go (PAtom r e1 e2) = PAtom r (go e1) (go e2)     go (PKVar k su') = PKVar k $ su' `appendSubst` su0-    go (PGrad k su' i e) = PGrad k (su' `appendSubst` su0) i (go e)     go (PAll _ _) = panic Nothing "substExprV: PAll"     go (PExist _ _) = panic Nothing "substExprV: PExist"     go p = p@@ -887,9 +886,9 @@   | RInst   (RInstance LocBareTypeParsed)                 -- ^ refined 'instance' definition   | Invt    LocBareTypeParsed                             -- ^ 'invariant' specification   | Using  (LocBareTypeParsed, LocBareTypeParsed)         -- ^ 'using' declaration (for local invariants on a type)-  | Alias   (Located (RTAlias Symbol BareTypeParsed))     -- ^ 'type' alias declaration-  | EAlias  (Located (RTAlias Symbol (ExprV LocSymbol)))  -- ^ 'predicate' alias declaration-  | Embed   (Located LHName, FTycon, TCArgs)              -- ^ 'embed' declaration+  | Alias   (RTAlias Symbol BareTypeParsed)               -- ^ 'type' alias declaration+  | EAlias  (RTAlias Symbol (ExprV LocSymbol))            -- ^ 'predicate' alias declaration+  | Embed   (Located LHName, Sort, TCArgs)                -- ^ 'embed' declaration   | Qualif  (QualifierV LocSymbol)                        -- ^ 'qualif' definition   | LVars   (Located LHName)                              -- ^ 'lazyvar' annotation, defer checks to *use* sites   | Lazy    (Located LHName)                              -- ^ 'lazy' annotation, skip termination check on binder@@ -899,6 +898,7 @@   | Insts   (Located LHName)                              -- ^ 'auto-inst' or 'ple' annotation; use ple locally on binder   | HMeas   (Located LHName)                              -- ^ 'measure' annotation; lift Haskell binder as measure   | Reflect (Located LHName)                              -- ^ 'reflect' annotation; reflect Haskell binder as function in logic+  | Stratified (Located LHName)                           -- ^ 'stratified' annotation; stratification check for type declarations   | PrivateReflect LocSymbol                              -- ^ 'private-reflect' annotation   | OpaqueReflect (Located LHName)                        -- ^ 'opaque-reflect' annotation   | Inline  (Located LHName)                              -- ^ 'inline' annotation;  inline (non-recursive) binder as an alias@@ -956,9 +956,9 @@   = "invariant" <+> pprintTidy k (parsedToBareType <$> t) ppPspec k (Using (t1, t2))   = "using" <+> pprintTidy k (parsedToBareType <$> t1) <+> "as" <+> pprintTidy k (parsedToBareType <$> t2)-ppPspec k (Alias   (Loc _ _ rta))+ppPspec k (Alias rta)   = "type" <+> pprintTidy k (fmap parsedToBareType rta)-ppPspec k (EAlias  (Loc _ _ rte))+ppPspec k (EAlias rte)   = "predicate" <+> pprintTidy k rte ppPspec k (Embed   (lx, tc, NoArgs))   = "embed" <+> pprintTidy k (val lx)         <+> "as" <+> pprintTidy k tc@@ -984,6 +984,8 @@   = "measure" <+> pprintTidy k (val lx) ppPspec k (Reflect lx)   = "reflect" <+> pprintTidy k (val lx)+ppPspec k (Stratified lx)+  = "stratified" <+> pprintTidy k (val lx) ppPspec k (PrivateReflect lx)   = "private-reflect" <+> pprintTidy k (val lx) ppPspec k (OpaqueReflect lx)@@ -1085,7 +1087,7 @@   , Measure.newtyDecls = [d | NTDecl d <- xs]   , Measure.aliases    = [a | Alias  a <- xs]   , Measure.ealiases   = [e | EAlias e <- xs]-  , Measure.embeds     = tceFromList [(c, (fTyconSort tc, a)) | Embed (c, tc, a) <- xs]+  , Measure.embeds     = tceFromList [(c, (s, a)) | Embed (c, s, a) <- xs]   , Measure.qualifiers = [q | Qualif q <- xs]   , Measure.lvars      = S.fromList [d | LVars d  <- xs]   , Measure.autois     = S.fromList [s | Insts s <- xs]@@ -1106,6 +1108,7 @@   , Measure.rewriteWith = M.fromList [s | Rewritewith s <- xs]   , Measure.bounds     = M.fromList [(bname i, i) | PBound i <- xs]   , Measure.reflects   = S.fromList [s | Reflect s <- xs]+  , Measure.stratified = S.fromList [s | Stratified s <- xs]   , Measure.privateReflects = S.fromList [s | PrivateReflect s <- xs]   , Measure.opaqueReflects = S.fromList [s | OpaqueReflect s <- xs]   , Measure.hmeas      = S.fromList [s | HMeas  s <- xs]@@ -1129,6 +1132,7 @@     -- TODO: These next two are synonyms, kill one     <|> fallbackSpecP "axiomatize"  (fmap Reflect locBinderLHNameP)     <|> fallbackSpecP "reflect"     (fmap Reflect locBinderLHNameP)+    <|> fallbackSpecP "stratified"  (fmap Stratified tyConThisModuleBindLHNameP)     <|> (reserved "private-reflect" >> fmap PrivateReflect axiomP  )     <|> (reserved "opaque-reflect" >> fmap OpaqueReflect locBinderLHNameP  ) @@ -1205,7 +1209,7 @@ axiomP = locBinderP  datavarianceP :: Parser (Located LHName, [Variance])-datavarianceP = liftM2 (,) (locUpperIdLHNameP LHTcName) (many varianceP)+datavarianceP = liftM2 (,) (locUpperIdLHNameP (LHTcName LHAnyModuleNameF)) (many varianceP)  dsizeP :: Parser ([Located BareTypeParsed], Located Symbol) dsizeP = liftM2 (,) (parens $ sepBy (located genBareTypeP) comma) locBinderP@@ -1280,35 +1284,33 @@ genBareTypeP :: Parser BareTypeParsed genBareTypeP = bareTypeP -embedP :: Parser (Located LHName, FTycon, TCArgs)+embedP :: Parser (Located LHName, Sort, TCArgs) embedP = do-  x <- locUpperIdLHNameP LHTcName+  x <- locUpperIdLHNameP (LHTcName LHAnyModuleNameF)   a <- try (reserved "*" >> return WithArgs) <|> return NoArgs -- TODO: reserved "*" looks suspicious   _ <- reserved "as"-  t <- fTyConP-  return (x, t, a)+  s <- sortP+  return (x, s, a)   --  = xyP locUpperIdP symbolTCArgs (reserved "as") fTyConP  -aliasP :: Parser (Located (RTAlias Symbol BareTypeParsed))+aliasP :: Parser (RTAlias Symbol BareTypeParsed) aliasP  = rtAliasP id     bareTypeP <?> "aliasP" -ealiasP :: Parser (Located (RTAlias Symbol (ExprV LocSymbol)))+ealiasP :: Parser (RTAlias Symbol (ExprV LocSymbol)) ealiasP = try (rtAliasP symbol predP)       <|> rtAliasP symbol exprP       <?> "ealiasP"  -- | Parser for a LH type synonym.-rtAliasP :: (Symbol -> tv) -> Parser ty -> Parser (Located (RTAlias tv ty))+rtAliasP :: (Symbol -> tv) -> Parser ty -> Parser (RTAlias tv ty) rtAliasP f bodyP-  = do pos  <- getSourcePos-       name <- upperIdP+  = do lname <- locBinderLogicNameP        args <- many aliasIdP        reservedOp "="        body <- bodyP-       posE <- getSourcePos        let (tArgs, vArgs) = partition (isSmall . headSym) args-       return $ Loc pos posE (RTA name (f <$> tArgs) vArgs body)+       return $ RTA lname (f <$> tArgs) vArgs body  logDefineP :: Parser BPspec logDefineP =@@ -1525,8 +1527,11 @@ bbindP   = lowerIdP <* reservedOp "::"  tyConBindLHNameP :: Parser (Located LHName)-tyConBindLHNameP = locUpperIdLHNameP LHTcName+tyConBindLHNameP = locUpperIdLHNameP (LHTcName LHAnyModuleNameF) +tyConThisModuleBindLHNameP :: Parser (Located LHName)+tyConThisModuleBindLHNameP = locUpperIdLHNameP (LHTcName LHThisModuleNameF)+ dataConP :: [Symbol] -> Parser DataCtorParsed dataConP as = do   x   <- dataConLHNameP@@ -1593,7 +1598,7 @@  emptyDecl :: LocSymbol -> SourcePos -> Maybe (SizeFunV LocSymbol) -> DataDeclParsed emptyDecl x pos fsize@(Just _)-  = DataDecl (DnName $ makeUnresolvedLHName LHTcName <$> x) [] [] Nothing pos fsize Nothing DataUser+  = DataDecl (DnName $ makeUnresolvedLHName (LHTcName LHAnyModuleNameF) <$> x) [] [] Nothing pos fsize Nothing DataUser emptyDecl x pos _   = uError (ErrBadData (sourcePosSrcSpan pos) (pprint (val x)) msg)   where@@ -1609,7 +1614,7 @@   return      $ DataDecl dn as ps (Just dcs) pos fsize pTy DataUser  dataDeclName :: SourcePos -> LocSymbol -> Bool -> [DataCtorParsed] -> DataName-dataDeclName _ x True  _     = DnName $ makeUnresolvedLHName LHTcName <$> x  -- vanilla data    declaration+dataDeclName _ x True  _     = DnName $ makeUnresolvedLHName (LHTcName LHAnyModuleNameF) <$> x  -- vanilla data    declaration dataDeclName _ _ False (d:_) = DnCon  $ dcName d                             -- family instance declaration dataDeclName p x _  _        = uError (ErrBadData (sourcePosSrcSpan p) (pprint (val x)) msg)   where

@@ -13,7 +13,6 @@  import           Debug.Trace (trace) import           Prelude                          hiding (error)-import           Language.Haskell.Liquid.GHC.TypeRep import           Liquid.GHC.API  as Ghc hiding ( get, mkTyArg                                                                 , showPpr                                                                 , DsM@@ -36,6 +35,7 @@ import           Data.Hashable import Data.HashMap.Strict (HashMap) import qualified Data.HashMap.Strict as HM+import GHC.Core.Type (ForAllTyBinder)  -------------------------------------------------------------------------------- -- | A-Normalize a module ------------------------------------------------------@@ -70,20 +70,20 @@   where     t'       = subst msg as as' bt     msg      = "WARNING: unable to renameVars on " ++ GM.showPpr x-    as'      = fst $ splitForAllTyCoVars $ exprType e-    (as, bt) = splitForAllTyCoVars (varType x)+    as'      = fst $ splitForAllForAllTyBinders $ exprType e+    (as, bt) = splitForAllForAllTyBinders (varType x) normalizeTyVars (Rec xes)    = Rec xes'   where     nrec     = normalizeTyVars <$> (uncurry NonRec <$> xes)     xes'     = (\case NonRec x e -> (x, e); _ -> impossible Nothing "This cannot happen") <$> nrec -subst :: String -> [TyVar] -> [TyVar] -> Type -> Type+subst :: String -> [ForAllTyBinder] -> [ForAllTyBinder] -> Type -> Type subst msg as as' bt   | length as == length as'-  = mkForAllTys (mkTyArg <$> as') $ substTy su bt+  = mkForAllTys as' $ substTy su bt   | otherwise-  = trace msg $ mkForAllTys (mkTyArg <$> as) bt-  where su = mkTvSubstPrs $ zip as (mkTyVarTys as')+  = trace msg $ mkForAllTys as bt+  where su = mkTvSubstPrs $ zip (map binderVar as) (mkTyVarTys (map binderVar as'))  -- | eta-expand CoreBinds with quantified types normalizeForAllTys :: CoreExpr -> CoreExpr

@@ -61,7 +61,7 @@   _                -> False  dfunIdSubst :: DFunId -> CoreExpr -> M.HashMap Id (Id, M.HashMap Id Id)-dfunIdSubst dfunId e = M.fromList $ zip auxIds (repeat (dfunId, methodToAux))+dfunIdSubst dfunId e = M.fromList [(auxId, (dfunId, methodToAux)) | auxId <- auxIds]  where   methodToAux = M.fromList     [ (m, aux) | m <- methods, aux <- auxIds, aux `isClassOpAuxOf` m ]

@@ -284,8 +284,8 @@                 } -- ^ sort error in specification    | ErrDupAlias { pos  :: !SrcSpan-                , var  :: !Doc                 , kind :: !Doc+                , var  :: !Doc                 , locs :: ![SrcSpan]                 } -- ^ multiple alias with same name error @@ -311,9 +311,10 @@                 } -- ^ duplicate fields in same datacon    | ErrDupNames { pos   :: !SrcSpan+                , kind  :: !Doc                 , var   :: !Doc                 , names :: ![Doc]-                } -- ^ name resolves to multiple possible GHC vars+                } -- ^ name resolves to multiple matches    | ErrBadData  { pos :: !SrcSpan                 , var :: !Doc@@ -484,10 +485,41 @@    | ErrCtorRefinement { pos :: !SrcSpan                       , ctorName :: !Doc-                      } -- ^ The refinement of a data constructor doesn't admit-                        -- a refinement on the return type that-                        -- isn't deemd safe-+                      }+    -- ^ The refinement of a data constructor doesn't admit a+    -- refinement on the return type that isn't deemd safe+  | ErrStratNotAdt { pos :: !SrcSpan+                   , tyName :: !Doc+                   }+    -- ^ Type was declared stratified but it is not an ADT+  | ErrStratNotRefCtor { pos :: !SrcSpan+                       , ctorName :: !Doc+                       , tyName :: !Doc+                       }+    -- ^ Type was declared stratified but one of its constructors is not a+    -- refinement constructor (i.e. it has no refinement)+  | ErrStratNotPropRet { pos :: !SrcSpan+                       , tyName :: !Doc+                       , ctorName :: !Doc+                       , retTy  :: !Doc+                       }+    -- ^ Type was declared stratified but one of its constructors does not+    -- return a Prop type+  | ErrStratOccProp { pos :: !SrcSpan+                      , tyName :: !Doc+                      , ctorName :: !Doc+                      , tyNR :: !Doc+                      }+    -- ^ Type was declared stratified but one of its constructors has a recursive+    -- occurence that is not a Prop type+  | ErrStratIdxNotSmall { pos :: !SrcSpan+                        , tyName :: !Doc+                        , ctorName :: !Doc+                        , retIdx :: !Doc+                        , occIdx :: !Doc+                        }+  -- ^ Type was declared stratified but one of its constructors has a recursive+  -- occurence whose index type is not a smaller   | ErrOther    { pos   :: SrcSpan                 , msg   :: !Doc                 } -- ^ Sigh. Other.@@ -901,8 +933,8 @@         $+$ dCtx         $+$ nest 4 (text "Duplicated definitions for field" <+> ppTicks x) -ppError' _ dCtx (ErrDupNames _ x ns)-  = text "Ambiguous specification symbol" <+> ppTicks x+ppError' _ dCtx (ErrDupNames _ k v ns)+  = text "Ambiguous specification symbol"  <+> ppTicks v <+> "for" <+> pprint k         $+$ dCtx         $+$ ppNames ns @@ -1063,13 +1095,50 @@              , "To deactivate or understand the need of positivity check, see:"              , " "              , nest 2 "https://ucsd-progsys.github.io/liquidhaskell/options/#positivity-check"+             , "or consider making the type stratified"+             , nest 2 "http://ucsd-progsys.github.io/liquidhaskell/specifications/#stratified-types"             ]  ppError' _ dCtx (ErrCtorRefinement _ ctorName)   = text "Refinement of the data constructor" <+> ctorName <+> "doesn't admit an arbitrary refinements on the return type"         $+$ dCtx-        $+$ nest 4 (text "Were you trying to use `Prop` from `Language.Haskell.Liquid.ProofCombinators`?")+        $+$ nest 4 (text "Were you trying to use `Ix` from `Language.Haskell.Liquid.ProofCombinators`?")         $+$ nest 4 (text "You can disable this error by enabling the flag `--allow-unsafe-constructors`")++ppError' _ dCtx (ErrStratNotAdt _ tyName)+  = text "The type" <+> tyName+      <+> "was declared stratified but it is not an algebraic data type"+      $+$ dCtx++ppError' _ dCtx (ErrStratNotRefCtor _ ctorName tyName)+  = text "The constructor" <+> ctorName+      <+> "of the type" <+> tyName+      <+> "was declared stratified but it is not a refinement constructor (i.e. it has no refinement)"+      $+$ dCtx++ppError' _ dCtx (ErrStratNotPropRet _ tyName ctorName retTy)+  = text "The constructor" <+> ctorName+      <+> "of the type" <+> tyName+      <+> "was declared stratified but it does not return an indexed type, instead it returns"+      <+> retTy+      $+$ dCtx++ppError' _ dCtx (ErrStratOccProp _ tyName ctorName tyNR)+  = text "The constructor" <+> ctorName+      <+> "of the type" <+> tyName+      <+> "was declared stratified but it has a recursive occurence of type"+      <+> tyNR+      <+> "which is not an indexed type"+      $+$ dCtx++ppError' _ dCtx (ErrStratIdxNotSmall _ tyName ctorName retIdx occIdx)+  = text "The constructor" <+> ctorName+      <+> "of the type" <+> tyName+      <+> "was declared stratified but it has a recursive occurence whose index"+      <+> occIdx+      <+> "is not smaller than the return index"+      <+> retIdx+      $+$ dCtx  ppError' _ dCtx (ErrParseAnn _ msg)   = text "Malformed annotation"

@@ -6,7 +6,12 @@ module Language.Haskell.Liquid.Types.Names   ( lenLocSymbol   , anyTypeSymbol+  , propSymbol+  , getPropIndex   , selfSymbol+  , tyTupleSizedSymbol+  , isTyTupleSizedSymbol+  , tmTupleSizedSymbol   , LogicName (..)   , LHResolvedName (..)   , LHName (..)@@ -32,6 +37,10 @@   , reflectGHCName   , reflectLHName   , updateLHNameSymbol+  , isNonReflectedLogicName+  , logicNameOriginModule+  , isResolvedLogicName+  , isGeneratedLogicName   ) where  import Control.DeepSeq@@ -39,6 +48,7 @@ import Data.Data (Data, gmapM, gmapT) import Data.Generics (extM, extT) import Data.Hashable+import Data.Maybe (isNothing) import Data.String (fromString) import qualified Data.Text                               as Text import GHC.Generics@@ -46,10 +56,21 @@ import GHC.Stack import Language.Fixpoint.Types import Language.Haskell.Liquid.GHC.Misc ( locNamedThing ) -- Symbolic GHC.Name+import Text.Read (readMaybe) import qualified Liquid.GHC.API as GHC  import GHC.Types (Any) +propSymbol :: Symbol+propSymbol = "Language.Haskell.Liquid.ProofCombinators.prop"++getPropIndex :: ReftV Symbol -> Maybe (ExprV Symbol)+getPropIndex (Reft (v, PAtom Eq (EApp (EVar n) (EVar v')) idx))+  | n == propSymbol+  , v == v'+  = Just idx+getPropIndex _ = Nothing+ -- RJ: Please add docs lenLocSymbol :: Located Symbol lenLocSymbol = dummyLoc $ symbol ("autolen" :: String)@@ -60,6 +81,20 @@ selfSymbol :: Symbol selfSymbol = symbol ("liquid_internal_this" :: String) +tyTupleSizedSymbol :: Int -> Symbol+tyTupleSizedSymbol n | n < 0     = error "tyTupleSizedSymbol: negative arity"+                     | otherwise = symbol $ "Tuple" ++ show n++isTyTupleSizedSymbol :: Symbol -> Maybe Int+isTyTupleSizedSymbol s = Text.stripPrefix "Tuple" (symbolText s)+                     >>= readMaybe . Text.unpack++tmTupleSizedSymbol :: Int -> Symbol+tmTupleSizedSymbol n | n < 0     = error "tmTupleSizedSymbol: negative arity"+                     | n == 0    = "()"+                     | n == 1    = "MkSolo"+                     | otherwise = symbol $ "(" <> replicate (n - 1) ',' <> ")"+ -- | A name for an entity that does not exist in Haskell -- -- For instance, this can be used to represent predicate aliases@@ -89,7 +124,8 @@       LHRIndex Word   deriving (Data, Eq, Generic, Ord) --- | A name that is potentially unresolved.+-- | A name that is potentially unresolved, carrying along the 'Symbol'+-- found by the parser. data LHName     = -- | In order to integrate the resolved names gradually, we keep the       -- unresolved names.@@ -117,11 +153,11 @@   hashWithSalt s (LHNUnresolved ns sym) = s `hashWithSalt` ns `hashWithSalt` sym  data LHNameSpace-    = LHTcName-    | LHDataConName LHThisModuleNameFlag-    | LHVarName LHThisModuleNameFlag-    | LHLogicNameBinder-    | LHLogicName+    = LHTcName LHThisModuleNameFlag       -- ^ Type constructors+    | LHDataConName LHThisModuleNameFlag  -- ^ Data constructors with procedence+    | LHVarName LHThisModuleNameFlag      -- ^ Variables with procedence+    | LHLogicNameBinder                   -- ^ Logic names (LHS)+    | LHLogicName                         -- ^ Logic names (RHS)   deriving (Data, Eq, Generic, Ord, Show)  instance B.Binary LHNameSpace@@ -374,6 +410,21 @@       )       (symbol n) +isNonReflectedLogicName :: LHName -> Bool+isNonReflectedLogicName lhname = isResolvedLogicName lhname && (isNothing . maybeReflectedLHName) lhname+ maybeReflectedLHName :: LHName -> Maybe GHC.Name maybeReflectedLHName (LHNResolved (LHRLogic (LogicName _ _ m)) _) = m maybeReflectedLHName _ = Nothing++isResolvedLogicName :: LHName -> Bool+isResolvedLogicName (LHNResolved (LHRLogic (LogicName {})) _) = True+isResolvedLogicName _ = False++isGeneratedLogicName :: LHName -> Bool+isGeneratedLogicName (LHNResolved (LHRLogic (GeneratedLogicName _)) _) = True+isGeneratedLogicName _ = False++logicNameOriginModule :: LHName -> GHC.Module+logicNameOriginModule (LHNResolved (LHRLogic (LogicName _ m _)) _) = m+logicNameOriginModule n = error $ "logicNameOriginModule: Not a logic name " ++ show n

@@ -446,7 +446,7 @@ freeArgsPs p (RHole r)   = freeArgsPsRef p r freeArgsPs p (RRTy env r _ t)-  = L.nub $ concatMap (freeArgsPs p) (snd <$> env) ++ freeArgsPsRef p r ++ freeArgsPs p t+  = L.nub $ concatMap (freeArgsPs p . snd) env ++ freeArgsPsRef p r ++ freeArgsPs p t  freeArgsPsRef :: PVar t1 -> UReft t -> [F.Symbol] freeArgsPsRef p (MkUReft _ (Pr ps)) = [x | (_, x, w) <- concatMap pargs ps', F.EVar x == w]

@@ -64,6 +64,7 @@ import           Language.Haskell.Liquid.GHC.Misc import           Language.Haskell.Liquid.Misc import           Language.Haskell.Liquid.Types.Errors+import           Language.Haskell.Liquid.Types.Names (LHName (..), getLHNameSymbol, lhNameToResolvedSymbol) import           Language.Haskell.Liquid.Types.RType import           Language.Haskell.Liquid.Types.RTypeOp import           Language.Haskell.Liquid.Types.Types@@ -169,6 +170,11 @@                                  , nest 2 $ text "axiom-map"                                  , nest 4 $ pprint am                                  ]++instance F.Fixpoint LHName where+  toFix lhname = case lhname of+    LHNUnresolved { }  -> pprintSymbol . getLHNameSymbol $ lhname+    LHNResolved { } -> pprint . lhNameToResolvedSymbol $ lhname  -------------------------------------------------------------------------------- -- | Pretty Printing RefType ---------------------------------------------------

@@ -54,6 +54,9 @@   , Predicate   , PredicateV (..) +  -- * Expression Arguments+  , notExprArg+   -- * Manipulating `Predicates`   , emapExprVM   , mapPredicateV@@ -336,9 +339,8 @@       PKVar k su -> PKVar k <$> emapSubstVM (f . (domain su ++) . (acc ++)) su       PAll bnds e -> PAll bnds <$> go (map fst bnds ++ acc) e       PExist bnds e -> PExist bnds <$> go (map fst bnds ++ acc) e-      PGrad k su gi e ->-        PGrad k <$> emapSubstVM (f . (acc ++)) su <*> pure gi <*> go (domain su ++ acc) e       ECoerc srt0 srt1 e -> ECoerc srt0 srt1 <$> go acc e+      ELet x e1 e2 -> ELet x <$> go acc e1 <*> go (x:acc) e2      domain (Su m) = M.keys m @@ -776,6 +778,10 @@ makeRTVar :: tv -> RTVar tv s makeRTVar a = RTVar a (RTVNoInfo True) +notExprArg :: RTypeV v c tv r -> Bool+notExprArg (RExprArg _) = False+notExprArg _            = True+ instance (Eq tv) => Eq (RTVar tv s) where   t1 == t2 = ty_var_value t1 == ty_var_value t2 @@ -857,7 +863,7 @@ emapUReftVM f g (MkUReft r p) = MkUReft <$> g r <*> emapPredicateVM f p  type BRType      = RTypeV Symbol BTyCon BTyVar    -- ^ "Bare" parsed version-type BRTypeV v   = RTypeV v BTyCon BTyVar         -- ^ "Bare" parsed version+type BRTypeV v   = RTypeV v      BTyCon BTyVar    -- ^ "Bare" parsed version type RRType      = RTypeV Symbol RTyCon RTyVar    -- ^ "Resolved" version type BSort       = BRType    () type BSortV v    = BRTypeV v ()

@@ -107,7 +107,7 @@ import           Text.PrettyPrint.HughesPJ hiding ((<>), first) import           Language.Fixpoint.Misc import           Language.Fixpoint.Types hiding (DataDecl (..), DataCtor (..), panic, shiftVV, Predicate, isNumeric)-import           Language.Fixpoint.Types.Visitor (mapKVars, Visitable)+import           Language.Fixpoint.Types.Visitor (trans, Visitable) import qualified Language.Fixpoint.Types as F import           Language.Haskell.Liquid.Types.Errors import           Language.Haskell.Liquid.Types.PrettyPrint@@ -550,8 +550,8 @@  tyConBTyCon :: TyCon -> BTyCon tyConBTyCon tc =-    mkBTyCon $-      makeResolvedLHName (LHRGHC (getName tc)) . tyConName <$> GM.locNamedThing tc+  mkBTyCon $+    makeResolvedLHName (LHRGHC (getName tc)) . tyConName <$> GM.locNamedThing tc   --- NV TODO : remove this code!!!@@ -1431,12 +1431,12 @@       = mkEApp (dummyLoc $ symbol c) (eVar <$> xs)  isBaseDataCon :: DataCon -> Bool-isBaseDataCon c = and $ isBaseTy <$> map irrelevantMult (dataConOrigArgTys c ++ dataConRepArgTys c)+isBaseDataCon c = all (isBaseTy . irrelevantMult) (dataConOrigArgTys c ++ dataConRepArgTys c)  isBaseTy :: Type -> Bool isBaseTy (TyVarTy _)      = True isBaseTy (AppTy _ _)      = False-isBaseTy (TyConApp _ ts)  = and $ isBaseTy <$> ts+isBaseTy (TyConApp _ ts)  = all isBaseTy ts isBaseTy FunTy{}          = False isBaseTy (ForAllTy _ _)   = False isBaseTy (LitTy _)        = True@@ -1476,9 +1476,6 @@   = TyVarTy α toType useRFInfo (RApp RTyCon{rtc_tc = c} ts _ _)   = TyConApp c (toType useRFInfo <$> filter notExprArg ts)-  where-    notExprArg (RExprArg _) = False-    notExprArg _            = True toType useRFInfo (RAllE _ _ t)   = toType useRFInfo t toType useRFInfo (REx _ _ t)@@ -1541,18 +1538,37 @@ rTypeSort tce = typeSort tce . toType True  ---------------------------------------------------------------------------------applySolution :: (Functor f) => FixSolution -> f SpecType -> f SpecType+applySolution+  :: (Functor f)+  => FInfo a -> M.HashMap KVar (Delayed Expr) -> f SpecType -> f SpecType ---------------------------------------------------------------------------------applySolution = fmap . fmap . mapReft' . appSolRefa+applySolution si = fmap . fmap . mapReft' . appSolRefa si   where     mapReft' f (MkUReft (Reft (x, z)) p) = MkUReft (Reft (x, f z)) p  appSolRefa :: Visitable t-           => M.HashMap KVar Expr -> t -> t-appSolRefa s p = mapKVars f p+           => GInfo c a -> M.HashMap KVar (Delayed Expr) -> t -> t+appSolRefa si s = mapKVars f0   where-    f k        = Just $ M.lookupDefault PTop k s+    f0 k        = Just $ forceDelayed $ M.lookupDefault (Delayed PTop) k s +    mapKVars :: Visitable t => (KVar -> Maybe Expr) -> t -> t+    mapKVars f = trans txK+      where+        txK (PKVar k su)+          | Just p' <- f k =+              rapierSubstExpr (substSymbolsSet su) (renameDomain k su) p'+        txK p = p++        -- The parameters of kvars all seem to have prefix $ and suffix ##k_+        -- at the point where mapKVars is used. We compensate for that here.+        renameDomain k (Su m) =+          Su $ M.fromList+            [ (consSym '$' (suffixSymbol v "k_"), e)+            | v <- kvarDomain si k+            , let e = M.lookupDefault (EVar v) v m+            ]+ -------------------------------------------------------------------------------- -- shiftVV :: Int -- SpecType -> Symbol -> SpecType shiftVV :: (TyConable c, Reftable (f Reft), Functor f)@@ -1583,7 +1599,7 @@ -- MOVE TO TYPES instance (Show tv, Show ty) => Show (RTAlias tv ty) where   show (RTA n as xs t) =-    printf "type %s %s %s = %s" (symbolString n)+    printf "type %s %s %s = %s" (symbolString . getLHNameSymbol . val $ n)       (unwords (show <$> as))       (unwords (show <$> xs))       (show t)@@ -1611,10 +1627,13 @@     go τ                = FObj (typeUniqueSymbol τ)  tyConFTyCon :: TCEmb TyCon -> TyCon -> [Sort] -> Sort-tyConFTyCon tce c ts = case tceLookup c tce of-                         Just (t, WithArgs) -> t-                         Just (t, NoArgs)   -> fApp t ts-                         Nothing            -> fApp (fTyconSort niTc) ts+-- ignore the nat arguments of the Any types, see test/pos/T2535A.hs+-- tyConFTyCon _ c _ | Ghc.zonkAnyTyCon  == c = FObj (symbol c)+tyConFTyCon tce c ts =+  case tceLookup c tce of+    Just (t, WithArgs) -> t+    Just (t, NoArgs)   -> fApp t ts+    Nothing            -> fApp (fTyconSort niTc) ts   where     niTc             = symbolNumInfoFTyCon (dummyLoc $ tyConName c) (isNumCls c) (isFracCls c)     -- oldRes           = F.notracepp _msg $ M.lookupDefault def c tce

@@ -55,6 +55,7 @@   , SpecMeasure   , VarOrLocSymbol   , emapSpecM+  , emapRTAlias   , fromBareSpecLHName   , fromBareSpecParsed   , mapSpecLName@@ -147,7 +148,7 @@  In order to produce these spec types we have to gather information about the module being compiled by using the GHC API and retain enough context of the compiled 'Module' in order to be able to construct the types-introduced aboves. The rest of this module introduced also these intermediate structures.+introduced above. The rest of this module introduces also these intermediate structures. -}  -- $targetInfo@@ -166,9 +167,9 @@   getConfig = getConfig . giSpec  -- | The 'TargetSrc' type is a collection of all the things we know about a module being currently--- checked. It include things like the name of the module, the list of 'CoreBind's,+-- checked. It includes things like the name of the module, the list of 'CoreBind's, -- the 'TyCon's declared in this module (that includes 'TyCon's for classes), typeclass instances--- and so and so forth. It might be consider a sort of 'ModGuts' embellished with LH-specific+-- and so on and so forth. It might be considered a sort of 'ModGuts' embellished with LH-specific -- information (for example, 'giDefVars' are populated with datacons from the module plus the -- let vars derived from the A-normalisation). data TargetSrc = TargetSrc@@ -197,7 +198,7 @@  -- | A 'TargetSpec' is what we /actually check via LiquidHaskell/. It is created as part of 'mkTargetSpec' -- alongside the 'LiftedSpec'. It shares a similar structure with a 'BareSpec', but manipulates and--- transforms the data in preparation to the checking process.+-- transforms the data in preparation for the checking process. data TargetSpec = TargetSpec   { gsSig    :: !GhcSpecSig   , gsQual   :: !GhcSpecQual@@ -242,6 +243,7 @@  data GhcSpecSig = SpSig   { gsTySigs   :: ![(Var, LocSpecType)]           -- ^ Asserted Reftypes+  , gsStratCtos :: ![Name]                        -- ^ Stratified Ctors   , gsAsmSigs  :: ![(Var, LocSpecType)]           -- ^ Assumed Reftypes   , gsAsmReflects  :: ![(Var, Var)]               -- ^ Assumed Reftypes (left is the actual function name and right the pretended one)   , gsRefSigs  :: ![(Var, LocSpecType)]           -- ^ Reflected Reftypes@@ -258,6 +260,7 @@ instance Semigroup GhcSpecSig where   x <> y = SpSig     { gsTySigs   = gsTySigs x   <> gsTySigs y+    , gsStratCtos = gsStratCtos x <> gsStratCtos y     , gsAsmSigs  = gsAsmSigs x  <> gsAsmSigs y     , gsAsmReflects = gsAsmReflects x <> gsAsmReflects y     , gsRefSigs  = gsRefSigs x  <> gsRefSigs y@@ -277,7 +280,7 @@   instance Monoid GhcSpecSig where-  mempty = SpSig mempty mempty mempty mempty mempty mempty mempty mempty mempty mempty mempty+  mempty = SpSig mempty mempty mempty mempty mempty mempty mempty mempty mempty mempty mempty mempty  data GhcSpecData = SpData   { gsCtors      :: ![(Var, LocSpecType)]         -- ^ Data Constructor Measure Sigs@@ -359,7 +362,7 @@ -- $bareSpec  -- | A 'BareSpec' is the spec we derive by parsing the Liquid Haskell annotations of a single file. As--- such, it contains things which are relevant for validation and lifting; it contains things like+-- such, it contains things which are relevant for validation and lifting: -- the pragmas the user defined, the termination condition (if termination-checking is enabled) and so -- on and so forth. /Crucially/, as a 'BareSpec' is still subject to \"preflight checks\", it may contain -- duplicates (e.g. duplicate measures, duplicate type declarations etc.) and therefore most of the fields@@ -387,8 +390,8 @@   , ialiases   :: ![(F.Located ty, F.Located ty)]                     -- ^ Data type invariants to be checked   , dataDecls  :: ![DataDeclP lname ty]                               -- ^ Predicated data definitions   , newtyDecls :: ![DataDeclP lname ty]                               -- ^ Predicated new type definitions-  , aliases    :: ![F.Located (RTAlias F.Symbol (BareTypeV lname))]   -- ^ RefType aliases-  , ealiases   :: ![F.Located (RTAlias F.Symbol (F.ExprV lname))]     -- ^ Expression aliases+  , aliases    :: ![RTAlias F.Symbol (BareTypeV lname)]               -- ^ RefType aliases+  , ealiases   :: ![RTAlias F.Symbol (F.ExprV lname)]                 -- ^ Expression aliases. See [NOTE:EXPRESSION-ALIASES]   , embeds     :: !(F.TCEmb (F.Located LHName))                       -- ^ GHC-Tycon-to-fixpoint Tycon map   , qualifiers :: ![F.QualifierV lname]                               -- ^ Qualifiers in source files   , lvars      :: !(S.HashSet (F.Located LHName))                     -- ^ Variables that should be checked in the environment they are used@@ -397,13 +400,14 @@   , rewriteWith :: !(M.HashMap (F.Located LHName) [F.Located LHName]) -- ^ Definitions using rewrite rules   , fails      :: !(S.HashSet (F.Located LHName))                     -- ^ These Functions should be unsafe   , reflects   :: !(S.HashSet (F.Located LHName))                     -- ^ Binders to reflect+  , stratified :: !(S.HashSet (F.Located LHName))                     -- ^ Type declaration to check for stratification   , privateReflects :: !(S.HashSet F.LocSymbol)                       -- ^ Private binders to reflect   , opaqueReflects :: !(S.HashSet (F.Located LHName))                 -- ^ Binders to opaque-reflect   , autois     :: !(S.HashSet (F.Located LHName))                     -- ^ Automatically instantiate axioms in these Functions   , hmeas      :: !(S.HashSet (F.Located LHName))                     -- ^ Binders to turn into measures using haskell definitions   , inlines    :: !(S.HashSet (F.Located LHName))                     -- ^ Binders to turn into logic inline using haskell definitions   , ignores    :: !(S.HashSet (F.Located LHName))                     -- ^ Binders to ignore during checking; that is DON't check the corebind.-  , autosize   :: !(S.HashSet (F.Located LHName))                     -- ^ Type Constructors that get automatically sizing info+  , autosize   :: !(S.HashSet (F.Located LHName))                     -- ^ Type Constructors that get sizing info automatically   , pragmas    :: ![F.Located String]                                 -- ^ Command-line configurations passed in through source   , cmeasures  :: ![MeasureV lname (F.Located ty) ()]                 -- ^ Measures attached to a type-class   , imeasures  :: ![MeasureV lname (F.Located ty) (F.Located LHName)] -- ^ Mappings from (measure,type) -> measure@@ -439,7 +443,7 @@   :: Monad m   =>      -- | The bscope setting, which affects which names-     -- are considered to be in scope in refinment types.+     -- are considered to be in scope in refinement types.      Bool      -- | For names that have a local environment return the names in scope.   -> (LHName -> [F.Symbol])@@ -460,8 +464,8 @@     ialiases <- mapM (bimapM (traverse fnull) (traverse fnull)) (ialiases sp)     dataDecls <- mapM (emapDataDeclM bscp vf f) (dataDecls sp)     newtyDecls <- mapM (emapDataDeclM bscp vf f) (newtyDecls sp)-    aliases <- mapM (traverse (emapRTAlias (emapBareTypeVM bscp vf))) (aliases sp)-    ealiases <- mapM (traverse (emapRTAlias (\e -> emapExprVM (vf . (++ e))))) $ ealiases sp+    aliases <- mapM (emapRTAlias (emapBareTypeVM bscp vf)) (aliases sp)+    ealiases <- mapM (emapRTAlias (\e -> emapExprVM (vf . (++ e)))) (ealiases sp)     qualifiers <- mapM (emapQualifierM vf) $ qualifiers sp     cmeasures <- mapM (emapMeasureM vf (traverse . f)) (cmeasures sp)     imeasures <- mapM (emapMeasureM vf (traverse . f)) (imeasures sp)@@ -569,8 +573,8 @@       , sigs = map (fmap (fmap (mapRTypeV f . mapReft (mapUReftV f (fmap f))))) sigs       , dataDecls = map (mapDataDeclV f) dataDecls       , newtyDecls = map (mapDataDeclV f) newtyDecls-      , aliases = map (fmap (fmap (mapRTypeV f . fmap (mapUReftV f (fmap f))))) aliases-      , ealiases = map (fmap (fmap (fmap f))) ealiases+      , aliases = map (fmap (mapRTypeV f . fmap (mapUReftV f (fmap f)))) aliases+      , ealiases = map (fmap (fmap f)) ealiases       , qualifiers = map (fmap f) qualifiers       , cmeasures = map (mapMeasureV f) cmeasures       , imeasures = map (mapMeasureV f) imeasures@@ -588,8 +592,8 @@     mapRelationalV f1 (n0, n1, a, b, e0, e1) =       (n0, n1, fmap (mapRTypeV f1 . mapReft (mapUReftV f1 (fmap f1))) a, fmap (mapRTypeV f1 . mapReft (mapUReftV f1 (fmap f1))) b, fmap f1 e0, fmap f1 e1) --- /NOTA BENE/: These instances below are considered legacy, because merging two 'Spec's together doesn't--- really make sense, and we provide this only for legacy purposes.+-- /NOTA BENE/: The instances below are provided for legacy purposes only, because merging two 'Spec's together doesn't+-- really make sense. instance Semigroup (Spec lname ty) where   s1 <> s2     = Spec { measures   =           measures   s1 ++ measures   s2@@ -623,6 +627,7 @@            , rewriteWith = M.union  (rewriteWith s1)  (rewriteWith s2)            , fails      = S.union   (fails    s1)  (fails    s2)            , reflects   = S.union   (reflects s1)  (reflects s2)+           , stratified = S.union (stratified s1) (stratified s2)            , privateReflects = S.union (privateReflects s1) (privateReflects s2)            , opaqueReflects   = S.union   (opaqueReflects s1)  (opaqueReflects s2)            , hmeas      = S.union   (hmeas    s1)  (hmeas    s2)@@ -659,6 +664,7 @@            , autois     = S.empty            , hmeas      = S.empty            , reflects   = S.empty+           , stratified = S.empty            , privateReflects = S.empty            , opaqueReflects = S.empty            , inlines    = S.empty@@ -687,7 +693,7 @@ -- The general motivations for lifting a spec are (a) name resolution, (b) the fact that some info is -- only relevant for checking the body of functions but does not need to be exported, e.g. -- termination measures, or the fact that a type signature was assumed.--- A 'LiftedSpec' is /what we serialise on disk and what the clients should will be using/.+-- A 'LiftedSpec' is /what we serialise on disk and what the clients will be using/. -- -- What we /do not/ have compared to a 'BareSpec': --@@ -728,10 +734,10 @@     -- ^ Predicated data definitions   , liftedNewtyDecls :: HashSet DataDeclLHName     -- ^ Predicated new type definitions-  , liftedAliases    :: HashSet (F.Located (RTAlias F.Symbol BareTypeLHName))+  , liftedAliases    :: HashSet (RTAlias F.Symbol BareTypeLHName)     -- ^ RefType aliases-  , liftedEaliases   :: HashSet (F.Located (RTAlias F.Symbol (F.ExprV LHName)))-    -- ^ Expression aliases+  , liftedEaliases   :: HashSet (RTAlias F.Symbol (F.ExprV LHName))+    -- ^ Expression aliases. See [NOTE:EXPR-ALIASES]   , liftedEmbeds     :: F.TCEmb (F.Located LHName)     -- ^ GHC-Tycon-to-fixpoint Tycon map   , liftedQualifiers :: HashSet (F.QualifierV LHName)@@ -1011,6 +1017,7 @@   , rewrites   = mempty   , rewriteWith = mempty   , reflects   = mempty+  , stratified = mempty   , privateReflects = liftedPrivateReflects a   , opaqueReflects   = mempty   , autois     = liftedAutois a

@@ -368,24 +368,29 @@                                          "\nRHS      :" ++ showPpr rhs  ----------------------------------------------------------------------------------- | Refinement Type Aliases+-- | Refinement Type and Expression Aliases -------------------------------------------------------------------------------- data RTAlias x a = RTA-  { rtName  :: Symbol             -- ^ name of the alias+  { rtName  :: F.Located LHName   -- ^ name of the alias with its definition's location   , rtTArgs :: [x]                -- ^ type parameters   , rtVArgs :: [Symbol]           -- ^ value parameters   , rtBody  :: a                  -- ^ what the alias expands to-  -- , rtMod   :: !ModName           -- ^ module where alias was defined   } deriving (Eq, Data, Generic, Functor, Foldable, Traversable)     deriving Hashable via Generically (RTAlias x a)     deriving B.Binary via Generically (RTAlias x a) -- TODO support ghosts in aliases? +-- | A map over a 'RTAlias' type parameters. mapRTAVars :: (a -> b) -> RTAlias a ty -> RTAlias b ty mapRTAVars f rt = rt { rtTArgs = f <$> rtTArgs rt } -lmapEAlias :: LMap -> F.Located (RTAlias Symbol Expr)-lmapEAlias (LMap v ys e) = F.atLoc v (RTA (F.val v) [] ys e) -- (F.loc v) (F.loc v)+-- | Transform a logic equation to an expression alias.+--+-- Used when constructing 'Language.Haskell.Liquid.Types.Specs.GhcSpec'+-- to include Haskell inlines and 'LogicMap' definitions in the alias+-- environment for expansion. See [NOTE:EXPRESSION-ALIASES]+lmapEAlias :: LMap -> RTAlias Symbol Expr+lmapEAlias (LMap v ys e) = RTA (makeGeneratedLogicLHName <$> v) [] ys e   -- | The type used during constraint generation, used@@ -558,11 +563,11 @@ getModString = moduleNameString . getModName  ----------------------------------------------------------------------------------- | Refinement Type Aliases ---------------------------------------------------+-- | Refinement Type and Expression Aliases Environment -------------------------------------------------------------------------------- data RTEnv tv t = RTE-  { typeAliases :: M.HashMap Symbol (F.Located (RTAlias tv t))-  , exprAliases :: M.HashMap Symbol (F.Located (RTAlias Symbol Expr))+  { typeAliases :: M.HashMap LHName (RTAlias tv t)+  , exprAliases :: M.HashMap LHName (RTAlias Symbol Expr)   }  

@@ -78,9 +78,9 @@  -- | @output@ creates the pretty printed output ---------------------------------------------------------------------------------------------mkOutput :: Config -> ErrorResult -> FixSolution -> AnnInfo (Annot SpecType) -> Output Doc+mkOutput :: Config -> ErrorResult -> FInfo a -> FixDelayedSolution -> AnnInfo (Annot SpecType) -> Output Doc ---------------------------------------------------------------------------------------------mkOutput cfg res sol anna+mkOutput cfg res si sol anna   = O { o_vars   = Nothing       -- , o_errors = []       , o_types  = toDoc <$> annTy@@ -90,7 +90,7 @@       }   where     annTmpl      = closeAnnots anna-    annTy        = tidySpecType Lossy <$> applySolution sol annTmpl+    annTy        = tidySpecType Lossy <$> applySolution si sol annTmpl     toDoc        = rtypeDoc tidy     tidy         = if shortNames cfg then Lossy else Full 

@@ -20,14 +20,11 @@  module Language.Haskell.Liquid.UX.CmdLine (    -- * Get Command Line Configuration-     getOpts, mkOpts, defConfig, config+     getOpts, defConfig     -- * Update Configuration With Pragma    , withPragmas -   -- * Canonicalize Paths in Config-   , canonicalizePaths-    -- * Collecting errors    , addErrors @@ -59,11 +56,9 @@ import System.Console.CmdArgs.Text import GitHash -import Data.List                           (nub)+import Data.List                           (nub, intercalate)  -import System.FilePath                     (isAbsolute, takeDirectory, (</>))- import qualified Language.Fixpoint.Types.Config as FC import qualified Language.Fixpoint.Misc as F import Language.Fixpoint.Types.Names@@ -97,7 +92,10 @@ -- Parsing Command Line---------------------------------------------------------- --------------------------------------------------------------------------------- config :: Mode (CmdArgs Config)-config = cmdArgsMode $ Config {+config = cmdArgsMode defConfig++defConfig :: Config+defConfig = Config {   loggingVerbosity     = enum [ Minimal      &= name "minimal" &= help "Minimal logging verbosity"            , Quiet        &= name "quiet"   &= help "Silent logging verbosity"@@ -105,15 +103,6 @@            , Loud         &= name "verbose" &= help "Verbose logging"            ] - , files-    = def &= typ "TARGET"-          &= args-          &= typFile-- , idirs-    = def &= typDir-          &= help "Paths to Spec Include Directory "-  , fullcheck      = def            &= help "Full Checking: check all binders (DEFAULT)"@@ -150,25 +139,25 @@           &= name "check-var"   , pruneUnsorted-    = def &= help "Disable prunning unsorted Predicates"+    = False &= help "Disable prunning unsorted Predicates"           &= name "prune-unsorted"   , notermination-    = def+    = False           &= help "Disable Termination Check"           &= name "no-termination-check"   , nopositivity-    = def+    = False           &= help "Disable Data Type Positivity Check"           &= name "no-positivity-check"   , rankNTypes-    = def &= help "Adds precise reasoning on presence of rankNTypes"+    = False &= help "Adds precise reasoning on presence of rankNTypes"           &= name "rankNTypes"   , noclasscheck-    = def+    = False           &= help "Disable Class Instance Check"           &= name "no-class-check" @@ -176,37 +165,24 @@     = def &= name "no-structural-termination"           &= help "Disable structural termination check" - , gradual-    = def &= help "Enable gradual refinement type checking"-          &= name "gradual"-  , bscope-    = def &= help "scope of the outer binders on the inner refinements"+    = False &= help "scope of the outer binders on the inner refinements"           &= name "bscope" - , gdepth-    = 1-    &= help "Size of gradual conretizations, 1 by default"-    &= name "gradual-depth"-- , ginteractive-    = def &= help "Interactive Gradual Solving"-          &= name "ginteractive"-  , totalHaskell-    = def &= help "Check for termination and totality; overrides no-termination flags"+    = False &= help "Check for termination and totality; overrides no-termination flags"           &= name "total-Haskell"   , nowarnings-    = def &= help "Don't display warnings, only show errors"+    = False &= help "Don't display warnings, only show errors"           &= name "no-warnings"   , noannotations-    = def &= help "Don't create intermediate annotation files"+    = False &= help "Don't create intermediate annotation files"           &= name "no-annotations"   , checkDerived-    = def &= help "Check GHC generated binders (e.g. Read, Show instances)"+    = False &= help "Check GHC generated binders (e.g. Read, Show instances)"           &= name "check-derived"   , caseExpandDepth@@ -214,15 +190,15 @@           &= name "max-case-expand"   , notruetypes-    = def &= help "Disable Trueing Top Level Types"+    = False &= help "Disable Trueing Top Level Types"           &= name "no-true-types"   , nototality-    = def &= help "Disable totality check"+    = False &= help "Disable totality check"           &= name "no-totality"   , cores-    = def &= help "Use m cores to solve logical constraints"+    = Just 1 &= help "Use the given number of cores to solve logical constraints (default: 1). Warning: unpredictable performance. See https://github.com/ucsd-progsys/liquidhaskell/issues/2562"   , minPartSize     = FC.defaultMinPartSize@@ -235,7 +211,7 @@              "size. Overrides the minpartsize option.")   , smtsolver-    = def &= help "Name of SMT-Solver"+    = Nothing &= help "Name of SMT-Solver"   , noCheckUnknown     = def &= explicit@@ -246,46 +222,27 @@     = defaultMaxParams &= help "Restrict qualifier mining to those taking at most `m' parameters (2 by default)"   , shortNames-    = def &= name "short-names"+    = False &= name "short-names"           &= help "Print shortened names, i.e. drop all module qualifiers."   , shortErrors-    = def &= name "short-errors"+    = False &= name "short-errors"           &= help "Don't show long error messages, just line numbers." - , cabalDir-    = def &= name "cabal-dir"-          &= help "Find and use .cabal to add paths to sources for imported files"-- , ghcOptions-    = def &= name "ghc-option"-          &= typ "OPTION"-          &= help "Pass this option to GHC"-- , cFiles-    = def &= name "c-files"-          &= typ "OPTION"-          &= help "Tell GHC to compile and link against these files"-- , port-     = defaultPort-          &= name "port"-          &= help "Port at which lhi should listen"-  , exactDC-    = def &= help "Exact Type for Data Constructors"+    = False &= help "Exact Type for Data Constructors"           &= name "exact-data-cons"   , noADT-    = def &= help "Do not generate ADT representations in refinement logic"+    = False &= help "Do not generate ADT representations in refinement logic"           &= name "no-adt"   , expectErrorContaining-    = def &= help "Expect an error which containing the provided string from verification (can be provided more than once)"+    = [] &= help "Expect an error which containing the provided string from verification (can be provided more than once)"           &= name "expect-error-containing"   , expectAnyError-    = def &= help "Expect an error, no matter which kind or what it contains"+    = False &= help "Expect an error, no matter which kind or what it contains"           &= name "expect-any-error"   , scrapeInternals@@ -347,103 +304,88 @@           -- PLE-OPT &= name "automatic-instances"    , proofLogicEval-    = def+    = False         &= help "Enable Proof-by-Logical-Evaluation"         &= name "ple"    , pleWithUndecidedGuards-    = def+    = False         &= help "Unfold invocations with undecided guards in PLE"         &= name "ple-with-undecided-guards"         &= explicit -  , oldPLE-    = def-        &= help "Enable Proof-by-Logical-Evaluation"-        &= name "oldple"-   , interpreter-    = def+    = False         &= help "Use an interpreter to assist PLE in solving constraints"         &= name "interpreter"    , proofLogicEvalLocal-    = def+    = False         &= help "Enable Proof-by-Logical-Evaluation locally, per function"         &= name "ple-local"    , etabeta-    = def+    = False         &= help "Eta expand and beta reduce terms to aid PLE"         &= name "etabeta"-  +   , dependantCase-    = def+    = False         &= help "Allow PLE to reason about dependent cases"         &= name "dependant-case"    , extensionality-    = def+    = False         &= help "Enable extensional interpretation of function equality"         &= name "extensionality"    , nopolyinfer-    = def+    = False         &= help "No inference of polymorphic type application. Gives imprecision, but speedup."         &= name "fast"    , reflection-    = def+    = False         &= help "Enable reflection of Haskell functions and theorem proving"         &= name "reflection"    , compileSpec-    = def+    = False         &= name "compile-spec"         &= help "Only compile specifications (into .bspec file); skip verification" -  , noCheckImports-    = def-        &= name "no-check-imports"-        &= help "Do not check the transitive imports; only check the target files."-   , typeclass-    = def+    = False         &= help "Enable Typeclass"         &= name "typeclass"   , auxInline-    = def+    = False         &= help "Enable inlining of class methods"         &= name "aux-inline"   ,     rwTerminationCheck-    = def+    = False         &= name "rw-termination-check"         &= help (   "Enable the rewrite divergence checker. "                  ++ "Can speed up verification if rewriting terminates, but can also cause divergence."                 )   ,     skipModule-    = def+    = False         &= name "skip-module"         &= help "Completely skip this module, don't even compile any specifications in it."-  ,-    noLazyPLE-    = def-        &= name "no-lazy-ple"-        &= help "Don't use Lazy PLE"    , fuel     = Nothing         &= help "Maximum fuel (per-function unfoldings) for PLE"    , environmentReduction-    = def+    = False         &= explicit         &= name "environment-reduction"         &= help "perform environment reduction (disabled by default)"   , noEnvironmentReduction-    = def+    = False         &= explicit         &= name "no-environment-reduction"         &= help "Don't perform environment reduction"@@ -467,42 +409,41 @@       &= help "Stop loading LHAssumptions modules for imports in these packages."       &= typ "PACKAGE"   , dumpOpaqueReflections-    = def &= help "Dump all generated opaque reflections"+    = False &= help "Dump all generated opaque reflections"           &= name "dump-opaque-reflections"           &= explicit   , dumpPreNormalizedCore-    = def &= help "Dump pre-normalized core (before a-normalization)"+    = False &= help "Dump pre-normalized core (before a-normalization)"           &= name "dump-pre-normalized-core"           &= explicit+  , dumpNormalizedCore+    = False &= help "Dump a-normalized core"+          &= name "dump-normalized-core"+          &= explicit   , allowUnsafeConstructors-    = def &= help "Allow refining constructors with unsafe refinements"+    = False &= help "Allow refining constructors with unsafe refinements"           &= name "allow-unsafe-constructors"           &= explicit-  } &= program "liquid"+  , ddumpTimings+    = False &= help "Dump time measures of the Liquid Haskell plugin"+          &= name "ddump-timings"+          &= explicit+  } &= program "liquidhaskell"     &= help    "Refinement Types for Haskell"     &= summary copyright-    &= details [ "LiquidHaskell is a Refinement Type based verifier for Haskell"-               , ""-               , "To check a Haskell file foo.hs, type:"-               , "  liquid foo.hs "-               ]--defaultPort :: Int-defaultPort = 3000+    &= details [ "LiquidHaskell is a Refinement Type based verifier for Haskell" ]  getOpts :: [String] -> IO Config getOpts as = do   cfg0   <- envCfg-  cfg1   <- mkOpts =<< cmdArgsRun'-                         config { modeValue = (modeValue config)-                                                { cmdArgsValue   = cfg0-                                                }-                                }-                         as-  cfg2   <- fixConfig cfg1-  let cfg3 = if json cfg2 then cfg2 {loggingVerbosity = Quiet} else cfg2-  setVerbosity (cmdargsVerbosity $ loggingVerbosity cfg3)-  withSmtSolver cfg3+  cfg1   <- cmdArgsRun'+              config { modeValue = (modeValue config)+                                      { cmdArgsValue   = cfg0 }+                     }+                     as+  let cfg2 = if json cfg1 then cfg1 {loggingVerbosity = Quiet} else cfg1+  setVerbosity (cmdargsVerbosity $ loggingVerbosity cfg2)+  withSmtSolver cfg2  cmdArgsRun' :: Mode (CmdArgs a) -> [String] -> IO a cmdArgsRun' md as@@ -524,12 +465,13 @@                    case found of                      Just _ -> return cfg                      Nothing -> panic Nothing (missingSmtError smt)-    Nothing  -> do smts <- mapM findSmtSolver [FC.Z3, FC.Cvc4, FC.Mathsat]+    Nothing  -> do smts <- mapM findSmtSolver smtLookupOrder                    case catMaybes smts of                      (s:_) -> return (cfg {smtsolver = Just s})                      _     -> panic Nothing noSmtError   where-    noSmtError = "LiquidHaskell requires an SMT Solver, i.e. z3, cvc4, or mathsat to be installed."+    smtLookupOrder = [FC.Z3, FC.Cvc5, FC.Cvc4, FC.Mathsat]+    noSmtError = "LiquidHaskell requires one of the following SMT solvers to be installed: " ++ intercalate ", " (show <$> smtLookupOrder) ++ "."     missingSmtError smt = "Could not find SMT solver '" ++ show smt ++ "'. Is it on your PATH?"  findSmtSolver :: FC.SMTSolver -> IO (Maybe FC.SMTSolver)@@ -537,28 +479,6 @@     FC.Z3mem -> return $ Just FC.Z3mem     smt      -> maybe Nothing (const $ Just smt) <$> findExecutable (show smt) -fixConfig :: Config -> IO Config-fixConfig config' = do-  pwd <- getCurrentDirectory-  cfg <- canonicalizePaths pwd config'-  return $ canonConfig cfg---- | Attempt to canonicalize all `FilePath's in the `Config' so we don't have---   to worry about relative paths.-canonicalizePaths :: FilePath -> Config -> IO Config-canonicalizePaths pwd cfg = do-  tgt   <- canonicalizePath pwd-  isdir <- doesDirectoryExist tgt-  is    <- mapM (canonicalize tgt isdir) $ idirs cfg-  cs    <- mapM (canonicalize tgt isdir) $ cFiles cfg-  return $ cfg { idirs = is, cFiles = cs }--canonicalize :: FilePath -> Bool -> FilePath -> IO FilePath-canonicalize tgt isdir f-  | isAbsolute f = return f-  | isdir        = canonicalizePath (tgt </> f)-  | otherwise    = canonicalizePath (takeDirectory tgt </> f)- envCfg :: IO Config envCfg = do   so <- lookupEnv "LIQUIDHASKELL_OPTS"@@ -599,27 +519,6 @@   ]  --- [NOTE:searchpath]--- 1. we used to add the directory containing the file to the searchpath,---    but this is bad because GHC does NOT do this, and it causes spurious---    "duplicate module" errors in the following scenario---      > tree---      .---      ├── Bar.hs---      └── Foo---          ├── Bar.hs---          └── Goo.hs---    If we run `liquid Foo/Goo.hs` and that imports Bar, GHC will not know---    whether we mean to import Bar.hs or Foo/Bar.hs--- 2. tests fail if you flip order of idirs'--mkOpts :: Config -> IO Config-mkOpts cfg = do-  let files' = F.sortNub $ files cfg-  return     $ cfg { files       = files'-                                   -- See NOTE [searchpath]-                   }- -------------------------------------------------------------------------------- -- | Updating options --------------------------------------------------------------------------------@@ -630,10 +529,10 @@   }  ---------------------------------------------------------------------------------withPragmas :: MonadIO m => Config -> FilePath -> [Located String] -> (Config -> m a) -> m a+withPragmas :: MonadIO m => Config -> [Located String] -> (Config -> m a) -> m a ---------------------------------------------------------------------------------withPragmas cfg fp ps action-  = do cfg' <- liftIO $ (processPragmas cfg ps >>= canonicalizePaths fp) <&> canonConfig+withPragmas cfg ps action+  = do cfg' <- liftIO $ processPragmas cfg ps <&> canonConfig        -- As the verbosity is set /globally/ via the cmdargs lib, re-set it.        liftIO $ setVerbosity (cmdargsVerbosity $ loggingVerbosity cfg')        res <- action cfg'@@ -649,100 +548,12 @@       cmdArgsApply  -- | Note that this function doesn't process list arguments properly, like--- 'cFiles' or 'expectErrorContaining'+-- 'expectErrorContaining' -- TODO: This is only used to parse the contents of the env var LIQUIDHASKELL_OPTS -- so it should be able to parse multiple arguments instead. See issue #1990. parsePragma :: Located String -> IO Config parsePragma = processPragmas defConfig . (:[]) -defConfig :: Config-defConfig = Config-  { loggingVerbosity         = Minimal-  , files                    = def-  , idirs                    = def-  , fullcheck                = def-  , linear                   = def-  , stringTheory             = def-  , higherorder              = def-  , smtTimeout               = def-  , higherorderqs            = def-  , diffcheck                = def-  , saveQuery                = def-  , checks                   = def-  , nostructuralterm         = def-  , noCheckUnknown           = def-  , notermination            = False-  , nopositivity             = False-  , rankNTypes               = False-  , noclasscheck             = False-  , gradual                  = False-  , bscope                   = False-  , gdepth                   = 1-  , ginteractive             = False-  , totalHaskell             = def -- True-  , nowarnings               = def-  , noannotations            = def-  , checkDerived             = False-  , caseExpandDepth          = 2-  , notruetypes              = def-  , nototality               = False-  , pruneUnsorted            = def-  , exactDC                  = def-  , noADT                    = def-  , expectErrorContaining    = def-  , expectAnyError           = False-  , cores                    = def-  , minPartSize              = FC.defaultMinPartSize-  , maxPartSize              = FC.defaultMaxPartSize-  , maxParams                = defaultMaxParams-  , smtsolver                = def-  , shortNames               = def-  , shortErrors              = def-  , cabalDir                 = def-  , ghcOptions               = def-  , cFiles                   = def-  , port                     = defaultPort-  , scrapeInternals          = False-  , elimStats                = False-  , elimBound                = Nothing-  , json                     = False-  , counterExamples          = False-  , timeBinds                = False-  , untidyCore               = False-  , eliminate                = FC.Some-  , noPatternInline          = False-  , noSimplifyCore           = False-  -- PLE-OPT , autoInstantiate   = def-  , noslice                  = False-  , noLiftedImport           = False-  , proofLogicEval           = False-  , pleWithUndecidedGuards   = False-  , oldPLE                   = False-  , interpreter              = False-  , proofLogicEvalLocal      = False-  , etabeta                  = False-  , dependantCase            = False-  , reflection               = False-  , extensionality           = False-  , nopolyinfer              = False-  , compileSpec              = False-  , noCheckImports           = False-  , typeclass                = False-  , auxInline                = False-  , rwTerminationCheck       = False-  , skipModule               = False-  , noLazyPLE                = False-  , fuel                     = Nothing-  , environmentReduction     = False-  , noEnvironmentReduction   = False-  , inlineANFBindings        = False-  , pandocHtml               = False-  , excludeAutomaticAssumptionsFor = []-  , dumpOpaqueReflections    = False-  , dumpPreNormalizedCore    = False-  , allowUnsafeConstructors  = False-  }- -- | Write the annotations (i.e. the files in the \".liquid\" hidden folder) and -- report the result of the checking using a supplied function, or using an -- implicit JSON function, if @json@ flag is set.@@ -842,9 +653,9 @@     orHeader = text "LIQUID: ERROR:" <+> text s   , orMessages = map (cErrToSpanned k . errToFCrash) xs   }-resDocs k (F.Unsafe _ xs)   =+resDocs k (F.Unsafe stats xs)   =   OutputResult {-    orHeader   = text "LIQUID: UNSAFE"+    orHeader   = text $ "LIQUID: UNSAFE (" <> show (Solver.numChck stats) <> " constraints checked)"   , orMessages = map (cErrToSpanned k) (nub xs)   } 

@@ -40,8 +40,6 @@ -- NOTE: adding strictness annotations breaks the help message data Config = Config   { loggingVerbosity         :: Verbosity  -- ^ the logging verbosity to use (defaults to 'Minimal')-  , files                    :: [FilePath] -- ^ source files to check-  , idirs                    :: [FilePath] -- ^ path to directory for including specs   , diffcheck                :: Bool       -- ^ check subset of binders modified (+ dependencies) since last check   , linear                   :: Bool       -- ^ uninterpreted integer multiplication and division   , stringTheory             :: Bool       -- ^ interpretation of string theory in the logic@@ -58,10 +56,7 @@   , noclasscheck             :: Bool       -- ^ disable checking class instances   -- , structuralTerm        :: Bool       -- ^ use structural termination checker   , nostructuralterm         :: Bool       -- ^ disable structural termination check-  , gradual                  :: Bool       -- ^ enable gradual type checking   , bscope                   :: Bool       -- ^ scope of the outer binders on the inner refinements-  , gdepth                   :: Int        -- ^ depth of gradual concretization-  , ginteractive             :: Bool       -- ^ interactive gradual solving   , totalHaskell             :: Bool       -- ^ Check for termination and totality, Overrides no-termination flags   , nowarnings               :: Bool       -- ^ disable warnings output (only show errors)   , noannotations            :: Bool       -- ^ disable creation of intermediate annotation files@@ -74,14 +69,10 @@   , minPartSize              :: Int        -- ^ Minimum size of a partition   , maxPartSize              :: Int        -- ^ Maximum size of a partition. Overrides minPartSize   , maxParams                :: Int        -- ^ the maximum number of parameters to accept when mining qualifiers-  , smtsolver                :: Maybe SMTSolver  -- ^ name of smtsolver to use [default: try z3, cvc4, mathsat in order]+  , smtsolver                :: Maybe SMTSolver  -- ^ SMT solver to use [if `Nothing`, try looking one up using the order defined in L.H.L.UX.CmdLine.withSmtSolver]   , shortNames               :: Bool       -- ^ drop module qualifers from pretty-printed names.   , shortErrors              :: Bool       -- ^ don't show subtyping errors and contexts.-  , cabalDir                 :: Bool       -- ^ find and use .cabal file to include paths to sources for imported modules-  , ghcOptions               :: [String]   -- ^ command-line options to pass to GHC-  , cFiles                   :: [String]   -- ^ .c files to compile and link against (for GHC)   , eliminate                :: Eliminate  -- ^ eliminate (i.e. don't use qualifs for) for "none", "cuts" or "all" kvars-  , port                     :: Int        -- ^ port at which lhi should listen   , exactDC                  :: Bool       -- ^ Automatically generate singleton types for data constructors   , noADT                    :: Bool       -- ^ Disable ADTs (only used with exactDC)   , expectErrorContaining    :: [String]   -- ^ expect failure from Liquid with at least one of the following messages@@ -100,7 +91,6 @@   , noLiftedImport           :: Bool       -- ^ Disable loading lifted specifications (for "legacy" libs)   , proofLogicEval           :: Bool       -- ^ Enable proof-by-logical-evaluation   , pleWithUndecidedGuards   :: Bool       -- ^ Unfold invocations with undecided guards in PLE-  , oldPLE                   :: Bool       -- ^ Enable proof-by-logical-evaluation   , interpreter              :: Bool       -- ^ Use an interpreter to assist PLE   , proofLogicEvalLocal      :: Bool       -- ^ Enable proof-by-logical-evaluation locally, per function   , etabeta                  :: Bool       -- ^ Eta expand and beta reduce terms to aid PLE@@ -109,13 +99,11 @@   , nopolyinfer              :: Bool       -- ^ No inference of polymorphic type application.   , reflection               :: Bool       -- ^ Allow "reflection"; switches on "--higherorder" and "--exactdc"   , compileSpec              :: Bool       -- ^ Only "compile" the spec -- into .bspec file -- don't do any checking.-  , noCheckImports           :: Bool       -- ^ Do not check the transitive imports   , typeclass                :: Bool        -- ^ enable typeclass support.-  , auxInline                :: Bool        -- ^ +  , auxInline                :: Bool        -- ^   , rwTerminationCheck       :: Bool       -- ^ Enable termination checking for rewriting   , skipModule               :: Bool       -- ^ Skip this module entirely (don't even compile any specs in it)-  , noLazyPLE                :: Bool-  , fuel                     :: Maybe Int  -- ^ Maximum PLE "fuel" (unfold depth) (default=infinite) +  , fuel                     :: Maybe Int  -- ^ Maximum PLE "fuel" (unfold depth) (default=infinite)   , environmentReduction     :: Bool       -- ^ Perform environment reduction   , noEnvironmentReduction   :: Bool       -- ^ Don't perform environment reduction   , inlineANFBindings        :: Bool       -- ^ Inline ANF bindings.@@ -124,7 +112,10 @@   , excludeAutomaticAssumptionsFor :: [String]   , dumpOpaqueReflections    :: Bool       -- Dumps all opaque reflections to the stdout   , dumpPreNormalizedCore    :: Bool       -- Dumps the prenormalized core (before a-normalization)+  , dumpNormalizedCore       :: Bool       -- Dumps the a-normalized core   , allowUnsafeConstructors  :: Bool       -- ^ Allow refining constructors with unsafe refinements+  , ddumpTimings             :: Bool       -- ^ Dump time measures of the Liquid Haskell plugin+                                           -- Only needed to work around https://github.com/haskell/cabal/issues/11116   } deriving (Generic, Data, Show, Eq)  allowPLE :: Config -> Bool

@@ -34,11 +34,11 @@ type CtxM = M.HashMap F.Symbol (WithModel SpecType)  -------------------------------------------------------------------------tidyError :: Config -> F.FixSolution -> Error -> Error+tidyError :: Config -> Error -> Error -------------------------------------------------------------------------tidyError cfg sol+tidyError cfg   = fmap (tidySpecType tidy)-  . tidyErrContext tidy sol+  . tidyErrContext tidy   where     tidy = configTidy cfg @@ -47,8 +47,8 @@   | shortNames cfg = F.Lossy   | otherwise      = F.Full -tidyErrContext :: F.Tidy -> F.FixSolution -> Error -> Error-tidyErrContext k _ e@(ErrSubType {})+tidyErrContext :: F.Tidy -> Error -> Error+tidyErrContext k e@(ErrSubType {})   = e { ctx = c', tact = F.subst θ tA, texp = F.subst θ tE }     where       (θ, c') = tidyCtx k xs (ctx e)@@ -56,7 +56,7 @@       tA      = tact e       tE      = texp e -tidyErrContext _ _ e@(ErrSubTypeModel {})+tidyErrContext _ e@(ErrSubTypeModel {})   = e { ctxM = c', tactM = fmap (F.subst θ) tA, texp = fmap (F.subst θ) tE }     where       (θ, c') = tidyCtxM xs $ ctxM e@@ -64,7 +64,7 @@       tA      = tactM e       tE      = texp e -tidyErrContext k _ e@(ErrAssType {})+tidyErrContext k e@(ErrAssType {})   = e { ctx = c', cond = F.subst θ p }     where       m       = ctx e@@ -72,7 +72,7 @@       xs      = F.syms p       p       = cond e -tidyErrContext _ _ e+tidyErrContext _ e   = e  --------------------------------------------------------------------------------

@@ -90,12 +90,13 @@   (\t -> (`SigD` t) . lhNameToName <$> names)     <$> simplifyBareType id (head names) (quantifyFreeRTy $ parsedToBareType $ val ty) mkSpecDecs (Alias rta) =-  return . TySynD name tvs <$> simplifyBareType parsedToBareType lsym (rtBody (val rta))+  return . TySynD name tvs <$> simplifyBareType parsedToBareType lsym (rtBody rta)   where-    lsym = F.atLoc rta n-    name = symbolName n-    n    = rtName (val rta)-    tvs  = (\a -> PlainTV (symbolName a) BndrReq) <$> rtTArgs (val rta)+    lsym = F.atLoc (rtName rta) sym+    name = symbolName sym+    -- We use the symbol returned by the parser+    sym  = getLHNameSymbol . val $ rtName rta+    tvs  = (\a -> PlainTV (symbolName a) BndrReq) <$> rtTArgs rta mkSpecDecs _ =   Right [] 

@@ -95,7 +95,7 @@     | s <- wiredTheorySyms     , let srt = F.tsSort $                   fromMaybe (panic Nothing ("unknown symbol: " ++ show s)) $-                    F.lookupSEnv s (F.theorySymbols F.Z3)+                    F.lookupSEnv s (F.theorySymbols F.Z3 <> F.theorySymbols F.Cvc5)     ]   where     wiredTheorySyms =@@ -113,6 +113,7 @@       , "Set_sub"       , "Set_add"       , "Set_com"+      , "Set_card"        , "Bag_count"       , "Bag_empty"@@ -121,6 +122,10 @@       , "Bag_sub"       , "Bag_union"       , "Bag_union_max"++      , "FF_val"+      , "FF_add"+      , "FF_mul"        , "strLen"       ]

@@ -152,8 +152,8 @@           "embed Set as Set_Set"      , testCase "qualif" $-       parseSingleSpec "qualif Foo(v:Int): v < 0" @?==-          "qualif Foo defined at <test>:1:8"+       parseSingleSpec "qualif Foo(v:Int) { v < 0 }" @?==+          "qualif Foo(v: int) { v < 0 } // defined at <test>:1:8"      , testCase "lazyvar" $        parseSingleSpec "lazyvar z" @?==@@ -376,11 +376,10 @@           @?==           unlines           [ "predicate ValidChunk V  XS  N  = "-          , "  (not (len XS == 0) =>"-          , "     (1 < N && 1 < len XS => len V < len XS)"-          , "     && (len XS <= N => len V == 1)"-          , "  )"-          , "  && (len XS == 0 => len V == 0)"+          , "  if len XS == 0 "+          , "     then len V == 0"+          , "     else (1 < len XS && 1 < N => len V < len XS)"+          , "          && (len XS <= N => len V == 1)"           ]