liquidhaskell-boot 0.9.12.2.1 → 0.9.14.1

raw patch · 70 files changed

+2235/−1616 lines, 70 filesdep ~ghcdep ~liquid-fixpointPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: ghc, liquid-fixpoint

API changes (from Hackage documentation)

Files

• ghc-api-tests/GhcApiTests.hs +124/−62
• liquidhaskell-boot.cabal +7/−7
• src-ghc/Liquid/GHC/API.hs +11/−6
• src-ghc/Liquid/GHC/API/Extra.hs +14/−3
• src/Language/Haskell/Liquid/Bare.hs +47/−20
• src/Language/Haskell/Liquid/Bare/Axiom.hs +10/−7
• src/Language/Haskell/Liquid/Bare/Check.hs +42/−50
• src/Language/Haskell/Liquid/Bare/Class.hs +2/−2
• src/Language/Haskell/Liquid/Bare/DataType.hs +48/−10
• src/Language/Haskell/Liquid/Bare/Elaborate.hs +4/−3
• src/Language/Haskell/Liquid/Bare/Expand.hs +47/−9
• src/Language/Haskell/Liquid/Bare/Measure.hs +14/−19
• src/Language/Haskell/Liquid/Bare/Misc.hs +0/−52
• src/Language/Haskell/Liquid/Bare/Plugged.hs +4/−4
• src/Language/Haskell/Liquid/Bare/Resolve.hs +71/−43
• src/Language/Haskell/Liquid/Bare/Types.hs +55/−54
• src/Language/Haskell/Liquid/Constraint/Constraint.hs +7/−6
• src/Language/Haskell/Liquid/Constraint/Env.hs +2/−1
• src/Language/Haskell/Liquid/Constraint/Fresh.hs +1/−1
• src/Language/Haskell/Liquid/Constraint/Generate.hs +269/−58
• src/Language/Haskell/Liquid/Constraint/Init.hs +6/−4
• src/Language/Haskell/Liquid/Constraint/Monad.hs +27/−0
• src/Language/Haskell/Liquid/Constraint/Qualifier.hs +3/−2
• src/Language/Haskell/Liquid/Constraint/RewriteCase.hs +10/−9
• src/Language/Haskell/Liquid/Constraint/Split.hs +3/−2
• src/Language/Haskell/Liquid/Constraint/Termination.hs +0/−1
• src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs +6/−4
• src/Language/Haskell/Liquid/Constraint/Types.hs +10/−3
• src/Language/Haskell/Liquid/GHC/Interface.hs +0/−1
• src/Language/Haskell/Liquid/GHC/Misc.hs +9/−65
• src/Language/Haskell/Liquid/GHC/Play.hs +11/−11
• src/Language/Haskell/Liquid/GHC/Plugin.hs +7/−4
• src/Language/Haskell/Liquid/GHC/Plugin/Serialisation.hs +12/−9
• src/Language/Haskell/Liquid/GHC/Plugin/SpecFinder.hs +34/−3
• src/Language/Haskell/Liquid/GHC/Resugar.hs +20/−20
• src/Language/Haskell/Liquid/GHC/SpanStack.hs +2/−2
• src/Language/Haskell/Liquid/GHC/TypeRep.hs +28/−28
• src/Language/Haskell/Liquid/LHNameResolution.hs +24/−31
• src/Language/Haskell/Liquid/Liquid.hs +21/−21
• src/Language/Haskell/Liquid/Measure.hs +9/−6
• src/Language/Haskell/Liquid/Misc.hs +0/−1
• src/Language/Haskell/Liquid/Parse.hs +43/−22
• src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs +143/−96
• src/Language/Haskell/Liquid/Transforms/QuestionMark.hs +70/−0
• src/Language/Haskell/Liquid/Transforms/RefSplit.hs +1/−1
• src/Language/Haskell/Liquid/Transforms/Rewrite.hs +1/−1
• src/Language/Haskell/Liquid/Types/Bounds.hs +1/−93
• src/Language/Haskell/Liquid/Types/Errors.hs +30/−7
• src/Language/Haskell/Liquid/Types/Fresh.hs +13/−12
• src/Language/Haskell/Liquid/Types/Generics.hs +1/−1
• src/Language/Haskell/Liquid/Types/Literals.hs +1/−1
• src/Language/Haskell/Liquid/Types/Meet.hs +2/−2
• src/Language/Haskell/Liquid/Types/Names.hs +18/−1
• src/Language/Haskell/Liquid/Types/PredType.hs +27/−27
• src/Language/Haskell/Liquid/Types/PrettyPrint.hs +64/−45
• src/Language/Haskell/Liquid/Types/RType.hs +262/−167
• src/Language/Haskell/Liquid/Types/RTypeOp.hs +150/−127
• src/Language/Haskell/Liquid/Types/RefType.hs +265/−305
• src/Language/Haskell/Liquid/Types/Specs.hs +2/−2
• src/Language/Haskell/Liquid/Types/Types.hs +52/−7
• src/Language/Haskell/Liquid/Types/Visitors.hs +6/−6
• src/Language/Haskell/Liquid/UX/Annotate.hs +1/−2
• src/Language/Haskell/Liquid/UX/CmdLine.hs +19/−8
• src/Language/Haskell/Liquid/UX/Config.hs +7/−6
• src/Language/Haskell/Liquid/UX/Errors.hs +7/−5
• src/Language/Haskell/Liquid/UX/QuasiQuoter.hs +0/−1
• src/Language/Haskell/Liquid/UX/Tidy.hs +6/−6
• src/Language/Haskell/Liquid/WiredIn.hs +2/−1
• tests/Parser.hs +19/−19
• tests/WiredInTests.hs +1/−1

@@ -1,6 +1,7 @@ {-# LANGUAGE ViewPatterns #-}  import           Control.Monad+import           Control.Monad.IO.Class (liftIO) import           Data.List (find) import           Data.Time (getCurrentTime) import           Liquid.GHC.API@@ -11,13 +12,13 @@     , LitNumType(..)     , Literal(..)     , apiCommentsParsedSource-    , gopt_set     , occNameString     , pAT_ERROR_ID     , showPprQualified     , splitDollarApp     , untick     )+import           Liquid.GHC.API.Extra (addNoInlinePragmasToBinds) import           Test.Tasty import           Test.Tasty.HUnit import           Test.Tasty.Runners.AntXML@@ -29,12 +30,14 @@ import qualified GHC.Data.EnumSet as EnumSet import qualified GHC.Data.FastString as GHC import qualified GHC.Data.StringBuffer as GHC+import qualified GHC.Driver.Main as GHC (hscDesugar) import qualified GHC.Parser as Parser import qualified GHC.Parser.Lexer as GHC import qualified GHC.Types.Id as GHC import qualified GHC.Types.Name as GHC import qualified GHC.Types.SrcLoc as GHC import qualified GHC.Unit.Module.ModGuts as GHC+import qualified GHC.Unit.Types as GHC import qualified GHC.Utils.Error as GHC  import GHC.Paths (libdir)@@ -51,7 +54,8 @@       , testCase "caseDesugaring" testCaseDesugaring       , testCase "numericLiteralDesugaring" testNumLitDesugaring       , testCase "dollarDesugaring" testDollarDesugaring-      , testCase "localBindingsDesugaring" testLocalBindingsDesugaring+      , testCase "deadBindingPreservation" testDeadBindingPreservation+      , testCase "exportedBindingNotInlined" testExportedBindingNotInlined       ]  -- Tests that Liquid.GHC.API.Extra.apiComments can retrieve the comments in@@ -91,7 +95,7 @@     parseMod str filepath = do       let location = GHC.mkRealSrcLoc (GHC.mkFastString filepath) 1 1           buffer = GHC.stringToStringBuffer str-          popts = GHC.mkParserOpts EnumSet.empty GHC.emptyDiagOpts [] False True True True+          popts = GHC.mkParserOpts EnumSet.empty GHC.emptyDiagOpts False True True True           parseState = GHC.initParserState popts buffer location       case GHC.unP Parser.parseModule parseState of         GHC.POk _ result -> return result@@ -107,10 +111,6 @@           , "        True -> ()"           ] -        fBind (GHC.NonRec b _e) =-          occNameString (GHC.occName b) == "f"-        fBind _ = False-         -- Expected desugaring:         --         -- CaseDesugaring.f@@ -123,8 +123,8 @@         --            GHC.Types.True -> GHC.Tuple.()         --          }         ---        isExpectedDesugaring p = case find fBind p of-          Just (GHC.NonRec _ e0)+        isExpectedDesugaring p = case findExpr "f" p of+          Just e0             | Lam x (untick -> Case (Var x') _ _ [alt0, _alt1]) <- e0             , x == x'             , Alt DEFAULT [] e1 <- alt0@@ -149,18 +149,14 @@           , "f = 1"           ] -        fBind (GHC.NonRec b _e) =-          occNameString (GHC.occName b) == "f"-        fBind _ = False-         -- Expected desugaring:         --         -- NumLitDesugaring.f         --      = \@a dict -> fromInteger @a dict (GHC.Num.Integer.IS 1#)         ---        isExpectedDesugaring p = case find fBind p of-          Just (GHC.NonRec _ e0)-            | Lam _a (Lam _dict (untick -> App fromIntegerApp (App (Var vIS) lit))) <- e0+        isExpectedDesugaring p = case findExpr "f" p of+          Just e0+            | Lam _a (Lam _dict (untick . dropLets -> App fromIntegerApp (App (Var vIS) lit))) <- e0             , App (App (Var vFromInteger) _aty) _numDict <- fromIntegerApp             , GHC.idName vFromInteger  == GHC.fromIntegerName             , GHC.nameStableString (GHC.idName vIS) == GHC.nameStableString GHC.integerISDataConName@@ -173,6 +169,10 @@       fail $ unlines $         "Unexpected desugaring:" : map showPprQualified coreProgram +dropLets :: GHC.CoreExpr -> GHC.CoreExpr+dropLets (Let _ e) = dropLets e+dropLets e         = e+ -- | Tests that dollar sign desugars as Liquid Haskell expects. testDollarDesugaring :: IO () testDollarDesugaring = do@@ -182,12 +182,8 @@           , "f = (\\_ -> ()) $ 'a'"           ] -        fBind (GHC.NonRec b _e) =-          occNameString (GHC.occName b) == "f"-        fBind _ = False--        isExpectedDesugaring p = case find fBind p of-          Just (GHC.NonRec _ e0)+        isExpectedDesugaring p = case findExpr "f" p of+          Just e0             | Just (Lam _ _, App _ (Lit (LitChar 'a'))) <- splitDollarApp e0             -> True           _ -> False@@ -197,52 +193,118 @@       fail $ unlines $         "Unexpected desugaring:" : map showPprQualified coreProgram --- | Test that local bindings are preserved.-testLocalBindingsDesugaring :: IO ()-testLocalBindingsDesugaring = do+-- | Find the Core expression bound to the given name.+findExpr :: String -> GHC.CoreProgram -> Maybe GHC.CoreExpr+findExpr _ [] =+  Nothing+findExpr name (p:ps) = case p of+  GHC.NonRec b e+    | occNameString (GHC.occName b) == name+    -> Just e+  GHC.Rec binds+    | Just (_, e) <- find (\(b, _e) -> occNameString (GHC.occName b) == name) binds+    -> Just e+  _ -> findExpr name ps+++compileToCore :: String -> String -> IO [GHC.CoreBind]+compileToCore modName inputSource = do+    GHC.runGhc (Just libdir) $ do+      (_, tcMod) <- typecheckSourceCode modName inputSource+      dsMod <- GHC.desugarModule tcMod+      return $ GHC.mg_binds $ GHC.dm_core_module dsMod++typecheckSourceCode+  :: GHC.GhcMonad m => String -> String -> m (GHC.ModSummary, GHC.TypecheckedModule)+typecheckSourceCode modName inputSource = do+    now <- liftIO getCurrentTime+    df1 <- GHC.getSessionDynFlags+    GHC.setSessionDynFlags $ df1 { GHC.backend = GHC.interpreterBackend }+    let target = GHC.Target+               { GHC.targetId           = GHC.TargetFile (modName ++ ".hs") Nothing+               , GHC.targetUnitId       = GHC.homeUnitId_ df1+               , GHC.targetAllowObjCode = False+               , GHC.targetContents     = Just (GHC.stringToStringBuffer inputSource, now)+               }+    GHC.setTargets [target]+    void $ GHC.depanal [] False++    ms <- GHC.getModSummary+            (GHC.mkModule GHC.mainUnit (GHC.mkModuleName modName))+    tm <- GHC.parseModule ms >>= GHC.typecheckModule+    return (ms, tm)++-- | Like 'compileToCore' but applies 'addNoInlinePragmasToBinds' before+-- desugaring, simulating what LH's plugin does to preserve bindings that+-- would otherwise be inlined away.+compileToCoreWithLH :: String -> String -> IO [GHC.CoreBind]+compileToCoreWithLH modName inputSource = do+    GHC.runGhc (Just libdir) $ do+      (ms, tcMod) <- typecheckSourceCode modName inputSource+      let (tcg, _) = GHC.tm_internals_ tcMod+          tcg' = addNoInlinePragmasToBinds tcg+      hsc_env <- GHC.getSession+      guts <- liftIO $ GHC.hscDesugar hsc_env ms tcg'+      return $ GHC.mg_binds guts++-- | Tests that dead bindings (unused where-clause bindings) are preserved+-- when 'addNoInlinePragmasToBinds' marks Ids as exported.+testDeadBindingPreservation :: IO ()+testDeadBindingPreservation = do     let inputSource = unlines-          [ "module LocalBindingsDesugaring where"-          , "f :: ()"-          , "f = z"+          [ "module DeadBindingPreservation where"+          , "f :: Int -> ()"+          , "f x = ()"           , "  where"-          , "    z = ()"+          , "    z = x + 1"           ] -        fBind (GHC.NonRec b _e) =-          occNameString (GHC.occName b) == "f"-        fBind _ = False--        isExpectedDesugaring p = case find fBind p of-          Just (GHC.NonRec _ (Let (GHC.NonRec b _) _))-            -> occNameString (GHC.occName b) == "z"-          _ -> False+        -- The dead binding 'z' should still appear in the Core output.+        hasDeadBinding p = case findExpr "f" p of+          Just e -> hasLetNamed "z" e+          _      -> False -    coreProgram <- compileToCore "LocalBindingsDesugaring" inputSource-    unless (isExpectedDesugaring coreProgram) $+    coreProgram <- compileToCoreWithLH "DeadBindingPreservation" inputSource+    unless (hasDeadBinding coreProgram) $       fail $ unlines $-        "Unexpected desugaring:" : map showPprQualified coreProgram+        "Dead binding 'z' was eliminated:" : map showPprQualified coreProgram +-- | Tests that a binding marked as exported is not inlined even when it+-- occurs exactly once (i.e. it would normally be inlined by the simple+-- optimizer).+testExportedBindingNotInlined :: IO ()+testExportedBindingNotInlined = do+    let inputSource = unlines+          [ "module ExportedBindingNotInlined where"+          , "f :: Int -> Int"+          , "f x = z"+          , "  where"+          , "    z = x + 1"+          ] -compileToCore :: String -> String -> IO [GHC.CoreBind]-compileToCore modName inputSource = do-    now <- getCurrentTime-    GHC.runGhc (Just libdir) $ do-      df1 <- GHC.getSessionDynFlags-      GHC.setSessionDynFlags $ df1-        { GHC.backend = GHC.interpreterBackend-        }-         `gopt_set` GHC.Opt_InsertBreakpoints-      let target = GHC.Target {-                   GHC.targetId           = GHC.TargetFile (modName ++ ".hs") Nothing-                 , GHC.targetUnitId       = GHC.homeUnitId_ df1-                 , GHC.targetAllowObjCode = False-                 , GHC.targetContents     = Just (GHC.stringToStringBuffer inputSource, now)-                 }-      GHC.setTargets [target]-      void $ GHC.load GHC.LoadAllTargets+        -- The binding 'z' is used exactly once. Without the exported+        -- marking, the simple optimizer would inline it. With it,+        -- 'z' should still appear as a let-binding.+        hasBinding p = case findExpr "f" p of+          Just e -> hasLetNamed "z" e+          _      -> False -      dsMod <- GHC.getModSummary (GHC.mkModuleName modName)-             >>= GHC.parseModule-             >>= GHC.typecheckModule-             >>= GHC.desugarModule-      return $ GHC.mg_binds $ GHC.dm_core_module dsMod+    coreProgram <- compileToCoreWithLH "ExportedBindingNotInlined" inputSource+    unless (hasBinding coreProgram) $+      fail $ unlines $+        "Binding 'z' was inlined:" : map showPprQualified coreProgram++-- | Check if an expression contains a let-binding with the given name.+hasLetNamed :: String -> GHC.CoreExpr -> Bool+hasLetNamed name = go+  where+    go (Let (GHC.NonRec b _) body) =+      occNameString (GHC.occName b) == name || go body+    go (Let (GHC.Rec pairs) body) =+      any (\(b, _) -> occNameString (GHC.occName b) == name) pairs || go body+    go (Lam _ e) = go e+    go (App e1 e2) = go e1 || go e2+    go (GHC.Case _ _ _ alts) = any (\(Alt _ _ rhs) -> go rhs) alts+    go (GHC.Cast e _) = go e+    go (GHC.Tick _ e) = go e+    go _ = False

@@ -1,6 +1,6 @@ cabal-version:      2.4 name:               liquidhaskell-boot-version:            0.9.12.2.1+version:            0.9.14.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)@@ -13,7 +13,7 @@ category:           Language homepage:           https://github.com/ucsd-progsys/liquidhaskell build-type:         Simple-tested-with:        GHC == 9.12.2+tested-with:        GHC == 9.14.1  source-repository head   type:     git@@ -80,6 +80,7 @@                       Language.Haskell.Liquid.Termination.Structural                       Language.Haskell.Liquid.Transforms.ANF                       Language.Haskell.Liquid.Transforms.CoreToLogic+                      Language.Haskell.Liquid.Transforms.QuestionMark                       Language.Haskell.Liquid.Transforms.RefSplit                       Language.Haskell.Liquid.Transforms.Rewrite                       Language.Haskell.Liquid.Transforms.Simplify@@ -136,13 +137,13 @@                     , filepath             >= 1.3                     , fingertree           >= 0.1                     , exceptions           < 0.11-                    , ghc                  ^>= 9.12+                    , ghc                  ^>= 9.14                     , ghc-boot                     , ghc-prim                     , gitrev                     , hashable             >= 1.3 && < 1.6                     , hscolour             >= 1.22-                    , liquid-fixpoint      == 0.9.6.3.5+                    , liquid-fixpoint      == 0.9.6.3.6                     , mtl                  >= 2.1                     , optparse-applicative < 0.20                     , githash@@ -162,10 +163,9 @@                     , extra   default-language:   Haskell98   default-extensions: PatternGuards, RecordWildCards, DoAndIfThenElse-  ghc-options:        -W -fwarn-missing-signatures-+  ghc-options:        -W -fwarn-missing-signatures -Wno-x-partial   if flag(devel)-    ghc-options:      -Wall -Werror+    ghc-options:      -Wall -Werror -Wno-x-partial  test-suite wiredin-tests   type:             exitcode-stdio-1.0

