Fix #9404 by removing tcInfExpr.

See the ticket for more info about the new algorithm. This is a small
simplification, unifying the treatment of type checking in a few
similar situations.

compiler/typecheck/TcExpr.lhs

@@ -124,16 +124,9 @@ tcInferRho expr = addErrCtxt (exprCtxt expr) (tcInferRhoNC expr)
 
 tcInferRhoNC (L loc expr)
   = setSrcSpan loc $
-    do { (expr', rho) <- tcInfExpr expr
+    do { (expr', rho) <- tcInfer (tcExpr expr)
        ; return (L loc expr', rho) }
 
-tcInfExpr :: HsExpr Name -> TcM (HsExpr TcId, TcRhoType)
-tcInfExpr (HsVar f)     = tcInferId f
-tcInfExpr (HsPar e)     = do { (e', ty) <- tcInferRhoNC e
-                             ; return (HsPar e', ty) }
-tcInfExpr (HsApp e1 e2) = tcInferApp e1 [e2]
-tcInfExpr e             = tcInfer (tcExpr e)
-
 tcHole :: OccName -> TcRhoType -> TcM (HsExpr TcId)
 tcHole occ res_ty
  = do { ty <- newFlexiTyVarTy liftedTypeKind
@@ -326,13 +319,15 @@ tcExpr (OpApp arg1 op fix arg2) res_ty
        -- Eg we do not want to allow  (D#  $  4.0#)   Trac #5570
        --    (which gives a seg fault)
        -- We do this by unifying with a MetaTv; but of course
-       -- it must allow foralls in the type it unifies with (hence PolyTv)!
+       -- it must allow foralls in the type it unifies with (hence ReturnTv)!
        --
        -- The result type can have any kind (Trac #8739),
        -- so we can just use res_ty
 
        -- ($) :: forall (a:*) (b:Open). (a->b) -> a -> b
-       ; a_ty <- newPolyFlexiTyVarTy
+       ; a_tv <- newReturnTyVar liftedTypeKind
+       ; let a_ty = mkTyVarTy a_tv
+
        ; arg2' <- tcArg op (arg2, arg2_ty, 2)
 
        ; co_a   <- unifyType arg2_ty   a_ty      -- arg2 ~ a
@@ -936,23 +931,6 @@ mk_app_msg :: LHsExpr Name -> SDoc
 mk_app_msg fun = sep [ ptext (sLit "The function") <+> quotes (ppr fun)
                      , ptext (sLit "is applied to")]
 
-----------------
-tcInferApp :: LHsExpr Name -> [LHsExpr Name] -- Function and args
-           -> TcM (HsExpr TcId, TcRhoType) -- Translated fun and args
-
-tcInferApp (L _ (HsPar e))     args = tcInferApp e args
-tcInferApp (L _ (HsApp e1 e2)) args = tcInferApp e1 (e2:args)
-tcInferApp fun args
-  = -- Very like the tcApp version, except that there is
-    -- no expected result type passed in
-    do  { (fun1, fun_tau) <- tcInferFun fun
-        ; (co_fun, expected_arg_tys, actual_res_ty)
-              <- matchExpectedFunTys (mk_app_msg fun) (length args) fun_tau
-        ; args1 <- tcArgs fun args expected_arg_tys
-        ; let fun2 = mkLHsWrapCo co_fun fun1
-              app  = foldl mkHsApp fun2 args1
-        ; return (unLoc app, actual_res_ty) }
-
 ----------------
 tcInferFun :: LHsExpr Name -> TcM (LHsExpr TcId, TcRhoType)
 -- Infer and instantiate the type of a function

compiler/typecheck/TcMType.lhs

@@ -19,12 +19,12 @@ module TcMType (
   newFlexiTyVar,
   newFlexiTyVarTy,              -- Kind -> TcM TcType
   newFlexiTyVarTys,             -- Int -> Kind -> TcM [TcType]
-  newPolyFlexiTyVarTy,
+  newReturnTyVar,
   newMetaKindVar, newMetaKindVars,
   mkTcTyVarName, cloneMetaTyVar,
 
   newMetaTyVar, readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef,
-  newMetaDetails, isFilledMetaTyVar, isFlexiMetaTyVar,
+  newMetaDetails, isFilledMetaTyVar, isUnfilledMetaTyVar,
 
   --------------------------------
   -- Creating new evidence variables
@@ -311,7 +311,7 @@ newMetaTyVar meta_info kind
   = do  { uniq <- newUnique
         ; let name = mkTcTyVarName uniq s
               s = case meta_info of
-                        PolyTv     -> fsLit "s"
+                        ReturnTv   -> fsLit "r"
                         TauTv      -> fsLit "t"
                         FlatMetaTv -> fsLit "fmv"
                         SigTv      -> fsLit "a"
@@ -363,9 +363,9 @@ isFilledMetaTyVar tv
         ; return (isIndirect details) }
   | otherwise = return False
 
-isFlexiMetaTyVar :: TyVar -> TcM Bool
+isUnfilledMetaTyVar :: TyVar -> TcM Bool
 -- True of a un-filled-in (Flexi) meta type variable
-isFlexiMetaTyVar tv
+isUnfilledMetaTyVar tv
   | not (isTcTyVar tv) = return False
   | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
   = do  { details <- readMutVar ref
@@ -448,9 +448,8 @@ newFlexiTyVarTy kind = do
 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
 newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
 
-newPolyFlexiTyVarTy :: TcM TcType
-newPolyFlexiTyVarTy = do { tv <- newMetaTyVar PolyTv liftedTypeKind
-                         ; return (TyVarTy tv) }
+newReturnTyVar :: Kind -> TcM TcTyVar
+newReturnTyVar kind = newMetaTyVar ReturnTv kind
 
 tcInstTyVars :: [TKVar] -> TcM (TvSubst, [TcTyVar])
 -- Instantiate with META type variables

compiler/typecheck/TcType.lhs

@@ -269,6 +269,35 @@ Similarly consider
 When doing kind inference on {S,T} we don't want *skolems* for k1,k2,
 because they end up unifying; we want those SigTvs again.
 
+Note [ReturnTv]
+~~~~~~~~~~~~~~~
+We sometimes want to convert a checking algorithm into an inference
+algorithm. An easy way to do this is to "check" that a term has a
+metavariable as a type. But, we must be careful to allow that metavariable
+to unify with *anything*. (Well, anything that doesn't fail an occurs-check.)
+This is what ReturnTv means.
+
+For example, if we have
+
+  (undefined :: (forall a. TF1 a ~ TF2 a => a)) x
+
+we'll call (tcInfer . tcExpr) on the function expression. tcInfer will
+create a ReturnTv to represent the expression's type. We really need this
+ReturnTv to become set to (forall a. TF1 a ~ TF2 a => a) despite the fact
+that this type mentions type families and is a polytype.
+
+However, we must also be careful to make sure that the ReturnTvs really
+always do get unified with something -- we don't want these floating
+around in the solver. So, we check after running the checker to make
+sure the ReturnTv is filled. If it's not, we set it to a TauTv.
+
+We can't ASSERT that no ReturnTvs hit the solver, because they
+can if there's, say, a kind error that stops checkTauTvUpdate from
+working. This happens in test case typecheck/should_fail/T5570, for
+example.
+
+See also the commentary on #9404.
+
 \begin{code}
 -- A TyVarDetails is inside a TyVar
 data TcTyVarDetails
@@ -307,7 +336,9 @@ data MetaInfo
                    -- A TauTv is always filled in with a tau-type, which
                    -- never contains any ForAlls
 
-   | PolyTv        -- Like TauTv, but can unify with a sigma-type
+   | ReturnTv      -- Can unify with *anything*. Used to convert a
+                   -- type "checking" algorithm into a type inference algorithm.
+                   -- See Note [ReturnTv]
 
    | SigTv         -- A variant of TauTv, except that it should not be
                    -- unified with a type, only with a type variable
@@ -481,7 +512,7 @@ pprTcTyVarDetails (MetaTv { mtv_info = info, mtv_untch = untch })
   = pp_info <> colon <> ppr untch
   where
     pp_info = case info of
-                PolyTv     -> ptext (sLit "poly")
+                ReturnTv   -> ptext (sLit "return")
                 TauTv      -> ptext (sLit "tau")
                 SigTv      -> ptext (sLit "sig")
                 FlatMetaTv -> ptext (sLit "fuv")
@@ -1133,7 +1164,7 @@ occurCheckExpand :: DynFlags -> TcTyVar -> Type -> OccCheckResult Type
 -- Check whether
 --   a) the given variable occurs in the given type.
 --   b) there is a forall in the type (unless we have -XImpredicativeTypes
---                                     or it's a PolyTv
+--                                     or it's a ReturnTv
 --   c) if it's a SigTv, ty should be a tyvar
 --
 -- We may have needed to do some type synonym unfolding in order to
@@ -1152,13 +1183,13 @@ occurCheckExpand dflags tv ty
 
     impredicative
       = case details of
-          MetaTv { mtv_info = PolyTv } -> True
-          MetaTv { mtv_info = SigTv }  -> False
-          MetaTv { mtv_info = TauTv }  -> xopt Opt_ImpredicativeTypes dflags
-                                       || isOpenTypeKind (tyVarKind tv)
+          MetaTv { mtv_info = ReturnTv } -> True
+          MetaTv { mtv_info = SigTv }    -> False
+          MetaTv { mtv_info = TauTv }    -> xopt Opt_ImpredicativeTypes dflags
+                                         || isOpenTypeKind (tyVarKind tv)
                                           -- Note [OpenTypeKind accepts foralls]
                                           -- in TcUnify
-          _other                       -> True
+          _other                         -> True
           -- We can have non-meta tyvars in given constraints
 
     -- Check 'ty' is a tyvar, or can be expanded into one

compiler/typecheck/TcUnify.lhs

@@ -46,6 +46,7 @@ import TyCon
 import TysWiredIn
 import Var
 import VarEnv
+import VarSet
 import ErrUtils
 import DynFlags
 import BasicTypes
@@ -338,10 +339,19 @@ tcSubType origin ctxt ty_actual ty_expected
                       PatSigOrigin -> TypeEqOrigin { uo_actual = ty2, uo_expected = ty1 }
                       _other       -> TypeEqOrigin { uo_actual = ty1, uo_expected = ty2 }
 
+-- | Infer a type using a type "checking" function by passing in a ReturnTv,
+-- which can unify with *anything*. See also Note [ReturnTv] in TcType
 tcInfer :: (TcType -> TcM a) -> TcM (a, TcType)
-tcInfer tc_infer = do { ty  <- newFlexiTyVarTy openTypeKind
-                      ; res <- tc_infer ty
-                      ; return (res, ty) }
+tcInfer tc_check
+  = do { tv  <- newReturnTyVar openTypeKind
+       ; let ty = mkTyVarTy tv
+       ; res <- tc_check ty
+       ; whenM (isUnfilledMetaTyVar tv) $  -- checking was uninformative
+         do { traceTc "Defaulting an un-filled ReturnTv to a TauTv" empty
+            ; tau_ty <- newFlexiTyVarTy openTypeKind
+            ; writeMetaTyVar tv tau_ty }
+       ; return (res, ty) }
+  where
 
 -----------------
 tcWrapResult :: HsExpr TcId -> TcRhoType -> TcRhoType -> TcM (HsExpr TcId)
@@ -844,7 +854,7 @@ nicer_to_update_tv1 tv1 _     _     = isSystemName (Var.varName tv1)
 ----------------
 checkTauTvUpdate :: DynFlags -> TcTyVar -> TcType -> TcM (Maybe TcType)
 --    (checkTauTvUpdate tv ty)
--- We are about to update the TauTv/PolyTv tv with ty.
+-- We are about to update the TauTv/ReturnTv tv with ty.
 -- Check (a) that tv doesn't occur in ty (occurs check)
 --       (b) that kind(ty) is a sub-kind of kind(tv)
 --
@@ -873,6 +883,9 @@ checkTauTvUpdate dflags tv ty
        ; case sub_k of
            Nothing           -> return Nothing
            Just LT           -> return Nothing
+           _  | is_return_tv -> if tv `elemVarSet` tyVarsOfType ty
+                                then return Nothing
+                                else return (Just ty1)
            _  | defer_me ty1   -- Quick test
               -> -- Failed quick test so try harder
                  case occurCheckExpand dflags tv ty1 of
@@ -882,11 +895,12 @@ checkTauTvUpdate dflags tv ty
               | otherwise   -> return (Just ty1) }
   where
     info = ASSERT2( isMetaTyVar tv, ppr tv ) metaTyVarInfo tv
+      -- See Note [ReturnTv] in TcType
+    is_return_tv = case info of { ReturnTv -> True; _ -> False }
 
     impredicative = xopt Opt_ImpredicativeTypes dflags
                  || isOpenTypeKind (tyVarKind tv)
                        -- Note [OpenTypeKind accepts foralls]
-                 || case info of { PolyTv -> True;  _ -> False }
 
     defer_me :: TcType -> Bool
     -- Checks for (a) occurrence of tv
@@ -917,7 +931,6 @@ we can instantiate it with Int#.  So we also allow such type variables
 to be instantiate with foralls.  It's a bit of a hack, but seems
 straightforward.
 
-
 Note [Conservative unification check]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 When unifying (tv ~ rhs), w try to avoid creating deferred constraints

compiler/utils/MonadUtils.hs

@@ -21,6 +21,7 @@ module MonadUtils
         , anyM, allM
         , foldlM, foldlM_, foldrM
         , maybeMapM
+        , whenM
         ) where
 
 -------------------------------------------------------------------------------
@@ -149,3 +150,8 @@ foldrM k z (x:xs) = do { r <- foldrM k z xs; k x r }
 maybeMapM :: Monad m => (a -> m b) -> (Maybe a -> m (Maybe b))
 maybeMapM _ Nothing  = return Nothing
 maybeMapM m (Just x) = liftM Just $ m x
+
+-- | Monadic version of @when@, taking the condition in the monad
+whenM :: Monad m => m Bool -> m () -> m ()
+whenM mb thing = do { b <- mb
+                    ; when b thing }

testsuite/tests/typecheck/should_compile/all.T

@@ -422,5 +422,6 @@ test('T8856', normal, compile, [''])
 test('T9117', normal, compile, [''])
 test('T9117_2', expect_broken('9117'), compile, [''])
 test('T9708', normal, compile_fail, [''])
-test('T9404', expect_broken(9404), compile, [''])
-test('T9404b', expect_broken(9404), compile, [''])
+test('T9404', normal, compile, [''])
+test('T9404b', normal, compile, [''])
+test('T7220', normal, compile, [''])

testsuite/tests/typecheck/should_fail/T7220.stderr

-
-T7220.hs:24:6:
-    Cannot instantiate unification variable ‘b0’
-    with a type involving foralls: forall b. (C A b, TF b ~ Y) => b
-      Perhaps you want ImpredicativeTypes
-    In the expression: f :: (forall b. (C A b, TF b ~ Y) => b) -> X
-    In the expression: (f :: (forall b. (C A b, TF b ~ Y) => b) -> X) u
-    In an equation for ‘v’:
-        v = (f :: (forall b. (C A b, TF b ~ Y) => b) -> X) u

testsuite/tests/typecheck/should_fail/all.T

@@ -291,7 +291,6 @@ test('T6161', normal, compile_fail, [''])
 test('T7368', normal, compile_fail, [''])
 test('T7264', normal, compile_fail, [''])
 test('T6069', normal, compile_fail, [''])
-test('T7220', normal, compile_fail, [''])
 test('T7410', normal, compile_fail, [''])
 test('T7453', normal, compile_fail, [''])
 test('T7525', normal, compile_fail, [''])