Initial version of typed holes support under allow-typed-holes flag

docs/mkDocs/docs/options.md

@@ -732,3 +732,67 @@ an import of a module coming from package `PACKAGE`. e.g.
 `--exclude-automatic-assumptions-for=vector` would stop loading
 `_LHAssumptions` modules for any imports coming from package
 `vector`.
+
+## Warn on Term Holes
+
+**Options:** `warn-on-term-holes`
+
+LiquidHaskell can be configured to emit warnings whenever it encounters incomplete terms, known as *holes*.
+
+To create a hole you need to have a binding with the name `hole` in the scope by adding:
+
+      hole = undefined
+
+To use a hole you simply insert the `hole` in any place
+where you want to get more type information. For example:
+```haskell
+hole = undefined
+
+{-@ listLength :: xs:[a] -> {v : Nat | v == len xs} @-}
+listLength :: [a] -> Int
+listLength [] = hole -- Hole inserted here
+listLength (_:xs) = 1 + listLength xs
+```
+
+This flag is particularly useful during development, ensuring that any placeholders in your specifications are reviewed and completed before final evaluation.
+
+To activate this behavior, use the `--warn-on-term-holes` flag either:
+
+1. As a pragma in your source file:
+    ```haskell
+    {-@ LIQUID "--warn-on-term-holes" @-}
+    ```
+2. As a plugin option:
+    ```
+    ghc-options: -fplugin-opt=LiquidHaskell:--warn-on-term-holes
+    ```
+
+When enabled, LiquidHaskell issues a warning for each term hole it discovers, for example:
+
+```haskell
+typed-holes/Example1.hs:25:13: error:
+    Hole Found
+Example1.hole :: {v : [a] | false}
+in the context
+  Example1.<> : forall a .
+                x1:[a] -> x2:[a] -> {VV : [a] | VV == Example1.<> x1 x2}
+
+  lq_anf$##7205759403792797257##dWZ : {v : [a] | v == Example1.<> lq_anf$##7205759403792797256##dWY x##aFc
+                                                 && GHC.Types_LHAssumptions.len v >= 0}
+
+  Example1.hole : forall a . a
+
+  Example1.empty : forall a .
+                   {VV : [a] | VV == Example1.empty
+                               && VV == GHC.Types.[]}
+
+  lq_anf$##7205759403792797256##dWY : {v : [a] | v == Example1.empty
+                                                 && v == GHC.Types.[]
+                                                 && GHC.Types_LHAssumptions.len v >= 0}
+
+  x##aFc : {VV##1043 : [a] | GHC.Types_LHAssumptions.len VV##1043 >= 0}
+hole found
+   |
+25 |         === hole
+   |             ^^^^
+```

liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Generate.hs

@@ -68,9 +68,11 @@ import           Language.Haskell.Liquid.Bare.DataType (dataConMap, makeDataConC
 import Language.Haskell.Liquid.UX.Config
     ( HasConfig(getConfig),
       Config(typeclass, gradual, checkDerived, extensionality,
-             nopolyinfer, noADT, dependantCase, exactDC, rankNTypes),
+             nopolyinfer, noADT, dependantCase, exactDC, rankNTypes, warnOnTermHoles),
       patternFlag,
-      higherOrderFlag )
+      higherOrderFlag, warnOnTermHoles )
+import qualified GHC.Data.Strict as Strict
+
 
 --------------------------------------------------------------------------------
 -- | Constraint Generation: Toplevel -------------------------------------------
@@ -97,12 +99,32 @@ consAct γ cfg info = do
   hws <- gets hsWfs
   fcs <- concat <$> mapM (splitC (typeclass (getConfig info))) hcs
   fws <- concat <$> mapM splitW hws
+  when (warnOnTermHoles cfg) emitConsolidatedHoleWarnings
   modify $ \st -> st { fEnv     = fEnv    st `mappend` feEnv (fenv γ)
                      , cgLits   = litEnv   γ
                      , cgConsts = cgConsts st `mappend` constEnv γ
                      , fixCs    = fcs
                      , fixWfs   = fws }
 
+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 --------------
 --------------------------------------------------------------------------------
@@ -217,9 +239,17 @@ consCB _ γ (NonRec x def)
 
 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
+    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
@@ -295,14 +325,49 @@ addPToEnv γ π
   = do γπ <- γ += ("addSpec1", pname π, pvarRType π)
        foldM (+=) γπ [("addSpec2", x, ofRSort t) | (t, x, _) <- pargs π]
 
+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 Initial App and sequent Tick nodes from an expression.
+stripTicks :: CoreExpr -> CoreExpr
+stripTicks (App (Tick _ e) _) = stripTicks e
+stripTicks (Tick _ e)         = stripTicks e
+stripTicks e          = e
+
+-- Traverse the expression to get the last Tick information.
+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
+
+-- A helper to check if the variable name indicates a typed hole.
+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
 
 --------------------------------------------------------------------------------
@@ -371,9 +436,18 @@ cconsE' γ e@(Cast e' c) t
        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 
+    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
@@ -456,7 +530,8 @@ cconsLazyLet γ (Let (NonRec x ex) e) t
 cconsLazyLet _ _ _
   = panic Nothing "Constraint.Generate.cconsLazyLet called on invalid inputs"
 
---------------------------------------------------------------------------------
+
+---------------------------------------------------------
 -- | Bidirectional Constraint Generation: SYNTHESIS ----------------------------
 --------------------------------------------------------------------------------
 consE :: CGEnv -> CoreExpr -> CG SpecType
@@ -495,44 +570,20 @@ consE γ (Var x)
 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
-  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))
-
+consE γ e'@(App _ _) =
+  do
+    t <- if warnOnTermHoles (getConfig γ) then synthesizeWithHole else consEApp γ e'
+    checkANFHoleInExpr e' t
+    return t
+  where 
+    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
@@ -578,6 +629,68 @@ consE γ e@(Coercion _)
 
 consE _ e@(Type t)
   = panic Nothing $ "consE cannot handle type " ++ GM.showPpr (e, t)
+
+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 ()
+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 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

liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Init.hs

@@ -301,6 +301,9 @@ initCGI cfg info = CGInfo {
   , 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

liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Monad.hs

@@ -21,6 +21,7 @@ import           Language.Fixpoint.Misc hiding (errorstar)
 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,24 @@ addA !l xo@Nothing  !t (AI m)
 addA _ _ _ !a
   = a
 
+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 γ]
+
+addHoleANF :: (Var, SrcSpan) -> Var -> CoreExpr -> SpecType -> CG ()
+addHoleANF uniqueVar anfVar e t = 
+  modify $ \s -> s { hsHolesExprs = M.insertWith (++) uniqueVar [(anfVar, e, t)] (hsHolesExprs s) }
+
+linkANFToHole :: Var -> (Var, SrcSpan) -> CG ()
+linkANFToHole anf h = modify $ \s -> s { hsANFHoles = M.insert anf h $ hsANFHoles s }
+
+isANFInHole :: Var -> CG (Maybe (Var, SrcSpan))
+isANFInHole anf = gets (M.lookup anf . hsANFHoles)
 
 lookupNewType :: Ghc.TyCon -> CG (Maybe SpecType)
 lookupNewType tc

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

@@ -239,6 +239,9 @@ data CGInfo = CGInfo
   , 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)])
   }