Move hole detection from synthesis to checking

Author: matheussbernardo

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

@@ -387,9 +387,17 @@ 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
+      isItHole <- detectTypedHole γ e
+      case isItHole of
+        Just (srcSpan, x) -> addHole (RealSrcSpan srcSpan Strict.Nothing) x t γ
+        _ -> return ()
 
 lambdaSingleton :: CGEnv -> F.TCEmb TyCon -> Var -> CoreExpr -> CG (UReft F.Reft)
 lambdaSingleton γ tce x e
@@ -512,18 +520,43 @@ consE γ (Var x)
 consE _ (Lit c)
   = refreshVV $ uRType $ literalFRefType c
 
-consE γ e'@(App _ _) =
-  do
-    t <- if (warnOnTermHoles (getConfig γ)) then synthesizeWithHole else consEApp γ e'
-    return t
-  where 
-    synthesizeWithHole = do
-      isItHole <- detectTypedHole γ e'
-      t <- consEApp γ e'
-      _ <- case isItHole of
-        Just (srcSpan, x) -> addHole (RealSrcSpan srcSpan Strict.Nothing) x t γ
-        _ -> return ()
-      return t
+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 γ (Lam α e) | isTyVar α
   = do γ' <- updateEnvironment γ α