@@ -244,6 +244,7 @@     , bindersOfBinds     , cmpAlt     , collectArgs+    , collectArgsTicks     , collectBinders     , collectTyAndValBinders     , collectTyBinders@@ -331,11 +332,12 @@ import GHC.Core.Predicate             as Ghc     ( getClassPredTys_maybe     , getClassPredTys-    , isEvVarType+    , isPredTy+    , isSimplePredTy     , isEqPred+    , isEqClassPred     , isClassPred     , isDictId-    , isNomEqPred     , mkClassPred     ) import GHC.Core.Reduction             as Ghc@@ -417,7 +419,7 @@     , varType     ) import GHC.Core.Unify                 as Ghc-    ( ruleMatchTyKiX, tcUnifyTy )+    ( ruleMatchTyKiX, tcUnifyTy, tcMatchTy ) import GHC.Core.Utils                 as Ghc (exprType) import GHC.Data.Bag                   as Ghc     ( Bag, bagToList )@@ -521,9 +523,8 @@     ) import GHC.Tc.Errors.Types            as Ghc     ( mkTcRnUnknownMessage )-import GHC.Tc.Gen.App                 as Ghc (tcInferSigma) import GHC.Tc.Gen.Bind                as Ghc (tcValBinds)-import GHC.Tc.Gen.Expr                as Ghc (tcInferRho)+import GHC.Tc.Gen.Expr                as Ghc (tcInferRho, tcInferSigma) import GHC.Tc.Solver                  as Ghc     ( InferMode(NoRestrictions)     , captureTopConstraints@@ -714,6 +715,7 @@     , mkVarUnqual     , mkUnqual     , nameRdrName+    , noUserRdr     ) import GHC.Types.SourceError          as Ghc     ( SourceError@@ -784,9 +786,12 @@     ( FindResult(Found, NoPackage, FoundMultiple, NotFound)     , findExposedPackageModule     , findImportedModule+    , findPluginModule     ) import GHC.Unit.Home.ModInfo          as Ghc-    ( HomePackageTable, HomeModInfo(hm_iface), lookupHpt )+    ( HomeModInfo(hm_iface) )+import GHC.Unit.Home.PackageTable     as Ghc+    ( HomePackageTable, lookupHpt ) import GHC.Unit.Module                as Ghc     ( GenWithIsBoot(gwib_isBoot, gwib_mod)     , IsBootInterface(NotBoot, IsBoot)

@@ -44,7 +44,7 @@ import GHC.Core.Coercion              as Ghc import GHC.Core.DataCon               as Ghc import GHC.Core.Make                  (pAT_ERROR_ID)-import GHC.Core.Type                  as Ghc hiding (typeKind , isPredTy, extendCvSubst, linear)+import GHC.Core.Type                  as Ghc hiding (typeKind , extendCvSubst, linear) import GHC.Data.FastString            as Ghc import GHC.Data.Maybe import qualified GHC.Data.Strict@@ -122,11 +122,18 @@     spanToLineColumn =       fmap (\s -> (srcSpanStartLine s, srcSpanStartCol s)) . srcSpanToRealSrcSpan --- | Adds NOINLINE pragmas to all bindings in the module.+-- | Adds NOINLINE pragmas to all bindings in the module and sets them as+-- exported identifiers. -- -- This prevents the simple optimizer from inlining such bindings which might -- have specs that would otherwise be left dangling. --+-- Setting the exported flag prevents both inlining and removal of dead bindings+-- in the simple optimizer. NOINLINE is redundant with this, but it expresseses+-- the intent more clearly. Note also that Language.Haskell.Liquid.Transform.Rewrite.inlineLoopBreaker+-- depends at the moment on NOINLINE being inserted to tell appart bindings in+-- the original program from generated bindings.+-- -- https://gitlab.haskell.org/ghc/ghc/-/issues/24386 -- addNoInlinePragmasToBinds :: TcGblEnv -> TcGblEnv@@ -150,7 +157,7 @@         pat -> gmapT (id `extT` markPat) pat      markId :: Id -> Id-    markId var = var `setInlinePragma` neverInlinePragma+    markId var = setIdExported (var `setInlinePragma` neverInlinePragma)      -- The AbsBinds come from the GHC typechecker to handle polymorphism,     -- overloading, and recursion, so those don't correspond directly to@@ -160,6 +167,10 @@     -- See     -- https://github.com/ucsd-progsys/liquidhaskell/issues/2257 for more     -- context.+    --+    -- The first binding inside abs_binds is not given NOINLINE (to avoid+    -- interfering with the polymorphism wrapper), but nested where-clause+    -- bindings inside it are still marked via the generic traversal.     markAbsBinds :: AbsBinds -> AbsBinds     markAbsBinds absBinds0@AbsBinds{ abs_binds = binds, abs_exports = exports }  =         absBinds0

@@ -450,10 +450,29 @@  makeEmbeds :: GhcSrc -> Bare.GHCTyLookupEnv -> [Ms.BareSpec] -> F.TCEmb Ghc.TyCon makeEmbeds src env-  = Bare.addClassEmbeds (_gsCls src) (_gsFiTcs src)+  = addBoolEmbed+  . Bare.addClassEmbeds (_gsCls src) (_gsFiTcs src)   . mconcat   . map (makeTyConEmbeds env) +-- | Add the bool embedding+--+-- This is equivalent to the user adding the annotation+--+-- > {-@ embed Bool as bool @-}+--+-- It is needed by --adt, which produces checkers that+-- return a Bool. Without this embed annotation, the SMT solver would+-- reject the checkers as ill-sorted.+--+-- We used to have an embed annotation in LHAssumption modules, but it+-- was not in effect when the user did not import the necessary modules.+--+addBoolEmbed :: F.TCEmb Ghc.TyCon -> F.TCEmb Ghc.TyCon+addBoolEmbed embs+  | Mb.isJust (F.tceLookup Ghc.boolTyCon embs) = embs+  | otherwise                                  = F.tceInsert Ghc.boolTyCon F.boolSort F.NoArgs embs+ makeTyConEmbeds :: Bare.GHCTyLookupEnv -> Ms.BareSpec -> F.TCEmb Ghc.TyCon makeTyConEmbeds env spec   = F.tceFromList [ (tc, t) | (c,t) <- F.tceToList (Ms.embeds spec), tc <- symTc c ]@@ -506,11 +525,11 @@                 -> Ms.BareSpec makeLiftedSpec0 cfg src embs lmap mySpec = mempty   { Ms.ealiases  = lmapEAlias . snd <$> Bare.makeHaskellInlines cfg src embs lmap mySpec-  , Ms.dataDecls = Bare.makeHaskellDataDecls cfg mySpec tcs+  , Ms.dataDecls = Bare.makeHaskellDataDecls mySpec tcs   }   where     tcs          = uniqNub (_gsTcs src ++ refTcs)-    refTcs       = reflectedTyCons cfg embs cbs  mySpec+    refTcs       = reflectedTyCons embs cbs  mySpec     cbs          = _giCbs       src  uniqNub :: (Ghc.Uniquable a) => [a] -> [a]@@ -521,29 +540,37 @@ -- | 'reflectedTyCons' returns the list of `[TyCon]` that must be reflected but --   which are defined *outside* the current module e.g. in Base or somewhere --   that we don't have access to the code.+--+--   We collect TyCons from the data constructors actually used in the bodies of+--   reflected functions and measure functions, rather than those mentioned in+--   their type signatures. This avoids generating selectors for types that are+--   only referenced in signatures but not actually pattern-matched. -reflectedTyCons :: Config -> TCEmb Ghc.TyCon -> [Ghc.CoreBind] -> Ms.BareSpec -> [Ghc.TyCon]-reflectedTyCons cfg embs cbs spec-  | exactDCFlag cfg = filter (not . isEmbedded embs)-                    $ concatMap varTyCons-                    $ reflectedVars spec cbs ++ measureVars spec cbs-  | otherwise       = []+reflectedTyCons :: TCEmb Ghc.TyCon -> [Ghc.CoreBind] -> Ms.BareSpec -> [Ghc.TyCon]+reflectedTyCons embs cbs spec =+    [ tyCon+    | fv <- freeVars S.empty relevantBinds+    , dc <- case Ghc.idDetails fv of+        Ghc.DataConWrapId dc -> [dc]+        Ghc.DataConWorkId dc -> [dc]+        _                    -> []+    , let tyCon = Ghc.dataConTyCon dc+    , not (isEmbedded embs tyCon)+    ]+  where+    reflMeasVarSet = S.fromList $ reflectedVars spec cbs ++ measureVars spec cbs+    relevantBinds  = filter (isRelevantBind reflMeasVarSet) cbs +isRelevantBind :: S.HashSet Ghc.Var -> Ghc.CoreBind -> Bool+isRelevantBind vars (Ghc.NonRec v _) = v `S.member` vars+isRelevantBind vars (Ghc.Rec pairs)  = any ((`S.member` vars) . fst) pairs+ -- | We cannot reflect embedded tycons (e.g. Bool) as that gives you a sort --   conflict: e.g. what is the type of is-True? does it take a GHC.Types.Bool --   or its embedding, a bool? isEmbedded :: TCEmb Ghc.TyCon -> Ghc.TyCon -> Bool isEmbedded embs c = F.tceMember c embs -varTyCons :: Ghc.Var -> [Ghc.TyCon]-varTyCons = specTypeCons . ofType . Ghc.varType--specTypeCons           :: SpecType -> [Ghc.TyCon]-specTypeCons         = foldRType tc []-  where-    tc acc t@RApp {} = rtc_tc (rt_tycon t) : acc-    tc acc _         = acc- reflectedVars :: Ms.BareSpec -> [Ghc.CoreBind] -> [Ghc.Var] reflectedVars spec cbs =     filter@@ -1286,7 +1313,7 @@     tycons        = tcs ++ wiredTyCons     datacons      = Bare.makePluggedDataCon (typeclass cfg) embs tyi <$> (concat dcs ++ wiredDataCons)     tds           = [(name, tcpCon tcp, dd) | (name, tcp, Just dd) <- tcDds]-    (diag1, adts) = Bare.makeDataDecls cfg embs myName tds       datacons+    (diag1, adts) = Bare.makeDataDecls embs myName tds       datacons     dm            = Bare.dataConMap adts     dcSelectors   = concatMap (Bare.makeMeasureSelectors cfg dm) (if reflection cfg then charDataCon:datacons else datacons)     fiTcs         = _gsFiTcs (Bare.reSrc env)@@ -1396,7 +1423,7 @@       , shouldBeUsedForScanning $ makeGHCLHName (Ghc.getName v) (symbol v)       ]     tcs           = S.toList $ Ghc.dataConTyCon `S.map` Bare.getReflDCs measEnv varsUsedForTcScanning-    dataDecls     = Bare.makeHaskellDataDecls cfg spec tcs+    dataDecls     = Bare.makeHaskellDataDecls spec tcs     tyi           = Bare.tcTyConMap    tycEnv     embs          = Bare.tcEmbs        tycEnv     dm            = Bare.tcDataConMap  tycEnv

@@ -336,8 +336,8 @@   -> (LocSpecType, F.Equation) makeAssumeType cfg tce lmap dm sym mbT v def   = ( sym {val = aty at `strengthenRes` F.subst su ref}-    , F.mkEquation -        symbolV +    , F.mkEquation+        symbolV         (fmap (second $ F.sortSubst sortSub) xts)         (F.sortSubstInExpr sortSub (F.subst su le))         (F.sortSubst sortSub out)@@ -362,9 +362,9 @@     bbs        = filter isBoolBind xs      -- rTypeSortExp produces monomorphic sorts from polymorphic types.-    -- As an example, for -    -- id :: a -> a ... id x = x -    -- we got: +    -- As an example, for+    -- id :: a -> a ... id x = x+    -- we got:     -- define id (x : a#foobar) : a#foobar = { (x : a#foobar) }     -- Using FObj instead of a real type variable (FVar i) This code solves the     -- issue by creating a sort substitution that replaces those "fake" type variables@@ -374,13 +374,16 @@     sortSub     = F.mkSortSubst $ zip (fmap F.symbol tyVars) (F.FVar <$> freeSort)     -- We need sorts that aren't polluted by rank-n types, we can't just look at     -- the term to determine statically what is the "maximum" sort bound ex:-    -- freeSort = [1 + (maximum $ -1 : F.sortAbs out : fmap (F.sortAbs . snd) xts) ..] +    -- freeSort = [1 + (maximum $ -1 : F.sortAbs out : fmap (F.sortAbs . snd) xts) ..]     -- as some variable may be bound to something of rank-n type.  In     -- SortCheck.hs in fixpoint they just start at 42 for some reason.  I think     -- Negative Debruijn indices (levels :^)) are safer     freeSort    = [-1, -2 ..] -    (xs, def') = GM.notracePpr "grabBody" $ grabBody allowTC (Ghc.expandTypeSynonyms τ) $ normalize allowTC def+    (xs, def') =+      GM.notracePpr "grabBody" $+      grabBody allowTC (Ghc.expandTypeSynonyms τ) $+      normalizeCoreExpr allowTC def     su         = F.mkSubst  $ zip (F.symbol     <$> xs) xArgs                            ++ zip (simplesymbol <$> xs) xArgs     xts        = [(F.symbol x, rTypeSortExp tce t) | (x, t) <- aargs at]

@@ -4,8 +4,9 @@ {-# LANGUAGE RecordWildCards     #-} {-# LANGUAGE OverloadedStrings   #-} {-# LANGUAGE DeriveTraversable   #-}+{-# LANGUAGE TypeOperators       #-} -{-# OPTIONS_GHC -Wno-x-partial #-}+{-# OPTIONS_GHC -Wno-incomplete-record-selectors #-}  module Language.Haskell.Liquid.Bare.Check   ( checkTargetSpec@@ -224,16 +225,16 @@   | otherwise                       = Left diagnostics   where     diagnostics      :: Diagnostics-    diagnostics      =  runReader (foldMapM (checkBind allowHO bsc "measure"      emb tcEnv env) (gsMeas       (gsData tsp))) ef+    diagnostics      =  runReader (foldMapM (checkBind bsc "measure"      emb tcEnv env) (gsMeas       (gsData tsp))) ef                      <> condNull noPrune-                        (runReader (foldMapM (checkBind allowHO bsc "constructor"  emb tcEnv env) (txCtors $ gsCtors      (gsData tsp))) ef)-                     <> runReader (foldMapM (checkBind allowHO bsc "assume"       emb tcEnv env) (gsAsmSigs    (gsSig tsp))) ef-                     <> runReader (foldMapM (checkBind allowHO bsc "reflect"      emb tcEnv env . (\sig@(_,s) -> F.notracepp (show (ty_info (toRTypeRep (F.val s)))) sig)) (gsRefSigs (gsSig tsp))) ef-                     <> runReader (checkTySigs allowHO bsc cbs            emb tcEnv env                (gsSig tsp)) ef+                        (runReader (foldMapM (checkBind bsc "constructor"  emb tcEnv env) (txCtors $ gsCtors      (gsData tsp))) ef)+                     <> runReader (foldMapM (checkBind bsc "assume"       emb tcEnv env) (gsAsmSigs    (gsSig tsp))) ef+                     <> runReader (foldMapM (checkBind bsc "reflect"      emb tcEnv env . (\sig@(_,s) -> F.notracepp (show (ty_info (toRTypeRep (F.val s)))) sig)) (gsRefSigs (gsSig tsp))) ef+                     <> runReader (checkTySigs bsc cbs            emb tcEnv env                (gsSig tsp)) ef                      -- ++ mapMaybe (checkTerminationExpr             emb       env) (gsTexprs     (gsSig  sp))-                     <> runReader (foldMapM (checkBind allowHO bsc "class method" emb tcEnv env) (clsSigs      (gsSig tsp))) ef-                     <> runReader (foldMapM (checkInv allowHO bsc emb tcEnv env)                 (gsInvariants (gsData tsp))) ef-                     <> runReader (checkIAl allowHO bsc emb tcEnv env                            (gsIaliases   (gsData tsp))) ef+                     <> runReader (foldMapM (checkBind bsc "class method" emb tcEnv env) (clsSigs      (gsSig tsp))) ef+                     <> runReader (foldMapM (checkInv bsc emb tcEnv env)                 (gsInvariants (gsData tsp))) ef+                     <> runReader (checkIAl bsc emb tcEnv env                            (gsIaliases   (gsData tsp))) ef                      <> runReader (checkMeasures emb env ms) ef                      <> checkClassMeasures                                        ms                      <> checkClassMethods (gsCls src) (gsCMethods (gsVars tsp)) (gsTySigs     (gsSig tsp))@@ -267,7 +268,6 @@     clsSigs sp       = [ (v, t) | (v, t) <- gsTySigs sp, isJust (isClassOpId_maybe v) ]     sigs             = gsTySigs (gsSig tsp) ++ gsAsmSigs (gsSig tsp) ++ gsCtors (gsData tsp)     -- allowTC          = typeclass (getConfig sp)-    allowHO          = higherOrderFlag tsp     bsc              = bscope (getConfig tsp)     noPrune          = not (pruneFlag tsp)     txCtors ts       = [(v, fmap (fmap (fmap (F.filterUnMatched temps))) t) | (v, t) <- ts]@@ -318,8 +318,7 @@   ---------------------------------------------------------------------------------checkTySigs :: Bool-            -> BScope+checkTySigs :: BScope             -> [CoreBind]             -> F.TCEmb TyCon             -> Bare.TyConMap@@ -327,7 +326,7 @@             -> GhcSpecSig             -> ElabM Diagnostics ---------------------------------------------------------------------------------checkTySigs allowHO bsc cbs emb tcEnv senv sig =+checkTySigs bsc cbs emb tcEnv senv sig =   do ef <- ask      pure $ mconcat (runReader (traverse (check senv) topTs) ef)                    -- = concatMap (check env) topTs@@ -337,7 +336,7 @@                    -- ++ coreVisitor checkVisitor env [] cbs   where     check :: F.SEnv F.SortedReft -> (Var, (LocSpecType, Maybe [Located F.Expr])) -> ElabM Diagnostics-    check          = checkSigTExpr allowHO bsc emb tcEnv+    check          = checkSigTExpr bsc emb tcEnv     locTm          = M.fromList locTs     (locTs, topTs) = Bare.partitionLocalBinds vtes     vtes           = [ (x, (t, es)) | (x, t) <- gsTySigs sig, let es = M.lookup x vExprs]@@ -355,14 +354,14 @@                          Nothing -> pure emptyDiagnostics                          Just t  -> check env (v, t) -checkSigTExpr :: Bool -> BScope -> F.TCEmb TyCon -> Bare.TyConMap -> F.SEnv F.SortedReft+checkSigTExpr :: BScope -> F.TCEmb TyCon -> Bare.TyConMap -> F.SEnv F.SortedReft               -> (Var, (LocSpecType, Maybe [Located F.Expr]))               -> ElabM Diagnostics-checkSigTExpr allowHO bsc emb tcEnv env (x, (t, es)) =+checkSigTExpr bsc emb tcEnv env (x, (t, es)) =   do ef <- ask      pure $ runReader mbErr1 ef <> runReader mbErr2 ef    where-    mbErr1 = checkBind allowHO bsc empty emb tcEnv env (x, t)+    mbErr1 = checkBind bsc "checkSigTExpr" emb tcEnv env (x, t)     mbErr2 = maybe (pure emptyDiagnostics) (checkTerminationExpr emb env . (x, t,)) es     -- mbErr2 = checkTerminationExpr emb env . (x, t,) =<< es @@ -389,44 +388,41 @@      checkWFSize ef f tcp = ((f, tcp),) <$> runReader (checkSortFull (F.srcSpan tcp) (F.insertSEnv x (mkTySort (tcpCon tcp)) env) F.intSort (f x)) ef     x                 = "x" :: F.Symbol-    mkTySort tc       = rTypeSortedReft emb (ofType $ TyConApp tc (TyVarTy <$> tyConTyVars tc) :: RRType ())+    mkTySort tc       = rTypeSortedReft emb (ofType $ TyConApp tc (TyVarTy <$> tyConTyVars tc) :: RRType NoReft)      isWiredInLenFn :: SizeFun -> Bool     isWiredInLenFn IdSizeFun           = False     isWiredInLenFn (SymSizeFun locSym) = isWiredIn locSym -checkInv :: Bool-         -> BScope+checkInv :: BScope          -> F.TCEmb TyCon          -> Bare.TyConMap          -> 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 bsc emb tcEnv env (_, t) =+  checkTy bsc err emb tcEnv env t   where     err              = ErrInvt (GM.sourcePosSrcSpan $ loc t) (val t) -checkIAl :: Bool-         -> BScope+checkIAl :: BScope          -> F.TCEmb TyCon          -> Bare.TyConMap          -> F.SEnv F.SortedReft          -> [(LocSpecType, LocSpecType)]          -> ElabM Diagnostics-checkIAl allowHO bsc emb tcEnv env ss =-  do ds <- traverse (checkIAlOne allowHO bsc emb tcEnv env) ss+checkIAl bsc emb tcEnv env ss =+  do ds <- traverse (checkIAlOne bsc emb tcEnv env) ss      pure $ mconcat ds -checkIAlOne :: Bool-            -> BScope+checkIAlOne :: BScope             -> F.TCEmb TyCon             -> Bare.TyConMap             -> F.SEnv F.SortedReft             -> (LocSpecType, LocSpecType)             -> ElabM Diagnostics-checkIAlOne allowHO bsc emb tcEnv env (t1, t2) =-  do cs <- traverse (\t -> checkTy allowHO bsc (err t) emb tcEnv env t) [t1, t2]+checkIAlOne bsc emb tcEnv env (t1, t2) =+  do cs <- traverse (\t -> checkTy bsc (err t) emb tcEnv env t) [t1, t2]      pure $ mconcat $ checkEq : cs   where     err    t = ErrIAl (GM.sourcePosSrcSpan $ loc t) (val t)@@ -446,16 +442,15 @@     err1s               = checkDuplicateRTAlias msg as  checkBind :: (PPrint v)-          => Bool-          -> BScope+          => BScope           -> Doc           -> F.TCEmb TyCon           -> Bare.TyConMap           -> 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 bsc s emb tcEnv env (v, t) =+  checkTy bsc msg emb tcEnv env t   where     msg                      = ErrTySpec (GM.fSrcSpan t) (Just s) (pprint v) (val t) @@ -493,16 +488,15 @@     rSort   = rTypeSortedReft emb     cmpZero e = F.PAtom F.Le (F.expr (0 :: Int)) (val e) -checkTy :: Bool-        -> BScope+checkTy :: BScope         -> (Doc -> Error)         -> F.TCEmb TyCon         -> Bare.TyConMap         -> F.SEnv F.SortedReft         -> LocSpecType         -> ElabM Diagnostics-checkTy allowHO bsc mkE emb tcEnv env t =-  do me <- checkRType allowHO bsc emb env (Bare.txRefSort tcEnv emb t)+checkTy bsc mkE emb tcEnv env t =+  do me <- checkRType bsc emb env (Bare.txRefSort tcEnv emb t)      pure $ case me of               Nothing -> emptyDiagnostics               Just d  -> mkDiagnostics mempty [mkE d]@@ -571,19 +565,18 @@ ------------------------------------------------------------------------------------------------ -- | @checkRType@ determines if a type is malformed in a given environment --------------------- -------------------------------------------------------------------------------------------------checkRType :: Bool -> BScope -> F.TCEmb TyCon -> F.SEnv F.SortedReft -> LocSpecType -> ElabM (Maybe Doc)+checkRType :: BScope -> F.TCEmb TyCon -> F.SEnv F.SortedReft -> LocSpecType -> ElabM (Maybe Doc) -------------------------------------------------------------------------------------------------checkRType allowHO bsc emb senv lt =+checkRType bsc emb senv lt =   do ef <- ask      let f env me r err = err <|> runReader (checkReft (F.srcSpan lt) env emb me r) ef      pure $     checkAppTys st             <|> checkAbstractRefs st-            <|> efoldReft farg bsc cb (tyToBind emb) (rTypeSortedReft emb) f insertPEnv senv Nothing st+            <|> efoldReft bsc cb (tyToBind emb) (rTypeSortedReft emb) f insertPEnv senv Nothing st   where     -- isErasable         = if allowTC then isEmbeddedDict else isClass     st                 = val lt     cb c ts            = classBinds emb (rRCls c ts)-    farg _ t           = allowHO || isBase t  -- NOTE: this check should be the same as the one in addCGEnv      insertPEnv p γ     = insertsSEnv γ (fmap (rTypeSortedReft emb) <$> pbinds p)     pbinds p           = (pname p, pvarRType p :: RSort) : [(x, tx) | (tx, x, _) <- pargs p]@@ -625,7 +618,7 @@   checkAbstractRefs-  :: (PPrint t, Reftable t, SubsTy RTyVar RSort t, Reftable (RTProp RTyCon RTyVar (UReft t))) =>+  :: (PPrint t, IsReft t, ReftBind t ~ F.Symbol, ReftVar t ~ F.Symbol, SubsTy RTyVar RSort t) =>      RType RTyCon RTyVar (UReft t) -> Maybe Doc checkAbstractRefs rt = go rt   where@@ -683,7 +676,7 @@     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)))+checkReft                    :: (PPrint r, IsReft r, ReftBind r ~ F.Symbol, ReftVar r ~ F.Symbol, SubsTy RTyVar (RType RTyCon RTyVar NoReft) 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. checkReft sp env emb (Just t) _ = do me <- checkSortedReftFull sp env r@@ -717,8 +710,7 @@   where     txerror = ErrMeas (GM.sourcePosSrcSpan src) (pprint n) -checkMBody :: (PPrint r, Reftable r,SubsTy RTyVar RSort r, Reftable (RTProp RTyCon RTyVar r))-           => F.SEnv F.SortedReft+checkMBody :: F.SEnv F.SortedReft            -> F.TCEmb TyCon            -> t            -> SpecType@@ -740,14 +732,14 @@     ct    = ofType $ dataConWrapperType c :: SpecType  checkMBodyUnify-  :: RType t t2 t1 -> RType c tv r -> [(t2,RType c tv (),RType c tv r)]+  :: RType t t2 t1 -> RType c tv r -> [(t2,RType c tv NoReft,RType c tv r)] checkMBodyUnify = go   where     go (RVar tv _) t      = [(tv, toRSort t, t)]     go t@RApp{} t'@RApp{} = concat $ zipWith go (rt_args t) (rt_args t')     go _ _                = [] -checkMBody' :: (PPrint r, Reftable r, SubsTy RTyVar RSort r, Reftable (RTProp RTyCon RTyVar r))+checkMBody' :: (PPrint r, IsReft r, ReftBind r ~ F.Symbol, ReftVar r ~ F.Symbol, SubsTy RTyVar RSort r)             => F.TCEmb TyCon             -> RType RTyCon RTyVar r             -> F.SEnv F.SortedReft@@ -806,12 +798,12 @@           ++ " contains an inner refinement."  -isRefined :: Reftable r => RType c tv r -> Bool+isRefined :: ToReft r => RType c tv r -> Bool isRefined ty   | Just r <- stripRTypeBase ty = not $ isTauto r   | otherwise = False -hasInnerRefinement :: Reftable r => RType c tv r -> Bool+hasInnerRefinement :: ToReft r => RType c tv r -> Bool hasInnerRefinement (RFun _ _ rIn rOut _) =   isRefined rIn || isRefined rOut hasInnerRefinement (RAllT _ ty  _) =

@@ -91,8 +91,8 @@     tyvsmap       = case Bare.runMapTyVars allowTC t0 st err of                           Left e  -> Ex.throw e                           Right s -> Bare.vmap s-    su            = [(y, rTyVar x)           | (x, y) <- tyvsmap]-    su'           = [(y, RVar (rTyVar x) ()) | (x, y) <- tyvsmap] :: [(RTyVar, RSort)]+    su            = [(y, rTyVar x)               | (x, y) <- tyvsmap]+    su'           = [(y, RVar (rTyVar x) NoReft) | (x, y) <- tyvsmap] :: [(RTyVar, RSort)]     coSub         = M.fromList [(F.symbol y, F.FObj (F.symbol x)) | (y, x) <- su]     ps'           = fmap (subts su') <$> ps     cs'           = [(F.dummySymbol, RApp c ts [] mempty) | (c, ts) <- cs ]

@@ -213,15 +213,12 @@  type DataPropDecl = (DataDecl, Maybe SpecType) -makeDataDecls :: Config -> F.TCEmb Ghc.TyCon -> ModName+makeDataDecls :: F.TCEmb Ghc.TyCon -> ModName               -> [(ModName, Ghc.TyCon, DataPropDecl)]               -> [Located DataConP]               -> (Diagnostics, [F.DataDecl])-makeDataDecls cfg tce name tds ds-  | makeDecls        = (mkDiagnostics warns [], okDecs)-  | otherwise        = (mempty, [])+makeDataDecls tce name tds ds = (mkDiagnostics warns [], okDecs)   where-    makeDecls        = exactDCFlag cfg && not (noADT cfg)     warns            =       (mkWarnDecl . fmap pprint . dataNameSymbol . tycName . fst . fst . snd <$> badTcs) ++       (mkWarnDecl . (\d -> F.atLoc d (pprint $ F.symbol d)) <$> badDecs)@@ -513,7 +510,10 @@ -- constructor we list in a datatype is indeed a constructor of that corresponding -- Haskell datatype. ----- We also check that constructors do not have duplicate fields.+-- We also check that constructors do not have duplicate fields, and that any+-- field name reused across constructors would induce the same selector sort.+-- This rejects ambiguous data annotations such as using the same selector name+-- for different field types in different constructors. -- checkDataCtors :: Bare.Env -> ModName -> Ghc.TyCon -> DataDecl -> Maybe [DataCtor] -> Bare.Lookup [DataCtor] checkDataCtors _env _name _c _dd Nothing     = return []@@ -526,7 +526,9 @@   mbDcs <- mapM (Bare.failMaybe env name . Bare.lookupGhcDataConLHName env . dcName) cons   let rdcs = S.fromList . fmap F.symbol . Mb.catMaybes $ mbDcs   if dcs == rdcs-    then mapM checkDataCtorDupField cons+    then do+      cons' <- mapM checkDataCtorDupField cons+      checkDataCtorFieldTypes cons'     else Left [errDataConMismatch (getLHNameSymbol <$> dataNameSymbol (tycName dd)) dcs rdcs]  -- | Checks whether the given data constructor has duplicate fields.@@ -541,11 +543,47 @@       dups        = [ x | (x, ts) <- Misc.groupList xts, 2 <= length ts ]       err lc x    = ErrDupField (GM.sourcePosSrcSpan $ loc lc) (pprint $ val lc) (pprint x) +-- | Checks whether selectors shared across constructors have compatible types.+--+-- We only reject field names that would denote different selector sorts, because+-- those become duplicate logic definitions once selector measures are generated.+checkDataCtorFieldTypes :: [DataCtor] -> Bare.Lookup [DataCtor]+checkDataCtorFieldTypes ds+  | []     <- errs = return ds+  | e : _  <- errs = Left [e]+  | otherwise      = impossible Nothing "checkDataCtorFieldTypes"+  where+    errs = [ err x xts+           | (x, xts) <- Misc.groupList fieldTys+           , let tys = Misc.nubHashOn (\(_, s, _) -> s) xts+           , 2 <= length tys+           ]++    fieldTys =+      [ ( lhNameToUnqualifiedSymbol x+        , (dcName d, toRSort t, t)+        )+      | d <- ds+      , Mb.isNothing (dcResult d)+      , (x, t) <- dcFields d+      , not (GM.isTmpSymbol (lhNameToUnqualifiedSymbol x))+      ]++    err x xts@((dc, _, _) : _) =+      ErrBadData (GM.fSrcSpan dc) (pprint x) $+        PJ.text "Field has incompatible selector types across constructors:"+        PJ.$+$ PJ.nest 4 (PJ.vcat [ PJ.parens (pprint (val dc')) <+> pprint x <+> "::" <+> pprint t | (dc', _, t) <- xts ])+    err _ [] =+      impossible Nothing "checkDataCtorFieldTypes"+ selectDD :: (a, [DataDecl]) -> Either [DataDecl] DataDecl selectDD (_,[d]) = Right d-selectDD (_, ds) = case [ d | d <- ds, tycKind d == DataReflected ] of-                     [d] -> Right d-                     _   -> Left  ds+selectDD (_, ds) = case [ d | d <- ds, tycKind d == DataUser ] of+                     [du] -> case [ d | d <- ds, tycKind d == DataReflected ] of+                        [dr] -> Right dr+                        [] -> Right du+                        drs -> Left drs+                     dus -> Left dus  groupVariances :: [DataDecl]                -> [(Located LHName, [Variance])]

@@ -5,6 +5,7 @@ {-# LANGUAGE LambdaCase                #-} {-# LANGUAGE OverloadedStrings         #-} {-# LANGUAGE TemplateHaskellQuotes     #-}+{-# LANGUAGE FlexibleContexts          #-}  {-# OPTIONS_GHC -Wno-orphans #-} @@ -181,7 +182,7 @@   deriving (Functor)  -- It's probably ok to treat (RType c tv ()) as a leaf..-type RTPropF c tv f = Ref (RType c tv ()) f+type RTPropF c tv f = Ref (RType c tv NoReft) f   -- | SpecType with Holes.@@ -281,12 +282,12 @@   canonicalizeDictBinder-  :: F.Subable a => [F.Symbol] -> (a, [F.Symbol]) -> (a, [F.Symbol])+  :: (F.Subable a, F.PPrint (F.Variable a), Ord (F.Variable a)) => [F.Variable a] -> (a, [F.Variable a]) -> (a, [F.Variable a]) canonicalizeDictBinder [] (e', bs') = (e', bs') canonicalizeDictBinder bs (e', [] ) = (e', bs) canonicalizeDictBinder bs (e', bs') = (renameDictBinder bs bs' e', bs)  where-  renameDictBinder :: (F.Subable a) => [F.Symbol] -> [F.Symbol] -> a -> a+  renameDictBinder :: (F.Subable a, F.PPrint (F.Variable a), Ord (F.Variable a)) => [F.Variable a] -> [F.Variable a] -> a -> a   renameDictBinder []          _  = id   renameDictBinder _           [] = id   renameDictBinder canonicalDs ds = F.substa $ \x -> M.lookupDefault x x tbl

@@ -2,10 +2,11 @@ --   and the pipeline for "cooking" a @BareType@ into a @SpecType@. --   TODO: _only_ export `makeRTEnv`, `cookSpecType` and maybe `qualifyExpand`... +{-# LANGUAGE FlexibleContexts      #-} {-# LANGUAGE FlexibleInstances     #-} {-# LANGUAGE PartialTypeSignatures #-} {-# LANGUAGE OverloadedStrings     #-}-{-# OPTIONS_GHC -Wno-x-partial #-}+{-# LANGUAGE TypeOperators         #-}  module Language.Haskell.Liquid.Bare.Expand   ( -- * Create alias expansion environment@@ -42,7 +43,7 @@ import qualified Language.Fixpoint.Types               as F -- import qualified Language.Fixpoint.Types.Visitor       as F import qualified Language.Fixpoint.Misc                as Misc-import           Language.Fixpoint.Types (Expr, ExprV(..), SourcePos) -- , Symbol, symbol)+import           Language.Fixpoint.Types (Expr, ExprV, ExprBV(..), SourcePos) -- , Symbol, symbol) import qualified Language.Haskell.Liquid.GHC.Misc      as GM import qualified Liquid.GHC.API       as Ghc import           Language.Haskell.Liquid.Types.Errors@@ -132,7 +133,7 @@  -- | @renameRTVArgs@ ensures that @RTAlias@ value parameters have distinct names --   to avoid variable capture e.g. as in tests-names-pos-Capture01.hs-renameRTVArgs :: (F.PPrint a, F.Subable a) => RTAlias x a -> RTAlias x a+renameRTVArgs :: (F.PPrint a, F.Subable a, F.Variable a ~ F.Symbol) => RTAlias x a -> RTAlias x a renameRTVArgs rt = rt { rtVArgs = newArgs                       , rtBody  = F.notracepp msg $ F.subst su (rtBody rt)                       }@@ -288,7 +289,7 @@     go (PAtom _ e1 e2) = go e1 ++ go e2     go (ETApp e _)     = go e     go (ETAbs e _)     = go e-    go (PKVar _ _)     = []+    go PKVar{} = []     go (PExist _ e)    = go e     go_alias f         = [f | M.member f table ] @@ -332,13 +333,13 @@     = expandReft     rtEnv l -- apply expression aliases     . expandBareType rtEnv l -- apply type       aliases -instance Expand () where+instance Expand (NoReftB b) where   expand _ _ = id -instance Expand (BRType ()) where+instance Expand (BRType NoReft) where   expand rtEnv l     = expandReft     rtEnv l -- apply expression aliases-    . void+    . (NoReft <$)     . expandBareType rtEnv l -- apply type       aliases     . fmap (const mempty) @@ -514,6 +515,7 @@     f =   (if doplug || not allowTC then plugHoles allowTC sigEnv name x else id)         . fmap (RT.addTyConInfo embs tyi)         . Bare.txRefSort tyi embs+        . checkExtraAbsRef embs tyi         . fmap txExpToBind -- What does this function DO         . (specExpandType rtEnv . fmap (generalizeWith x))         . (if doplug || not allowTC then maybePlug allowTC sigEnv name x else id)@@ -540,6 +542,42 @@ generalizeWith  Bare.RawTV   t = t generalizeWith _             t = RT.generalize t +-- | Check for extra abstract refinement arguments (lambda-form) on type+--   constructors that don't declare enough PVar parameters.  This must run+--   BEFORE 'txRefSort' and 'addTyConInfo' so that only user-written RProps+--   are present (system-generated default RProps from 'rtPropTop' have not+--   been added yet).  See GitHub issue #2603.+checkExtraAbsRef :: F.TCEmb Ghc.TyCon -> Bare.TyConMap -> LocSpecType -> LocSpecType+checkExtraAbsRef embs tyi lt = walkCheck (GM.fSrcSpan lt) (val lt) `seq` lt+  where+    walkCheck sp (RAllT _ t _)      = walkCheck sp t+    walkCheck sp (RAllP _ t)        = walkCheck sp t+    walkCheck sp (RFun _ _ t1 t2 _) = walkCheck sp t1 `seq` walkCheck sp t2+    walkCheck sp (RApp rc ts rs _)+      | not (null lambdaRest)+      = uError $ ErrOther sp $ PJ.vcat+          [ PJ.text "Type constructor" PJ.<+> PJ.text (GM.showPpr (rtc_tc rc))+              PJ.<+> if nExpected == 0+                       then PJ.text "does not accept abstract refinement arguments,"+                       else PJ.text "expects" PJ.<+> PJ.int nExpected+                         PJ.<+> PJ.text "abstract refinement argument(s),"+          , PJ.text "but was given" PJ.<+> PJ.int nGiven PJ.<> PJ.text "."+          ]+      | otherwise = foldWalk sp ts+      where+        (_, pvs)    = RT.appRTyCon embs tyi rc ts+        nExpected   = length pvs+        nGiven      = length rs+        (_, rrest)  = splitAt nExpected rs+        lambdaRest  = [r | r@(RProp binds _) <- rrest, not (null binds)]+    walkCheck sp (RAllE _ t1 t2)    = walkCheck sp t1 `seq` walkCheck sp t2+    walkCheck sp (REx _ t1 t2)      = walkCheck sp t1 `seq` walkCheck sp t2+    walkCheck sp (RAppTy t1 t2 _)   = walkCheck sp t1 `seq` walkCheck sp t2+    walkCheck sp (RRTy xts _ _ t)   = foldWalk sp (snd <$> xts) `seq` walkCheck sp t+    walkCheck _  _                   = ()++    foldWalk sp = L.foldl' (\acc t -> acc `seq` walkCheck sp t) ()+ generalizeVar :: Ghc.Var -> SpecType -> SpecType generalizeVar v t = mkUnivs [(a, mempty) | a <- as] [] t   where@@ -653,7 +691,7 @@     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 e@(PKVar _ _)    = e+    go e@PKVar{}        = e     go e@(ESym _)       = e     go e@(ECon _)       = e @@ -681,7 +719,7 @@ -------------------------------------------------------------------------------- -- | Expand Alias Application -------------------------------------------------- ---------------------------------------------------------------------------------expandApp :: F.Subable ty => F.SourcePos -> RTAlias F.Symbol ty -> [Expr] -> ty+expandApp :: (F.Subable ty, F.Variable ty ~ F.Symbol) => F.SourcePos -> RTAlias F.Symbol ty -> [Expr] -> ty expandApp l re es   | Just su <- args = F.subst su (rtBody re)   | otherwise       = Ex.throw err

@@ -164,20 +164,15 @@   --------------------------------------------------------------------------------makeHaskellDataDecls :: Config -> Ms.BareSpec -> [Ghc.TyCon]-                     -> [DataDecl]+makeHaskellDataDecls :: Ms.BareSpec -> [Ghc.TyCon] -> [DataDecl] ---------------------------------------------------------------------------------makeHaskellDataDecls cfg spec tcs-  | exactDCFlag cfg = Bare.dataDeclSize spec-                    . Mb.mapMaybe tyConDataDecl-                    -- . F.tracepp "makeHaskellDataDecls-3"-                    . zipMap   (hasDataDecl spec . fst)-                    -- . F.tracepp "makeHaskellDataDecls-2"-                    . liftableTyCons-                    -- . F.tracepp "makeHaskellDataDecls-1"-                    . filter isReflectableTyCon-                    $ tcs-  | otherwise       = []+makeHaskellDataDecls spec tcs =+    Bare.dataDeclSize spec+    . Mb.mapMaybe tyConDataDecl+    . zipMap   (hasDataDecl spec . fst)+    . liftableTyCons+    . filter isReflectableTyCon+    $ tcs   isReflectableTyCon :: Ghc.TyCon -> Bool@@ -261,7 +256,7 @@  makeMeasureSelectors :: Config -> Bare.DataConMap -> Located DataConP -> [Measure SpecType Ghc.DataCon] makeMeasureSelectors cfg dm (Loc l l' c)-  = Misc.condNull (exactDCFlag cfg) (checker : Mb.mapMaybe go' fields) --  internal measures, needed for reflection+  = checker : Mb.mapMaybe go' fields --  internal measures, needed for reflection  ++ Misc.condNull autofields (Mb.mapMaybe go fields) --  user-visible measures.   where     dc         = dcpCon    c@@ -302,8 +297,8 @@     err                  = panic Nothing $ "DataCon " ++ show dc ++ "does not have " ++ show i ++ " fields"  -- bkDataCon :: DataCon -> Int -> ([RTVar RTyVar RSort], [SpecType], (Symbol, SpecType, RReft))-bkDataCon :: (Reftable (RTProp RTyCon RTyVar r), PPrint r, Reftable r) => Bool -> Ghc.DataCon -> Int -> ([RTVar RTyVar RSort], [RRType r], (F.Symbol, RFInfo, RRType r, r))-bkDataCon permitTC dcn nFlds  = (as, ts, (F.dummySymbol, classRFInfo permitTC, t, mempty))+bkDataCon :: (PPrint r, IsReft r) => Bool -> Ghc.DataCon -> Int -> ([RTVar RTyVar RSort], [RRType r], (F.Symbol, RFInfo, RRType r, r))+bkDataCon permitTC dcn nFlds  = (as, ts, (F.dummySymbol, classRFInfo permitTC, t, trueReft))   where     ts                = RT.ofType <$> Misc.takeLast nFlds (map Ghc.irrelevantMult _ts)     t                 = -- Misc.traceShow ("bkDataConResult" ++ GM.showPpr (dc, _t, _t0)) $@@ -570,7 +565,7 @@     msg   = "QUALIFY-EXPAND-BODY" ++ F.showpp (bs, body d)  -------------------------------------------------------------------------------varMeasures :: (Monoid r) => Bare.Env -> [(F.Symbol, Located (RRType r))]+varMeasures :: (IsReft r) => Bare.Env -> [(F.Symbol, Located (RRType r))] ------------------------------------------------------------------------------ varMeasures env =   [ (F.symbol v, varSpecType v)@@ -583,10 +578,10 @@                             ++ Bare.meClassSyms measEnv -- cms'                             ++ varMeasures env -varSpecType :: (Monoid r) => Ghc.Var -> Located (RRType r)+varSpecType :: (IsReft r) => Ghc.Var -> Located (RRType r) varSpecType = fmap (RT.ofType . Ghc.varType) . GM.locNamedThing -varBareType :: (Monoid r) => Ghc.Var -> Located (BRType r)+varBareType :: (IsReft r) => Ghc.Var -> Located (BRType r) varBareType = fmap (RT.bareOfType . Ghc.varType) . GM.locNamedThing  varLocSym :: Ghc.Var -> LocSymbol

@@ -52,58 +52,6 @@  -} -{--HEAD-freeSymbols :: (Reftable r, Reftable r1, F.Reftable r2, TyConable c, TyConable c1, TyConable c2)-            => [F.Symbol]-            -> [(a1, Located (RType c2 tv2 r2))]-            -> [(a, Located (RType c1 tv1 r1))]-            -> [Located (RType c tv r)]-            -> [LocSymbol]-freeSymbols xs' xts yts ivs =  [ lx | lx <- Misc.sortNub $ zs ++ zs' ++ zs'' , not (M.member (val lx) knownM) ]-  where-    knownM                  = M.fromList [ (x, ()) | x <- xs' ]-    zs                      = concatMap freeSyms (snd <$> xts)-    zs'                     = concatMap freeSyms (snd <$> yts)-    zs''                    = concatMap freeSyms ivs------------------------------------------------------------------------------------freeSyms :: (Reftable r, TyConable c) => Located (RType c tv r) -> [LocSymbol]---------------------------------------------------------------------------------freeSyms ty    = [ F.atLoc ty x | x <- tySyms ]-  where-    tySyms     = Misc.sortNub $ concat $ efoldReft (\_ _ -> True) False (\_ _ -> []) (const []) (const ()) f (const id) F.emptySEnv [] (val ty)-    f γ _ r xs = let F.Reft (v, _) = toReft r in-                 [ x | x <- F.syms r, x /= v, not (x `F.memberSEnv` γ)] : xs----- ABOVE IS THE T1773 STUFF---- BELOW IS THE develop-classes STUFF---- freeSymbols :: (Reftable r, Reftable r1, F.Reftable r2, TyConable c, TyConable c1, TyConable c2)---             => [F.Symbol]---             -> [(a1, Located (RType c2 tv2 r2))]---             -> [(a, Located (RType c1 tv1 r1))]---             -> [(Located (RType c tv r))]---             -> [LocSymbol]--- freeSymbols xs' xts yts ivs =  [ lx | lx <- Misc.sortNub $ zs ++ zs' ++ zs'' , not (M.member (val lx) knownM) ]---   where---     knownM                  = M.fromList [ (x, ()) | x <- xs' ]---     zs                      = concatMap freeSyms (snd <$> xts)---     zs'                     = concatMap freeSyms (snd <$> yts)---     zs''                    = concatMap freeSyms ivs------ freeSyms :: (Reftable r, TyConable c) => Located (RType c tv r) -> [LocSymbol]--- freeSyms ty    = [ F.atLoc ty x | x <- tySyms ]---   where---     tySyms     = Misc.sortNub $ concat $ efoldReft (\_ _ -> True) False (\_ _ -> []) (\_ -> []) (const ()) f (const id) F.emptySEnv [] (val ty)---     f γ _ r xs = let F.Reft (v, _) = toReft r in---                  [ x | x <- F.syms r, x /= v, not (x `F.memberSEnv` γ)] : xs---} ------------------------------------------------------------------------------- -- Renaming Type Variables in Haskell Signatures ------------------------------ -------------------------------------------------------------------------------

@@ -180,8 +180,8 @@     tyvsmap      = case Bare.runMapTyVars allowTC (toType False rt) st err of                           Left e  -> Ex.throw e                           Right s -> Bare.vmap s-    su           = [(y, rTyVar x)           | (x, y) <- tyvsmap]-    su'          = [(y, RVar (rTyVar x) ()) | (x, y) <- tyvsmap] :: [(RTyVar, RSort)]+    su           = [(y, rTyVar x)               | (x, y) <- tyvsmap]+    su'          = [(y, RVar (rTyVar x) NoReft) | (x, y) <- tyvsmap] :: [(RTyVar, RSort)]     coSub        = M.fromList [(F.symbol y, F.FObj (F.symbol x)) | (y, x) <- su]     ps'          = fmap (subts su') <$> ps     cs'          = [(F.dummySymbol, RApp c ts [] mempty) | (c, ts) <- cs2 ]@@ -282,8 +282,8 @@     -- 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)-    -- Removing length check because Haskell types can contain kinds which is safe based on the comment above -    --   | length ts == length ts'            +    -- 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)) 

@@ -9,6 +9,7 @@ {-# LANGUAGE PartialTypeSignatures #-} {-# LANGUAGE ConstraintKinds       #-} {-# LANGUAGE TupleSections         #-}+{-# LANGUAGE TypeOperators         #-}  module Language.Haskell.Liquid.Bare.Resolve   ( -- * Creating the Environment@@ -24,7 +25,7 @@   , lookupGhcDataConLHName   , lookupGhcDnTyCon   , lookupGhcIdLHName-  , lookupLocalVar+  , lookupLetBoundVar   , lookupGhcTyConLHName   , lookupGhcTyThingFromName   , lookupGhcId@@ -59,7 +60,6 @@ import qualified Data.Maybe                        as Mb import qualified Data.HashMap.Strict               as M import           GHC.Stack-import           Text.Megaparsec.Pos (sourceColumn, sourceLine) import qualified Text.PrettyPrint.HughesPJ         as PJ  import qualified Language.Fixpoint.Types               as F@@ -121,15 +121,14 @@ makeLocalVars :: [Ghc.CoreBind] -> LocalVars makeLocalVars = localVarMap . localBinds --- TODO: rewrite using CoreVisitor localBinds :: [Ghc.CoreBind] -> [LocalVarDetails] localBinds                    = concatMap (bgoT [])   where-    bgoT g (Ghc.NonRec _ e) = go g e-    bgoT g (Ghc.Rec xes)    = concatMap (go g . snd) xes-    pgo g isRec (x, e)      = mkLocalVarDetails g isRec x : go g e-    bgo g (Ghc.NonRec x e)  = pgo g False (x, e)-    bgo g (Ghc.Rec xes)     = concatMap (pgo g True) xes+    bgoT g (Ghc.NonRec x e) = pgo g True False (x, e)+    bgoT g (Ghc.Rec xes)    = concatMap (pgo g True True) xes+    pgo g isTopLevel isRec (x, e) = mkLocalVarDetails g isTopLevel isRec x : go g e+    bgo g (Ghc.NonRec x e)  = pgo g False False (x, e)+    bgo g (Ghc.Rec xes)     = concatMap (pgo g False True) xes     go g (Ghc.App e a)       = concatMap (go g) [e, a]     go g (Ghc.Lam x e)       = go (x:g) e     go g (Ghc.Let b e)       = bgo g b ++ go (Ghc.bindersOf b ++ g) e@@ -139,10 +138,11 @@     go _ (Ghc.Var _)         = []     go _ _                   = [] -    mkLocalVarDetails g isRec v = LocalVarDetails+    mkLocalVarDetails g isTopLevel isRec v = LocalVarDetails       { lvdSourcePos = F.sp_start $ F.srcSpan v       , lvdVar = v       , lvdLclEnv = g+      , lvdIsTopLevel = isTopLevel       , lvdIsRec = isRec       } @@ -186,39 +186,41 @@ isEmptySymbol :: F.Symbol -> Bool isEmptySymbol x = F.lengthSym x == 0 --- | @lookupLocalVar@ takes as input the list of "global" (top-level) vars---   that also match the name @lx@; we then pick the "closest" definition.+-- | @lookupLetBoundVar@ yields the name of the closest let-bound definition. --   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+--+-- This function never returns a top-level variable.+--+-- PRECONDITION: the input symbol is not qualified.+--+lookupLetBoundVar :: LocalVars -> LocSymbol -> Maybe Ghc.Var+lookupLetBoundVar localVars lx+   | GM.isQualifiedSym x = error $ "lookupLetBoundVar: called on a qualified symbol: " ++ show lx+   | otherwise = findNearest lxn kvs   where-    kvs                   = prioritizeRecBinds (M.lookupDefault [] x (lvSymbols localVars)) ++ gs-    gs                    = [(F.sp_start $ F.srcSpan v, Left v) | v <- gvs]-    lxn                   = F.sp_start $ F.srcSpan lx-    (_, x)                = unQualifySymbol (F.val lx)+    x = F.val lx+    kvs = prioritizeRecBinds (M.lookupDefault [] x (lvSymbols localVars))+    lxn = F.sp_start $ F.srcSpan lx      -- Sometimes GHC produces multiple bindings that have the same source     -- location. To select among these, we give preference to the recursive     -- bindings which might need termination metrics.     prioritizeRecBinds lvds =       let (recs, nrecs) = L.partition lvdIsRec lvds-       in map lvdToPair (recs ++ nrecs)-    lvdToPair lvd = (lvdSourcePos lvd, Right (lvdVar lvd))--    findNearest :: F.SourcePos -> [(F.SourcePos, b)] -> Maybe b-    findNearest key kvs1 = argMin [ (posDistance key k, v) | (k, v) <- kvs1 ]+       in recs ++ nrecs -    -- We prefer the var with the smaller distance, or equal distance-    -- but left of the spec, or not left of the spec but below it.-    posDistance a b =-      ( abs (F.unPos (sourceLine a) - F.unPos (sourceLine b))-      , sourceColumn a < sourceColumn b -- Note: False is prefered/smaller to True-      , sourceLine a > sourceLine b-      )+    findNearest :: F.SourcePos -> [LocalVarDetails] -> Maybe Ghc.Var+    findNearest key = pickByLocation key .  L.sortBy (compare `on` lvdSourcePos) -    argMin :: (Ord k) => [(k, v)] -> Maybe v-    argMin = Mb.listToMaybe . map snd . L.sortBy (compare `on` fst)+    pickByLocation :: F.SourcePos -> [LocalVarDetails] -> Maybe Ghc.Var+    pickByLocation _ [] = Nothing+    pickByLocation _ [lvd]+      | lvdIsTopLevel lvd = Nothing+      | otherwise = Just $ lvdVar lvd+    pickByLocation key (lvd0 : xs@(lvd1 : _))+      | lvdSourcePos lvd1 < key  = pickByLocation key xs+      | lvdSourcePos lvd0 < key  = pickByLocation key [lvd1]+      | otherwise = pickByLocation key [lvd0]   lookupGhcDnTyCon :: Env -> ModName -> DataName -> Lookup (Maybe Ghc.TyCon)@@ -363,9 +365,12 @@  -------------------------------------------------------------------------------- type Expandable r = ( PPrint r-                    , Reftable r-                    , SubsTy RTyVar (RType RTyCon RTyVar ()) r-                    , Reftable (RTProp RTyCon RTyVar r)+                    , IsReft r+                    , ReftBind r ~ F.Symbol+                    , ReftVar r ~ F.Symbol+                    , F.Subable r+                    , F.Variable r ~ F.Symbol+                    , SubsTy RTyVar (RType RTyCon RTyVar NoReft) r                     , HasCallStack)  ofBRType :: (Expandable r) => Env -> ([F.Symbol] -> r -> r) -> F.SourcePos -> BRType r@@ -451,13 +456,13 @@ -- TODO expandTypeSynonyms here to bareTCApp r (Loc _ _ c) rs ts | Ghc.isFamilyTyCon c && isTrivial t   = expandRTypeSynonyms (t `RT.strengthen` r)-  where t = RT.rApp c ts rs mempty+  where t = RT.rApp c ts rs trueReft  bareTCApp r (Loc _ _ c) rs ts   = RT.rApp c ts rs r  -tyApp :: Reftable r => RType c tv r -> [RType c tv r] -> [RTProp c tv r] -> r+tyApp :: Meet r => RType c tv r -> [RType c tv r] -> [RTProp c tv r] -> r       -> RType c tv r tyApp (RApp c ts rs r) ts' rs' r' = RApp c (ts ++ ts') (rs ++ rs') (r `meet` r') tyApp t                []  []  r  = t `RT.strengthen` r@@ -507,11 +512,32 @@ addSymSortRef sp rc p r i = addSymSortRef' sp rc i p r  addSymSortRef' :: (PPrint s) => Ghc.SrcSpan -> s -> Int -> RPVar -> SpecProp -> SpecProp-addSymSortRef' _ _ _ p (RProp s (RVar v r)) | isDummy v-  = RProp xs t+addSymSortRef' sp rc i p (RProp s (RVar v r)) | isDummy v+  = if length s > length (pargs p)+    then uError $ ErrPartPred sp (pprint rc) (pprint $ pname p) i (length (pargs p) + 1) (length s + 1)+    else RProp xs t     where-      t  = ofRSort (pvType p) `RT.strengthen` r-      xs = spliceArgs "addSymSortRef 1" s p+      -- When the lambda provides fewer args than the PVar expects,+      -- the lambda's refinement variable (last lambda arg) should bind+      -- to the next PVar parameter position, not to the value type.+      -- e.g. for p :: a -> a -> b -> Bool, {\x y -> x >= y} should+      -- bind x→arg1, y→arg2 (not y→value).+      nLambdaArgs = length s + 1  -- s bindings + 1 refvar+      nPVarArgs   = length (pargs p) + 1  -- pargs + 1 value+      (s', r')+        | nLambdaArgs < nPVarArgs+        , MkUReft (F.Reft (rv, body)) prd <- r+        = -- Promote the refvar to a regular binding; the body still refers+          -- to rv which now names the (length s + 1)th PVar arg.+          -- Use a fresh vv as the Reft binder (value variable).+          let vv    = F.vv (Just 0)+              -- Sort placeholder; spliceArgs replaces it with the PVar's sort+              dSort = Misc.fst3 (last (pargs p))+          in (s ++ [(rv, dSort)], MkUReft (F.Reft (vv, body)) prd)+        | otherwise+        = (s, r)+      t  = ofRSort (pvType p) `RT.strengthen` r'+      xs = spliceArgs "addSymSortRef 1" s' p  addSymSortRef' sp rc i p (RProp _ (RHole r@(MkUReft _ (Pr [up]))))   | length xs == length ts@@ -527,8 +553,10 @@ addSymSortRef' _ _ _ _ (RProp s (RHole r))   = RProp s (RHole r) -addSymSortRef' _ _ _ p (RProp s t)-  = RProp xs t+addSymSortRef' sp rc i p (RProp s t)+  = if length s > length (pargs p)+    then uError $ ErrPartPred sp (pprint rc) (pprint $ pname p) i (length (pargs p) + 1) (length s + 1)+    else RProp xs t     where       xs = spliceArgs "addSymSortRef 2" s p 

@@ -1,43 +1,43 @@ -- | This module has the code that uses the GHC definitions to: --   1. MAKE a name-resolution environment,---   2. USE the environment to translate plain symbols into Var, TyCon, etc. +--   2. USE the environment to translate plain symbols into Var, TyCon, etc. -module Language.Haskell.Liquid.Bare.Types -  ( -- * Name resolution environment +module Language.Haskell.Liquid.Bare.Types+  ( -- * Name resolution environment     Env (..)   , GHCTyLookupEnv (..)-  , TyThingMap +  , TyThingMap   , ModSpecs   , LocalVars(..)   , LocalVarDetails (..)      -- * Tycon and Datacon processing environment-  , TycEnv (..) +  , TycEnv (..)   , DataConMap   , RT.TyConMap -    -- * Signature processing environment +    -- * Signature processing environment   , SigEnv (..) -    -- * Measure related environment +    -- * Measure related environment   , MeasEnv (..) -    -- * Misc +    -- * Misc   , PlugTV (..)   , plugSrc-  , varRSort +  , varRSort   , varSortedReft   , failMaybe-  ) where +  ) where -import qualified Text.PrettyPrint.HughesPJ             as PJ +import qualified Text.PrettyPrint.HughesPJ             as PJ import qualified Data.HashSet                          as S import qualified Data.HashMap.Strict                   as M-import qualified Language.Fixpoint.Types               as F +import qualified Language.Fixpoint.Types               as F import qualified Language.Haskell.Liquid.Measure       as Ms import           Language.Haskell.Liquid.Types.DataDecl import           Language.Haskell.Liquid.Types.Names-import qualified Language.Haskell.Liquid.Types.RefType as RT +import qualified Language.Haskell.Liquid.Types.RefType as RT import           Language.Haskell.Liquid.Types.RType import           Language.Haskell.Liquid.Types.Types import           Language.Haskell.Liquid.Types.Specs   hiding (BareSpec)@@ -49,29 +49,29 @@ type ModSpecs = M.HashMap ModName Ms.BareSpec  ---------------------------------------------------------------------------------- | See [NOTE: Plug-Holes-TyVars] for a rationale for @PlugTV@ +-- | See [NOTE: Plug-Holes-TyVars] for a rationale for @PlugTV@ ------------------------------------------------------------------------------- -data PlugTV v -  = HsTV v  -- ^ Use tyvars from GHC specification (in the `v`) +data PlugTV v+  = HsTV v  -- ^ Use tyvars from GHC specification (in the `v`)   | LqTV v  -- ^ Use tyvars from Liquid specification-  | GenTV   -- ^ Generalize ty-vars +  | GenTV   -- ^ Generalize ty-vars   | RawTV   -- ^ Do NOT generalize ty-vars (e.g. for type-aliases)   deriving (Show)  -instance (Show v, F.PPrint v) => F.PPrint (PlugTV v) where -  pprintTidy _ = PJ.text . show -   -plugSrc ::  PlugTV v -> Maybe v -plugSrc (HsTV v) = Just v -plugSrc (LqTV v) = Just v +instance (Show v, F.PPrint v) => F.PPrint (PlugTV v) where+  pprintTidy _ = PJ.text . show++plugSrc ::  PlugTV v -> Maybe v+plugSrc (HsTV v) = Just v+plugSrc (LqTV v) = Just v plugSrc _        = Nothing  ---------------------------------------------------------------------------------- | Name resolution environment +-- | Name resolution environment --------------------------------------------------------------------------------data Env = RE +data Env = RE   { reTyLookupEnv :: GHCTyLookupEnv   , reTcGblEnv  :: Ghc.TcGblEnv   , reInstEnvs  :: Ghc.InstEnvs@@ -89,8 +89,8 @@        , gtleTypeEnv :: Ghc.TypeEnv        } -instance HasConfig Env where -  getConfig = reCfg +instance HasConfig Env where+  getConfig = reCfg  data LocalVars = LocalVars   { -- | A map from names to lists of pairs of @Ghc.Var@ and@@ -104,36 +104,37 @@   { lvdSourcePos :: F.SourcePos   , lvdVar :: Ghc.Var   , lvdLclEnv :: [Ghc.Var]+  , lvdIsTopLevel :: Bool  -- ^ Is the variable defined at the top-level?   , lvdIsRec :: Bool  -- ^ Is the variable defined in a letrec?   } deriving Show  ---------------------------------------------------------------------------------- | A @TyThingMap@ is used to resolve symbols into GHC @TyThing@ and, +-- | A @TyThingMap@ is used to resolve symbols into GHC @TyThing@ and, --   from there into Var, TyCon, DataCon, etc. ------------------------------------------------------------------------------- type TyThingMap = M.HashMap F.Symbol [(F.Symbol, Ghc.TyThing)]  ---------------------------------------------------------------------------------- | A @SigEnv@ contains the needed to process type signatures +-- | A @SigEnv@ contains the needed to process type signatures --------------------------------------------------------------------------------data SigEnv = SigEnv -  { sigEmbs       :: !(F.TCEmb Ghc.TyCon) -  , sigTyRTyMap   :: !RT.TyConMap +data SigEnv = SigEnv+  { sigEmbs       :: !(F.TCEmb Ghc.TyCon)+  , sigTyRTyMap   :: !RT.TyConMap   , sigExports    :: !(S.HashSet StableName)   , sigRTEnv      :: !BareRTEnv   }  ---------------------------------------------------------------------------------- | A @TycEnv@ contains the information needed to process Type- and Data- Constructors +-- | A @TycEnv@ contains the information needed to process Type- and Data- Constructors --------------------------------------------------------------------------------data TycEnv = TycEnv +data TycEnv = TycEnv   { tcTyCons      :: ![TyConP]   , tcDataCons    :: ![DataConP]   , tcSelMeasures :: ![Measure SpecType Ghc.DataCon]   , tcSelVars     :: ![(Ghc.Var, LocSpecType)]-  , tcTyConMap    :: !RT.TyConMap +  , tcTyConMap    :: !RT.TyConMap   , tcAdts        :: ![F.DataDecl]-  , tcDataConMap  :: !DataConMap +  , tcDataConMap  :: !DataConMap   , tcEmbs        :: !(F.TCEmb Ghc.TyCon)   , tcName        :: !ModName   }@@ -141,16 +142,16 @@ type DataConMap = M.HashMap (F.Symbol, Int) F.Symbol  ---------------------------------------------------------------------------------- | Intermediate representation for Measure information +-- | Intermediate representation for Measure information ------------------------------------------------------------------------------- -- REBARE: used to be output of makeGhcSpecCHOP2-data MeasEnv = MeasEnv -  { meMeasureSpec :: !(MSpec SpecType Ghc.DataCon)          -  , meClassSyms   :: ![(F.Symbol, Located (RRType F.Reft))] +data MeasEnv = MeasEnv+  { meMeasureSpec :: !(MSpec SpecType Ghc.DataCon)+  , meClassSyms   :: ![(F.Symbol, Located (RRType F.Reft))]   , meSyms        :: ![(F.Symbol, Located (RRType F.Reft))]-  , meDataCons    :: ![(Ghc.Var,  LocSpecType)]           -  , meClasses     :: ![DataConP]                           -  , meMethods     :: ![(ModName, Ghc.Var, LocSpecType)]  +  , meDataCons    :: ![(Ghc.Var,  LocSpecType)]+  , meClasses     :: ![DataConP]+  , meMethods     :: ![(ModName, Ghc.Var, LocSpecType)]   , meOpaqueRefl  :: ![(Ghc.Var, Measure (Located BareType) (F.Located LHName))] -- the opaque-reflected symbols and the corresponding measures   } @@ -159,8 +160,8 @@     { meMeasureSpec = meMeasureSpec a <> meMeasureSpec b     , meClassSyms   = meClassSyms a <> meClassSyms b     , meSyms        = meSyms a <> meSyms b-    , meDataCons    = meDataCons a <> meDataCons b  -    , meClasses     = meClasses a <> meClasses b                       +    , meDataCons    = meDataCons a <> meDataCons b+    , meClasses     = meClasses a <> meClasses b     , meMethods     = meMethods a <> meMethods b     , meOpaqueRefl  = meOpaqueRefl a <> meOpaqueRefl b     }@@ -179,21 +180,21 @@ ------------------------------------------------------------------------------- -- | Converting @Var@ to @Sort@ --------------------------------------------------------------------------------varSortedReft :: F.TCEmb Ghc.TyCon -> Ghc.Var -> F.SortedReft -varSortedReft emb = RT.rTypeSortedReft emb . varRSort +varSortedReft :: F.TCEmb Ghc.TyCon -> Ghc.Var -> F.SortedReft+varSortedReft emb = RT.rTypeSortedReft emb . varRSort  varRSort  :: Ghc.Var -> RSort varRSort  = RT.ofType . Ghc.varType  ---------------------------------------------------------------------------------- | Handling failed resolution +-- | Handling failed resolution ------------------------------------------------------------------------------- failMaybe :: Env -> ModName -> Either e r -> Either e (Maybe r)-failMaybe env name res = case res of -  Right r -> Right (Just r) -  Left  e -> if isTargetModName env name +failMaybe env name res = case res of+  Right r -> Right (Just r)+  Left  e -> if isTargetModName env name               then Left e-              else Right Nothing +              else Right Nothing -isTargetModName :: Env -> ModName -> Bool -isTargetModName env name = name == _giTargetMod (reSrc env) +isTargetModName :: Env -> ModName -> Bool+isTargetModName env name = name == _giTargetMod (reSrc env)

@@ -1,4 +1,5 @@ {-# LANGUAGE FlexibleInstances    #-}+{-# LANGUAGE TypeOperators        #-}  {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} @@ -16,7 +17,7 @@ import Language.Haskell.Liquid.Types.Types import Language.Haskell.Liquid.Constraint.Types import Language.Haskell.Liquid.Constraint.Env-import Language.Fixpoint.Types+import Language.Fixpoint.Types hiding (trueReft)  -------------------------------------------------------------------------------- addConstraints :: CGEnv -> [(Symbol, SpecType)] -> CGEnv@@ -31,7 +32,7 @@ constraintToLogic γ (LC ts) = pAnd (constraintToLogicOne γ <$> ts)  -- RJ: The code below is atrocious. Please fix it!-constraintToLogicOne :: (Reftable r) => REnv -> [(Symbol, RRType r)] -> Expr+constraintToLogicOne :: (IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol) => REnv -> [(Symbol, RRType r)] -> Expr constraintToLogicOne γ binds   = pAnd [subConstraintToLogicOne           (zip xs xts)@@ -44,14 +45,14 @@    r        = snd $ last binds    xss      = combinations ((\t -> [(x, t) | x <- localBindsOfType t γ]) <$> ts) -subConstraintToLogicOne :: (Foldable t, Reftable r, Reftable r1)-                        => t (Symbol, (Symbol, RType t1 t2 r))-                        -> (Symbol, (Symbol, RType t3 t4 r1)) -> Expr+subConstraintToLogicOne :: (Foldable t, IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol)+                        => t (Symbol, (Symbol, RType c tv r))+                        -> (Symbol, (Symbol, RType c tv r)) -> Expr subConstraintToLogicOne xts (sym', (sym, rt)) = PImp (pAnd rs) r   where         (rs , symExprs) = foldl go ([], []) xts         ([r], _ ) = go ([], symExprs) (sym', (sym, rt))-        go (acc, su) (x', (x, t)) = let (Reft(v, p)) = toReft (fromMaybe mempty (stripRTypeBase t))+        go (acc, su) (x', (x, t)) = let (Reft(v, p)) = toReft (fromMaybe trueReft (stripRTypeBase t))                                         su'          = (x', EVar x):(v, EVar x) : su                                     in                                      (subst (mkSubst su') p : acc, su')

@@ -6,6 +6,7 @@ {-# LANGUAGE OverloadedStrings         #-} {-# LANGUAGE ImplicitParams            #-} {-# LANGUAGE PartialTypeSignatures     #-}+{-# LANGUAGE TypeOperators             #-}  -- | This module defines the representation for Environments needed --   during constraint generation.@@ -194,7 +195,7 @@   is    <- (:) <$> addBind l x (rTypeSortedReft' γ' tem t) <*> addClassBind γ' l t   return $ γ' { fenv = insertsFEnv (fenv γ) is } -rTypeSortedReft' :: (PPrint r, Reftable r, SubsTy RTyVar RSort r, Reftable (RTProp RTyCon RTyVar r))+rTypeSortedReft' :: (PPrint r, IsReft r, ReftBind r ~ F.Symbol, ReftVar r ~ F.Symbol, SubsTy RTyVar RSort r)     => CGEnv -> F.Templates -> RRType r -> F.SortedReft rTypeSortedReft' γ t   = pruneUnsortedReft (feEnv $ fenv γ) t . f

@@ -11,7 +11,7 @@  module Language.Haskell.Liquid.Constraint.Fresh   ( -- module Language.Haskell.Liquid.Types.Fresh-    -- , +    -- ,     refreshArgsTop   , freshTyType   , freshTyExpr

@@ -8,10 +8,11 @@ {-# LANGUAGE OverloadedStrings         #-} {-# LANGUAGE ImplicitParams            #-} {-# LANGUAGE NamedFieldPuns            #-}+{-# LANGUAGE TypeOperators             #-}  {-# OPTIONS_GHC -Wno-orphans #-} {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}-{-# OPTIONS_GHC -Wno-x-partial #-}+{-# OPTIONS_GHC -Wno-incomplete-record-selectors #-}  -- | This module defines the representation of Subtyping and WF Constraints, --   and the code for syntax-directed constraint generation.@@ -70,10 +71,73 @@ import Language.Haskell.Liquid.UX.Config     ( HasConfig(getConfig),       Config(typeclass, checkDerived, extensionality,-             nopolyinfer, noADT, dependantCase, exactDC, rankNTypes),+             nopolyinfer, dependantCase, rankNTypes, warnOnTermHoles),       patternFlag,-      higherOrderFlag )+      higherOrderFlag, warnOnTermHoles )+import qualified GHC.Data.Strict as Strict +-- Note [Term holes]+--+-- The term-hole implementation in this module is a small, opt-in pipeline that+-- is only active when @warnOnTermHoles@ is enabled.+--+-- The thesis motivating this feature chose constraint generation as the hook for+-- hole support because this is the first phase where LiquidHaskell already knows+-- the refined types and local environment that make a warning actionable. An+-- earlier location-based approach would have been more modular, but the needed+-- query from source locations back into constraint generation was not feasible.+--+-- The implementation also uses a stable hole naming convention, recognized by+-- 'isVarHole', instead of depending on GHC surface syntax alone. This keeps the+-- matching logic local to Core while reducing the amount of desugaring detail we+-- have to reconstruct.+--+-- 1. We detect direct occurrences of a typed hole with 'detectTypedHole', which+--    peels away ticks via 'stripTicks', recovers the hole source span with+--    'lastTick', and recognizes @hole@ binders with 'isVarHole'. We need this+--    normalization-aware detection because holes can appear under GHC-introduced+--    @App@ and @Tick@ nodes, and the warning should still point at the original+--    source span.+--+-- 2. We remember hole-shaped let-bindings in 'consCB''s local @checkLetHole@+--    helper. That helper records which ANF binder names a hole by calling+--    'linkANFToHole'. This step is needed because LiquidHaskell's ANF+--    normalization can float a hole into a fresh @let@ binder, and later useful+--    constraints may mention only that ANF name instead of the original hole.+--+-- 3. We record the type and environment of each direct hole occurrence while+--    generating constraints. In checking mode, 'cconsE''s local @maybeAddHole@+--    stores the expected type with 'addHole'. In synthesis mode, 'consE''s+--    local @synthesizeWithHole@ first synthesizes the application's type and+--    then stores that synthesized type with 'addHole'. We need both sites:+--    checking gives the expected type when one is available, while synthesis+--    covers cases like applications where checking alone would only report an+--    uninformative base type for the hole.+--+-- 4. We attach ANF expressions that participate in a hole by running+--    'checkANFHoleInExpr' from 'cconsE' and from the application case of+--    'consE'. That helper walks the expression with 'collectVars', resolves any+--    binder previously linked by 'linkANFToHole' through 'isANFInHole', and+--    saves the expression/type pair with 'addHoleANF'. This is what recovers the+--    surrounding refined constraints that users actually need when the hole sits+--    inside a larger normalized expression.+--+-- 5. After constraint generation finishes, 'consAct' calls+--    'emitConsolidatedHoleWarnings'. It merges the stored hole metadata with the+--    collected ANF expressions and emits one 'ErrHole' warning per hole, using+--    the environment captured by 'addHole' so the warning reports the local+--    typing context that was in scope at the hole. Delaying emission until the+--    end is important: only then do we have the direct hole information, the ANF+--    links, and the extra constraints together in one place.+--+-- Term holes were developed during the Master's thesis+--+-- Enhancing Proof Development in LiquidHaskell: Implementation and Evaluation of Typed Holes+-- MATHEUS DE SOUSA BERNARDO+-- Chalmers University of Technology, 2025+--+-- https://odr.chalmers.se/server/api/core/bitstreams/640ee29b-b13a-44d5-9e20-200a91a11021/content+ -------------------------------------------------------------------------------- -- | Constraint Generation: Toplevel ------------------------------------------- --------------------------------------------------------------------------------@@ -99,6 +163,7 @@   fcs <- concat <$> mapM (splitC (typeclass (getConfig info))) hcs   fws <- concat <$> mapM splitW hws   checkStratCtors γ sSpc+  when (warnOnTermHoles cfg) emitConsolidatedHoleWarnings   modify $ \st -> st { fEnv     = fEnv    st `mappend` feEnv (fenv γ)                      , cgLits   = litEnv   γ                      , cgConsts = cgConsts st `mappend` constEnv γ@@ -200,6 +265,29 @@                   | otherwise                   = False +-- | Emit one warning per recorded term hole after constraint generation has+--   collected both the hole metadata and any ANF expressions linked to it.+--+-- See Note [Term holes]+emitConsolidatedHoleWarnings :: CG ()+emitConsolidatedHoleWarnings = do+  holes     <- gets hsHoles+  holeExprs <- gets hsHolesExprs++  let mergedHoles+                  = [(h+                    , holeInfo+                    , M.findWithDefault [] (h, srcSpan) holeExprs+                    )+                    | ((h, srcSpan), holeInfo) <- M.toList holes+                    ]++  forM_ mergedHoles $ \(h, holeInfo, anfs) -> do+    let γ        = snd . info $ holeInfo+    let anfs'    = map (\(v, x, t) -> (F.symbol v, x, t)) anfs+    addWarning $ ErrHole (hloc holeInfo) "hole found" (reLocal $ renv γ) (F.symbol h) (htype holeInfo) anfs'++ -------------------------------------------------------------------------------- -- | Ensure that the instance type is a subtype of the class type -------------- --------------------------------------------------------------------------------@@ -314,9 +402,18 @@  consCB _ γ (NonRec x e)   = do to  <- varTemplate γ (x, Nothing)+       when (warnOnTermHoles (getConfig γ)) checkLetHole        to' <- consBind False γ (x, e, to) >>= addPostTemplate γ        extender γ (x, makeSingleton γ (simplify e) <$> to')-+  where+    -- See Note [Term holes]+    checkLetHole =+      do+        let isItHole = detectTypedHole e+        case isItHole of+          Just (srcSpan, var) -> do+            linkANFToHole x (var, RealSrcSpan srcSpan Strict.Nothing)+          _ -> return () grepDictionary :: CoreExpr -> Maybe (Var, [Type]) grepDictionary = go []   where@@ -379,9 +476,20 @@ killSubstReft :: F.Reft -> F.Reft killSubstReft = trans ks   where-    ks (F.PKVar k _) = F.PKVar k mempty-    ks p             = p+    ks (F.PKVar k _ _) = F.PKVar k mempty mempty+    ks p                = p +-- | Add a type variable → sort mapping to every PKVar in a SpecType.+-- Used during type application to record how type variables are instantiated,+-- so the solver can apply the correct sort substitution to qualifier solutions.+addTyVarSubToKVars :: F.Symbol -> F.Sort -> SpecType -> SpecType+addTyVarSubToKVars sym sort = fmap (fmap (trans addSub))+  where+    addSub (F.PKVar k tsu su) =+      let tsu' = M.map (F.applyCoercion sym sort) tsu+       in F.PKVar k (M.insert sym sort tsu') su+    addSub e                  = e+ defAnn :: Bool -> t -> Annot t defAnn True  = AnnRDf defAnn False = AnnDef@@ -392,14 +500,58 @@   = do γπ <- γ += ("addSpec1", pname π, pvarRType π)        foldM (+=) γπ [("addSpec2", x, ofRSort t) | (t, x, _) <- pargs π] +-- | Detect a direct typed-hole occurrence in Core and recover the source span+--   that GHC attached to it, if present. The helper deliberately matches the+--   stable @.hole@ naming convention after stripping wrappers introduced by+--   desugaring and normalization.+--+-- See Note [Term holes]+detectTypedHole :: CoreExpr -> Maybe (RealSrcSpan, Var)+detectTypedHole e =+  case stripTicks e of+    Var x | isVarHole x ->+      case lastTick e of+        Just (SourceNote src _) -> Just (src, x)+        _                       -> Nothing+    _ -> Nothing++-- | Remove the outer application and tick wrappers that GHC places around a+--   hole so 'detectTypedHole' can inspect the underlying binder.+stripTicks :: CoreExpr -> CoreExpr+stripTicks (App (Tick _ e) _) = stripTicks e+stripTicks (Tick _ e)         = stripTicks e+stripTicks e          = e++-- | Traverse an expression and keep the innermost tick, which is the source+--   note used to report the hole location.+lastTick :: Expr b -> Maybe CoreTickish+lastTick (Tick t e) =+  case lastTick e of+    Just t' -> Just t'+    Nothing -> Just t+lastTick (App e a) =+  case lastTick a of+    Just ta -> Just ta+    Nothing -> lastTick e+lastTick _ = Nothing++-- | Check whether a Core binder name follows GHC's @.hole@ naming scheme for+--   typed holes.+isVarHole :: Var -> Bool+isVarHole x = isHoleStr (F.symbolString (F.symbol x))+  where+    isHoleStr s =+      case break (== '.') s of+        (_, '.':rest) -> rest == "hole"+        _             -> False+ -------------------------------------------------------------------------------- -- | Bidirectional Constraint Generation: CHECKING ----------------------------- -------------------------------------------------------------------------------- cconsE :: CGEnv -> CoreExpr -> SpecType -> CG () -------------------------------------------------------------------------------- cconsE g e t = do-  -- NOTE: tracing goes here-  -- traceM $ printf "cconsE:\n  expr = %s\n  exprType = %s\n  lqType = %s\n" (showPpr e) (showPpr (exprType e)) (showpp t)+  checkANFHoleInExpr e t   cconsE' g e t  --------------------------------------------------------------------------------@@ -468,9 +620,20 @@        addC (SubC γ (F.notracepp ("Casted Type for " ++ GM.showPpr e ++ "\n init type " ++ showpp t) t') t) ("cconsE Cast: " ++ GM.showPpr e)  cconsE' γ e t-  = do te  <- consE γ e+  = do+       when (warnOnTermHoles (getConfig γ))  maybeAddHole+       te  <- consE γ e        te' <- instantiatePreds γ e te >>= addPost γ        addC (SubC γ te' t) ("cconsE: " ++ "\n t = " ++ showpp t ++ "\n te = " ++ showpp te ++ GM.showPpr e)+  where+    -- See Note [Term holes]+    -- Record the expected type of a direct hole encountered in checking mode.+    maybeAddHole = do+      let isItHole = detectTypedHole e+      case isItHole of+        Just (srcSpan, x) -> do+          addHole (RealSrcSpan srcSpan Strict.Nothing) x t γ+        _ -> return ()  lambdaSingleton :: CGEnv -> F.TCEmb TyCon -> Var -> CoreExpr -> CG (UReft F.Reft) lambdaSingleton γ tce x e@@ -553,7 +716,8 @@ cconsLazyLet _ _ _   = panic Nothing "Constraint.Generate.cconsLazyLet called on invalid inputs" ---------------------------------------------------------------------------------++--------------------------------------------------------- -- | Bidirectional Constraint Generation: SYNTHESIS ---------------------------- -------------------------------------------------------------------------------- consE :: CGEnv -> CoreExpr -> CG SpecType@@ -592,44 +756,23 @@ consE _ (Lit c)   = refreshVV $ uRType $ literalFRefType c -consE γ e'@(App e a@(Type τ))-  = do RAllT α te _ <- checkAll ("Non-all TyApp with expr", e) γ <$> consE γ e-       t            <- if not (nopolyinfer (getConfig γ)) && isPos α && isGenericVar (ty_var_value α) te-                         then freshTyType (typeclass (getConfig γ)) TypeInstE e τ-                         else trueTy (typeclass (getConfig γ)) τ-       addW          $ WfC γ t-       t'           <- refreshVV t-       tt0          <- instantiatePreds γ e' (subsTyVarMeet' (ty_var_value α, t') te)-       let tt        = makeSingleton γ (simplify e') $ subsTyReft γ (ty_var_value α) τ tt0-       return $ case rTVarToBind α of-         Just (x, _) -> maybe (checkUnbound γ e' x tt a) (F.subst1 tt . (x,)) (argType τ)-         Nothing     -> tt+consE γ e'@(App _ _) =+  do+    t <- if warnOnTermHoles (getConfig γ) then synthesizeWithHole else consEApp γ e'+    checkANFHoleInExpr e' t+    return t   where-    isPos α = not (extensionality (getConfig γ)) || rtv_is_pol (ty_var_info α)--consE γ e'@(App e a) | Just aDict <- getExprDict γ a-  = case dhasinfo (dlookup (denv γ) aDict) (getExprFun γ e) of-      Just riSig -> return $ fromRISig riSig-      _          -> do-        ([], πs, te) <- bkUniv <$> consE γ e-        te'          <- instantiatePreds γ e' $ foldr RAllP te πs-        (γ', te''')  <- dropExists γ te'-        te''         <- dropConstraints γ te'''-        updateLocA {- πs -} (exprLoc e) te''-        let RFun x _ tx t _ = checkFun ("Non-fun App with caller ", e') γ te''-        cconsE γ' a tx-        addPost γ'        $ maybe (checkUnbound γ' e' x t a) (F.subst1 t . (x,)) (argExpr γ a)--consE γ e'@(App e a)-  = do ([], πs, te) <- bkUniv <$> consE γ {- GM.tracePpr ("APP-EXPR: " ++ GM.showPpr (exprType e)) -} e-       te1        <- instantiatePreds γ e' $ foldr RAllP te πs-       (γ', te2)  <- dropExists γ te1-       te3        <- dropConstraints γ te2-       updateLocA (exprLoc e) te3-       let RFun x _ tx t _ = checkFun ("Non-fun App with caller ", e') γ te3-       cconsE γ' a tx-       makeSingleton γ' (simplify e') <$> addPost γ' (maybe (checkUnbound γ' e' x t a) (F.subst1 t . (x,)) (argExpr γ $ simplify a))-+    -- See Note [Term holes]+    -- Record the synthesized type of a direct hole encountered in synthesis+    -- mode before the caller consumes it.+    synthesizeWithHole = do+      let isItHole = detectTypedHole e'+      t <- consEApp γ e'+      _ <- case isItHole of+        Just (srcSpan, x) -> do+          addHole (RealSrcSpan srcSpan Strict.Nothing) x t γ+        _ -> return ()+      return t consE γ (Lam α e) | isTyVar α   = do γ' <- updateEnvironment γ α        t' <- consE γ' e@@ -676,6 +819,79 @@ consE _ e@(Type t)   = panic Nothing $ "consE cannot handle type " ++ GM.showPpr (e, t) +-- | Attach the current expression and inferred type to any ANF binders that+--   were previously recognized as naming a term hole. This compensates for ANF+--   normalization, which often moves the informative constraints from the hole+--   occurrence onto the fresh binder that stands for it.+--+-- See Note [Term holes]+checkANFHoleInExpr :: CoreExpr -> SpecType -> CG ()+checkANFHoleInExpr e t = do+  let vars = collectVars e+  forM_ vars $ \var -> do+    isANF <- isANFInHole var+    case isANF of+      Just uniqueVar -> addHoleANF uniqueVar var e t+      _ -> return ()+-- | Collect every variable mentioned in a Core expression so+--   'checkANFHoleInExpr' can look for ANF binders linked to a hole.+collectVars :: CoreExpr -> [Var]+collectVars (Var x) = [x]+collectVars (App e1 e2) = collectVars e1 ++ collectVars e2+collectVars (Lam x e) = x : collectVars e+collectVars (Let (NonRec x e1) e2) = x : collectVars e1 ++ collectVars e2+collectVars (Let (Rec xes) e) =+  let (xs, es) = unzip xes+  in xs ++ concatMap collectVars es ++ collectVars e+collectVars (Case e x _ alts) =+  x : collectVars e ++ concatMap collectAltVars alts+  where collectAltVars (Alt _ xs e') = xs ++ collectVars e'+collectVars _ = []++consEApp :: CGEnv -> CoreExpr -> CG SpecType+consEApp γ e'@(App e a@(Type τ))+  = do+       RAllT α te _ <- checkAll ("Non-all TyApp with expr", e) γ <$> consE γ e+       t            <- if not (nopolyinfer (getConfig γ)) && isPos α && isGenericVar (ty_var_value α) te+                         then freshTyType (typeclass (getConfig γ)) TypeInstE e τ+                         else trueTy (typeclass (getConfig γ)) τ+       addW          $ WfC γ t+       t'           <- refreshVV t+       tt0          <- instantiatePreds γ e' (subsTyVarMeet' (ty_var_value α, t') te)+       let tyVarSym  = F.symbol (ty_var_value α)+           tyVarSort = typeSort (emb γ) (Ghc.expandTypeSynonyms τ)+           tt0'      = addTyVarSubToKVars tyVarSym tyVarSort tt0+           tt        = makeSingleton γ (simplify e') $ subsTyReft γ (ty_var_value α) τ tt0'+       return $ case rTVarToBind α of+         Just (x, _) -> maybe (checkUnbound γ e' x tt a) (F.subst1 tt . (x,)) (argType τ)+         Nothing     -> tt+  where+    isPos α = not (extensionality (getConfig γ)) || rtv_is_pol (ty_var_info α)++consEApp γ e'@(App e a) | Just aDict <- getExprDict γ a+  = case dhasinfo (dlookup (denv γ) aDict) (getExprFun γ e) of+      Just riSig -> return $ fromRISig riSig+      _          -> do+        ([], πs, te) <- bkUniv <$> consE γ e+        te'          <- instantiatePreds γ e' $ foldr RAllP te πs+        (γ', te''')  <- dropExists γ te'+        te''         <- dropConstraints γ te'''+        updateLocA {- πs -} (exprLoc e) te''+        let RFun x _ tx t _ = checkFun ("Non-fun App with caller ", e') γ te''+        cconsE γ' a tx+        addPost γ'        $ maybe (checkUnbound γ' e' x t a) (F.subst1 t . (x,)) (argExpr γ a)++consEApp γ e'@(App e a)+  = do ([], πs, te) <- bkUniv <$> consE γ {- GM.tracePpr ("APP-EXPR: " ++ GM.showPpr (exprType e)) -} e+       te1        <- instantiatePreds γ e' $ foldr RAllP te πs+       (γ', te2)  <- dropExists γ te1+       te3        <- dropConstraints γ te2+       updateLocA (exprLoc e) te3+       let RFun x _ tx t _ = checkFun ("Non-fun App with caller ", e') γ te3+       cconsE γ' a tx+       makeSingleton γ' (simplify e') <$> addPost γ' (maybe (checkUnbound γ' e' x t a) (F.subst1 t . (x,)) (argExpr γ $ simplify a))+consEApp _ _ = panic Nothing "Constraint.Generate.consEApp called on invalid inputs"+ caseKVKind ::[Alt Var] -> KVKind caseKVKind [Alt (DataAlt _) _ (Var _)] = ProjectE caseKVKind cs                          = CaseE (length cs)@@ -817,7 +1033,7 @@   = do t0 <- trueTy (typeclass (getConfig γ)) τ        tx <- varRefType γ x        let t = mergeCastTys t0 tx-       let ce = if typeclass (getConfig γ) && noADT (getConfig γ) then F.expr x+       let ce = if typeclass (getConfig γ) then F.expr x                   else eCoerc (typeSort (emb γ) $ Ghc.expandTypeSynonyms $ varType x)                          (typeSort (emb γ) τ)                          $ F.expr x@@ -915,7 +1131,7 @@   return t -------------------------------------------------------------------------------- -checkUnbound :: (Show a, Show a2, F.Subable a)+checkUnbound :: (Show a, Show a2, F.Subable a, F.Variable a ~ F.Symbol)              => CGEnv -> CoreExpr -> F.Symbol -> a -> a2 -> a checkUnbound γ e x t a   | x `notElem` F.syms t = t@@ -1025,9 +1241,7 @@ altReft γ acs DEFAULT    = mconcat ([notLiteralReft l | LitAlt l <- acs] ++ [notDataConReft d | DataAlt d <- acs])   where     notLiteralReft   = maybe mempty F.notExprReft . snd . literalConst (emb γ)-    notDataConReft d | exactDC (getConfig γ)-                     = F.Reft (F.vv_, F.PNot (F.EApp (F.EVar $ makeDataConChecker d) (F.EVar F.vv_)))-                     | otherwise = mempty+    notDataConReft d = F.Reft (F.vv_, F.PNot (F.EApp (F.EVar $ makeDataConChecker d) (F.EVar F.vv_))) altReft _ _ _            = panic Nothing "Constraint : altReft"  unfoldR :: SpecType -> SpecType -> [Var] -> (SpecType, [SpecType], SpecType)@@ -1097,7 +1311,7 @@ -------------------------------------------------------------------------------- argType :: Type -> Maybe F.Expr argType (LitTy (NumTyLit i)) = mkI i-argType (LitTy (StrTyLit s)) = mkS $ bytesFS s+argType (LitTy (StrTyLit s)) = Just $ mkS $ bytesFS s argType (TyVarTy x)          = Just $ F.EVar $ F.symbol $ varName x argType t   | F.symbol (GM.showPpr t) == anyTypeSymbol@@ -1208,7 +1422,7 @@ -- | RJ: `nomeet` replaces `strengthenS` for `strengthen` in the definition --   of `varRefType`. Why does `tests/neg/strata.hs` fail EVEN if I just replace --   the `otherwise` case? The fq file holds no answers, both are sat.-strengthenTop :: (PPrint r, Reftable r) => RType c tv r -> r -> RType c tv r+strengthenTop :: (PPrint r, Meet r) => RType c tv r -> r -> RType c tv r strengthenTop (RApp c ts rs r) r'   = RApp c ts rs   $ meet r r' strengthenTop (RVar a r) r'         = RVar a         $ meet r r' strengthenTop (RFun b i t1 t2 r) r' = RFun b i t1 t2 $ meet r r'@@ -1217,16 +1431,13 @@ strengthenTop t _                   = t  -- TODO: this is almost identical to RT.strengthen! merge them!-strengthenMeet :: (PPrint r, Reftable r) => RType c tv r -> r -> RType c tv r+strengthenMeet :: (PPrint r, Meet r) => RType c tv r -> r -> RType c tv r strengthenMeet (RApp c ts rs r) r'  = RApp c ts rs (r `meet` r') strengthenMeet (RVar a r) r'        = RVar a       (r `meet` r') strengthenMeet (RFun b i t1 t2 r) r'= RFun b i t1 t2 (r `meet` r') strengthenMeet (RAppTy t1 t2 r) r'  = RAppTy t1 t2 (r `meet` r') strengthenMeet (RAllT a t r) r'     = RAllT a (strengthenMeet t r') (r `meet` r') strengthenMeet t _                  = t---- topMeet :: (PPrint r, Reftable r) => r -> r -> r--- topMeet r r' = r `meet` r'  -------------------------------------------------------------------------------- -- | Cleaner Signatures For Rec-bindings ---------------------------------------

@@ -5,7 +5,6 @@ {-# LANGUAGE TupleSections             #-} {-# LANGUAGE MultiParamTypeClasses     #-} {-# LANGUAGE OverloadedStrings         #-}-{-# OPTIONS_GHC -Wno-x-partial #-}  -- | This module defines the representation of Subtyping and WF Constraints, --   and the code for syntax-directed constraint generation.@@ -64,11 +63,11 @@        f0''     <- refreshArgs' =<< grtyTop info                      -- default TOP reftype      (for exported vars without spec)        let f0'   = if notruetypes $ getConfig sp then [] else f0''        f1       <- refreshArgs'   defaults                            -- default TOP reftype      (for all vars)-       f1'      <- refreshArgs' $ makeExactDc dcsty                   -- data constructors+       f1'      <- refreshArgs' $ strengthenDc dcsty                  -- data constructors        f2       <- refreshArgs' $ assm info                           -- assumed refinements      (for imported vars)        f3'      <- refreshArgs' =<< recSelectorsTy info                      -- assumed refinements      (for record selectors)        f3       <- addPolyInfo' <$> refreshArgs' (vals gsAsmSigs (gsSig sp))                 -- assumed refinedments     (with `assume`)-       f40      <- makeExactDc <$> refreshArgs' (vals gsCtors (gsData sp)) -- constructor refinements  (for measures)+       f40      <- strengthenDc <$> refreshArgs' (vals gsCtors (gsData sp)) -- constructor refinements  (for measures)        f5       <- refreshArgs' $ vals gsInSigs (gsSig sp)                   -- internal refinements     (from Haskell measures)        fi       <- refreshArgs' $ catMaybes $ [(x,) . val <$> getMethodType mt | (x, mt) <- gsMethods $ gsSig $ giSpec info ]        (invs1, f41) <- traverse refreshArgs' $ makeAutoDecrDataCons dcsty  (gsAutosize (gsTerm sp)) dcs@@ -94,7 +93,7 @@     is autoinv   = mkRTyConInv    (gsInvariants (gsData sp) ++ ((Nothing,) <$> autoinv))     addPolyInfo' = if reflection (getConfig info) then map (fmap addPolyInfo) else id -    makeExactDc dcs = if exactDCFlag info then map strengthenDataConType dcs else dcs+    strengthenDc = map strengthenDataConType  addPolyInfo :: SpecType -> SpecType addPolyInfo t = mkUnivs (go <$> as) ps t'@@ -301,6 +300,9 @@   , allowHO       = higherOrderFlag cfg   , ghcI          = info   , unsorted      = F.notracepp "UNSORTED" $ F.makeTemplates $ gsUnsorted $ gsData spc+  , hsHoles      = M.empty+  , hsANFHoles   = M.empty+  , hsHolesExprs = M.empty   }   where     tce        = gsTcEmbeds nspc

@@ -21,6 +21,7 @@ import           Language.Haskell.Liquid.GHC.Misc -- (concatMapM) import           Liquid.GHC.API as Ghc hiding (panic, showPpr) + -------------------------------------------------------------------------------- -- | `addC` adds a subtyping constraint into the global pool. --------------------------------------------------------------------------------@@ -116,6 +117,32 @@ addA _ _ _ !a   = a +-- | Record a term hole together with the type we assigned to it and the local+--   environment needed to render a useful warning later.+addHole :: SrcSpan -> Var -> SpecType -> CGEnv -> CG ()+addHole loc x t γ = do+  exists <- gets (M.member (x, loc) . hsHoles)+  unless exists $+    modify $ \s -> s { hsHoles = M.insert (x, loc) (holeInfo (s, γ)) $ hsHoles s }+  where+    holeInfo = HoleInfo t loc env+    env      = mconcat [renv γ, grtys γ, assms γ, intys γ]++-- | Remember an ANF expression that mentions a hole-linked binder so the final+--   warning can report the surrounding expressions that constrain the hole.+addHoleANF :: (Var, SrcSpan) -> Var -> CoreExpr -> SpecType -> CG ()+addHoleANF uniqueVar anfVar e t =+  modify $ \s -> s { hsHolesExprs = M.insertWith (++) uniqueVar [(anfVar, e, t)] (hsHolesExprs s) }++-- | Associate an ANF binder with the concrete hole occurrence it was created+--   from so later traversals can recover the original hole.+linkANFToHole :: Var -> (Var, SrcSpan) -> CG ()+linkANFToHole anf h = modify $ \s -> s { hsANFHoles = M.insert anf h $ hsANFHoles s }++-- | Resolve an ANF binder back to the hole occurrence that introduced it, if+--   the binder was previously linked by 'linkANFToHole'.+isANFInHole :: Var -> CG (Maybe (Var, SrcSpan))+isANFInHole anf = gets (M.lookup anf . hsANFHoles)  lookupNewType :: Ghc.TyCon -> CG (Maybe SpecType) lookupNewType tc

@@ -1,6 +1,7 @@ {-# LANGUAGE OverloadedStrings     #-} {-# LANGUAGE PartialTypeSignatures #-} {-# LANGUAGE FlexibleContexts      #-}+{-# LANGUAGE TypeOperators         #-}  module Language.Haskell.Liquid.Constraint.Qualifier   ( giQuals@@ -186,7 +187,7 @@     insertsSEnv'              = foldr (\(x, t) γ -> insertSEnv x (rTypeSort tce t) γ)  -refTopQuals :: (PPrint t, Reftable t, SubsTy RTyVar RSort t, Reftable (RTProp RTyCon RTyVar (UReft t)))+refTopQuals :: (PPrint t, IsReft t,  ReftBind t ~ Symbol, ReftVar t ~ Symbol, SubsTy RTyVar RSort t)             => SEnv Sort             -> ElabFlags             -> SourcePos@@ -213,7 +214,7 @@       msg t = panic Nothing $ "Qualifier.refTopQuals: no typebase" ++ showpp t       γ'    = unionSEnv' γ lEnv -mkPQual :: (PPrint r, Reftable r, SubsTy RTyVar RSort r, Reftable (RTProp RTyCon RTyVar r))+mkPQual :: (PPrint r, IsReft r,  ReftBind r ~ Symbol, ReftVar r ~ Symbol, SubsTy RTyVar RSort r)         => SEnv Sort         -> SourcePos         -> TCEmb TyCon

@@ -1,5 +1,6 @@-module Language.Haskell.Liquid.Constraint.RewriteCase -    (getCaseRewrites) +{-# OPTIONS_GHC -Wno-incomplete-record-selectors #-}+module Language.Haskell.Liquid.Constraint.RewriteCase+    (getCaseRewrites)     where  import           Language.Fixpoint.Types@@ -23,7 +24,7 @@         globals = toSet $ reGlobal $ renv     γ     in unloop        $ concatMap (uncurry $ unify ctors globals)-       $ groupUnifiableEqualities +       $ groupUnifiableEqualities        $ getEqualities refinement     where toSet = S.fromList . M.keys @@ -50,8 +51,8 @@         go e1 (EVar s2) | isLocal s2 = [(s2, e1)]         -- TODO: Tecnically we could also unify under lambdas but you have to be         -- carefull about alpha equivalence idk if the effort is worth it.-        go e1 e2 -            -- Performing the unification under constructor is safe because +        go e1 e2+            -- Performing the unification under constructor is safe because             -- C a₁ ... aₙ = C b₁ ... bₙ ⟺ ∀ n . a₁ = bₙ             | (EVar name1 , args1) <- splitEApp e2             , (EVar name2 , args2) <- splitEApp e1@@ -62,7 +63,7 @@         go _ _ = []          isCtor  name = name `S.member` ctors-        isLocal name = not (name `S.member` globals +        isLocal name = not (name `S.member` globals                            || name `S.member` ctors                            || isPrefixOfSym anfPrefix name) @@ -101,8 +102,8 @@ -- | Drops rewrites that would cause an infinite loop. The procedure is order -- biased as rewrites earlier in the list take precedence. unloop :: [(Symbol, Expr)] -> LocalRewrites-unloop = LocalRewrites . toRewrites . foldl' doInsert empty -    where doInsert ar (s, e) = ar `fromMaybe` insert ar s e +unloop = LocalRewrites . toRewrites . foldl' doInsert empty+    where doInsert ar (s, e) = ar `fromMaybe` insert ar s e  -- | Get the "raw" list of rewrites toRewrites :: AcyclicRewrites -> M.HashMap Symbol Expr@@ -133,6 +134,6 @@               -- 1. If the rewrite is closing a loop               -- 2. If the rewrite by itself is a cycle               = Just $ insertUnsafe ar s e-              | otherwise +              | otherwise               = Nothing     where insertUnsafe (AR m) s' e' = AR $ M.insert s' e' m

@@ -1,6 +1,7 @@ {-# LANGUAGE OverloadedStrings     #-} {-# LANGUAGE PartialTypeSignatures #-} {-# LANGUAGE FlexibleContexts      #-}+{-# LANGUAGE TypeOperators         #-}  {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} @@ -127,7 +128,7 @@      isHO  <- gets allowHO      return $ bsplitW' γ t temp isHO -bsplitW' :: (PPrint r, Reftable r, SubsTy RTyVar RSort r, Reftable (RTProp RTyCon RTyVar r))+bsplitW' :: (PPrint r, IsReft r, ReftBind r ~ F.Symbol, ReftVar r ~ F.Symbol, SubsTy RTyVar RSort r)          => CGEnv -> RRType r -> F.Templates -> Bool -> [F.WfC Cinfo] bsplitW' γ t temp isHO   | isHO || F.isNonTrivial r'@@ -275,7 +276,7 @@     r2  = F.RR F.boolSort $ F.Reft (vv, F.EVar vv)     vv  = "vvRec"     ci  = Ci src err (cgVar γ)-    err = Just $ ErrAssType src o (text $ show o ++ "type error") g (rHole rr)+    err = Just $ ErrAssType src o (text $ show o ++ "type error") Nothing g (rHole rr)     rr  = toReft r     tag = getTag γ     src = getLocation γ

@@ -1,5 +1,4 @@ {-# LANGUAGE TupleSections #-}-{-# OPTIONS_GHC -Wno-x-partial #-} -- | This module defines code for generating termination constraints.  module Language.Haskell.Liquid.Constraint.Termination (

@@ -59,7 +59,7 @@   , 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.etaElim        = extensionality cfg   , FC.extensionality = extensionality    cfg   , FC.interpreter    = interpreter    cfg   , FC.rwTermination  = rwTerminationCheck cfg@@ -81,7 +81,9 @@     ls               = fEnv     cgi     consts           = cgConsts cgi     ks               = kuts     cgi-    adts             = cgADTs   cgi+    cfg              = getConfig info+    makeDecls        = adtFlag cfg+    adts             = if makeDecls then cgADTs   cgi else mempty     qs               = giQuals info (fEnv cgi)     bi               = (\x -> Ci x Nothing Nothing) <$> bindSpans cgi     aHO              = allowHO cgi@@ -199,8 +201,8 @@  -- [TODO:missing-sorts] data-constructors often have unelaboratable 'define' so either -- 1. Make `elaborate` robust so it doesn't crash and returns maybe or--- 2. Make the `ctor` well-sorted or --- 3. Don't create `define` for the ctor. +-- 2. Make the `ctor` well-sorted or+-- 3. Don't create `define` for the ctor. -- Unfortunately 3 breaks a bunch of tests...  makeSimplify :: (Var, SpecType) -> [F.Rewrite]

@@ -239,6 +239,9 @@   , ghcI          :: !TargetInfo   , dataConTys    :: ![(Var, SpecType)]                  -- ^ Refined Types of Data Constructors   , unsorted      :: !F.Templates                        -- ^ Potentially unsorted expressions+  , hsHoles       :: !(M.HashMap (Var, SrcSpan) (HoleInfo (CGInfo, CGEnv) SpecType)) -- Information about holes in terms+  , hsANFHoles    :: !(M.HashMap Var  (Var, SrcSpan))+  , hsHolesExprs  :: !(M.HashMap (Var, SrcSpan)  [(Var, CoreExpr, SpecType)])   }  @@ -329,14 +332,18 @@ goodInvs _ (RInv []  t _)   = Just t goodInvs ts (RInv ts' t _)-  | and (zipWith unifiable ts' (toRSort <$> ts))+  | and (zipWith invMatchesTarget ts' (toRSort <$> ts))   = Just t   | otherwise   = Nothing  -unifiable :: RSort -> RSort -> Bool-unifiable t1 t2 = isJust $ tcUnifyTy (toType False t1) (toType False t2)+-- | Check that the target type arg is an instance of the invariant's type arg.+-- Uses one-directional matching (tcMatchTy) so that a type variable in the+-- target does NOT unify with a structured invariant arg. This prevents e.g.+-- an invariant for [Diff [a]] from being applied to a plain [a] binder.+invMatchesTarget :: RSort -> RSort -> Bool+invMatchesTarget inv tgt = isJust $ tcMatchTy (toType False inv) (toType False tgt)  addRInv :: RTyConInv -> (Var, SpecType) -> (Var, SpecType) addRInv m (x, t)

@@ -13,7 +13,6 @@ {-# OPTIONS_GHC -Wno-orphans #-} {-# OPTIONS_GHC -Wwarn=deprecations #-} {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}-{-# OPTIONS_GHC -Wno-x-partial #-}  module Language.Haskell.Liquid.GHC.Interface ( 

@@ -14,7 +14,6 @@  {-# OPTIONS_GHC -Wno-incomplete-patterns #-} -- TODO(#1918): Only needed for GHC <9.0.1. {-# OPTIONS_GHC -Wno-orphans #-}-{-# OPTIONS_GHC -Wno-x-partial #-}  -- | This module contains a wrappers and utility functions for -- accessing GHC module information. It should NEVER depend on@@ -46,7 +45,7 @@ import           Control.Arrow                              (second) import           Control.Monad                              ((>=>), foldM, when) import qualified Text.PrettyPrint.HughesPJ                  as PJ-import           Language.Fixpoint.Types                    hiding (L, panic, Loc (..), SrcSpan, Constant, SESearch (..))+import           Language.Fixpoint.Types                    hiding (L, panic, Loc (..), SrcSpan, Constant, SESearchB (..)) import qualified Language.Fixpoint.Types                    as F import           Language.Fixpoint.Misc                     (safeHead, safeLast, errorstar) -- , safeLast, safeInit) import           Language.Haskell.Liquid.Misc               (keyDiff)@@ -359,14 +358,6 @@ realTcArity :: TyCon -> Arity realTcArity = tyConArity -{--  tracePpr ("realTcArity of " ++ showPpr c-     ++ "\n tyConKind = " ++ showPpr (tyConKind c)-     ++ "\n kindArity = " ++ show (kindArity (tyConKind c))-     ++ "\n kindArity' = " ++ show (kindArity' (tyConKind c)) -- this works for TypeAlias-     ) $ kindArity' (tyConKind c)--}- kindTCArity :: TyCon -> Arity kindTCArity = go . tyConKind   where@@ -416,8 +407,6 @@ tyConTyVarsDef c   | noTyVars c = []   | otherwise  = Ghc.tyConTyVars c-  --where-  --  none         = tracepp ("tyConTyVarsDef: " ++ show c) (noTyVars c)  noTyVars :: TyCon -> Bool noTyVars c =  Ghc.isPrimTyCon c || Ghc.isPromotedDataCon c@@ -522,11 +511,6 @@  dropModuleNames  :: Symbol -> Symbol dropModuleNames = dropModuleNamesCorrect-{- -dropModuleNames = mungeNames lastName sepModNames "dropModuleNames: "- where-   lastName msg = symbol . safeLast msg--}  dropModuleNamesCorrect  :: Symbol -> Symbol dropModuleNamesCorrect = F.symbol . go . F.symbolText@@ -547,11 +531,6 @@                 Nothing -> T.intercalate "." (reverse acc)     getModule' = T.takeWhile (/= '.') -{- -takeModuleNamesOld  = mungeNames initName sepModNames "takeModuleNames: "-  where-    initName msg = symbol . T.intercalate "." . safeInit msg--} dropModuleUnique :: Symbol -> Symbol dropModuleUnique = mungeNames headName sepUnique   "dropModuleUnique: "   where@@ -751,7 +730,7 @@     msg     =  "isGoodCaseBind v = " ++ show v  isPredType :: Type -> Bool-isPredType = anyF [ isClassPred, isNomEqPred, isEqPred ]+isPredType = anyF [ isClassPred, isEqClassPred, isEqPred ]  anyF :: [a -> Bool] -> a -> Bool anyF ps x = or [ p x | p <- ps ]@@ -784,21 +763,6 @@  -- partially stolen from GHC'sa exprType --- elaborateHsExprInst---   :: GhcMonad m => LHsExpr GhcPs -> m (Messages, Maybe CoreExpr)--- elaborateHsExprInst expr = elaborateHsExpr TM_Inst expr----- elaborateHsExpr---   :: GhcMonad m => TcRnExprMode -> LHsExpr GhcPs -> m (Messages, Maybe CoreExpr)--- elaborateHsExpr mode expr =---   withSession $ \hsc_env -> liftIO $ hscElabHsExpr hsc_env mode expr---- hscElabHsExpr :: HscEnv -> TcRnExprMode -> LHsExpr GhcPs -> IO (Messages, Maybe CoreExpr)--- hscElabHsExpr hsc_env0 mode expr = runInteractiveHsc hsc_env0 $ do---   hsc_env <- Ghc.getHscEnv---   liftIO $ elabRnExpr hsc_env mode expr- elabRnExpr :: LHsExpr GhcPs -> TcRn CoreExpr elabRnExpr rdr_expr = do     (rn_expr, _fvs) <- rnLExpr rdr_expr@@ -815,7 +779,7 @@     let { fresh_it = itName uniq (getLocA rdr_expr) }     ((_qtvs, _dicts, evbs, _), residual)          <- captureConstraints $-            simplifyInfer tclvl NoRestrictions+            simplifyInfer NotTopLevel tclvl NoRestrictions                           []    {- No sig vars -}                           [(fresh_it, res_ty)]                           lie@@ -896,30 +860,10 @@ -- | Run a computation in GHC's typechecking monad with wired in values locally bound in the typechecking environment. withWiredIn :: TcM a -> TcM a withWiredIn m = discardConstraints $ do-  -- undef <- lookupUndef   wiredIns <- mkWiredIns-  -- snd <$> tcValBinds Ghc.NotTopLevel (binds undef wiredIns) (sigs wiredIns) m-  (_, _, a) <- tcValBinds Ghc.NotTopLevel [] (sigs wiredIns) m-  return a+  snd <$> tcValBinds Ghc.NotTopLevel [] (sigs wiredIns) m   where-  -- lookupUndef = do-  --   lookupOrig gHC_ERR (Ghc.mkVarOcc "undefined")-  --   -- tcLookupGlobal undefName--  -- binds :: Name -> [TcWiredIn] -> [(Ghc.RecFlag, LHsBinds GhcRn)]-  -- binds undef wiredIns = map (\w -> -  --     let ext = Ghc.unitNameSet undef in -- $ varName $ tyThingId undef in-  --     let co_fn = idHsWrapper in-  --     let matches = -  --           let ctxt = LambdaExpr in-  --           let grhss = GRHSs Ghc.noExtField [Ghc.L locSpan (GRHS Ghc.noExtField [] (Ghc.L locSpan (HsVar Ghc.noExtField (Ghc.L locSpan undef))))] (Ghc.L locSpan emptyLocalBinds) in-  --           MG Ghc.noExtField (Ghc.L locSpan [Ghc.L locSpan (Match Ghc.noExtField ctxt [] grhss)]) Ghc.Generated -  --     in-  --     let b = FunBind ext (Ghc.L locSpan $ tcWiredInName w) matches co_fn [] in-  --     (Ghc.NonRecursive, unitBag (Ghc.L locSpan b))-  --   ) wiredIns-   sigs wiredIns = concatMap (\w ->       let inf = maybeToList $ do             (fPrec, fDir) <- tcWiredInFixity w@@ -951,11 +895,11 @@   nameToTy = Ghc.L locSpanAnn . HsTyVar Ghc.noAnn Ghc.NotPromoted    boolTy' :: LHsType GhcRn-  boolTy' = nameToTy $ toLoc boolTyConName+  boolTy' = nameToTy $ toLoc . Ghc.noUserRdr $ boolTyConName     -- boolName <- lookupOrig (Module (stringToUnitId "Data.Bool") (mkModuleName "Data.Bool")) (Ghc.mkVarOcc "Bool")     -- return $ Ghc.L locSpan $ HsTyVar Ghc.noExtField Ghc.NotPromoted $ Ghc.L locSpan boolName-  intTy' = nameToTy $ toLoc intTyConName-  listTy lt = toLoc $ HsAppTy Ghc.noExtField (nameToTy $ toLoc listTyConName) lt+  intTy' = nameToTy $ toLoc . Ghc.noUserRdr $ intTyConName+  listTy lt = toLoc $ HsAppTy Ghc.noExtField (nameToTy $ toLoc . Ghc.noUserRdr $ listTyConName) lt    -- infixr 1 ==> :: Bool -> Bool -> Bool   impl = do@@ -973,7 +917,7 @@   eq = do     n <- toName "=="     aName <- toLoc <$> toName "a"-    let aTy = nameToTy aName+    let aTy = nameToTy . fmap Ghc.noUserRdr $ aName     let ty = toLoc $ HsForAllTy Ghc.noExtField              (mkHsForAllInvisTele Ghc.noAnn                [ toLoc $@@ -992,7 +936,7 @@   len = do     n <- toName "len"     aName <- toLoc <$> toName "a"-    let aTy = nameToTy aName+    let aTy = nameToTy . fmap Ghc.noUserRdr $ aName     let ty = toLoc $ HsForAllTy Ghc.noExtField                (mkHsForAllInvisTele Ghc.noAnn                  [ toLoc $

@@ -22,8 +22,8 @@ -------------------------------------------------------------------------------  -- If the type constructor T is in the input list and its data constructors Di, Dj--- use T in non strictly positive positions, --- then (T,(Di, Dj)) will appear in the result list.  +-- use T in non strictly positive positions,+-- then (T,(Di, Dj)) will appear in the result list.  getNonPositivesTyCon :: [TyCon] -> [(TyCon, [DataCon])] getNonPositivesTyCon tcs = Mb.mapMaybe go (M.toList $ makeOccurrences tcs)@@ -33,20 +33,20 @@                       xs -> Just (tc, fst <$> xs)  --- OccurrenceMap maps type constructors to their TyConOccurrence. +-- OccurrenceMap maps type constructors to their TyConOccurrence. -- for each of their data constructor. For example, for the below data definition--- data T a = P (T a) | N (T a -> Int) | Both (T a -> T a) | None +-- data T a = P (T a) | N (T a -> Int) | Both (T a -> T a) | None -- the entry below should get generated---  OccurrenceMap +--  OccurrenceMap -- = T |-> [(P, [ --          (P,    TyConOcc [T] []) --          (N,    TyConOcc [Int] [T]) --          (Both, TyConOcc [T] [T]) --          (None, TyConOcc [] [])---         ])] --- For positivity check, ultimately we only care about self occurences, --- but we keep track of all the TyCons for the mutually inductive data types. --- We separate the occurences per data constructor only to provide better error messages. +--         ])]+-- For positivity check, ultimately we only care about self occurences,+-- but we keep track of all the TyCons for the mutually inductive data types.+-- We separate the occurences per data constructor only to provide better error messages. type OccurrenceMap = M.HashMap TyCon [(DataCon, TyConOccurrence)]  data TyConOccurrence@@ -81,14 +81,14 @@     mergeApp m (TyConOcc pos neg) =         let TyConOcc pospos posneg = mconcat (findOccurrence m <$> pos)             TyConOcc negpos negneg = mconcat (findOccurrence m <$> neg)-        -- Keep positive, flip negative +        -- Keep positive, flip negative         in TyConOcc (L.nub (pos <> pospos <> negneg)) (L.nub (neg <> negpos <> posneg))       tycontypes tc = concatMap dctypes $ tyConDataCons tc     dctypes    dc = irrelevantMult <$> dataConOrigArgTys dc -    -- Construct the map for all TyCons that appear in the definitions +    -- Construct the map for all TyCons that appear in the definitions     tycons' = L.nub (concatMap tcs (concatMap tycontypes tycons) ++ tycons)      tcs (TyConApp tc' ts) = tc': concatMap tcs ts

@@ -65,6 +65,7 @@ import qualified Language.Haskell.Liquid.Measure         as Ms import           Language.Haskell.Liquid.Parse import           Language.Haskell.Liquid.Transforms.ANF+import           Language.Haskell.Liquid.Transforms.QuestionMark import           Language.Haskell.Liquid.Types.Errors import           Language.Haskell.Liquid.Types.PrettyPrint import           Language.Haskell.Liquid.Types.Specs@@ -525,17 +526,17 @@     debugLog $ "mg_tcs => " ++ O.showSDocUnsafe (O.ppr $ mg_tcs modGuts0)      hscEnv <- getTopEnv+    tcg <- getGblEnv     let preNormalizedCore = preNormalizeCore moduleCfg modGuts0         modGuts = modGuts0 { mg_binds = preNormalizedCore }         file = LH.modSummaryHsFile lhModuleSummary-    targetSrc  <- liftIO $ makeTargetSrc moduleCfg file modGuts hscEnv+    targetSrc  <- liftIO $ makeTargetSrc moduleCfg file modGuts hscEnv (tcg_rdr_env tcg)     logger <- getLogger      -- See https://github.com/ucsd-progsys/liquidhaskell/issues/1711     -- Due to the fact the internals can throw exceptions from pure code at any point, we need to     -- call 'evaluate' to force any exception and catch it, if we can. -    tcg <- getGblEnv     let localVars = Resolve.makeLocalVars preNormalizedCore         eBareSpec = resolveLHNames           moduleCfg@@ -591,12 +592,14 @@               -> FilePath               -> ModGuts               -> HscEnv+              -> GlobalRdrEnv               -> IO TargetSrc-makeTargetSrc cfg file modGuts hscEnv = do+makeTargetSrc cfg file modGuts hscEnv rdrEnv = do   when (dumpPreNormalizedCore cfg) $ do     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+  coreBindsANF <- anormalize cfg hscEnv modGuts+  let coreBinds = eliminateQuestionMark rdrEnv coreBindsANF   when (dumpNormalizedCore cfg) $ do     putStrLn "\n*************** normalized CoreBinds *****************\n"     putStrLn $ unlines $ L.intersperse "" $ map (GHC.showPpr (GHC.hsc_dflags hscEnv)) coreBinds

@@ -43,16 +43,19 @@ getLiquidLibBytes :: GHC.Module                         -> GHC.ExternalPackageState                         -> GHC.HomePackageTable-                        -> Maybe LiquidLibBytes-getLiquidLibBytes thisModule eps hpt =-    asum [extractFromHpt, getLiquidLibBytesFromEPS thisModule eps]+                        -> IO (Maybe LiquidLibBytes)+getLiquidLibBytes thisModule eps hpt = do+    fromHpt <- extractFromHpt+    pure $ asum [fromHpt, getLiquidLibBytesFromEPS thisModule eps]   where-    extractFromHpt :: Maybe LiquidLibBytes+    extractFromHpt :: IO (Maybe LiquidLibBytes)     extractFromHpt = do-      modInfo <- GHC.lookupHpt hpt (GHC.moduleName thisModule)-      guard (thisModule == (GHC.mi_module . GHC.hm_iface $ modInfo))-      xs <- mapM (GHC.fromSerialized LiquidLibBytes . GHC.ifAnnotatedValue) (GHC.mi_anns . GHC.hm_iface $ modInfo)-      listToMaybe xs+      mb_modInfo <- GHC.lookupHpt hpt (GHC.moduleName thisModule)+      pure $ do+          modInfo <- mb_modInfo+          guard (thisModule == (GHC.mi_module . GHC.hm_iface $ modInfo))+          xs <- mapM (GHC.fromSerialized LiquidLibBytes . GHC.ifAnnotatedValue) (GHC.mi_anns . GHC.hm_iface $ modInfo)+          listToMaybe xs  newtype LiquidLibBytes = LiquidLibBytes { unLiquidLibBytes :: [Word8] } @@ -71,7 +74,7 @@   -> GHC.NameCache   -> IO (Maybe LiquidLib) deserialiseLiquidLib thisModule eps hpt nameCache = do-    let mlibbs = getLiquidLibBytes thisModule eps hpt+    mlibbs <- getLiquidLibBytes thisModule eps hpt     case mlibbs of       Just (LiquidLibBytes ws) -> do         let bs = B.pack ws

@@ -2,6 +2,23 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE RankNTypes   #-} +{-+Note [Module Visibility and Lookup in GHC]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+GHC distinguishes between two module visibility namespaces:++- **Regular packages** (`-package`): modules are found by `findImportedModule`,+  which searches `findExposedPackageModule`.+- **Plugin packages** (`-plugin-package`): modules are found by+  `findPluginModule`, which searches `findExposedPluginPackageModule`.++Whenever a module is looked up, we start with `findImportedModule` to check+regular packages, and if that fails, we fall back to `findPluginModule` to check+plugin packages. This allows us to support both visibility namespaces without+requiring users to mind how they specify dependencies.++-}+ module Language.Haskell.Liquid.GHC.Plugin.SpecFinder     ( findRelevantSpecs     , SpecFinderResult(..)@@ -63,8 +80,16 @@                                    | otherwise = do       let assumptionsModName = assumptionsModuleName m       -- loadInterface might mutate the EPS if the module is-      -- not already loaded-      res <- liftIO $ findImportedModule hscEnv assumptionsModName NoPkgQual+      -- not already loaded.+      --+      -- Try findImportedModule first (for -package), then fall back to+      -- findPluginModule (for -plugin-package).+      -- See Note [Module Visibility and Lookup in GHC] for details.+      res <- liftIO $ do+        r <- findImportedModule hscEnv assumptionsModName NoPkgQual+        case r of+          Found{} -> pure r+          _       -> findPluginModule hscEnv assumptionsModName       case res of         Found _ assumptionsMod -> do           _ <- initIfaceTcRn $ loadInterface "liquidhaskell assumptions" assumptionsMod ImportBySystem@@ -112,7 +137,13 @@       res <- findImportedModule env mn (renamePkgQual (hsc_unit_env env) mn (Just "liquidhaskell"))       case res of         Found _ mdl -> pure $ Just (toStableModule mdl)-        _           -> pure Nothing+        _ -> do+          -- Fall back to plugin package visibility+          -- See Note [Module Visibility and Lookup in GHC] for details.+          res2 <- findPluginModule env mn+          case res2 of+            Found _ mdl -> pure $ Just (toStableModule mdl)+            _           -> pure Nothing  -- | Static associative map of the 'ModuleName' that needs to be filtered from the final 'TargetDependencies' -- due to some particular configuration options.

@@ -23,8 +23,8 @@ import qualified Data.List as L import           Liquid.GHC.API  as Ghc import qualified Language.Haskell.Liquid.GHC.Misc as GM-import qualified Language.Fixpoint.Types          as F -import qualified Text.PrettyPrint.HughesPJ        as PJ +import qualified Language.Fixpoint.Types          as F+import qualified Text.PrettyPrint.HughesPJ        as PJ -- import           Debug.Trace  --------------------------------------------------------------------------------@@ -70,23 +70,23 @@     , patE     :: !CoreExpr  -- ^ e     } -instance F.PPrint Pattern where +instance F.PPrint Pattern where   pprintTidy  = ppPat -ppPat :: F.Tidy -> Pattern -> PJ.Doc -ppPat k (PatReturn e m d t rv) = -  "PatReturn: " -  PJ.$+$ +ppPat :: F.Tidy -> Pattern -> PJ.Doc+ppPat k (PatReturn e m d t rv) =+  "PatReturn: "+  PJ.$+$   F.pprintKVs k-    [ ("rv" :: PJ.Doc, GM.pprDoc rv) -    , ("e " :: PJ.Doc, GM.pprDoc e) -    , ("m " :: PJ.Doc, GM.pprDoc m) -    , ("$d" :: PJ.Doc, GM.pprDoc d) -    , ("t " :: PJ.Doc, GM.pprDoc t) -    ] -ppPat _ _  = "TODO: PATTERN" -    +    [ ("rv" :: PJ.Doc, GM.pprDoc rv)+    , ("e " :: PJ.Doc, GM.pprDoc e)+    , ("m " :: PJ.Doc, GM.pprDoc m)+    , ("$d" :: PJ.Doc, GM.pprDoc d)+    , ("t " :: PJ.Doc, GM.pprDoc t)+    ]+ppPat _ _  = "TODO: PATTERN" + _mbId :: CoreExpr -> Maybe Var _mbId (Var x)    = Just x _mbId (Tick _ e) = _mbId e@@ -109,14 +109,14 @@   = Just (PatProject xe x t c ys i)  -{- TEMPORARILY DISABLED: TODO-REBARE; in reality it hasn't been working AT ALL -   since at least the GHC 8.2.1 port (?) because the TICKs get in the way -   of recognizing the pattern? Anyways, messes up +{- TEMPORARILY DISABLED: TODO-REBARE; in reality it hasn't been working AT ALL+   since at least the GHC 8.2.1 port (?) because the TICKs get in the way+   of recognizing the pattern? Anyways, messes up -     tests/pattern/pos/Return00.hs  +     tests/pattern/pos/Return00.hs     because we treat _all_ types of the form `m a` as "invariant" in the parameter `a`.-   Looks like the above tests only pass in earlier LH versions because this pattern +   Looks like the above tests only pass in earlier LH versions because this pattern    was NOT getting tickled!  exprArgs _e (Var op, [Type m, d, Type t, e])

@@ -50,7 +50,7 @@ instance Show Span where   show (Var x)   = show x   show (Tick tt) = showPpr tt-  show (Span s)  = show s +  show (Span s)  = show s  -------------------------------------------------------------------------------- srcSpan :: SpanStack -> SrcSpan@@ -67,7 +67,7 @@   where     go (Var x)   = getSrcSpan x     go (Tick tt) = tickSrcSpan tt-    go (Span s)  = s +    go (Span s)  = s  maybeSpan :: Maybe SrcSpan -> SrcSpan -> Maybe SrcSpan maybeSpan d sp

@@ -21,28 +21,28 @@ instance Eq Type where   t1 == t2 = eqType' t1 t2 -eqType' :: Type -> Type -> Bool -eqType' (LitTy l1) (LitTy l2) -  = l1 == l2  +eqType' :: Type -> Type -> Bool+eqType' (LitTy l1) (LitTy l2)+  = l1 == l2 eqType' (CoercionTy _c1) (CoercionTy _c2) = True eqType'(CastTy t1 _c1) (CastTy t2 _c2) = eqType' t1 t2 eqType' (FunTy a1 m1 t11 t12) (FunTy a2 m2 t21 t22)-  = a1 == a2 && m1 == m2 && eqType' t11 t21 && eqType' t12 t22  -eqType' (ForAllTy (Bndr v1 _) t1) (ForAllTy (Bndr v2 _) t2) +  = a1 == a2 && m1 == m2 && eqType' t11 t21 && eqType' t12 t22+eqType' (ForAllTy (Bndr v1 _) t1) (ForAllTy (Bndr v2 _) t2)   = eqType' t1 (substType v2 (TyVarTy v1) t2)-eqType' (TyVarTy v1) (TyVarTy v2) -  = v1 == v2 -eqType' (AppTy t11 t12) (AppTy t21 t22) -  = eqType' t11 t21 && eqType' t12 t22  -eqType' (TyConApp c1 ts1) (TyConApp c2 ts2) -  = c1 == c2 && and (zipWith eqType' ts1 ts2) -eqType' _ _ -  = False +eqType' (TyVarTy v1) (TyVarTy v2)+  = v1 == v2+eqType' (AppTy t11 t12) (AppTy t21 t22)+  = eqType' t11 t21 && eqType' t12 t22+eqType' (TyConApp c1 ts1) (TyConApp c2 ts2)+  = c1 == c2 && and (zipWith eqType' ts1 ts2)+eqType' _ _+  = False -showTy :: Type -> String +showTy :: Type -> String showTy (TyConApp c ts) = "(RApp   " ++ showPpr c ++ " " ++ sep' ", " (showTy <$> ts) ++ ")"-showTy (AppTy t1 t2)   = "(TAppTy " ++ (showTy t1 ++ " " ++ showTy t2) ++ ")" -showTy (TyVarTy v)   = "(RVar " ++ show (symbol v)  ++ ")" +showTy (AppTy t1 t2)   = "(TAppTy " ++ (showTy t1 ++ " " ++ showTy t2) ++ ")"+showTy (TyVarTy v)   = "(RVar " ++ show (symbol v)  ++ ")" showTy (ForAllTy (Bndr v _) t)  = "ForAllTy " ++ show (symbol v) ++ ". (" ++  showTy t ++ ")" showTy (FunTy af _m1 t1 t2) = "FunTy " ++ showPpr af ++ " " ++ showTy t1 ++ ". (" ++  showTy t2 ++ ")" showTy (CastTy _ _)    = "CastTy"@@ -52,7 +52,7 @@ sep' :: String -> [String] -> String sep' _ [x] = x sep' _ []  = []-sep' s (x:xs) = x ++ s ++ sep' s xs +sep' s (x:xs) = x ++ s ++ sep' s xs   @@ -61,28 +61,28 @@ -------------------------------------------------------------------------------  substType :: TyVar -> Type -> Type -> Type-substType x tx (TyConApp c ts) +substType x tx (TyConApp c ts)   = TyConApp c (substType x tx <$> ts)-substType x tx (AppTy t1 t2)   +substType x tx (AppTy t1 t2)   = AppTy (substType x tx t1) (substType x tx t2)-substType x tx (TyVarTy y)   +substType x tx (TyVarTy y)   | symbol x == symbol y-  = tx +  = tx   | otherwise-  = TyVarTy y +  = TyVarTy y substType x tx (FunTy aaf m t1 t2)   = FunTy aaf m (substType x tx t1) (substType x tx t2)-substType x tx f@(ForAllTy b@(Bndr y _) t)  -  | symbol x == symbol y +substType x tx f@(ForAllTy b@(Bndr y _) t)+  | symbol x == symbol y   = f-  | otherwise +  | otherwise   = ForAllTy b (substType x tx t)-substType x tx (CastTy t c)    +substType x tx (CastTy t c)   = let ss = extendSubstInScopeSet (zipTvSubst [x] [tx]) (tyCoVarsOfCo c)      in CastTy (substType x tx t) (substCo ss c)-substType x tx (CoercionTy c)  +substType x tx (CoercionTy c)   = let ss = extendSubstInScopeSet (zipTvSubst [x] [tx]) (tyCoVarsOfCo c)      in CoercionTy $ substCo ss c substType _ _  (LitTy l)-  = LitTy l  +  = LitTy l 

@@ -79,7 +79,7 @@ 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)+import           Data.Maybe (mapMaybe, maybeToList) import qualified Data.Text                               as Text import qualified GHC.Types.Name.Occurrence @@ -259,49 +259,42 @@               -- 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+              NoSuchTypeAlias alts -> lookupGRELHName alts (LHTcName lcl) lname s         LHNUnresolved ns@(LHVarName lcl) s           | isDataCon s ->-              lookupGRELHName [] (LHDataConName lcl) lname s listToMaybe+              lookupGRELHName [] (LHDataConName lcl) lname s+          | not (LH.isQualifiedSym s)+          , Just v <- Resolve.lookupLetBoundVar localVars (atLoc lname s)+          ->+              pure $ LHNResolved (LHRGHC (GHC.getName v)) s           | otherwise ->               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@(LHDataConName _) s -> lookupGRELHName [] ns lname s listToMaybe+        LHNUnresolved ns@(LHDataConName _) s -> lookupGRELHName [] ns lname s         n@LHNResolved { } -> pure n -    lookupGRELHName alts ns lname s localNameLookup =+    lookupGRELHName alts ns lname s =       case maybeDropImported ns $ GHC.lookupGRE globalRdrEnv (mkLookupGRE ns s) of         [e] -> do           let n = GHC.greName e-              n' = fromMaybe n $ localNameLookup [n]-          pure $ LHNResolved (LHRGHC n') s+          pure $ LHNResolved (LHRGHC n) s         es@(_:_) -> do-          let topLevelNames = map GHC.greName es-          case localNameLookup topLevelNames of-            Just n | notElem n topLevelNames ->-              pure $ LHNResolved (LHRGHC n) s-            _ -> do-              addError-                (ErrDupNames-                   (LH.fSrcSpan lname)-                   "variable"-                   (pprint s)-                   (map (PJ.text . GHC.showPprUnsafe) es)-                )-              pure $ val lname-        [] ->-          case localNameLookup [] of-            Just n' ->-              pure $ LHNResolved (LHRGHC n') s-            Nothing -> do-              addError-                (errResolve alts (nameSpaceKind ns) "Cannot resolve name" (s <$ lname))-              pure $ val lname+          addError+            (ErrDupNames+               (LH.fSrcSpan lname)+               (nameSpaceKind ns)+               (pprint s)+               (map (PJ.text . GHC.showPprUnsafe) es)+            )+          pure $ val lname+        [] -> do+          addError+            (errResolve alts (nameSpaceKind ns) "Cannot resolve name" (s <$ lname))+          pure $ val lname      maybeDropImported ns es       | localNameSpace ns = filter GHC.isLocalGRE es@@ -471,7 +464,7 @@ -- 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. +-- is a value. fixExpressionArgsOfTypeAliases   :: InScopeEnv (RTAlias Symbol ())   -> BareSpecParsed@@ -528,7 +521,7 @@ --     {-@ type Prop E = {v:_ | prop v = E} @-} --   the parser will chomp in `Ev (plus n n)` as a `BareType` and so -- | @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

@@ -9,12 +9,12 @@  import           Prelude hiding (error) import           Data.Bifunctor-import qualified Data.HashSet as S +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 Data.List  as L import qualified Language.Haskell.Liquid.UX.DiffCheck as DC import           Language.Haskell.Liquid.Misc import qualified Language.Fixpoint.Misc as F@@ -103,21 +103,21 @@   let info1   = either (const info)    (\z -> info {giSpec = DC.newSpec z}) edc   let cbs''   = either id              DC.newBinds                          edc   let info2   = info1 { giSrc = (giSrc info1) {giCbs = cbs''}}-  let info3   = updTargetInfoTermVars info2 -  let cgi     = {-# SCC "generateConstraints" #-} generateConstraints $! info3 +  let info3   = updTargetInfoTermVars info2+  let cgi     = {-# SCC "generateConstraints" #-} generateConstraints $! info3   when False (dumpCs cgi)   -- whenLoud $ mapM_ putStrLn [ "****************** CGInfo ********************"                             -- , render (pprint cgi)                            ]   out        <- timedAction names $ solveCs cfg tgt cgi info3 names   return      $ mconcat [oldOut, out] -updTargetInfoTermVars    :: TargetInfo -> TargetInfo -updTargetInfoTermVars i  = updInfo i  (ST.terminationVars i) -  where +updTargetInfoTermVars    :: TargetInfo -> TargetInfo+updTargetInfoTermVars i  = updInfo i  (ST.terminationVars i)+  where     updInfo   info vs = info { giSpec = updSpec   (giSpec info) vs }     updSpec   sp   vs = sp   { gsTerm = updSpTerm (gsTerm sp)   vs }-    updSpTerm gsT  vs = gsT  { gsNonStTerm = S.fromList vs         } -      +    updSpTerm gsT  vs = gsT  { gsNonStTerm = S.fromList vs         }+ dumpCs :: CGInfo -> IO () dumpCs cgi = do   putStrLn "***************************** SubCs *******************************"@@ -137,12 +137,12 @@   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 (r,rf)        = splitFails (S.map val failBs) r0   let resErr        = second (applySolution finfo sol . cinfoError) <$> r   -- resModel_        <- fmap (e2u cfg sol) <$> getModels info cfg resErr   let resModel_     = cidE2u cfg <$> resErr   let resModel'     = resModel_  `addErrors` (e2u cfg <$> logErrors cgi)-                                 `addErrors` makeFailErrors (S.toList failBs) rf +                                 `addErrors` makeFailErrors (S.toList failBs) rf                                  `addErrors` makeFailUseErrors (S.toList failBs) (giCbs $ giSrc info)   let lErrors       = applySolution finfo sol <$> logErrors cgi   let resModel      = resModel' `addErrors` (e2u cfg <$> lErrors)@@ -161,6 +161,7 @@   where     attachSubcId es@ErrSubType{}      = es { cid = Just subcId }     attachSubcId es@ErrSubTypeModel{} = es { cid = Just subcId }+    attachSubcId es@ErrAssType{}      = es { cid = Just subcId }     attachSubcId es = es  -- writeCGI tgt cgi = {-# SCC "ConsWrite" #-} writeFile (extFileName Cgi tgt) str@@ -171,20 +172,20 @@ makeFailUseErrors :: [F.Located Var] -> [CoreBind] -> [UserError] makeFailUseErrors fbs cbs = [ mkError x bs | x <- fbs                                           , let bs = clients (val x)-                                          , not (null bs) ]  -  where +                                          , not (null bs) ]+  where     mkError x bs = ErrFailUsed (GM.sourcePosSrcSpan $ loc x) (pprint $ val x) (pprint <$> bs)     clients x    = map fst $ filter (elem x . snd) allClients -    allClients = concatMap go cbs +    allClients = concatMap go cbs      go :: CoreBind -> [(Var,[Var])]-    go (NonRec x e) = [(x, readVars e)] +    go (NonRec x e) = [(x, readVars e)]     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 ]  -  where +makeFailErrors bs cis = [ mkError x | x <- bs, notElem (val x) vs ]+  where     mkError  x = ErrFail (GM.sourcePosSrcSpan $ loc x) (pprint $ val x)     vs         = Mb.mapMaybe ci_var cis @@ -192,9 +193,8 @@ splitFails _ r@(F.Crash _ _) = (r,mempty) splitFails _ r@(F.Safe _)    = (r,mempty) splitFails fs (F.Unsafe s xs)  = (mkRes r, snd <$> rfails)-  where -    (rfails,r) = L.partition (Mb.maybe False (`S.member` fs) . ci_var . snd) xs +  where+    (rfails,r) = L.partition (Mb.maybe False (`S.member` fs) . ci_var . snd) xs     mkRes [] = F.Safe s-    mkRes ys = F.Unsafe s ys +    mkRes ys = F.Unsafe s ys -  

@@ -4,7 +4,7 @@ {-# LANGUAGE OverloadedStrings      #-} {-# LANGUAGE ConstraintKinds        #-} {-# LANGUAGE TupleSections    #-}-{-# OPTIONS_GHC -Wno-x-partial #-}+{-# LANGUAGE TypeOperators          #-}  module Language.Haskell.Liquid.Measure (   -- * Specifications@@ -149,13 +149,13 @@ resultTy :: RType c tv r -> RType c tv r resultTy = ty_res . toRTypeRep -strengthenResult :: Reftable r => RType c tv r -> r -> RType c tv r+strengthenResult :: Meet r => RType c tv r -> r -> RType c tv r strengthenResult t r = fromRTypeRep $ rep {ty_res = ty_res rep `strengthen` r}   where     rep              = toRTypeRep t  -noDummySyms :: (OkRT c tv r) => RType c tv r -> RType c tv r+noDummySyms :: (OkRT c tv r, Subable r, Variable r ~ Symbol, IsReft r) => RType c tv r -> RType c tv r noDummySyms t   | any isDummy (ty_binds rep)   = subst su $ fromRTypeRep $ rep{ty_binds = xs'}@@ -187,7 +187,10 @@       = Just $ mkSubst $ zipWith (\y x -> (fst x, EVar $ fst y)) xts1' xts2'       | otherwise       = panic (Just $ sourcePosSrcSpan lc) ("The types for the wrapper and worker data constructors cannot be merged\n"-          ++ show t1 ++ "\n" ++ show t2 )+          ++ show t1 ++ "\n" ++ show t2 ++ "\n"+          ++ "If there are UNPACK pragmas in effect, consider compiling with\n"+          ++ "-fomit-interface-pragmas to ignore them.\n"+          ++ "See https://github.com/ucsd-progsys/liquidhaskell/issues/2629")  -- should constructors have implicits? probably not defRefType :: Bool -> Type -> Def (RRType Reft) DataCon -> RRType Reft@@ -219,14 +222,14 @@                       ++ zipWith g xs (ofType <$> ts)   | otherwise          = panicFieldNumMismatch sp dc nXs nTs     where-      (pts, ts)        = L.partition (\t -> notracepp ("isPredTy: " ++ showpp t) $ (if allowTC then isEmbeddedDictType else Ghc.isEvVarType ) t) allTs+      (pts, ts)        = L.partition (\t -> notracepp ("isPredTy: " ++ showpp t) $ (if allowTC then isEmbeddedDictType else Ghc.isSimplePredTy ) t) allTs       (_  , xs)        = L.partition (coArg . snd) allXs       nXs              = length xs       nTs              = length ts       g (x, Just t) _  = (x, classRFInfo allowTC, t, mempty)       g (x, _)      t  = (x, classRFInfo allowTC, t, mempty)       coArg Nothing    = False-      coArg (Just t)   = (if allowTC then isEmbeddedDictType else Ghc.isEvVarType ). toType False $ t+      coArg (Just t)   = (if allowTC then isEmbeddedDictType else Ghc.isSimplePredTy ). toType False $ t  panicFieldNumMismatch :: (PPrint a, PPrint a1, PPrint a3)                       => SrcSpan -> a3 -> a1 -> a -> a2

@@ -1,6 +1,5 @@ {-# LANGUAGE TupleSections #-} {-# LANGUAGE DoAndIfThenElse #-}-{-# OPTIONS_GHC -Wno-x-partial #-}  module Language.Haskell.Liquid.Misc where 

@@ -7,6 +7,7 @@ {-# LANGUAGE DeriveDataTypeable        #-} {-# LANGUAGE ScopedTypeVariables       #-} {-# LANGUAGE TemplateHaskellQuotes     #-}+{-# LANGUAGE TypeApplications          #-} {-# OPTIONS_GHC -Wno-orphans           #-}  module Language.Haskell.Liquid.Parse@@ -24,6 +25,7 @@ import           Data.Bifunctor                         (first) import qualified Data.Char                              as Char import qualified Data.Foldable                          as F+import           Data.Hashable                          (Hashable) import           Data.String import           Data.Void import           Prelude                                hiding (error)@@ -38,6 +40,7 @@ import qualified Text.PrettyPrint.HughesPJ              as PJ import           Text.PrettyPrint.HughesPJ.Compat       ((<+>)) import           Language.Fixpoint.Types                hiding (panic, SVar, DDecl, DataDecl, DataCtor (..), Error, R, Predicate)+import qualified Language.Fixpoint.Types                as F import           Language.Haskell.Liquid.GHC.Misc       hiding (getSourcePos) import           Language.Haskell.Liquid.Types.Bounds import           Language.Haskell.Liquid.Types.DataDecl@@ -89,7 +92,7 @@  instance ParseableV LocSymbol where   parseV = locSymbolP-  mkSu = Su . M.fromList . reverse . filter notTrivial+  mkSu = toKVarSubst . M.fromList . reverse . filter notTrivial     where       notTrivial (x, EVar y) = x /= val y       notTrivial _           = True@@ -269,7 +272,7 @@   = angles $ do       PC sb t <- parens btP       p       <- monoPredicateP-      return   $ PC sb (t `strengthenUReft` MkUReft trueReft p)+      return   $ PC sb (t `strengthenUReft` MkUReft F.trueReft p)  holePC :: Parser ParamComp holePC = do@@ -512,7 +515,7 @@                                ((snd <$> xts) ++ [t1]) <$> bareTypeP  trueURef :: UReftV v (ReftV v)-trueURef = MkUReft trueReft (Pr [])+trueURef = MkUReft F.trueReft (Pr [])  constraintEnvP :: Parser [(LocSymbol, BareTypeParsed)] constraintEnvP@@ -630,7 +633,7 @@  dummyP ::  Monad m => m (ReftV LocSymbol -> b) -> m b dummyP fm-  = fm `ap` return trueReft+  = fm `ap` return F.trueReft  symsP :: Monoid r       => Parser [(Symbol, RTypeV v c BTyVar r)]@@ -754,13 +757,13 @@   where     (ss, (v, _))  = (init symsf, last symsf)     symsf         = [(y, s) | ((_, s), y) <- syms']-    su            = mkSubstLocSymbol [(x, EVar $ dummyLoc y) | ((x, _), y) <- syms', x /= v]+    su            = mkSubstLocSymbol val [(x, EVar $ dummyLoc y) | ((x, _), y) <- syms', x /= v]     r             = Reft (v, substExprV val su epr) -mkSubstLocSymbol :: [(Symbol, ExprV LocSymbol)] -> SubstV LocSymbol-mkSubstLocSymbol = Su . M.fromList . reverse . filter notTrivial+mkSubstLocSymbol :: Hashable b => (v -> b) -> [(b, ExprBV b v)] -> KVarSubst b v+mkSubstLocSymbol toB = toKVarSubst . M.fromList . reverse . filter notTrivial   where-    notTrivial (x, EVar y) = x /= val y+    notTrivial (x, EVar y) = x /= toB y     notTrivial _           = True  bRVar :: tv -> PredicateV v -> r -> RTypeV v c tv (UReftV v r)@@ -777,7 +780,16 @@      -> [RTPropV LocSymbol BTyCon BTyVar (UReftV LocSymbol (ReftV LocSymbol))]      -> ReftV LocSymbol      -> BareTypeParsed-bTup [(_,t)] _ r+bTup [(_,t)] rs r+  | not (null rs)+  = case appendRProps t rs of+      Just t' | isTauto (fmap val r) -> t'+              | otherwise            -> t' `strengthenUReft` reftUReft r+      Nothing -> uError $ ErrOther GHC.noSrcSpan $ PJ.vcat+        [ PJ.text "Cannot apply abstract refinement arguments to a non-constructor type."+        , PJ.text "Abstract refinements can only be applied to type constructors, e.g."+        , PJ.text "    (T a b) <p>"+        ]   | isTauto (fmap val r)  = t   | otherwise  = t `strengthenUReft` reftUReft r bTup ts rs r@@ -796,7 +808,15 @@     makeProp i = RProp (reverse $ take i args) ((snd <$> ts)!!i)     rs'        = makeProp <$> [1..(length ts-1)] +-- | Append abstract refinement predicates to the RProp list of an RApp.+-- Returns Nothing if the type is not an RApp (predicates can't be attached).+appendRProps :: RTypeV v c tv r+             -> [RTPropV v c tv r]+             -> Maybe (RTypeV v c tv r)+appendRProps (RApp c ts rs r0) rs' = Just (RApp c ts (rs ++ rs') r0)+appendRProps _                _   = Nothing + -- Temporarily restore this hack benchmarks/esop2013-submission/Array.hs fails -- w/o it -- TODO RApp Int [] [p] true should be syntactically different than RApp Int [] [] p@@ -812,7 +832,7 @@ bAppTy :: Foldable t => BTyVar -> t BareTypeParsed -> ReftV LocSymbol -> BareTypeParsed bAppTy v ts r  = strengthenUReft ts' (reftUReft r)   where-    ts'        = foldl' (\a b -> RAppTy a b (uTop trueReft)) (RVar v (uTop trueReft)) ts+    ts'        = foldl' (\a b -> RAppTy a b (uTop F.trueReft)) (RVar v (uTop F.trueReft)) ts  strengthenUReft   :: BareTypeParsed -> UReftV LocSymbol (ReftV LocSymbol) -> BareTypeParsed@@ -824,14 +844,14 @@     meetReftV :: ReftV LocSymbol -> ReftV LocSymbol -> ReftV LocSymbol     meetReftV (Reft (v, ra)) (Reft (v', ra'))       | v == v'          = Reft (v , pAnd [ra, ra'])-      | v == dummySymbol = Reft (v', pAnd [ra', substExprV val (Su $ M.fromList [(v , EVar (dummyLoc v'))]) ra])-      | otherwise        = Reft (v , pAnd [ra, substExprV val (Su $ M.fromList [(v', EVar (dummyLoc v))]) ra'])+      | v == dummySymbol = Reft (v', pAnd [ra', substExprV val (toKVarSubst $ M.fromList [(v , EVar (dummyLoc v'))]) ra])+      | otherwise        = Reft (v , pAnd [ra, substExprV val (toKVarSubst $ M.fromList [(v', EVar (dummyLoc v))]) ra']) -substExprV :: (v -> Symbol) -> SubstV v -> ExprV v -> ExprV v-substExprV toSym su0 = go+substExprV :: Hashable b => (v -> b) -> KVarSubst b v -> ExprBV b v -> ExprBV b v+substExprV toB su0 = go   where     go (EApp f e) = EApp (go f) (go e)-    go (ELam x e) = ELam x (substExprV toSym (removeSubst su0 (fst x)) e)+    go (ELam x e) = ELam x (substExprV toB (removeSubst su0 (fst x)) e)     go (ECoerc a t e) = ECoerc a t (go e)     go (ENeg e) = ENeg (go e)     go (EBin op e1 e2) = EBin op (go e1) (go e2)@@ -844,25 +864,26 @@     go (PImp p1 p2) = PImp (go p1) (go p2)     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 (PKVar k tsu su') = PKVar k tsu (su' `appendSubst` su0)     go (PAll _ _) = panic Nothing "substExprV: PAll"     go (PExist _ _) = panic Nothing "substExprV: PExist"     go p = p -    appSubst (Su s) x = Mb.fromMaybe (EVar x) (M.lookup (toSym x) s)+    appSubst su x = Mb.fromMaybe (EVar x) (M.lookup (toB x) (fromKVarSubst su)) -    removeSubst (Su su) x = Su $ M.delete x su+    removeSubst su x = toKVarSubst $ M.delete x $ fromKVarSubst su -    appendSubst (Su s1) θ2@(Su s2) = Su $ M.union s1' s2+    appendSubst s1 s2 = toKVarSubst $ M.union s1' s2'       where-        s1' = substExprV toSym θ2 <$> s1+        s1' = substExprV toB s2 <$> fromKVarSubst s1+        s2' = fromKVarSubst s2   reftUReft :: r -> UReftV v r reftUReft r    = MkUReft r (Pr [])  predUReft :: PredicateV v -> UReftV v (ReftV v)-predUReft = MkUReft trueReft+predUReft = MkUReft F.trueReft  dummyTyId :: String dummyTyId = ""@@ -1375,7 +1396,7 @@             <|> parens (located bareTypeP)  -    mkVar v  = dummyLoc $ RVar v (uTop trueReft)+    mkVar v  = dummyLoc $ RVar v (uTop F.trueReft)   riMethodSigP :: Parser (Located LHName, RISig (Located BareTypeParsed))

@@ -7,7 +7,6 @@ {-# LANGUAGE UndecidableInstances   #-}  {-# OPTIONS_GHC -Wno-orphans #-}-{-# OPTIONS_GHC -Wno-x-partial #-}  module Language.Haskell.Liquid.Transforms.CoreToLogic   ( coreToDef@@ -20,7 +19,7 @@   , inlineSpecType   , measureSpecType   , weakenResult-  , normalize+  , normalizeCoreExpr   ) where  import           Data.Bifunctor (first)@@ -63,7 +62,7 @@ import Data.Ratio import GHC.Base ((+#), (-#), (*#)) -logicType :: (Reftable r) => Bool -> Type -> RRType r+logicType :: (IsReft r) => Bool -> Type -> RRType r logicType allowTC τ      = fromRTypeRep $ t { ty_binds = bs, ty_info = is, ty_args = as, ty_refts = rs}   where     t            = toRTypeRep $ ofType τ@@ -87,6 +86,7 @@     f              = dummyLoc (symbol v)     t              = ofType (GM.expandVarType v) :: SpecType     mkA            = EVar . fst+    mkReft :: Expr -> Reft     mkReft         = if isBool res then propReft else exprReft  -- | Refine types of measures: keep going until you find the last data con!@@ -100,6 +100,7 @@ measureSpecType :: Bool -> Var -> SpecType measureSpecType allowTC v = go mkT [] [(1::Int)..] st   where+    mkReft :: Expr -> Reft     mkReft | boolRes   = propReft            | otherwise = exprReft     mkT xs          = MkUReft (mkReft $ mkEApp locSym (EVar <$> reverse xs)) mempty@@ -174,7 +175,7 @@       , lsConfig = cfg       } -coreAltToDef :: (Reftable r) => Located LHName -> Var -> [Var] -> Var -> Type -> [C.CoreAlt]+coreAltToDef :: (IsReft r) => Located LHName -> Var -> [Var] -> Var -> Type -> [C.CoreAlt]              -> LogicM [Def (Located (RRType r)) DataCon] coreAltToDef locSym z zs y t alts   | not (null litAlts) = measureFail locSym "Cannot lift definition with literal alternatives"@@ -211,20 +212,20 @@     mkDef _ _ _ _ _ _ =       return [] -toArgs :: Reftable r => (Located (RRType r) -> b) -> [Var] -> [(Symbol, b)]+toArgs :: IsReft r => (Located (RRType r) -> b) -> [Var] -> [(Symbol, b)] toArgs f args = [(symbol x, f $ varRType x) | x <- args] -defArgs :: Monoid r => Located LHName -> [Type] -> [(Symbol, Maybe (Located (RRType r)))]+defArgs :: IsReft r => Located LHName -> [Type] -> [(Symbol, Maybe (Located (RRType r)))] defArgs x     = zipWith (\i t -> (defArg i, defRTyp t)) [0..]   where     defArg    = tempSymbol (lhNameToResolvedSymbol $ val x)     defRTyp   = Just . F.atLoc x . ofType -coreToDef :: Reftable r => Located LHName -> Var -> C.CoreExpr+coreToDef :: IsReft r => Located LHName -> Var -> C.CoreExpr           -> LogicM [Def (Located (RRType r)) DataCon]-coreToDef locSym _ s              = do +coreToDef locSym _ s              = do     allowTC <- reader $ typeclass . lsConfig-    go [] $ inlinePreds $ simplify allowTC s+    go [] $ inlinePreds $ simplifyCoreExpr allowTC s   where     go args   (C.Lam  x e)        = go (x:args) e     go args   (C.Tick _ e)        = go args e@@ -233,7 +234,7 @@       | Just t <- isMeasureArg z  = coreAltToDef locSym z zs z t [Alt C.DEFAULT [] e]     go _ _                        = measureFail locSym "Does not have a case-of at the top-level" -    inlinePreds   = inline (eqType boolTy . GM.expandVarType)+    inlinePreds   = inlineCoreExpr (eqType boolTy . GM.expandVarType)  measureFail       :: Located LHName -> String -> a measureFail x msg = panic sp e@@ -253,16 +254,16 @@     tcMb                = tyConAppTyCon_maybe t  -varRType :: (Reftable r) => Var -> Located (RRType r)+varRType :: (IsReft r) => Var -> Located (RRType r) varRType = GM.varLocInfo ofType  coreToFun :: LocSymbol -> Var -> C.CoreExpr ->  LogicM ([Var], Either Expr Expr)-coreToFun _ _v s = do +coreToFun _ _v s = do   allowTC <- reader $ typeclass . lsConfig-  go [] $ normalize allowTC s+  go [] $ normalizeCoreExpr allowTC s   where     go acc (C.Lam x e)  | isTyVar x = go acc e-    go acc (C.Lam x e)  = do +    go acc (C.Lam x e)  = do       allowTC <- reader $ typeclass . lsConfig       let isE = if allowTC then GM.isEmbeddedDictVar else isErasable       if isE x then go acc e else go (x:acc) e@@ -276,7 +277,7 @@ coreToLogic :: C.CoreExpr -> LogicM Expr coreToLogic cb = do   allowTC <- reader $ typeclass . lsConfig-  coreToLg $ normalize allowTC cb+  coreToLg $ normalizeCoreExpr allowTC cb   coreToLg :: C.CoreExpr -> LogicM Expr@@ -341,6 +342,9 @@ checkBoolAlts alts   = throw ("checkBoolAlts failed on " ++ GM.showPpr alts) +-- @casesToLg v e alts@ transforms a case expression with scrutinee @e@ and+-- alternatives @alts@ into a logic expression. The variable @v@ is the binder+-- for the scrutinee in the case alternatives. casesToLg :: Var -> Expr -> [C.CoreAlt] -> LogicM Expr casesToLg v e alts = mapM (altToLg e) normAlts >>= go   where@@ -369,11 +373,6 @@  altToLg :: Expr -> C.CoreAlt -> LogicM (C.AltCon, Expr) altToLg de (Alt a@(C.DataAlt d) xs e) = do-  ctorReflected <- reader (exactDCFlag . lsConfig)-  if not ctorReflected && not (primDataCon d) then do-    throw $  "Cannot lift to logic the constructor `" ++ show d-          ++ "` consider enabling either --exactdc or --reflection"-  else do     p  <- coreToLg e     dm <- reader lsDCMap     allowTC <- reader (typeclass . lsConfig)@@ -549,7 +548,7 @@ -- mkLit (LitInteger n _)  = mkI n mkLit (LitFloat  n)    = mkR n mkLit (LitDouble n)    = mkR n-mkLit (LitString    s)    = mkS s+mkLit (LitString    s) = Just (mkS s) mkLit (LitChar   c)    = mkC c mkLit _                 = Nothing -- ELit sym sort @@ -559,8 +558,8 @@ mkR :: Rational -> Maybe Expr mkR                    = Just . ECon . F.R . fromRational -mkS :: ByteString -> Maybe Expr-mkS                    = Just . ESym . SL  . decodeUtf8With lenientDecode+mkS :: ByteString -> Expr+mkS = ESym . SL  . decodeUtf8With lenientDecode  mkC :: Char -> Maybe Expr mkC                    = Just . ECon . (`F.L` F.charSort)  . repr@@ -598,79 +597,127 @@ isDead :: Id -> Bool isDead     = isDeadOcc . occInfo . Ghc.idInfo -class Simplify a where-  simplify :: Bool -> a -> a-  inline   :: (Id -> Bool) -> a -> a--  normalize :: Bool -> a -> a-  normalize allowTC = inline_preds . inline_anf . simplify allowTC-   where-    inline_preds = inline (eqType boolTy . GM.expandVarType)-    inline_anf   = inline isANF--instance Simplify C.CoreExpr where-  simplify _ e@(C.Var _)-    = e-  simplify _ e@(C.Lit _)-    = e-  simplify allowTC (C.App e (C.Type _))-    = simplify allowTC e-  simplify allowTC (C.App e (C.Var dict))  | (if allowTC then GM.isEmbeddedDictVar else isErasable) dict-    = simplify allowTC e-  simplify allowTC (C.App (C.Lam x e) _)   | isDead x-    = simplify allowTC e-  simplify allowTC (C.App e1 e2)-    = C.App (simplify allowTC e1) (simplify allowTC e2)-  simplify allowTC (C.Lam x e) | isTyVar x-    = simplify allowTC e-  simplify allowTC (C.Lam x e) | (if allowTC then GM.isEmbeddedDictVar else isErasable) x-    = simplify allowTC e-  simplify allowTC (C.Lam x e)-    = C.Lam x (simplify allowTC e)-  simplify allowTC (C.Let (C.NonRec x _) e) | (if allowTC then GM.isEmbeddedDictVar else isErasable) x-    = simplify allowTC e-  simplify allowTC (C.Let (C.Rec xes) e)    | all ((if allowTC then GM.isEmbeddedDictVar else isErasable) . fst) xes-    = simplify allowTC e-  simplify allowTC (C.Let xes e)-    = C.Let (simplify allowTC xes) (simplify allowTC e)-  simplify allowTC (C.Case e x _t alts@[Alt _ _ ee,_,_]) | isBangInteger alts-  -- XXX(matt): seems to be for debugging?-    = -- Misc.traceShow ("To simplify allowTC case") $-       sub (M.singleton x (simplify allowTC e)) (simplify allowTC ee)-  simplify allowTC (C.Case e x t alts)-    = C.Case (simplify allowTC e) x t (filter (not . isPatErrorAlt) (simplify allowTC <$> alts))-  simplify allowTC (C.Cast e c)-    = C.Cast (simplify allowTC e) c-  simplify allowTC (C.Tick _ e)-    = simplify allowTC e-  simplify _ (C.Coercion c)-    = C.Coercion c-  simplify _ (C.Type t)-    = C.Type t--  inline p (C.Let (C.NonRec x ex) e) | p x-                               = sub (M.singleton x (inline p ex)) (inline p e)-  inline p (C.Let xes e)       = C.Let (inline p xes) (inline p e)-  inline p (C.App e1 e2)       = C.App (inline p e1) (inline p e2)-  inline p (C.Lam x e)         = C.Lam x (inline p e)-  inline p (C.Case e x t alts) = C.Case (inline p e) x t (inline p <$> alts)-  inline p (C.Cast e c)        = C.Cast (inline p e) c-  inline p (C.Tick t e)        = C.Tick t (inline p e)-  inline _ (C.Var x)           = C.Var x-  inline _ (C.Lit l)           = C.Lit l-  inline _ (C.Coercion c)      = C.Coercion c-  inline _ (C.Type t)          = C.Type t-+-- | 'normalizeCoreExpr allowTC e' simplifies the Core expression 'e' by:+--   1. inlining predicates (i.e. applications of measures that return Bool)+--   2. inlining ANF variables (i.e. variables that are introduced by the ANF transformation)+--   3. simplifying the expression by removing dead binders and applications of+--      type arguments and dictionaries.+--+-- The 'allowTC' flag controls whether type class dictionaries are considered erasable+-- and will be removed from the expression.+--+normalizeCoreExpr :: Bool -> CoreExpr -> CoreExpr+normalizeCoreExpr allowTC = inline_preds . inline_anf . simplifyCoreExpr allowTC+  where+    inline_preds = inlineCoreExpr (eqType boolTy . GM.expandVarType)+    inline_anf   = inlineCoreExpr isANF -instance Simplify C.CoreBind where-  simplify allowTC (C.NonRec x e) = C.NonRec x (simplify allowTC e)-  simplify allowTC (C.Rec xes)    = C.Rec (fmap (simplify allowTC) <$> xes )+-- | 'simplifyCoreExpr allowTC e' simplifies the Core expression 'e' by removing+-- applications of type arguments and dictionaries, and by removing dead+-- binders.+--+-- The 'allowTC' flag controls whether type class dictionaries are considered+-- erasable.+--+-- If 'allowTC' is 'True', then type class dictionaries are considered erasable+-- and will be removed from the expression. If 'allowTC' is 'False', then type+-- class dictionaries are not considered erasable and will not be removed.+--+-- This function is used in 'normalizeCoreExpr' to simplify the Core expression+-- before inlining predicates and ANF variables.+--+-- The 'simplifyCoreExpr' function recursively traverses the Core expression and+-- applies the following simplifications:+--   1. It removes applications of type arguments (i.e. 'C.App e1 (C.Type _)').+--   2. It removes applications of variables that are considered erasable+--      (i.e. 'C.App e1 (C.Var v)' where 'v' is erasable).+--   3. It removes applications of lambda expressions where the binder is dead+--      (i.e. 'C.App (C.Lam x e) _' where 'x' is dead).+--   4. It removes lambda expressions where the binder is a type variable+--      (i.e. 'C.Lam x e' where 'x' is a type variable).+--   5. It removes lambda expressions where the binder is considered erasable+--      (i.e. 'C.Lam x e' where 'x' is erasable).+--   6. It removes non-recursive let bindings where the binder is considered+--      erasable (i.e. 'C.Let (C.NonRec x eb) e' where 'x' is erasable).+--   7. It removes recursive let bindings where all binders are considered+--      erasable (i.e. 'C.Let (C.Rec xes) e' where all 'x' in 'xes' are+--      erasable).+--   8. It simplifies case expressions that match on a boolean by checking if+--      the alternatives correspond to 'True' and 'False' and then substituting+--      the scrutinee with the appropriate alternative.+--   9. It simplifies case expressions by removing alternatives that correspond+--      to pattern match errors (i.e. 'isPatErrorAlt').+--   10. It recursively simplifies applications, casts, ticks, coercions, and+--       type expressions.+--+simplifyCoreExpr :: Bool -> CoreExpr -> CoreExpr+simplifyCoreExpr allowTC = go+  where+    isDictOrErasable = if allowTC then GM.isEmbeddedDictVar else isErasable -  inline p (C.NonRec x e) = C.NonRec x (inline p e)-  inline p (C.Rec xes)    = C.Rec (fmap (inline p) <$> xes)+    go :: CoreExpr -> CoreExpr+    go e@(C.Var _)+      = e+    go e@(C.Lit _)+      = e+    go (C.App e1 (C.Type _))+      = go e1+    go (C.App e1 (C.Var v))+      | isDictOrErasable v+      = go e1+    go (C.App (C.Lam x e) _)+      | isDead x+      = go e+    go (C.App e1 e2)+      = C.App (go e1) (go e2)+    go (C.Lam x e)+      | isTyVar x+      = go e+    go (C.Lam x e)+      | isDictOrErasable x+      = go e+    go (C.Lam x e)+      = C.Lam x (go e)+    go (C.Let (C.NonRec x eb) e)+      | isDictOrErasable x+      = go e+      | otherwise+      = C.Let (C.NonRec x (go eb)) (go e)+    go (C.Let (C.Rec xes) e)+      | all (isDictOrErasable . fst) xes+      = go e+      | otherwise+      = C.Let (C.Rec (map (fmap go) xes)) (go e)+    go (C.Case e x _t alts@[Alt _ _ ee,_,_])+      | isBangInteger alts+      = sub (M.singleton x (go e)) (go ee)+    go (C.Case e x t alts)+      = C.Case (go e) x t $+         filter+           (not . isPatErrorAlt)+           [ Alt c xs (go ealt) | Alt c xs ealt <- alts ]+    go (C.Cast e c)+      = C.Cast (go e) c+    go (C.Tick _ e)+      = go e+    go (C.Coercion c)+      = C.Coercion c+    go (C.Type t)+      = C.Type t -instance Simplify C.CoreAlt where-  simplify allowTC (Alt c xs e) = Alt c xs (simplify allowTC e)-    -- where xs   = F.tracepp _msg xs0-    --      _msg = "isCoVars? " ++ F.showpp [(x, isCoVar x, varType x) | x <- xs0]-  inline p (Alt c xs e) = Alt c xs (inline p e)+inlineCoreExpr :: (Id -> Bool) -> CoreExpr -> CoreExpr+inlineCoreExpr p (C.Let (C.NonRec x ex) e)+  | p x = sub (M.singleton x (inlineCoreExpr p ex)) (inlineCoreExpr p e)+  | otherwise = C.Let (C.NonRec x (inlineCoreExpr p ex)) (inlineCoreExpr p e)+inlineCoreExpr p (C.Let (C.Rec xes) e) = C.Let (C.Rec (map (fmap (inlineCoreExpr p)) xes)) (inlineCoreExpr p e)+inlineCoreExpr p (C.App e1 e2)       = C.App (inlineCoreExpr p e1) (inlineCoreExpr p e2)+inlineCoreExpr p (C.Lam x e)         = C.Lam x (inlineCoreExpr p e)+inlineCoreExpr p (C.Case e x t alts) =+  C.Case (inlineCoreExpr p e) x t+    [ Alt c xs (inlineCoreExpr p ealt) | Alt c xs ealt <- alts ]+inlineCoreExpr p (C.Cast e c)        = C.Cast (inlineCoreExpr p e) c+inlineCoreExpr p (C.Tick t e)        = C.Tick t (inlineCoreExpr p e)+inlineCoreExpr _ (C.Var x)           = C.Var x+inlineCoreExpr _ (C.Lit l)           = C.Lit l+inlineCoreExpr _ (C.Coercion c)      = C.Coercion c+inlineCoreExpr _ (C.Type t)          = C.Type t

@@ -0,0 +1,70 @@+{-# LANGUAGE PatternGuards #-}+-- | Eliminate applications of the '?' operator from Core after ANF.+--+-- After ANF, @e ? s@ becomes:+--+-- @+-- let a1 = e+-- let a2 = s+-- ... (?) \@A \@B a1 a2+-- @+--+-- This pass replaces @(?) \@A \@B a1 a2@ with just @a1@, so that no KVars+-- are introduced in the signature of @?@. The binding @a2 = s@ remains in+-- scope, so the lemma's postcondition still enters the environment during+-- constraint generation.++module Language.Haskell.Liquid.Transforms.QuestionMark (eliminateQuestionMark) where++import Liquid.GHC.API as Ghc++-- | Look up the '?' operator in the 'GlobalRdrEnv'. If found, eliminate all+-- its applications from the Core program. If not found (module doesn't import+-- ProofCombinators), return the bindings unchanged.+eliminateQuestionMark :: GlobalRdrEnv -> [CoreBind] -> [CoreBind]+eliminateQuestionMark rdrEnv cbs =+  case lookupQuestionMark rdrEnv of+    Nothing   -> cbs+    Just name -> map (goBind name) cbs++-- | Find the 'Name' of '?' from @Language.Haskell.Liquid.ProofCombinators@+-- in the renamer environment.+lookupQuestionMark :: GlobalRdrEnv -> Maybe Name+lookupQuestionMark rdrEnv =+  case lookupGRE rdrEnv (LookupRdrName rdrName SameNameSpace) of+    [gre] -> Just (greName gre)+    _     -> Nothing+  where+    rdrName = mkRdrQual (mkModuleName "Language.Haskell.Liquid.ProofCombinators")+                        (mkVarOcc "?")++goBind :: Name -> CoreBind -> CoreBind+goBind n (NonRec x e) = NonRec x (goExpr n e)+goBind n (Rec xes)    = Rec [(x, goExpr n e) | (x, e) <- xes]++goExpr :: Name -> CoreExpr -> CoreExpr+goExpr n e+  | Just firstArg <- isQuestionMarkApp n e = goExpr n firstArg+goExpr n (Lam x e)         = Lam x (goExpr n e)+goExpr n (Let b e)          = Let (goBind n b) (goExpr n e)+goExpr n (Case s x t alts) = Case (goExpr n s) x t [goAlt n a | a <- alts]+goExpr n (Cast e co)        = Cast (goExpr n e) co+goExpr n (Tick t e)         = Tick t (goExpr n e)+goExpr n (App f a)          = App (goExpr n f) (goExpr n a)+goExpr _ e                  = e -- Var, Lit, Type, Coercion++goAlt :: Name -> CoreAlt -> CoreAlt+goAlt n (Alt con bs e) = Alt con bs (goExpr n e)++-- | Detect a fully-saturated application of '?': four arguments total+-- (two types + two values), possibly wrapped in ticks.+-- Returns @Just arg1@ (the first value argument).+isQuestionMarkApp :: Name -> CoreExpr -> Maybe CoreExpr+isQuestionMarkApp name expr =+  case collectArgsTicks (const True) expr of+    (Var v, args, _ticks)+      | varName v == name+      , [_tA, _tB, a, _b] <- args+      -> Just a+    _ -> Nothing+

@@ -105,7 +105,7 @@   class IsFree a where-        isFree :: Symbol -> a -> Bool+        isFree :: Variable a -> a -> Bool  instance (Subable x) => (IsFree x) where         isFree x p = x `elem` syms p

@@ -42,7 +42,7 @@ rewriteBinds :: Config -> [CoreBind] -> [CoreBind] rewriteBinds cfg   | simplifyCore cfg-  = fmap (normalizeTuples +  = fmap (normalizeTuples        . rewriteBindWith undollar        . tidyTuples        . rewriteBindWith inlineLoopBreakerTx

@@ -17,7 +17,6 @@      RBEnv, RRBEnv, RRBEnvV, -    makeBound,     emapBoundM,     mapBoundTy @@ -26,8 +25,6 @@ import Prelude hiding (error) import Text.PrettyPrint.HughesPJ import GHC.Generics-import Data.List (partition)-import Data.Maybe import Data.Hashable import Data.Bifunctor as Bifunctor import Data.Data@@ -36,10 +33,8 @@ import qualified Data.HashMap.Strict as M  import qualified Language.Fixpoint.Types as F-import Language.Haskell.Liquid.Types.Errors-import Language.Haskell.Liquid.Types.RefType+import Language.Haskell.Liquid.Types.RefType () import Language.Haskell.Liquid.Types.RType-import Language.Haskell.Liquid.Types.RTypeOp import Language.Haskell.Liquid.Types.Types  @@ -103,90 +98,3 @@ instance Bifunctor Bound where   first  f (Bound s vs ps xs e) = Bound s (f <$> vs) (fmap f <$> ps) (fmap f <$> xs) e   second = fmap--makeBound :: (PPrint r, UReftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r)-          => RRBound RSort -> [RRType r] -> [F.Symbol] -> RRType r -> RRType r-makeBound (Bound _  vs ps xs expr) ts qs-         = RRTy cts mempty OCons-  where-    cts  = (\(x, t) -> (x, foldr subsTyVarMeet t su)) <$> cts'--    cts' = makeBoundType penv rs xs--    penv = zip (val . fst <$> ps) qs-    rs   = bkImp [] expr--    bkImp acc (F.PImp p q) = bkImp (p:acc) q-    bkImp acc p          = p:acc--    su  = [(α, toRSort t, t) | (RVar α _, t) <-  zip vs ts ]--makeBoundType :: (PPrint r, UReftable r)-              => [(F.Symbol, F.Symbol)]-              -> [F.Expr]-              -> [(LocSymbol, RSort)]-              -> [(F.Symbol, RRType r)]-makeBoundType penv (q:qs) xts = go xts-  where-    -- NV TODO: Turn this into a proper error-    go [] = panic Nothing "Bound with empty symbols"--    go [(x, t)]      = [(F.dummySymbol, tp t x), (F.dummySymbol, tq t x)]-    go ((x, t):xtss) = (val x, mkt t x) : go xtss--    mkt t x = ofRSort t `strengthen` ofUReft (MkUReft (F.Reft (val x, F.PTrue))-                                                (Pr $ M.lookupDefault [] (val x) ps))-    tp t x  = ofRSort t `strengthen` ofUReft (MkUReft (F.Reft (val x, F.pAnd rs))-                                                (Pr $ M.lookupDefault [] (val x) ps))-    tq t x  = ofRSort t `strengthen` makeRef penv x q--    (ps, rs) = partitionPs penv qs----- NV TODO: Turn this into a proper error-makeBoundType _ _ _           = panic Nothing "Bound with empty predicates"---partitionPs :: [(F.Symbol, F.Symbol)] -> [F.Expr] -> (M.HashMap F.Symbol [UsedPVar], [F.Expr])-partitionPs penv qs = Bifunctor.first makeAR $ partition (isPApp penv) qs-  where-    makeAR ps       = M.fromListWith (++) $ map (toUsedPVars penv) ps--isPApp :: [(F.Symbol, a)] -> F.Expr -> Bool-isPApp penv (F.EApp (F.EVar p) _)  = isJust $ lookup p penv-isPApp penv (F.EApp e _)         = isPApp penv e-isPApp _    _                  = False--toUsedPVars :: [(F.Symbol, F.Symbol)] -> F.Expr -> (F.Symbol, [PVar ()])-toUsedPVars penv q@(F.EApp _ expr) = (sym, [toUsedPVar penv q])-  where-    -- NV : TODO make this a better error-    sym = case {- unProp -} expr of {F.EVar x -> x; e -> todo Nothing ("Bound fails in " ++ show e) }-toUsedPVars _ _ = impossible Nothing "This cannot happen"--toUsedPVar :: [(F.Symbol, F.Symbol)] -> F.Expr -> PVar ()-toUsedPVar penv ee@(F.EApp _ _)-  = PV q () e (((), F.dummySymbol,) <$> es')-   where-     F.EVar e = {- unProp $ -} last es-     es'    = init es-     Just q = lookup p penv-     (F.EVar p, es) = F.splitEApp ee--toUsedPVar _ _ = impossible Nothing "This cannot happen"---- `makeRef` is used to make the refinement of the last implication,--- thus it can contain both concrete and abstract refinements--makeRef :: (UReftable r) => [(F.Symbol, F.Symbol)] -> LocSymbol -> F.Expr -> r-makeRef penv v (F.PAnd rs) = ofUReft (MkUReft (F.Reft (val v, F.pAnd rrs)) r)-  where-    r                    = Pr  (toUsedPVar penv <$> pps)-    (pps, rrs)           = partition (isPApp penv) rs--makeRef penv v rr-  | isPApp penv rr       = ofUReft (MkUReft (F.Reft(val v, F.PTrue)) r)-  where-    r                    = Pr [toUsedPVar penv rr]--makeRef _    v p         = ofReft (F.Reft (val v, p))

@@ -10,7 +10,6 @@  {-# OPTIONS_GHC -Wno-incomplete-patterns #-} -- TODO(#1918): Only needed for GHC <9.0.1. {-# OPTIONS_GHC -Wno-orphans #-} -- PPrint and aeson instances.-{-# OPTIONS_GHC -Wno-x-partial #-}  -- | This module contains the *types* related creating Errors. --   It depends only on Fixpoint and basic haskell libraries,@@ -249,6 +248,7 @@                , ctx  :: !(M.HashMap Symbol t)                , svar :: !Symbol                , thl  :: !t+               , anf  :: ![(Symbol, CoreExpr, t)]                } -- ^ hole type    | ErrHoleCycle@@ -259,6 +259,7 @@   | ErrAssType { pos  :: !SrcSpan                , obl  :: !Oblig                , msg  :: !Doc+               , cid  :: Maybe SubcId                , ctx  :: !(M.HashMap Symbol t)                , cond :: t                } -- ^ condition failure error@@ -801,10 +802,11 @@ -------------------------------------------------------------------------------- ppError' :: (PPrint a, Show a) => Tidy -> Doc -> TError a -> Doc ---------------------------------------------------------------------------------ppError' td dCtx (ErrAssType _ o _ c p)+ppError' td dCtx (ErrAssType _ o _ cid c p)   = pprintTidy td o         $+$ dCtx         $+$ ppFull td (ppPropInContext td p c)+        $+$ maybe mempty (\i -> text "Constraint id" <+> text (show i)) cid  ppError' td dCtx err@(ErrSubType _ _ _ _ _ tE)   | totalityType td tE@@ -817,10 +819,25 @@   = "Cycle of holes found"         $+$ pprint holes -ppError' _td _dCtx (ErrHole _ msg _ x t)+ppError' td dCtx (ErrHole _ msg c x t a)   = "Hole Found"         $+$ pprint x <+> "::" <+> pprint t+        $+$ dCtx+        $+$ ppContext td c         $+$ msg+        $+$ "Extra Constraints where hole appears as ANF var"+        $+$ (if null a+             then empty+             else nests 2 [ text "with expression types"+                          , vsep (+                              map (+                                \(v, e, t') ->+                                  text "ANF VAR is" <+> pprint v+                                  $+$ text "Expression is ["  <+> ppCoreExpr e <+> text "] and has type:"+                                  $+$ pprint t'+                              ) a+                            )+                          ])  ppError' td dCtx (ErrSubType _ _ cid c tA tE)   = text "Liquid Type Mismatch"@@ -975,11 +992,14 @@         $+$ dCtx         $+$ nest 4 (vcat                         [ "The" <+> text (Misc.intToString i) <+> "argument of" <+> c <+> "is predicate" <+> ppTicks p-                        , "which expects" <+> pprint eN <+> "arguments" <+> "but is given only" <+> pprint aN-                        , " "-                        , "Abstract predicates cannot be partially applied; for a possible fix see:"+                        , "which expects" <+> pprint eN <+> "arguments" <+> "but is given" <+> pprint aN                         , " "-                        , nest 4 "https://github.com/ucsd-progsys/liquidhaskell/issues/594"+                        , if eN > aN+                          then vcat [ "Abstract predicates cannot be partially applied; for a possible fix see:"+                                    , " "+                                    , nest 4 "https://github.com/ucsd-progsys/liquidhaskell/issues/594"+                                    ]+                          else "The provided predicate has too many arguments."                         ])  ppError' _ dCtx e@(ErrMismatch _ x msg τ t cause hsSp)@@ -1160,6 +1180,9 @@ ppList :: (PPrint a) => Doc -> [a] -> Doc ppList d ls   = nest 4 (sepVcat blankLine (d : [ text "*" <+> pprint l | l <- ls ]))++ppCoreExpr :: CoreExpr -> Doc+ppCoreExpr = text . showSDocQualified . ppr  -- | Convert a GHC error into a list of our errors. 

@@ -6,6 +6,7 @@ {-# LANGUAGE TupleSections         #-} {-# LANGUAGE UndecidableInstances  #-} {-# LANGUAGE ConstraintKinds       #-}+{-# LANGUAGE TypeOperators         #-}  module Language.Haskell.Liquid.Types.Fresh   ( Freshable(..)@@ -55,7 +56,7 @@ instance (Freshable m Integer, Monad m, Applicative m) => Freshable m F.Expr where   fresh  = kv <$> fresh     where-      kv = (`F.PKVar` mempty) . F.intKvar+      kv i = F.PKVar (F.intKvar i) mempty mempty  instance (Freshable m Integer, Monad m, Applicative m) => Freshable m [F.Expr] where   fresh = single <$> fresh@@ -72,13 +73,13 @@   true allowTC (MkUReft r _)    = MkUReft <$> true allowTC r    <*> return mempty   refresh allowTC (MkUReft r _) = MkUReft <$> refresh allowTC r <*> return mempty -instance (Freshable m Integer, Freshable m r, Reftable r ) => Freshable m (RRType r) where+instance (Freshable m Integer, Freshable m r, IsReft r, F.Subable r, F.Variable r ~ F.Symbol, ReftBind r ~ F.Symbol, ReftVar r ~ F.Symbol) => Freshable m (RRType r) where   fresh   = panic Nothing "fresh RefType"   refresh = refreshRefType   true    = trueRefType  ------------------------------------------------------------------------------------------------trueRefType :: (Freshable m Integer, Freshable m r, Reftable r) => Bool -> RRType r -> m (RRType r)+trueRefType :: (Freshable m Integer, Freshable m r, IsReft r, F.Subable r, F.Variable r ~ F.Symbol, ReftBind r ~ F.Symbol, ReftVar r ~ F.Symbol) => Bool -> RRType r -> m (RRType r) ----------------------------------------------------------------------------------------------- trueRefType allowTC (RAllT α t r)   = RAllT α <$> true allowTC t <*> true allowTC r@@ -97,7 +98,7 @@   = RApp c <$> mapM (true allowTC) ts <*> mapM (trueRef allowTC) rs <*> true allowTC r  trueRefType allowTC (RAppTy t t' _)-  = RAppTy <$> true allowTC t <*> true allowTC t' <*> return mempty+  = RAppTy <$> true allowTC t <*> true allowTC t' <*> return trueReft  trueRefType allowTC (RVar a r)   = RVar a <$> true allowTC r@@ -120,14 +121,14 @@ trueRefType _ t@(RHole _)   = return t -trueRef :: (Reftable r, Freshable f r, Freshable f Integer)+trueRef :: (Freshable f Integer, Freshable f r, IsReft r, F.Subable r, F.Variable r ~ F.Symbol, ReftBind r ~ F.Symbol, ReftVar r ~ F.Symbol)         => Bool -> Ref τ (RType RTyCon RTyVar r) -> f (Ref τ (RRType r)) trueRef _ (RProp _ (RHole _)) = panic Nothing "trueRef: unexpected RProp _ (RHole _))" trueRef allowTC (RProp s t) = RProp s <$> trueRefType allowTC t   ------------------------------------------------------------------------------------------------refreshRefType :: (Freshable m Integer, Freshable m r, Reftable r) => Bool -> RRType r -> m (RRType r)+refreshRefType :: (Freshable m Integer, Freshable m r, IsReft r, F.Subable r, F.Variable r ~ F.Symbol, ReftBind r ~ F.Symbol, ReftVar r ~ F.Symbol) => Bool -> RRType r -> m (RRType r) ----------------------------------------------------------------------------------------------- refreshRefType allowTC (RAllT α t r)   = RAllT α <$> refresh allowTC t <*> true allowTC r@@ -136,8 +137,8 @@   = RAllP π <$> refresh allowTC t  refreshRefType allowTC (RFun sym i t t' _)-  | sym == F.dummySymbol = (\b t1 t2 -> RFun b i t1 t2 mempty) <$> fresh <*> refresh allowTC t <*> refresh allowTC t'-  | otherwise          = (\t1 t2 -> RFun sym i t1 t2 mempty)   <$> refresh allowTC t <*> refresh allowTC t'+  | sym == F.dummySymbol = (\b t1 t2 -> RFun b i t1 t2 trueReft) <$> fresh <*> refresh allowTC t <*> refresh allowTC t'+  | otherwise          = (\t1 t2 -> RFun sym i t1 t2 trueReft)   <$> refresh allowTC t <*> refresh allowTC t'  refreshRefType _ (RApp rc ts _ _) | isClass rc   = return $ rRCls rc ts@@ -163,7 +164,7 @@ refreshRefType _ t   = return t -refreshRef :: (Reftable r, Freshable f r, Freshable f Integer)+refreshRef :: (Freshable f Integer, Freshable f r, IsReft r, F.Subable r, F.Variable r ~ F.Symbol, ReftBind r ~ F.Symbol, ReftVar r ~ F.Symbol)            => Bool -> Ref τ (RType RTyCon RTyVar r) -> f (Ref τ (RRType r)) refreshRef _ (RProp _ (RHole _)) = panic Nothing "refreshRef: unexpected (RProp _ (RHole _))" refreshRef allowTC (RProp s t) = RProp <$> mapM freshSym s <*> refreshRefType allowTC t@@ -260,14 +261,14 @@       return $ RProp [(x, t) | (x, (_, t)) <- zip xs s] $ F.subst su t'  ---------------------------------------------------------------------------------refreshHoles :: (F.Symbolic t, Reftable r, TyConable c, Freshable f r)+refreshHoles :: (F.Symbolic t, IsReft r, ReftBind r ~ F.Symbol, ReftVar r ~ F.Symbol, TyConable c, Freshable f r)              => Bool -> [(t, RType c tv r)] -> f ([F.Symbol], [(t, RType c tv r)]) refreshHoles allowTC vts = first catMaybes . unzip . map extract <$> mapM (refreshHoles' allowTC) vts   where   --   extract :: (t, t1, t2) -> (t, (t1, t2))     extract (a,b,c) = (a,(b,c)) -refreshHoles' :: (F.Symbolic a, Reftable r, TyConable c, Freshable m r)+refreshHoles' :: (F.Symbolic a, IsReft r, ReftBind r ~ F.Symbol, ReftVar r ~ F.Symbol, TyConable c, Freshable m r)               => Bool -> (a, RType c tv r) -> m (Maybe F.Symbol, a, RType c tv r) refreshHoles' allowTC (x,t)   | noHoles t = return (Nothing, x, t)@@ -276,5 +277,5 @@     tx r | hasHole r = refresh allowTC r          | otherwise = return r -noHoles :: (Reftable r, TyConable c) => RType c tv r -> Bool+noHoles :: (IsReft r, ReftBind r ~ F.Symbol, ReftVar r ~ F.Symbol, TyConable c) => RType c tv r -> Bool noHoles = and . foldReft False (\_ r bs -> not (hasHole r) : bs) []

@@ -16,7 +16,7 @@  -- * 'Hashable' -instance (Eq (Generically a), Generic a, GHashable Zero (Rep a)) => Hashable (Generically a) where+instance (Generic a, Eq (Rep a ()), GHashable Zero (Rep a)) => Hashable (Generically a) where   hashWithSalt s (Generically a) = genericHashWithSalt s a  -- * 'Binary'

@@ -1,6 +1,6 @@ {-# LANGUAGE OverloadedStrings #-} -module Language.Haskell.Liquid.Types.Literals +module Language.Haskell.Liquid.Types.Literals   ( literalFRefType   , literalFReft   , literalConst

@@ -18,8 +18,8 @@     -- _err              = ErrMismatch lqSp v (text "meetVarTypes") hsD lqD hsSp     -- _hsD              = F.pprint hsT     -- _lqD              = F.pprint lqT-{- -  +{-+ _meetError :: F.TCEmb TyCon -> Error -> SpecType -> SpecType -> SpecType _meetError _emb _e t t'   -- // | meetable emb t t'

@@ -1,10 +1,15 @@+{-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings          #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TemplateHaskellQuotes #-}+{-# LANGUAGE TypeOperators #-} module Language.Haskell.Liquid.Types.Names-  ( lenLocSymbol+  ( CompatibleBinder(..)+  , lenLocSymbol   , anyTypeSymbol   , propSymbol   , getPropIndex@@ -70,6 +75,18 @@   , v == v'   = Just idx getPropIndex _ = Nothing++-- | Highly temporary class as a compatability layer to express that a binder,+-- especially type variables @tv@, are in the same namespace as another binder.+class CompatibleBinder b b' where+  coerceBinder :: b' -> b+  default coerceBinder :: b ~ b' => b' -> b+  coerceBinder = id++instance CompatibleBinder Symbol Symbol+instance CompatibleBinder (Located Symbol) (Located Symbol)+instance CompatibleBinder Symbol (Located Symbol) where+  coerceBinder (Loc _ _ s) = s  -- RJ: Please add docs lenLocSymbol :: Located Symbol

@@ -2,6 +2,7 @@ {-# LANGUAGE FlexibleInstances    #-} {-# LANGUAGE OverloadedStrings    #-} {-# LANGUAGE TupleSections        #-}+{-# LANGUAGE TypeOperators        #-} {-# LANGUAGE UndecidableInstances #-}  {-# OPTIONS_GHC -Wno-orphans #-}@@ -198,10 +199,10 @@     subst    = F.mkSubst [(x, F.EVar y) | (x, y) <- zip as1 bs]     rt'      = F.subst subst rt     makeVars = filter (`elem` fvs) $ zipWith (\v a -> RTVar v (rTVarInfo a :: RTVInfo RSort)) vs (fst $ splitForAllTyCoVars $ dataConRepType dc)-    makeVars' = map (, mempty) makeVars +    makeVars' = map (, mempty) makeVars     fvs = freeTyVars $ mkArrow [] ps ts' rt' -dataConTy :: Monoid r+dataConTy :: IsReft r           => M.HashMap RTyVar (RType RTyCon RTyVar r)           -> Type -> RType RTyCon RTyVar r dataConTy m (TyVarTy v)@@ -209,9 +210,9 @@ dataConTy m (FunTy _ _ t1 t2)   = rFun F.dummySymbol (dataConTy m t1) (dataConTy m t2) dataConTy m (ForAllTy (Bndr α _) t) -- α :: TyVar-  = RAllT (makeRTVar (RTV α)) (dataConTy m t) mempty+  = RAllT (makeRTVar (RTV α)) (dataConTy m t) trueReft dataConTy m (TyConApp c ts)-  = rApp c (dataConTy m <$> ts) [] mempty+  = rApp c (dataConTy m <$> ts) [] trueReft dataConTy _ _   = panic Nothing "ofTypePAppTy" @@ -243,17 +244,17 @@ --   then @pvarRType π@ returns an @RType@ with an @RTycon@ called --   @predRTyCon@ `RApp predRTyCon [T1, T2, T3]` ------------------------------------------------------------------------pvarRType :: (PPrint r, Reftable r) => PVar RSort -> RRType r+pvarRType :: (PPrint r, IsReft r) => PVar RSort -> RRType r ----------------------------------------------------------------------- pvarRType (PV _ k {- (PVProp τ) -} _ args) = rpredType k (fst3 <$> args) -- (ty:tys)   -- where   --   ty  = uRTypeGen τ   --   tys = uRTypeGen . fst3 <$> args -rpredType :: Reftable r+rpredType :: IsReft r           => RType RTyCon tv a           -> [RType RTyCon tv a] -> RType RTyCon tv r-rpredType t ts = RApp predRTyCon  (uRTypeGen <$> t : ts) [] mempty+rpredType t ts = RApp predRTyCon  (uRTypeGen <$> t : ts) [] trueReft  predRTyCon   :: RTyCon predRTyCon   = symbolRTyCon predName@@ -361,16 +362,15 @@ -- substRCon :: String -> (RPVar, SpecType) -> SpecType -> SpecType  substRCon-  :: (PPrint t, PPrint t2, Eq tv, Reftable r, Hashable tv, PPrint tv, PPrint r,-      SubsTy tv (RType RTyCon tv ()) r,-      SubsTy tv (RType RTyCon tv ()) (RType RTyCon tv ()),-      SubsTy tv (RType RTyCon tv ()) RTyCon,-      SubsTy tv (RType RTyCon tv ()) tv,-      Reftable (RType RTyCon tv r),-      SubsTy tv (RType RTyCon tv ()) (RTVar tv (RType RTyCon tv ())),+  :: (PPrint t, PPrint t2, Eq tv, IsReft r, Hashable tv, PPrint tv, PPrint r,+      F.Subable r, F.Variable r ~ F.Symbol, ReftBind r ~ F.Symbol, ReftVar r ~ F.Symbol,+      SubsTy tv (RType RTyCon tv NoReft) r,+      SubsTy tv (RType RTyCon tv NoReft) (RType RTyCon tv NoReft),+      SubsTy tv (RType RTyCon tv NoReft) RTyCon,+      SubsTy tv (RType RTyCon tv NoReft) tv,+      SubsTy tv (RType RTyCon tv NoReft) (RTVar tv (RType RTyCon tv NoReft)),       FreeVar RTyCon tv,-      Reftable (RTProp RTyCon tv r),-      Reftable (RTProp RTyCon tv ()))+      Meet (RType RTyCon tv r))   => [Char]   -> (t, Ref RSort (RType RTyCon tv r))   -> RType RTyCon tv r@@ -423,7 +423,7 @@     (epvs, pvs')               = L.partition (uPVar pv ==) pvs  -- TODO: rewrite using foldReft-freeArgsPs :: PVar (RType t t1 ()) -> RType t t1 (UReft t2) -> [F.Symbol]+freeArgsPs :: PVar (RType t t1 NoReft) -> RType t t1 (UReft t2) -> [F.Symbol] freeArgsPs p (RVar _ r)   = freeArgsPsRef p r freeArgsPs p (RFun _ _ t1 t2 r)@@ -454,19 +454,19 @@    ps' = f <$> filter (uPVar p ==) ps    f q = q {pargs = pargs q ++ drop (length (pargs q)) (pargs $ uPVar p)} -meetListWithPSubs :: (Foldable t, PPrint t1, Reftable b)+meetListWithPSubs :: (Foldable t, PPrint t1, F.Subable b, F.Variable b ~ F.Symbol, Meet b)                   => t (PVar t1) -> [(F.Symbol, RSort)] -> b -> b -> b meetListWithPSubs πs ss r1 r2    = L.foldl' (meetListWithPSub ss r1) r2 πs -meetListWithPSubsRef :: (Foldable t, Reftable (RType t1 t2 t3))+meetListWithPSubsRef :: (Foldable t, Meet (RType c tv r), TyConable c, IsReft r, F.Subable r, F.Variable r ~ F.Symbol, ReftBind r ~ F.Symbol)                      => t (PVar t4)                      -> [(F.Symbol, b)]-                     -> Ref τ (RType t1 t2 t3)-                     -> Ref τ (RType t1 t2 t3)-                     -> Ref τ (RType t1 t2 t3)+                     -> Ref τ (RType c tv r)+                     -> Ref τ (RType c tv r)+                     -> Ref τ (RType c tv r) meetListWithPSubsRef πs ss r1 r2 = L.foldl' (meetListWithPSubRef ss r1) r2 πs -meetListWithPSub ::  (Reftable r, PPrint t) => [(F.Symbol, RSort)]-> r -> r -> PVar t -> r+meetListWithPSub ::  (PPrint t, F.Subable r, F.Variable r ~ F.Symbol, Meet r) => [(F.Symbol, RSort)]-> r -> r -> PVar t -> r meetListWithPSub ss r1 r2 π   | all (\(_, x, F.EVar y) -> x == y) (pargs π)   = r2 `meet` r1@@ -477,12 +477,12 @@   where     su  = F.mkSubst [(x, y) | (x, (_, _, y)) <- zip (fst <$> ss) (pargs π)] -meetListWithPSubRef :: (Reftable (RType t t1 t2))+meetListWithPSubRef :: (Meet (RType c tv r), TyConable c, IsReft r, F.Subable r, F.Variable r ~ F.Symbol, ReftBind r ~ F.Symbol)                     => [(F.Symbol, b)]-                    -> Ref τ (RType t t1 t2)-                    -> Ref τ (RType t t1 t2)+                    -> Ref τ (RType c tv r)+                    -> Ref τ (RType c tv r)                     -> PVar t3-                    -> Ref τ (RType t t1 t2)+                    -> Ref τ (RType c tv r) meetListWithPSubRef _ (RProp _ (RHole _)) _ _ -- TODO: Is this correct?   = panic Nothing "PredType.meetListWithPSubRef called with invalid input" meetListWithPSubRef _ _ (RProp _ (RHole _)) _

@@ -19,6 +19,7 @@      -- * Printers   , rtypeDoc+  , ppTy    -- * Printing Lists (TODO: move to fixpoint)   , pprManyOrdered@@ -179,7 +180,7 @@ -------------------------------------------------------------------------------- -- | Pretty Printing RefType --------------------------------------------------- ---------------------------------------------------------------------------------instance (OkRT c tv r) => PPrint (RType c tv r) where+instance (OkRTBV b v c tv r) => PPrint (RTypeBV b v c tv r) where   -- RJ: THIS IS THE CRUCIAL LINE, the following prints short types.   pprintTidy _ = rtypeDoc F.Lossy   -- pprintTidy _ = ppRType topPrec@@ -205,7 +206,7 @@ pprints k c = sep . punctuate c . map (pprintTidy k)  ---------------------------------------------------------------------------------rtypeDoc :: (OkRT c tv r) => F.Tidy -> RType c tv r -> Doc+rtypeDoc :: (OkRTBV b v c tv r) => F.Tidy -> RTypeBV b v c tv r -> Doc -------------------------------------------------------------------------------- rtypeDoc k      = pprRtype (ppE k) topPrec   where@@ -219,27 +220,27 @@ type Prec = PprPrec  ---------------------------------------------------------------------------------pprRtype :: (OkRT c tv r) => PPEnv -> Prec -> RType c tv r -> Doc+pprRtype :: (OkRTBV b v c tv r) => PPEnv -> Prec -> RTypeBV b v c tv r -> Doc -------------------------------------------------------------------------------- pprRtype bb p t@(RAllT _ _ r)-  = ppTy r $ pprForall bb p t+  = ppTy bb r $ pprForall bb p t pprRtype bb p t@(RAllP _ _)   = pprForall bb p t-pprRtype _ _ (RVar a r)-  = ppTy r $ pprint a+pprRtype bb _ (RVar a r)+  = ppTy bb r $ pprint a pprRtype bb p t@RFun{}   = maybeParen p funPrec (pprRtyFun bb empty t) pprRtype bb p (RApp c [t] rs r)   | isList c-  = ppTy r $ brackets (pprRtype bb p t) <-> ppReftPs bb p rs+  = ppTy bb r $ brackets (pprRtype bb p t) <-> ppReftPs bb p rs pprRtype bb p (RApp c ts rs r)   | isTuple c-  = ppTy r $ parens (intersperse comma (pprRtype bb p <$> ts)) <-> ppReftPs bb p rs+  = ppTy bb r $ parens (intersperse comma (pprRtype bb p <$> ts)) <-> ppReftPs bb p rs pprRtype bb p (RApp c ts rs r)   | isEmpty rsDoc && isEmpty tsDoc-  = ppTy r $ ppT c+  = ppTy bb r $ ppT c   | otherwise-  = ppTy r $ parens $ ppT c <+> rsDoc <+> tsDoc+  = ppTy bb r $ parens $ ppT c <+> rsDoc <+> tsDoc   where     rsDoc            = ppReftPs bb p rs     tsDoc            = hsep (pprRtype bb p <$> ts)@@ -252,7 +253,7 @@ pprRtype _ _ (RExprArg e)   = braces $ pprint e pprRtype bb p (RAppTy t t' r)-  = ppTy r $ pprRtype bb p t <+> pprRtype bb p t'+  = ppTy bb r $ pprRtype bb p t <+> pprRtype bb p t' pprRtype bb p (RRTy e _ OCons t)   = sep [braces (pprRsubtype bb p e) <+> "=>", pprRtype bb p t] pprRtype bb p (RRTy e r o rt)@@ -261,8 +262,8 @@     ppe         = hsep (punctuate comma (ppxt <$> e)) <+> dcolon     ppp  doc    = text "<<" <+> doc <+> text ">>"     ppxt (x, t) = pprint x <+> ":" <+> pprRtype bb p t-pprRtype _ _ (RHole r)-  = ppTy r $ text "_"+pprRtype bb _ (RHole r)+  = ppTy bb r $ text "_"  ppTyConB :: TyConable c => PPEnv -> c -> Doc ppTyConB bb@@ -273,8 +274,8 @@ shortModules = text . F.symbolString . dropModuleNames . F.symbol . render  pprRsubtype-  :: (OkRT c tv r, PPrint a, PPrint (RType c tv r), PPrint (RType c tv ()))-  => PPEnv -> Prec -> [(a, RType c tv r)] -> Doc+  :: (OkRTBV b v c tv r, PPrint a, PPrint (RTypeBV b v c tv r), PPrint (RTypeBV b v c tv (NoReftB b)))+  => PPEnv -> Prec -> [(a, RTypeBV b v c tv r)] -> Doc pprRsubtype bb p e   = pprint_env <+> text "|-" <+> pprRtype bb p tl <+> "<:" <+> pprRtype bb p tr   where@@ -292,9 +293,9 @@   | otherwise                  = parens pretty  ppExists-  :: (OkRT c tv r, PPrint c, PPrint tv, PPrint (RType c tv r),-      PPrint (RType c tv ()))-  => PPEnv -> Prec -> RType c tv r -> Doc+  :: (OkRTBV b v c tv r, PPrint c, PPrint tv, PPrint (RTypeBV b v c tv r),+      PPrint (RTypeBV b v c tv (NoReftB b)))+  => PPEnv -> Prec -> RTypeBV b v c tv r -> Doc ppExists bb p rt   = text "exists" <+> brackets (intersperse comma [pprDbind bb topPrec x t | (x, t) <- ws]) <-> dot <-> pprRtype bb p rt'     where (ws,  rt')               = split [] rt@@ -302,8 +303,8 @@           split zs t                = (reverse zs, t)  ppAllExpr-  :: (OkRT c tv r, PPrint (RType c tv r), PPrint (RType c tv ()))-  => PPEnv -> Prec -> RType c tv r -> Doc+  :: (OkRTBV b v c tv r, PPrint (RTypeBV b v c tv r), PPrint (RTypeBV b v c tv (NoReftB b)))+  => PPEnv -> Prec -> RTypeBV b v c tv r -> Doc ppAllExpr bb p rt   = text "forall" <+> brackets (intersperse comma [pprDbind bb topPrec x t | (x, t) <- ws]) <-> dot <-> pprRtype bb p rt'     where@@ -312,19 +313,20 @@       split zs t              = (reverse zs, t)  ppReftPs-  :: (OkRT c tv r, PPrint (RType c tv r), PPrint (RType c tv ()),-      Reftable (Ref (RType c tv ()) (RType c tv r)))-  => t -> t1 -> [Ref (RType c tv ()) (RType c tv r)] -> Doc+  :: (OkRTBV b v c tv r, PPrint (RTypeBV b v c tv r), PPrint (RTypeBV b v c tv (NoReftB b)))+  => t -> t1 -> [RefB b (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v c tv r)] -> Doc ppReftPs _ _ rs-  | all isTauto rs   = empty+  | all trivial rs   = empty   | not (ppPs ppEnv) = empty   | otherwise        = angleBrackets $ hsep $ punctuate comma $ pprRef <$> rs+ where+  trivial (RProp _ t) = isTrivial t  pprDbind-  :: (OkRT c tv r, PPrint (RType c tv r), PPrint (RType c tv ()))-  => PPEnv -> Prec -> F.Symbol -> RType c tv r -> Doc+  :: (OkRTBV b v c tv r, PPrint (RTypeBV b v c tv r), PPrint (RTypeBV b v c tv (NoReftB b)))+  => PPEnv -> Prec -> b -> RTypeBV b v c tv r -> Doc pprDbind bb p x t-  | F.isNonSymbol x || (x == F.dummySymbol)+  | x == F.wildcard   = pprRtype bb p t   | otherwise   = pprint x <-> colon <-> pprRtype bb p t@@ -332,8 +334,8 @@   pprRtyFun-  :: ( OkRT c tv r, PPrint (RType c tv r), PPrint (RType c tv ()))-  => PPEnv -> Doc -> RType c tv r -> Doc+  :: ( OkRTBV b v c tv r, PPrint (RTypeBV b v c tv r), PPrint (RTypeBV b v c tv (NoReftB b)))+  => PPEnv -> Doc -> RTypeBV b v c tv r -> Doc pprRtyFun bb prefix rt = hsep (prefix : dArgs ++ [dOut])   where     dArgs               = concatMap ppArg args@@ -356,7 +358,7 @@   = pprRtype bb topPrec t -} -brkFun :: RType c tv r -> ([(F.Symbol, RType c tv r, Doc)], RType c tv r)+brkFun :: RTypeBV b v c tv r -> ([(b, RTypeBV b v c tv r, Doc)], RTypeBV b v c tv r) brkFun (RFun b _ t t' _)  = ((b, t, text "->") : args, out)   where (args, out) = brkFun t' brkFun out                = ([], out)@@ -364,7 +366,7 @@   -pprForall :: (OkRT c tv r) => PPEnv -> Prec -> RType c tv r -> Doc+pprForall :: (OkRTBV b v c tv r) => PPEnv -> Prec -> RTypeBV b v c tv r -> Doc pprForall bb p t = maybeParen p funPrec $ sep [                       pprForalls (ppPs bb) (fst <$> ty_vars trep) (ty_preds trep)                     , pprClss cls@@ -390,13 +392,13 @@     dπs False _               = empty     dπs True πs               = angleBrackets $ intersperse comma $ pprPvarDef bb p <$> πs -pprRtvarDef :: (PPrint tv) => [RTVar tv (RType c tv ())] -> Doc+pprRtvarDef :: (PPrint tv) => [RTVar tv (RTypeBV b v c tv (NoReftB b))] -> Doc pprRtvarDef = sep . map (pprint . ty_var_value)  pprCls-  :: (OkRT c tv r, PPrint a, PPrint (RType c tv r),-      PPrint (RType c tv ()))-  => PPEnv -> Prec -> a -> [RType c tv r] -> Doc+  :: (OkRTBV b v c tv r, PPrint a, PPrint (RTypeBV b v c tv r),+      PPrint (RTypeBV b v c tv (NoReftB b)))+  => PPEnv -> Prec -> a -> [RTypeBV b v c tv r] -> Doc pprCls bb p c ts   = pp c <+> hsep (map (pprRtype bb p) ts)   where@@ -404,38 +406,55 @@        | otherwise  = pprint  -pprPvarDef :: (OkRT c tv ()) => PPEnv -> Prec -> PVar (RType c tv ()) -> Doc+pprPvarDef :: (OkRTBV b v c tv (NoReftB b)) => PPEnv -> Prec -> PVarBV b v (RTypeBV b v c tv (NoReftB b)) -> Doc pprPvarDef bb p (PV s t _ xts)   = pprint s <+> dcolon <+> intersperse arrow dargs <+> pprPvarKind bb p t   where     dargs = [pprPvarSort bb p xt | (xt,_,_) <- xts]  -pprPvarKind :: (OkRT c tv ()) => PPEnv -> Prec -> RType c tv () -> Doc+pprPvarKind :: (OkRTBV b v c tv (NoReftB b)) => PPEnv -> Prec -> RTypeBV b v c tv (NoReftB b) -> Doc pprPvarKind bb p t = pprPvarSort bb p t <+> arrow <+> pprName F.boolConName  pprName :: F.Symbol -> Doc pprName                      = text . F.symbolString -pprPvarSort :: (OkRT c tv ()) => PPEnv -> Prec -> RType c tv () -> Doc+pprPvarSort :: (OkRTBV b v c tv (NoReftB b)) => PPEnv -> Prec -> RTypeBV b v c tv (NoReftB b) -> Doc pprPvarSort bb p t = pprRtype bb p t -pprRef :: (OkRT c tv r) => Ref (RType c tv ()) (RType c tv r) -> Doc+pprRef :: (OkRTBV b v c tv r) => RefB b (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v c tv r) -> Doc pprRef  (RProp ss s) = ppRefArgs (fst <$> ss) <+> pprint s -- pprRef (RProp ss s) = ppRefArgs (fst <$> ss) <+> pprint (fromMaybe mempty (stripRTypeBase s)) -ppRefArgs :: [F.Symbol] -> Doc+ppRefArgs :: (F.Binder b, PPrint b) => [b] -> Doc ppRefArgs [] = empty-ppRefArgs ss = text "\\" <-> hsep (ppRefSym <$> ss ++ [F.vv Nothing]) <+> arrow+ppRefArgs ss = text "\\" <-> hsep (ppRefSym <$> ss ++ [F.wildcard]) <+> arrow -ppRefSym :: (Eq a, IsString a, PPrint a) => a -> Doc-ppRefSym "" = text "_"-ppRefSym s  = pprint s+ppRefSym :: (F.Binder b, PPrint b) => b -> Doc+ppRefSym s | s == F.wildcard = text "_"+ppRefSym s                   = pprint s  dot :: Doc dot                = char '.' -instance (PPrint (PredicateV v), Reftable (PredicateV v), PPrint r, Reftable r) => PPrint (UReftV v r) where+ppTy ::+  ( Ord (ReftBind r), F.Fixpoint (ReftBind r), PPrint (ReftBind r)+  , Ord (ReftVar r), F.Fixpoint (ReftVar r), PPrint (ReftVar r)+  , ToReft r+  ) => PPEnv -> r -> Doc -> Doc+ppTy bb r0 t = doc+ where+  MkUReft r p = toUReft r0+  doc+    | isTauto r = tDoc+    | F.Reft (v, e) <- toReft r =+        braces (pprint v <+> colon <+> tDoc <+> text "|" <+> pprint e)+  tDoc+    | Pr [] <- p    = t+    | not (ppPs bb) = t+    | otherwise     = t <-> angleBrackets (pprint p)++instance (PPrint (PredicateBV b v), ToReft (PredicateBV b v), PPrint r, ToReft r) => PPrint (UReftBV b v r) where   pprintTidy k (MkUReft r p)     | isTauto r  = pprintTidy k p     | isTauto p  = pprintTidy k r

@@ -13,6 +13,8 @@ {-# LANGUAGE NamedFieldPuns             #-} {-# LANGUAGE TupleSections              #-} {-# LANGUAGE TypeFamilies               #-}+{-# LANGUAGE TypeOperators              #-}+{-# LANGUAGE ScopedTypeVariables        #-}  {-# OPTIONS_GHC -Wno-orphans #-} @@ -35,9 +37,9 @@   , isClassType, isEqType, isRVar, isBool, isEmbeddedClass    -- * Refinement Types-  , RType, RTypeV (..), Ref(..), RTProp, RTPropV, rPropP+  , RType, RTypeV, RTypeBV (..), Ref, RefB(..), RTProp, RTPropV, RTPropBV, rPropP   , RTyVar (..)-  , OkRT+  , OkRT, OkRTBV    -- * Classes describing operations on `RTypes`   , TyConable (..)@@ -50,9 +52,12 @@    -- * Predicate Variables   , PVar-  , PVarV (PV, pname, parg, ptype, pargs), pvType+  , PVarV+  , PVarBV (PV, pname, parg, ptype, pargs), pvType   , Predicate-  , PredicateV (..)+  , PredicateV+  , PredicateBV(..)+  , PredicateCompat(..)    -- * Expression Arguments   , notExprArg@@ -64,13 +69,16 @@   , mapPVarV   , emapPVarVM   , emapSubstVM-  , pvars, pappSym, pApp+  , pvars, pApp    -- * Refinements   , UReft-  , UReftV(..)+  , UReftV+  , UReftBV(..)   , mapUReftV   , emapUReftVM+  , NoReft+  , NoReftB(..)    -- * Parse-time entities describing refined data types   , SizeFun, SizeFunV (..), szFun@@ -95,7 +103,7 @@   , RSort   , UsedPVar   , UsedPVarV-  , RPVar, RReft, RReftV+  , RPVar, RReft, RReftV, RReftBV    -- * Printer Configuration   , PPEnv (..)@@ -105,10 +113,13 @@   -- * Refined Function Info   , RFInfo(..), defRFInfo, mkRFInfo, classRFInfo -  -- * Reftable/UReftable Instances-  , Reftable(..)-  , UReftable(..)-  , ToReftV(..)+  -- * Converting to and from refinements+  , ToReft(..)+  , Meet(..)+  , Top(..)+  , IsReft(..)+  , isTauto+  , trueReft   )   where @@ -149,11 +160,12 @@ import qualified Data.List                              as L import           Data.Maybe                             (mapMaybe) import           Data.List                              as L (nub)+import           Data.Proxy                             (Proxy(..)) import           Text.PrettyPrint.HughesPJ              hiding (first, (<>)) import           Language.Fixpoint.Misc  import qualified Language.Fixpoint.Types as F-import           Language.Fixpoint.Types (Expr, ExprV(..), SubstV(..), Symbol)+import           Language.Fixpoint.Types (Expr, ExprBV(..), KVarSubst, Symbol)  import           Language.Haskell.Liquid.GHC.Misc import           Language.Haskell.Liquid.Types.Names@@ -266,15 +278,16 @@ --------------------------------------------------------------------  type PVar t = PVarV Symbol t-data PVarV v t = PV-  { pname :: !Symbol+type PVarV v t = PVarBV Symbol v t+data PVarBV b v t = PV+  { pname :: !b   , ptype :: !t-  , parg  :: !Symbol-  , pargs :: ![(t, Symbol, F.ExprV v)]+  , parg  :: !b+  , pargs :: ![(t, b, F.ExprBV b v)]   } deriving (Generic, Data, Show, Functor)-  deriving B.Binary via Generically (PVarV v t)+  deriving B.Binary via Generically (PVarBV b v t) -mapPVarV :: (v -> v') -> (t -> t') -> PVarV v t -> PVarV v' t'+mapPVarV :: (v -> v') -> (t -> t') -> PVarBV b v t -> PVarBV b v' t' mapPVarV f g PV {..} =     PV       { ptype = g ptype@@ -283,7 +296,7 @@       }  -- | A map traversal that collects the local variables in scope-emapPVarVM :: Monad m => ([Symbol] -> v -> m v') -> ([Symbol] -> t -> m t') -> PVarV v t -> m (PVarV v' t')+emapPVarVM :: (Monad m, Hashable b) => ([b] -> v -> m v') -> ([b] -> t -> m t') -> PVarBV b v t -> m (PVarBV b v' t') emapPVarVM f g pv = do     ptype <- g (argSyms (pargs pv)) (ptype pv)     (_, pargs) <- forAccumM [] (pargs pv) $ \ss (t, s, e) -> do@@ -292,30 +305,28 @@   where     argSyms = map (\(_, s, _) -> s) -instance Eq (PVarV v t) where+instance Eq b => Eq (PVarBV b v t) where   pv == pv' = pname pv == pname pv' {- UNIFY: What about: && eqArgs pv pv' -} -instance Ord (PVarV v t) where+instance Ord b => Ord (PVarBV b v t) where   compare (PV n _ _ _)  (PV n' _ _ _) = compare n n' -instance (NFData v, NFData t) => NFData   (PVarV v t)+instance (NFData b, NFData v, NFData t) => NFData (PVarBV b v t) -instance Hashable (PVarV v a) where+instance Hashable b => Hashable (PVarBV b v a) where   hashWithSalt i (PV n _ _ _) = hashWithSalt i n -pvType :: PVarV v t -> t+pvType :: PVarBV b v t -> t pvType = ptype -instance F.PPrint (PVar a) where+instance (Ord b, F.Fixpoint b, Hashable b, F.PPrint b, Ord v, F.Fixpoint v, F.PPrint v) => F.PPrint (PVarBV b v a) where   pprintTidy _ = pprPvar -pprPvar :: PVar a -> Doc-pprPvar (PV s _ _ xts) = F.pprint s <+> hsep (F.pprint <$> dargs xts)-  where-    dargs              = map thd3 . takeWhile (\(_, x, y) -> F.EVar x /= y)+pprPvar :: (Ord b, F.Fixpoint b, Hashable b, F.PPrint b, Ord v, F.Fixpoint v, F.PPrint v) => PVarBV b v a -> Doc+pprPvar (PV s _ _ xts) = F.pprint s <+> hsep (F.pprint . thd3 <$> xts)  -- | A map traversal that collects the local variables in scope-emapExprVM :: Monad m => ([Symbol] -> v -> m v') -> ExprV v -> m (ExprV v')+emapExprVM :: (Monad m, Hashable b) => ([b] -> v -> m v') -> ExprBV b v -> m (ExprBV b v') emapExprVM f = go []   where     go acc = \case@@ -336,28 +347,30 @@       PImp e0 e1 -> PImp <$> go acc e0 <*> go acc e1       PIff e0 e1 -> PIff <$> go acc e0 <*> go acc e1       PAtom brel e0 e1 -> PAtom brel <$> go acc e0 <*> go acc e1-      PKVar k su -> PKVar k <$> emapSubstVM (f . (domain su ++) . (acc ++)) su+      PKVar k tsu su -> PKVar k tsu <$> 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       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+    domain m = M.keys $ F.fromKVarSubst m -emapSubstVM :: Monad m => ([Symbol] -> v -> m v') -> SubstV v -> m (SubstV v')-emapSubstVM f (Su m) = Su . M.fromList <$> mapM (traverse (emapExprVM f)) (M.toList m)+emapSubstVM :: (Monad m, Hashable b) => ([b] -> v -> m v') -> KVarSubst b v -> m (KVarSubst b v')+emapSubstVM f m = F.toKVarSubst . M.fromList <$> mapM (traverse (emapExprVM f)) (M.toList $ F.fromKVarSubst m)  -------------------------------------------------------------------------------- -- | Predicates ---------------------------------------------------------------- --------------------------------------------------------------------------------  type UsedPVar    = UsedPVarV Symbol-type UsedPVarV v = PVarV v ()+type UsedPVarV v = UsedPVarBV Symbol v+type UsedPVarBV b v = PVarBV b v ()  type Predicate = PredicateV Symbol-newtype PredicateV v = Pr [UsedPVarV v]+type PredicateV v = PredicateBV Symbol v+newtype PredicateBV b v = Pr [UsedPVarBV b v]   deriving (Generic, Data)-  deriving (B.Binary, Hashable) via Generically (PredicateV v)+  deriving (B.Binary, Hashable) via Generically (PredicateBV b v)  mapPredicateV :: (v -> v') -> PredicateV v -> PredicateV v' mapPredicateV f (Pr xs) = Pr (map (mapPVarV f (const ())) xs)@@ -366,7 +379,7 @@ emapPredicateVM :: Monad m => ([Symbol] -> v -> m v') -> PredicateV v -> m (PredicateV v') emapPredicateVM f (Pr xs) = Pr <$> mapM (emapPVarVM f (\_ _ -> pure ())) xs -instance Ord v => Eq (PredicateV v) where+instance (Ord b, Ord v) => Eq (PredicateBV b v) where   (Pr vs) == (Pr ws)       = and $ (length vs' == length ws') : [v == w | (v, w) <- zip vs' ws']         where@@ -380,14 +393,14 @@   mempty  = pdTrue   mappend = (<>) -instance Semigroup Predicate where+instance Eq b => Semigroup (PredicateBV b v) where   p <> p' = pdAnd [p, p'] -instance F.PPrint Predicate where+instance (Ord b, F.Fixpoint b, Hashable b, F.PPrint b, Ord v, F.Fixpoint v, F.PPrint v) => F.PPrint (PredicateBV b v) where   pprintTidy _ (Pr [])  = text "True"   pprintTidy k (Pr pvs) = hsep $ punctuate (text "&") (F.pprintTidy k <$> pvs) -instance Semigroup a => Semigroup (UReft a) where+instance (Semigroup a, Eq b) => Semigroup (UReftBV b v a) where   MkUReft x y <> MkUReft x' y' = MkUReft (x <> x') (y <> y')  instance (Monoid a) => Monoid (UReft a) where@@ -395,23 +408,25 @@   mappend = (<>)  -pdTrue :: Predicate+pdTrue :: PredicateBV b v pdTrue         = Pr [] -pdAnd :: Foldable t => t Predicate -> Predicate+pdAnd :: (Foldable t, Eq b) => t (PredicateBV b v) -> PredicateBV b v pdAnd ps       = Pr (nub $ concatMap pvars ps) -pvars :: Predicate -> [UsedPVar]+pvars :: PredicateBV b v -> [UsedPVarBV b v] pvars (Pr pvs) = pvs -instance F.Subable UsedPVar where+instance Hashable v => F.Subable (UsedPVarBV v v) where+  type Variable (UsedPVarBV v v) = v   syms pv         = [ y | (_, x, F.EVar y) <- pargs pv, x /= y ]   subst s pv      = pv { pargs = mapThd3 (F.subst s)  <$> pargs pv }   substf f pv     = pv { pargs = mapThd3 (F.substf f) <$> pargs pv }   substa f pv     = pv { pargs = mapThd3 (F.substa f) <$> pargs pv }  -instance F.Subable Predicate where+instance Hashable v => F.Subable (PredicateBV v v) where+  type Variable (PredicateBV v v) = v   syms     (Pr pvs) = concatMap F.syms   pvs   subst  s (Pr pvs) = Pr (F.subst s  <$> pvs)   substf f (Pr pvs) = Pr (F.substf f <$> pvs)@@ -440,6 +455,12 @@ instance F.Symbolic RTyVar where   symbol (RTV tv) = F.symbol tv -- tyVarUniqueSymbol tv +instance CompatibleBinder (F.Located Symbol) BTyVar where+  coerceBinder (BTV tv) = tv++instance CompatibleBinder Symbol BTyVar where+  coerceBinder tv = coerceBinder (coerceBinder tv :: F.Located Symbol)+ -- instance F.Symbolic RTyVar where   -- symbol (RTV tv) = F.symbol . getName $ tv -- rtyVarUniqueSymbol  :: RTyVar -> Symbol@@ -696,39 +717,42 @@ --------------------------------------------------------------------------------  type RTVU c tv = RTVUV Symbol c tv-type RTVUV v c tv = RTVar tv (RTypeV v c tv ())+type RTVUV v c tv = RTVUBV Symbol v c tv+type RTVUBV b v c tv = RTVar tv (RTypeBV b v c tv (NoReftB b)) type PVU c tv = PVUV Symbol c tv-type PVUV v c tv = PVarV v (RTypeV v c tv ())+type PVUV v c tv = PVarV v (RTypeV v c tv NoReft)+type PVUBV b v c tv = PVarBV b v (RTypeBV b v c tv (NoReftB b))  instance Show tv => Show (RTVU c tv) where   show (RTVar t _) = show t  type RType c tv r = RTypeV Symbol c tv r-data RTypeV v c tv r+type RTypeV v c tv = RTypeBV Symbol v c tv+data RTypeBV b v c tv r   = RVar {       rt_var    :: !tv     , rt_reft   :: !r     }    | RFun  {-      rt_bind   :: !Symbol+      rt_bind   :: !b     , rt_rinfo  :: !RFInfo-    , rt_in     :: !(RTypeV v c tv r)-    , rt_out    :: !(RTypeV v c tv r)+    , rt_in     :: !(RTypeBV b v c tv r)+    , rt_out    :: !(RTypeBV b v c tv r)     , rt_reft   :: !r     }    | RAllT {-      rt_tvbind :: !(RTVUV v c tv) -- RTVar tv (RType c tv ()))-    , rt_ty     :: !(RTypeV v c tv r)+      rt_tvbind :: !(RTVUBV b v c tv) -- RTVar tv (RType c tv ()))+    , rt_ty     :: !(RTypeBV b v c tv r)     , rt_ref    :: !r     }    -- | "forall x y <z :: Nat, w :: Int> . TYPE"   --               ^^^^^^^^^^^^^^^^^^^ (rt_pvbind)   | RAllP {-      rt_pvbind :: !(PVUV v c tv)-    , rt_ty     :: !(RTypeV v c tv r)+      rt_pvbind :: !(PVUBV b v c tv)+    , rt_ty     :: !(RTypeBV b v c tv r)     }    -- | For example, in [a]<{\h -> v > h}>, we apply (via `RApp`)@@ -736,42 +760,42 @@   --   * the `RTyCon` denoted by `[]`.   | RApp  {       rt_tycon  :: !c-    , rt_args   :: ![RTypeV v c tv r]-    , rt_pargs  :: ![RTPropV v c tv r]+    , rt_args   :: ![RTypeBV b v c tv r]+    , rt_pargs  :: ![RTPropBV b v c tv r]     , rt_reft   :: !r     }    | RAllE {-      rt_bind   :: !Symbol-    , rt_allarg :: !(RTypeV v c tv r)-    , rt_ty     :: !(RTypeV v c tv r)+      rt_bind   :: !b+    , rt_allarg :: !(RTypeBV b v c tv r)+    , rt_ty     :: !(RTypeBV b v c tv r)     }    | REx {-      rt_bind   :: !Symbol-    , rt_exarg  :: !(RTypeV v c tv r)-    , rt_ty     :: !(RTypeV v c tv r)+      rt_bind   :: !b+    , rt_exarg  :: !(RTypeBV b v c tv r)+    , rt_ty     :: !(RTypeBV b v c tv r)     } -  | RExprArg (F.Located (ExprV v))              -- ^ For expression arguments to type aliases+  | RExprArg (F.Located (ExprBV b v))           -- ^ For expression arguments to type aliases                                                 --   see tests/pos/vector2.hs   | RAppTy{-      rt_arg   :: !(RTypeV v c tv r)-    , rt_res   :: !(RTypeV v c tv r)+      rt_arg   :: !(RTypeBV b v c tv r)+    , rt_res   :: !(RTypeBV b v c tv r)     , rt_reft  :: !r     }    | RRTy  {-      rt_env   :: ![(Symbol, RTypeV v c tv r)]+      rt_env   :: ![(b, RTypeBV b v c tv r)]     , rt_ref   :: !r     , rt_obl   :: !Oblig-    , rt_ty    :: !(RTypeV v c tv r)+    , rt_ty    :: !(RTypeBV b v c tv r)     }    | RHole r -- ^ let LH match against the Haskell type and add k-vars, e.g. `x:_`             --   see tests/pos/Holes.hs   deriving (Eq, Generic, Data, Functor, Foldable, Traversable)-  deriving (B.Binary, Hashable) via Generically (RTypeV v c tv r)+  deriving (B.Binary, Hashable) via Generically (RTypeBV b v c tv r)  instance (NFData c, NFData tv, NFData r)       => NFData (RType c tv r) @@ -821,6 +845,8 @@ instance (NFData tv, NFData s)     => NFData   (RTVar tv s) instance (NFData s)                => NFData   (RTVInfo s) +type Ref τ t = RefB Symbol τ t+ -- | @Ref@ describes `Prop τ` and `HProp` arguments applied to type constructors. --   For example, in [a]<{\h -> v > h}>, we apply (via `RApp`) --   * the `RProp`  denoted by `{\h -> v > h}` to@@ -830,29 +856,31 @@ --   In contrast, the `Predicate` argument in `ur_pred` in the @UReft@ applies --   directly to any type and has semantics _independent of_ the data-type. -data Ref τ t = RProp-  { rf_args :: [(Symbol, τ)] -- ^ arguments. e.g. @h@ in the above example+data RefB b τ t = RProp+  { rf_args :: [(b, τ)] -- ^ arguments. e.g. @h@ in the above example   , rf_body :: t -- ^ Abstract refinement associated with `RTyCon`. e.g. @v > h@ in the above example   } deriving (Eq, Generic, Data, Functor, Foldable, Traversable)-    deriving (B.Binary, Hashable) via Generically (Ref τ t)+    deriving (B.Binary, Hashable) via Generically (RefB b τ t)  instance (NFData τ,   NFData t)   => NFData   (Ref τ t) -rPropP :: [(Symbol, τ)] -> r -> Ref τ (RTypeV v c tv r)+rPropP :: [(b, τ)] -> r -> RefB b τ (RTypeV v c tv r) rPropP τ r = RProp τ (RHole r)  -- | @RTProp@ is a convenient alias for @Ref@ that will save a bunch of typing. --   In general, perhaps we need not expose @Ref@ directly at all. type RTProp c tv r = RTPropV Symbol c tv r-type RTPropV v c tv r = Ref (RTypeV v c tv ()) (RTypeV v c tv r)+type RTPropV v c tv r = RTPropBV Symbol v c tv r+type RTPropBV b v c tv r = RefB b (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v c tv r)  type UReft r = UReftV F.Symbol r-data UReftV v r = MkUReft+type UReftV v r = UReftBV F.Symbol v r+data UReftBV b v r = MkUReft   { ur_reft   :: !r-  , ur_pred   :: !(PredicateV v)+  , ur_pred   :: !(PredicateBV b v)   }   deriving (Eq, Generic, Data, Functor, Foldable, Traversable)-  deriving (B.Binary, Hashable) via Generically (UReftV v r)+  deriving (B.Binary, Hashable) via Generically (UReftBV b v r)  mapUReftV :: (v -> v') -> (r -> r') -> UReftV v r -> UReftV v' r' mapUReftV f g (MkUReft r p) = MkUReft (g r) (mapPredicateV f p)@@ -862,16 +890,41 @@   => ([Symbol] -> v -> m v') -> (r -> m r') -> UReftV v r -> m (UReftV v' r') emapUReftVM f g (MkUReft r p) = MkUReft <$> g r <*> emapPredicateVM f p +type NoReft = NoReftB Symbol+data NoReftB b = NoReft+  deriving (Eq, Generic, Data, Functor, Foldable, Traversable)+  deriving (B.Binary, Hashable) via Generically (NoReftB b)++instance NFData (NoReftB b)++instance F.PPrint (NoReftB b) where+  pprintTidy _ _ = text $ show ()++instance Hashable b => F.Subable (NoReftB b) where+  type Variable (NoReftB b) = b+  syms _   = []+  substa _ = id+  substf _ = id+  subst _  = id+  subst1 r = const r++instance Semigroup (NoReftB b) where+  _ <> _ = NoReft++instance Monoid (NoReftB b) where+  mempty = NoReft+ type BRType      = RTypeV Symbol 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 ()-type RSort       = RRType    ()+type BSort       = BRType    NoReft+type BSortV v    = BRTypeV v NoReft+type RSort       = RRType    NoReft type BPVar       = PVar      BSort type RPVar       = PVar      RSort type RReft       = RReftV    F.Symbol-type RReftV v    = UReftV v (F.ReftV v)+type RReftV v    = RReftBV Symbol v+type RReftBV b v = UReftBV b v (F.ReftBV b v) type BareType    = BareTypeV F.Symbol type BareTypeParsed = BareTypeV F.LocSymbol type BareTypeLHName = BareTypeV LHName@@ -934,124 +987,166 @@ -- Should just make this a @Pretty@ instance but its too damn tedious -- to figure out all the constraints. -type OkRT c tv r = ( TyConable c-                   , F.PPrint tv, F.PPrint c, F.PPrint r-                   , Reftable r, Reftable (RTProp c tv ()), Reftable (RTProp c tv r)-                   , Eq c, Eq tv-                   , Hashable tv-                   )+type OkRT c tv r =+  ( TyConable c+  , F.PPrint tv, F.PPrint c, F.PPrint r, F.PPrint (ReftVar r)+  , F.Fixpoint (ReftVar r)+  , ToReft r+  , ReftBind r ~ F.Symbol+  , Eq c, Eq tv, Ord (ReftVar r)+  , Hashable tv+  ) -class Reftable r => UReftable r where-  ofUReft :: UReft F.Reft -> r-  ofUReft (MkUReft r _) = ofReft r+type OkRTBV b v c tv r =+  ( TyConable c+  , F.PPrint b, F.PPrint v, F.PPrint tv, F.PPrint c, F.PPrint r, F.PPrint (ReftVar r)+  , F.Fixpoint b, F.Fixpoint v, F.Fixpoint (ReftVar r)+  , F.Binder b+  , ToReft r+  , ReftBind r ~ b+  , Eq c, Eq tv, Ord b, Ord v, Ord (ReftVar r)+  , Hashable tv+  ) +-- | Types that have one associated refinement representible by a 'F.ReftBV'+class (F.Binder (ReftBind r), Eq (ReftVar r)) => ToReft r where+  type ReftVar r+  type ReftBind r+  type ReftBind r = Symbol+  toReft :: r -> F.ReftBV (ReftBind r) (ReftVar r)+  toUReft :: r -> UReftBV (ReftBind r) (ReftVar r) (F.ReftBV (ReftBind r) (ReftVar r))+  toUReft r = MkUReft (toReft r) pdTrue -instance UReftable (UReft F.Reft) where-   ofUReft r = r+-- | Types that can be combined conjunctively in some sense+class Semigroup r => Meet r where+  meet :: r -> r -> r+  meet = (<>) -instance UReftable () where-   ofUReft _ = mempty+-- | Types whose refinements can be cleared to true+class Top r where+  top :: r -> r -class ToReftV r where-  type ReftVar r-  toReftV  :: r -> F.ReftV (ReftVar r)+-- | Types that can be constructed from a 'F.ReftBV'+class (ToReft r, Meet r, Top r) => IsReft r where+  ofReft :: F.ReftBV (ReftBind r) (ReftVar r) -> r -instance ToReftV r => ToReftV (UReftV v r) where-  type ReftVar (UReftV v r) = ReftVar r-  toReftV = toReftV . ur_reft+trueReft :: IsReft r => r+trueReft = ofReft F.trueReft -instance ToReftV (F.ReftV v) where-  type ReftVar (F.ReftV v) = v-  toReftV = id+isTauto :: ToReft r => r -> Bool+isTauto r0 = F.isTautoReft r && null ps+ where+  MkUReft r (Pr ps) = toUReft r0 -instance ToReftV () where+instance (ToReft r, ReftBind r ~ b, ReftVar r ~ v) => ToReft (UReftBV b v r) where+  type ReftVar (UReftBV b v r) = ReftVar r+  type ReftBind (UReftBV b v r) = ReftBind r+  toReft = toReft . ur_reft+  toUReft (MkUReft r p) = MkUReft (toReft r) p++instance Top r => Top (UReftBV b v r) where+  top (MkUReft r _) = MkUReft (top r) pdTrue++instance (IsReft r, F.Binder v, ReftBind r ~ v, ReftVar r ~ v) => IsReft (UReftBV v v r) where+  ofReft r = MkUReft (ofReft r) pdTrue++instance (F.Binder b, Eq v) => ToReft (F.ReftBV b v) where+  type ReftVar (F.ReftBV b v) = v+  type ReftBind (F.ReftBV b v) = b+  toReft = id++instance (F.Binder b) => Top (F.ReftBV b v) where+  top _ = F.trueReft++instance (F.Binder v, F.Fixpoint v) => Meet (F.ReftBV v v) where++instance (F.Binder v, F.Fixpoint v, Eq v) => IsReft (F.ReftBV v v) where+  ofReft = id++instance ToReft () where   type ReftVar () = Symbol-  toReftV _ = F.trueReft+  toReft _ = F.trueReft -class (Monoid r, F.Subable r) => Reftable r where-  isTauto :: r -> Bool-  ppTy    :: r -> Doc -> Doc+instance Top () where+  top _ = () -  top     :: r -> r-  top _   =  mempty+instance IsReft () where+  ofReft _ = () -  meet    :: r -> r -> r-  meet    = mappend+instance F.Binder b => ToReft (NoReftB b) where+  type ReftVar (NoReftB b) = Symbol+  type ReftBind (NoReftB b) = b+  toReft _ = F.trueReft -  toReft  :: r -> F.Reft-  ofReft  :: F.Reft -> r+instance Top (NoReftB b) where+  top _ = NoReft -instance Semigroup F.Reft where+instance F.Binder b => IsReft (NoReftB b) where+  ofReft _ = NoReft++instance ToReft t => ToReft (RefB b τ t) where+  type ReftVar (RefB b τ t) = ReftVar t+  type ReftBind (RefB b τ t) = ReftBind t+  toReft (RProp _ t) = toReft t++instance Top t => Top (RefB b τ t) where+  top (RProp args t) = RProp args (top t)++instance (F.Binder b, Ord v, PredicateCompat b v) => ToReft (PredicateBV b v) where+  type ReftVar (PredicateBV b v) = v+  type ReftBind (PredicateBV b v) = b+  toReft (Pr [])       = F.trueReft+  toReft (Pr ps@(p:_)) = F.Reft (parg p, F.pAnd $ pToRef <$> ps)+  toUReft p = MkUReft F.trueReft p++instance Top (PredicateBV b v) where+  top _ = pdTrue++instance (F.Binder v, F.Fixpoint v) => Semigroup (F.ReftBV v v) where   (<>) = F.meetReft  instance Monoid F.Reft where   mempty  = F.trueReft   mappend = (<>) -instance Reftable () where-  isTauto _ = True-  ppTy _  d = d-  top  _    = ()-  meet _ _  = ()-  toReft _  = F.trueReft-  ofReft _  = ()+instance Meet () -instance Reftable F.Reft where-  isTauto  = all F.isTautoPred . F.conjuncts . F.reftPred-  ppTy     = pprReft-  toReft   = id-  ofReft   = id-  top (F.Reft (v,_)) = F.Reft (v, F.PTrue)+instance Meet (NoReftB b) -instance F.Subable r => F.Subable (UReft r) where+instance (Meet r, Eq v) => Meet (UReftBV v v r)++instance (F.Subable r, F.Variable r ~ v) => F.Subable (UReftBV v v r) where+  type Variable (UReftBV v v r) = v   syms (MkUReft r p)     = F.syms r ++ F.syms p   subst s (MkUReft r z)  = MkUReft (F.subst s r)  (F.subst s z)   substf f (MkUReft r z) = MkUReft (F.substf f r) (F.substf f z)   substa f (MkUReft r z) = MkUReft (F.substa f r) (F.substa f z) -instance (F.PPrint r, Reftable r) => Reftable (UReft r) where-  isTauto               = isTautoUreft-  ppTy                  = ppTyUreft-  toReft (MkUReft r ps) = toReft r `meet` toReft ps-  top (MkUReft r p)     = MkUReft (top r) (top p)-  ofReft r              = MkUReft (ofReft r) mempty- instance F.Expression (UReft ()) where   expr = F.expr . toReft -ppTyUreft :: Reftable r => UReft r -> Doc -> Doc-ppTyUreft u@(MkUReft r p) d-  | isTautoUreft u = d-  | otherwise      = pprReft r (ppTy p d)--pprReft :: (Reftable r) => r -> Doc -> Doc-pprReft r d = braces (F.pprint v <+> colon <+> d <+> text "|" <+> F.pprint r')-  where-    r'@(F.Reft (v, _)) = toReft r--isTautoUreft :: Reftable r => UReft r -> Bool-isTautoUreft u = isTauto (ur_reft u) && isTauto (ur_pred u)--instance Reftable Predicate where-  isTauto (Pr ps)      = null ps--  ppTy r d | isTauto r      = d-           | not (ppPs ppEnv) = d-           | otherwise        = d <-> angleBrackets (F.pprint r)--  toReft (Pr ps@(p:_))        = F.Reft (parg p, F.pAnd $ pToRef <$> ps)-  toReft _                    = F.trueReft--  ofReft = todo Nothing "TODO: Predicate.ofReft"+instance Meet Predicate -pToRef :: PVar a -> F.Expr-pToRef p = pApp (pname p) $ F.EVar (parg p) : (thd3 <$> pargs p)+pToRef :: PredicateCompat b v => PVarBV b v a -> F.ExprBV b v+pToRef p = pApp (pnameV p) $ F.EVar (pargV p) : (thd3 <$> pargs p) -pApp      :: Symbol -> [Expr] -> Expr+pApp      :: forall b v . PredicateCompat b v => v -> [ExprBV b v] -> ExprBV b v pApp p es = F.mkEApp fn (F.EVar p:es)   where-    fn    = F.dummyLoc (pappSym n)+    fn    = F.dummyLoc (pappV (Proxy :: Proxy b) n)     n     = length es -pappSym :: Show a => a -> Symbol-pappSym n  = F.symbol $ "papp" ++ show n+class PredicateCompat b v where+  pappV :: Proxy b -> Int -> v+  pnameV :: PVarBV b v a -> v+  pargV :: PVarBV b v a -> v++instance PredicateCompat Symbol Symbol where+  pappV _ n = F.symbol $ "papp" ++ show n+  pnameV p = pname p+  pargV p = parg p++instance PredicateCompat Symbol F.LocSymbol where+  pappV _ n = F.dummyLoc $ F.symbol $ "papp" ++ show n+  pnameV p = F.dummyLoc $ pname p+  pargV p = F.dummyLoc $ parg p