[Git][ghc/ghc][wip/T17173] Do eager instantation in terms

Simon Peyton Jones gitlab at gitlab.haskell.org
Thu Apr 9 13:34:39 UTC 2020



Simon Peyton Jones pushed to branch wip/T17173 at Glasgow Haskell Compiler / GHC


Commits:
8531783a by Simon Peyton Jones at 2020-04-09T14:33:55+01:00
Do eager instantation in terms

This is a first draft of a patch for #17173.

It will need a proper commit message before we are done!

- - - - -


14 changed files:

- compiler/GHC/Tc/Gen/Arrow.hs
- compiler/GHC/Tc/Gen/Bind.hs
- compiler/GHC/Tc/Gen/Expr.hs
- compiler/GHC/Tc/Gen/Expr.hs-boot
- compiler/GHC/Tc/Gen/HsType.hs
- compiler/GHC/Tc/Gen/Match.hs
- compiler/GHC/Tc/Gen/Pat.hs
- compiler/GHC/Tc/Module.hs
- compiler/GHC/Tc/TyCl/PatSyn.hs
- compiler/GHC/Tc/Utils/Monad.hs
- compiler/GHC/Tc/Utils/Unify.hs
- testsuite/tests/quantified-constraints/T17458.stderr
- testsuite/tests/typecheck/should_compile/T18005.hs
- testsuite/tests/typecheck/should_fail/T3176.stderr


Changes:

=====================================
compiler/GHC/Tc/Gen/Arrow.hs
=====================================
@@ -91,7 +91,7 @@ tcProc pat cmd exp_ty
         ; (co, (exp_ty1, res_ty)) <- matchExpectedAppTy exp_ty
         ; (co1, (arr_ty, arg_ty)) <- matchExpectedAppTy exp_ty1
         ; let cmd_env = CmdEnv { cmd_arr = arr_ty }
-        ; (pat', cmd') <- tcPat ProcExpr pat (mkCheckExpType arg_ty) $
+        ; (pat', cmd') <- tcCheckPat ProcExpr pat arg_ty $
                           tcCmdTop cmd_env cmd (unitTy, res_ty)
         ; let res_co = mkTcTransCo co
                          (mkTcAppCo co1 (mkTcNomReflCo res_ty))
@@ -371,7 +371,7 @@ tcArrDoStmt env _ (BodyStmt _ rhs _ _) res_ty thing_inside
 
 tcArrDoStmt env ctxt (BindStmt _ pat rhs _ _) res_ty thing_inside
   = do  { (rhs', pat_ty) <- tc_arr_rhs env rhs
-        ; (pat', thing)  <- tcPat (StmtCtxt ctxt) pat (mkCheckExpType pat_ty) $
+        ; (pat', thing)  <- tcCheckPat (StmtCtxt ctxt) pat pat_ty $
                             thing_inside res_ty
         ; return (mkTcBindStmt pat' rhs', thing) }
 


=====================================
compiler/GHC/Tc/Gen/Bind.hs
=====================================
@@ -1366,7 +1366,7 @@ tcLhs sig_fn no_gen (PatBind { pat_lhs = pat, pat_rhs = grhss })
             -- See Note [Existentials in pattern bindings]
         ; ((pat', nosig_mbis), pat_ty)
             <- addErrCtxt (patMonoBindsCtxt pat grhss) $
-               tcInferNoInst $ \ exp_ty ->
+               tcInferInst $ \ exp_ty ->   -- The ir_inst field is irrelevant for patterns
                tcLetPat inst_sig_fun no_gen pat exp_ty $
                mapM lookup_info nosig_names
 


=====================================
compiler/GHC/Tc/Gen/Expr.hs
=====================================
@@ -14,14 +14,9 @@
 -- | Typecheck an expression
 module GHC.Tc.Gen.Expr
    ( tcPolyExpr
-   , tcMonoExpr
-   , tcMonoExprNC
-   , tcInferSigma
-   , tcInferSigmaNC
-   , tcInferRho
-   , tcInferRhoNC
-   , tcSyntaxOp
-   , tcSyntaxOpGen
+   , tcMonoExpr, tcMonoExprNC
+   , tcInferRho, tcInferRhoNC, tcInferAppHead
+   , tcSyntaxOp, tcSyntaxOpGen
    , SyntaxOpType(..)
    , synKnownType
    , tcCheckId
@@ -151,25 +146,14 @@ tcMonoExprNC (L loc expr) res_ty
         ; return (L loc expr') }
 
 ---------------
-tcInferSigma, tcInferSigmaNC :: LHsExpr GhcRn -> TcM ( LHsExpr GhcTcId
-                                                    , TcSigmaType )
--- Infer a *sigma*-type.
-tcInferSigma expr = addErrCtxt (exprCtxt expr) (tcInferSigmaNC expr)
-
-tcInferSigmaNC (L loc expr)
-  = setSrcSpan loc $
-    do { (expr', sigma) <- tcInferNoInst (tcExpr expr)
-       ; return (L loc expr', sigma) }
-
 tcInferRho, tcInferRhoNC :: LHsExpr GhcRn -> TcM (LHsExpr GhcTcId, TcRhoType)
 -- Infer a *rho*-type. The return type is always (shallowly) instantiated.
 tcInferRho expr = addErrCtxt (exprCtxt expr) (tcInferRhoNC expr)
 
-tcInferRhoNC expr
-  = do { (expr', sigma) <- tcInferSigmaNC expr
-       ; (wrap, rho) <- topInstantiate (lexprCtOrigin expr) sigma
-       ; return (mkLHsWrap wrap expr', rho) }
-
+tcInferRhoNC (L loc expr)
+  = setSrcSpan loc $
+    do { (expr', rho) <- tcInferInst (tcExpr expr)
+       ; return (L loc expr', rho) }
 
 {-
 ************************************************************************
@@ -281,13 +265,9 @@ tcExpr e@(HsLamCase x matches) res_ty
               , text "requires"]
     match_ctxt = MC { mc_what = CaseAlt, mc_body = tcBody }
 
-tcExpr e@(ExprWithTySig _ expr sig_ty) res_ty
-  = do { let loc = getLoc (hsSigWcType sig_ty)
-       ; sig_info <- checkNoErrs $  -- Avoid error cascade
-                     tcUserTypeSig loc sig_ty Nothing
-       ; (expr', poly_ty) <- tcExprSig expr sig_info
-       ; let expr'' = ExprWithTySig noExtField expr' sig_ty
-       ; tcWrapResult e expr'' poly_ty res_ty }
+tcExpr e@(ExprWithTySig _ expr hs_ty) res_ty
+  = do { (expr', poly_ty) <- tcExprWithSig expr hs_ty
+       ; tcWrapResult e expr' poly_ty res_ty }
 
 {-
 Note [Type-checking overloaded labels]
@@ -352,7 +332,7 @@ tcExpr expr@(OpApp fix arg1 op arg2) res_ty
   | (L loc (HsVar _ (L lv op_name))) <- op
   , op_name `hasKey` dollarIdKey        -- Note [Typing rule for ($)]
   = do { traceTc "Application rule" (ppr op)
-       ; (arg1', arg1_ty) <- tcInferSigma arg1
+       ; (arg1', arg1_ty) <- tcInferAppHead arg1
 
        ; let doc   = text "The first argument of ($) takes"
              orig1 = lexprCtOrigin arg1
@@ -413,7 +393,7 @@ tcExpr expr@(OpApp fix arg1 op arg2) res_ty
 --      \ x -> op x expr
 
 tcExpr expr@(SectionR x op arg2) res_ty
-  = do { (op', op_ty) <- tcInferFun op
+  = do { (op', op_ty) <- tcInferAppHead op
        ; (wrap_fun, [arg1_ty, arg2_ty], op_res_ty)
                   <- matchActualFunTys (mk_op_msg op) fn_orig (Just (unLoc op)) 2 op_ty
        ; wrap_res <- tcSubTypeHR SectionOrigin (Just expr)
@@ -428,7 +408,7 @@ tcExpr expr@(SectionR x op arg2) res_ty
     -- See #13285
 
 tcExpr expr@(SectionL x arg1 op) res_ty
-  = do { (op', op_ty) <- tcInferFun op
+  = do { (op', op_ty) <- tcInferAppHead op
        ; dflags <- getDynFlags      -- Note [Left sections]
        ; let n_reqd_args | xopt LangExt.PostfixOperators dflags = 1
                          | otherwise                            = 2
@@ -1009,6 +989,23 @@ tcExpr other _ = pprPanic "tcMonoExpr" (ppr other)
   -- Include ArrForm, ArrApp, which shouldn't appear at all
   -- Also HsTcBracketOut, HsQuasiQuoteE
 
+
+{- *********************************************************************
+*                                                                      *
+             Expression with type signature e::ty
+*                                                                      *
+********************************************************************* -}
+
+tcExprWithSig :: LHsExpr GhcRn -> LHsSigWcType (NoGhcTc GhcRn)
+              -> TcM (HsExpr GhcTc, TcSigmaType)
+tcExprWithSig expr hs_ty
+  = do { sig_info <- checkNoErrs $  -- Avoid error cascade
+                     tcUserTypeSig loc hs_ty Nothing
+       ; (expr', poly_ty) <- tcExprSig expr sig_info
+       ; return (ExprWithTySig noExtField expr' hs_ty, poly_ty) }
+  where
+    loc = getLoc (hsSigWcType hs_ty)
+
 {-
 ************************************************************************
 *                                                                      *
@@ -1147,7 +1144,7 @@ tcApp _m_herald (L loc (HsVar _ (L _ fun_id))) args res_ty
     n_val_args = count isHsValArg args
 
 tcApp m_herald fun args res_ty
-  = do { (tc_fun, fun_ty) <- tcInferFun fun
+  = do { (tc_fun, fun_ty) <- tcInferAppHead fun
        ; tcFunApp m_herald fun tc_fun fun_ty args res_ty }
 
 ---------------------
@@ -1198,23 +1195,27 @@ mk_op_msg :: LHsExpr GhcRn -> SDoc
 mk_op_msg op = text "The operator" <+> quotes (ppr op) <+> text "takes"
 
 ----------------
-tcInferFun :: LHsExpr GhcRn -> TcM (LHsExpr GhcTcId, TcSigmaType)
--- Infer type of a function
-tcInferFun (L loc (HsVar _ (L _ name)))
-  = do { (fun, ty) <- setSrcSpan loc (tcInferId name)
-               -- Don't wrap a context around a plain Id
-       ; return (L loc fun, ty) }
-
-tcInferFun (L loc (HsRecFld _ f))
-  = do { (fun, ty) <- setSrcSpan loc (tcInferRecSelId f)
-               -- Don't wrap a context around a plain Id
-       ; return (L loc fun, ty) }
-
-tcInferFun fun
-  = tcInferSigma fun
-      -- NB: tcInferSigma; see GHC.Tc.Utils.Unify
-      -- Note [Deep instantiation of InferResult] in GHC.Tc.Utils.Unify
+tcInferAppHead :: LHsExpr GhcRn -> TcM (LHsExpr GhcTcId, TcSigmaType)
+-- Infer type of the head of an application,
+--   i.e. the 'f' in (f e1 ... en)
+-- We get back a SigmaType because we have special cases for
+--   * A bare identifier (just look it up)
+--     This case also covers a record selectro HsRecFld
+--   * An expression with a type signature (e :: ty)
+
+tcInferAppHead el@(L loc e)
+  = case e of
+      HsVar _ (L _ nm)        -> add_loc $ tcInferId nm
+      HsRecFld _ f            -> add_loc $ tcInferRecSelId f
+      ExprWithTySig _ e hs_ty -> add_loc_ctxt $ tcExprWithSig e hs_ty
+      _                       -> add_loc_ctxt $ tcInferInst (tcExpr e)
+  where
+    add_loc_ctxt thing = addErrCtxt (exprCtxt el) $
+                         add_loc thing
 
+    add_loc thing = setSrcSpan loc $
+                    do { (e', ty) <- thing
+                       ; return (L loc e', ty) }
 
 ----------------
 -- | Type-check the arguments to a function, possibly including visible type
@@ -1431,7 +1432,7 @@ tcSyntaxOpGen :: CtOrigin
               -> ([TcSigmaType] -> TcM a)
               -> TcM (a, SyntaxExprTc)
 tcSyntaxOpGen orig (SyntaxExprRn op) arg_tys res_ty thing_inside
-  = do { (expr, sigma) <- tcInferSigma $ noLoc op
+  = do { (expr, sigma) <- tcInferAppHead $ noLoc op
        ; traceTc "tcSyntaxOpGen" (ppr op $$ ppr expr $$ ppr sigma)
        ; (result, expr_wrap, arg_wraps, res_wrap)
            <- tcSynArgA orig sigma arg_tys res_ty $
@@ -1711,7 +1712,7 @@ tcCheckId name res_ty
        ; traceTc "tcCheckId" (vcat [ppr name, ppr actual_res_ty, ppr res_ty])
        ; addFunResCtxt False (HsVar noExtField (noLoc name)) actual_res_ty res_ty $
          tcWrapResultO (OccurrenceOf name) (HsVar noExtField (noLoc name)) expr
-                                                          actual_res_ty res_ty }
+                                           actual_res_ty res_ty }
 
 tcCheckRecSelId :: HsExpr GhcRn -> AmbiguousFieldOcc GhcRn -> ExpRhoType -> TcM (HsExpr GhcTcId)
 tcCheckRecSelId rn_expr f@(Unambiguous _ (L _ lbl)) res_ty


=====================================
compiler/GHC/Tc/Gen/Expr.hs-boot
=====================================
@@ -6,23 +6,15 @@ import GHC.Tc.Types        ( TcM )
 import GHC.Tc.Types.Origin ( CtOrigin )
 import GHC.Hs.Extension    ( GhcRn, GhcTcId )
 
-tcPolyExpr ::
-          LHsExpr GhcRn
-       -> TcSigmaType
-       -> TcM (LHsExpr GhcTcId)
-
-tcMonoExpr, tcMonoExprNC ::
-          LHsExpr GhcRn
-       -> ExpRhoType
-       -> TcM (LHsExpr GhcTcId)
-
-tcInferSigma ::
-          LHsExpr GhcRn
-       -> TcM (LHsExpr GhcTcId, TcSigmaType)
-
-tcInferRho, tcInferRhoNC ::
-          LHsExpr GhcRn
-       -> TcM (LHsExpr GhcTcId, TcRhoType)
+tcPolyExpr :: LHsExpr GhcRn -> TcSigmaType -> TcM (LHsExpr GhcTcId)
+
+tcMonoExpr, tcMonoExprNC
+  :: LHsExpr GhcRn -> ExpRhoType -> TcM (LHsExpr GhcTcId)
+
+tcInferRho, tcInferRhoNC
+  :: LHsExpr GhcRn-> TcM (LHsExpr GhcTcId, TcRhoType)
+
+tcInferAppHead :: LHsExpr GhcRn -> TcM (LHsExpr GhcTcId, TcSigmaType)
 
 tcSyntaxOp :: CtOrigin
            -> SyntaxExprRn


=====================================
compiler/GHC/Tc/Gen/HsType.hs
=====================================
@@ -60,7 +60,7 @@ module GHC.Tc.Gen.HsType (
         checkClassKindSig,
 
         -- Pattern type signatures
-        tcHsPatSigType, tcPatSig,
+        tcHsPatSigType,
 
         -- Error messages
         funAppCtxt, addTyConFlavCtxt
@@ -75,7 +75,6 @@ import GHC.Tc.Utils.Monad
 import GHC.Tc.Types.Origin
 import GHC.Core.Predicate
 import GHC.Tc.Types.Constraint
-import GHC.Tc.Types.Evidence
 import GHC.Tc.Utils.Env
 import GHC.Tc.Utils.TcMType
 import GHC.Tc.Validity
@@ -3345,58 +3344,6 @@ tcHsPatSigType ctxt sig_ty
 tcHsPatSigType _ (HsWC _ (XHsImplicitBndrs nec)) = noExtCon nec
 tcHsPatSigType _ (XHsWildCardBndrs nec)          = noExtCon nec
 
-tcPatSig :: Bool                    -- True <=> pattern binding
-         -> LHsSigWcType GhcRn
-         -> ExpSigmaType
-         -> TcM (TcType,            -- The type to use for "inside" the signature
-                 [(Name,TcTyVar)],  -- The new bit of type environment, binding
-                                    -- the scoped type variables
-                 [(Name,TcTyVar)],  -- The wildcards
-                 HsWrapper)         -- Coercion due to unification with actual ty
-                                    -- Of shape:  res_ty ~ sig_ty
-tcPatSig in_pat_bind sig res_ty
- = do  { (sig_wcs, sig_tvs, sig_ty) <- tcHsPatSigType PatSigCtxt sig
-        -- sig_tvs are the type variables free in 'sig',
-        -- and not already in scope. These are the ones
-        -- that should be brought into scope
-
-        ; if null sig_tvs then do {
-                -- Just do the subsumption check and return
-                  wrap <- addErrCtxtM (mk_msg sig_ty) $
-                          tcSubTypeET PatSigOrigin PatSigCtxt res_ty sig_ty
-                ; return (sig_ty, [], sig_wcs, wrap)
-        } else do
-                -- Type signature binds at least one scoped type variable
-
-                -- A pattern binding cannot bind scoped type variables
-                -- It is more convenient to make the test here
-                -- than in the renamer
-        { when in_pat_bind (addErr (patBindSigErr sig_tvs))
-
-        -- Now do a subsumption check of the pattern signature against res_ty
-        ; wrap <- addErrCtxtM (mk_msg sig_ty) $
-                  tcSubTypeET PatSigOrigin PatSigCtxt res_ty sig_ty
-
-        -- Phew!
-        ; return (sig_ty, sig_tvs, sig_wcs, wrap)
-        } }
-  where
-    mk_msg sig_ty tidy_env
-       = do { (tidy_env, sig_ty) <- zonkTidyTcType tidy_env sig_ty
-            ; res_ty <- readExpType res_ty   -- should be filled in by now
-            ; (tidy_env, res_ty) <- zonkTidyTcType tidy_env res_ty
-            ; let msg = vcat [ hang (text "When checking that the pattern signature:")
-                                  4 (ppr sig_ty)
-                             , nest 2 (hang (text "fits the type of its context:")
-                                          2 (ppr res_ty)) ]
-            ; return (tidy_env, msg) }
-
-patBindSigErr :: [(Name,TcTyVar)] -> SDoc
-patBindSigErr sig_tvs
-  = hang (text "You cannot bind scoped type variable" <> plural sig_tvs
-          <+> pprQuotedList (map fst sig_tvs))
-       2 (text "in a pattern binding signature")
-
 {- Note [Pattern signature binders]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 See also Note [Type variables in the type environment] in GHC.Tc.Utils.


=====================================
compiler/GHC/Tc/Gen/Match.hs
=====================================
@@ -422,8 +422,8 @@ tcGuardStmt _ (BodyStmt _ guard _ _) res_ty thing_inside
 tcGuardStmt ctxt (BindStmt _ pat rhs _ _) res_ty thing_inside
   = do  { (rhs', rhs_ty) <- tcInferRhoNC rhs
                                    -- Stmt has a context already
-        ; (pat', thing)  <- tcPat_O (StmtCtxt ctxt) (lexprCtOrigin rhs)
-                                    pat (mkCheckExpType rhs_ty) $
+        ; (pat', thing)  <- tcCheckPat_O (StmtCtxt ctxt) (lexprCtOrigin rhs)
+                                         pat rhs_ty $
                             thing_inside res_ty
         ; return (mkTcBindStmt pat' rhs', thing) }
 
@@ -456,7 +456,7 @@ tcLcStmt _ _ (LastStmt x body noret _) elt_ty thing_inside
 tcLcStmt m_tc ctxt (BindStmt _ pat rhs _ _) elt_ty thing_inside
  = do   { pat_ty <- newFlexiTyVarTy liftedTypeKind
         ; rhs'   <- tcMonoExpr rhs (mkCheckExpType $ mkTyConApp m_tc [pat_ty])
-        ; (pat', thing)  <- tcPat (StmtCtxt ctxt) pat (mkCheckExpType pat_ty) $
+        ; (pat', thing)  <- tcCheckPat (StmtCtxt ctxt) pat pat_ty $
                             thing_inside elt_ty
         ; return (mkTcBindStmt pat' rhs', thing) }
 
@@ -580,8 +580,7 @@ tcMcStmt ctxt (BindStmt _ pat rhs bind_op fail_op) res_ty thing_inside
                           [SynRho, SynFun SynAny SynRho] res_ty $
                \ [rhs_ty, pat_ty, new_res_ty] ->
                do { rhs' <- tcMonoExprNC rhs (mkCheckExpType rhs_ty)
-                  ; (pat', thing) <- tcPat (StmtCtxt ctxt) pat
-                                           (mkCheckExpType pat_ty) $
+                  ; (pat', thing) <- tcCheckPat (StmtCtxt ctxt) pat pat_ty $
                                      thing_inside (mkCheckExpType new_res_ty)
                   ; return (rhs', pat', thing, new_res_ty) }
 
@@ -840,8 +839,7 @@ tcDoStmt ctxt (BindStmt _ pat rhs bind_op fail_op) res_ty thing_inside
             <- tcSyntaxOp DoOrigin bind_op [SynRho, SynFun SynAny SynRho] res_ty $
                 \ [rhs_ty, pat_ty, new_res_ty] ->
                 do { rhs' <- tcMonoExprNC rhs (mkCheckExpType rhs_ty)
-                   ; (pat', thing) <- tcPat (StmtCtxt ctxt) pat
-                                            (mkCheckExpType pat_ty) $
+                   ; (pat', thing) <- tcCheckPat (StmtCtxt ctxt) pat pat_ty $
                                       thing_inside (mkCheckExpType new_res_ty)
                    ; return (rhs', pat', new_res_ty, thing) }
 
@@ -1038,7 +1036,7 @@ tcApplicativeStmts ctxt pairs rhs_ty thing_inside
       = setSrcSpan (combineSrcSpans (getLoc pat) (getLoc rhs)) $
         addErrCtxt (pprStmtInCtxt ctxt (mkBindStmt pat rhs))   $
         do { rhs' <- tcMonoExprNC rhs (mkCheckExpType exp_ty)
-           ; (pat', _) <- tcPat (StmtCtxt ctxt) pat (mkCheckExpType pat_ty) $
+           ; (pat', _) <- tcCheckPat (StmtCtxt ctxt) pat pat_ty $
                           return ()
            ; fail_op' <- tcMonadFailOp (DoPatOrigin pat) pat' fail_op body_ty
 
@@ -1054,7 +1052,7 @@ tcApplicativeStmts ctxt pairs rhs_ty thing_inside
                 tcStmtsAndThen ctxt tcDoStmt stmts (mkCheckExpType exp_ty) $
                 \res_ty  -> do
                   { L _ ret' <- tcMonoExprNC (noLoc ret) res_ty
-                  ; (pat', _) <- tcPat (StmtCtxt ctxt) pat (mkCheckExpType pat_ty) $
+                  ; (pat', _) <- tcCheckPat (StmtCtxt ctxt) pat pat_ty $
                                  return ()
                   ; return (ret', pat')
                   }


=====================================
compiler/GHC/Tc/Gen/Pat.hs
=====================================
@@ -16,8 +16,7 @@ module GHC.Tc.Gen.Pat
    ( tcLetPat
    , newLetBndr
    , LetBndrSpec(..)
-   , tcPat
-   , tcPat_O
+   , tcCheckPat, tcCheckPat_O, tcInferPat
    , tcPats
    , addDataConStupidTheta
    , badFieldCon
@@ -29,7 +28,7 @@ where
 
 import GhcPrelude
 
-import {-# SOURCE #-}   GHC.Tc.Gen.Expr( tcSyntaxOp, tcSyntaxOpGen, tcInferSigma )
+import {-# SOURCE #-}   GHC.Tc.Gen.Expr( tcSyntaxOp, tcSyntaxOpGen, tcInferAppHead )
 
 import GHC.Hs
 import GHC.Tc.Utils.Zonk
@@ -63,6 +62,7 @@ import Util
 import Outputable
 import qualified GHC.LanguageExtensions as LangExt
 import Control.Arrow  ( second )
+import Control.Monad  ( when )
 import ListSetOps ( getNth )
 
 {-
@@ -112,20 +112,29 @@ tcPats ctxt pats pat_tys thing_inside
   where
     penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt, pe_orig = PatOrigin }
 
-tcPat :: HsMatchContext GhcRn
-      -> LPat GhcRn -> ExpSigmaType
-      -> TcM a                     -- Checker for body
-      -> TcM (LPat GhcTcId, a)
-tcPat ctxt = tcPat_O ctxt PatOrigin
+tcInferPat :: HsMatchContext GhcRn -> LPat GhcRn
+           -> TcM a
+           -> TcM ((LPat GhcTcId, a), TcSigmaType)
+tcInferPat ctxt pat thing_inside
+  = tcInferInst $ \ exp_ty ->    -- The ir_inst flag is irrelevant in tcPat
+    tc_lpat pat exp_ty penv thing_inside
+ where
+    penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt, pe_orig = PatOrigin }
+
+tcCheckPat :: HsMatchContext GhcRn
+           -> LPat GhcRn -> TcSigmaType
+           -> TcM a                     -- Checker for body
+           -> TcM (LPat GhcTcId, a)
+tcCheckPat ctxt = tcCheckPat_O ctxt PatOrigin
 
 -- | A variant of 'tcPat' that takes a custom origin
-tcPat_O :: HsMatchContext GhcRn
-        -> CtOrigin              -- ^ origin to use if the type needs inst'ing
-        -> LPat GhcRn -> ExpSigmaType
-        -> TcM a                 -- Checker for body
-        -> TcM (LPat GhcTcId, a)
-tcPat_O ctxt orig pat pat_ty thing_inside
-  = tc_lpat pat pat_ty penv thing_inside
+tcCheckPat_O :: HsMatchContext GhcRn
+             -> CtOrigin              -- ^ origin to use if the type needs inst'ing
+             -> LPat GhcRn -> TcSigmaType
+             -> TcM a                 -- Checker for body
+             -> TcM (LPat GhcTcId, a)
+tcCheckPat_O ctxt orig pat pat_ty thing_inside
+  = tc_lpat pat (mkCheckExpType pat_ty) penv thing_inside
   where
     penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt, pe_orig = orig }
 
@@ -390,22 +399,25 @@ tc_pat penv (AsPat x (L nm_loc name) pat) pat_ty thing_inside
 
 tc_pat penv (ViewPat _ expr pat) overall_pat_ty thing_inside
   = do  {
-         -- Expr must have type `forall a1...aN. OPT' -> B`
-         -- where overall_pat_ty is an instance of OPT'.
-        ; (expr',expr'_inferred) <- tcInferSigma expr
-
-         -- expression must be a function
+         -- Using tcInferAppHead here, rather than tcMonoExpr, lets us
+         -- have view functions with types like:
+         --    (forall a. blah) -> forall b. burble
+         -- So the overall_pat_ty is (forall a. blah), while the
+         -- inner pattern is checked with (forall b. burble)
+        ; (expr',expr_ty) <- tcInferAppHead expr
+
+         -- Expression must be a function
         ; let expr_orig = lexprCtOrigin expr
               herald    = text "A view pattern expression expects"
         ; (expr_wrap1, [inf_arg_ty], inf_res_ty)
-            <- matchActualFunTys herald expr_orig (Just (unLoc expr)) 1 expr'_inferred
-            -- expr_wrap1 :: expr'_inferred "->" (inf_arg_ty -> inf_res_ty)
+            <- matchActualFunTys herald expr_orig (Just (unLoc expr)) 1 expr_ty
+            -- expr_wrap1 :: expr_ty "->" (inf_arg_ty -> inf_res_ty)
 
-         -- check that overall pattern is more polymorphic than arg type
+         -- Check that overall pattern is more polymorphic than arg type
         ; expr_wrap2 <- tcSubTypePat penv overall_pat_ty inf_arg_ty
             -- expr_wrap2 :: overall_pat_ty "->" inf_arg_ty
 
-         -- pattern must have inf_res_ty
+         -- Pattern must have inf_res_ty
         ; (pat', res) <- tc_lpat pat (mkCheckExpType inf_res_ty) penv thing_inside
 
         ; overall_pat_ty <- readExpType overall_pat_ty
@@ -665,6 +677,66 @@ because they won't be in scope when we do the desugaring
 
 
 ************************************************************************
+*                                                                      *
+            Pattern signatures   (pat :: type)
+*                                                                      *
+************************************************************************
+-}
+
+tcPatSig :: Bool                    -- True <=> pattern binding
+         -> LHsSigWcType GhcRn
+         -> ExpSigmaType
+         -> TcM (TcType,            -- The type to use for "inside" the signature
+                 [(Name,TcTyVar)],  -- The new bit of type environment, binding
+                                    -- the scoped type variables
+                 [(Name,TcTyVar)],  -- The wildcards
+                 HsWrapper)         -- Coercion due to unification with actual ty
+                                    -- Of shape:  res_ty ~ sig_ty
+tcPatSig in_pat_bind sig res_ty
+ = do  { (sig_wcs, sig_tvs, sig_ty) <- tcHsPatSigType PatSigCtxt sig
+        -- sig_tvs are the type variables free in 'sig',
+        -- and not already in scope. These are the ones
+        -- that should be brought into scope
+
+        ; if null sig_tvs then do {
+                -- Just do the subsumption check and return
+                  wrap <- addErrCtxtM (mk_msg sig_ty) $
+                          tcSubTypeET PatSigOrigin PatSigCtxt res_ty sig_ty
+                ; return (sig_ty, [], sig_wcs, wrap)
+        } else do
+                -- Type signature binds at least one scoped type variable
+
+                -- A pattern binding cannot bind scoped type variables
+                -- It is more convenient to make the test here
+                -- than in the renamer
+        { when in_pat_bind (addErr (patBindSigErr sig_tvs))
+
+        -- Now do a subsumption check of the pattern signature against res_ty
+        ; wrap <- addErrCtxtM (mk_msg sig_ty) $
+                  tcSubTypeET PatSigOrigin PatSigCtxt res_ty sig_ty
+
+        -- Phew!
+        ; return (sig_ty, sig_tvs, sig_wcs, wrap)
+        } }
+  where
+    mk_msg sig_ty tidy_env
+       = do { (tidy_env, sig_ty) <- zonkTidyTcType tidy_env sig_ty
+            ; res_ty <- readExpType res_ty   -- should be filled in by now
+            ; (tidy_env, res_ty) <- zonkTidyTcType tidy_env res_ty
+            ; let msg = vcat [ hang (text "When checking that the pattern signature:")
+                                  4 (ppr sig_ty)
+                             , nest 2 (hang (text "fits the type of its context:")
+                                          2 (ppr res_ty)) ]
+            ; return (tidy_env, msg) }
+
+patBindSigErr :: [(Name,TcTyVar)] -> SDoc
+patBindSigErr sig_tvs
+  = hang (text "You cannot bind scoped type variable" <> plural sig_tvs
+          <+> pprQuotedList (map fst sig_tvs))
+       2 (text "in a pattern binding signature")
+
+
+{- *********************************************************************
 *                                                                      *
         Most of the work for constructors is here
         (the rest is in the ConPatIn case of tc_pat)


=====================================
compiler/GHC/Tc/Module.hs
=====================================
@@ -56,7 +56,6 @@ import GHC.Iface.Env     ( externaliseName )
 import GHC.Tc.Gen.HsType
 import GHC.Tc.Validity( checkValidType )
 import GHC.Tc.Gen.Match
-import GHC.Tc.Utils.Instantiate( deeplyInstantiate )
 import GHC.Tc.Utils.Unify( checkConstraints )
 import GHC.Rename.HsType
 import GHC.Rename.Expr
@@ -2492,15 +2491,12 @@ tcRnExpr hsc_env mode rdr_expr
         -- Now typecheck the expression, and generalise its type
         -- it might have a rank-2 type (e.g. :t runST)
     uniq <- newUnique ;
-    let { fresh_it  = itName uniq (getLoc rdr_expr)
-        ; orig = lexprCtOrigin rn_expr } ;
+    let { fresh_it  = itName uniq (getLoc rdr_expr) } ;
     ((tclvl, res_ty), lie)
           <- captureTopConstraints $
              pushTcLevelM          $
-             do { (_tc_expr, expr_ty) <- tcInferSigma rn_expr
-                ; if inst
-                  then snd <$> deeplyInstantiate orig expr_ty
-                  else return expr_ty } ;
+             do { (_tc_expr, expr_ty) <- tc_infer rn_expr
+                ; return expr_ty } ;
 
     -- Generalise
     (qtvs, dicts, _, residual, _)
@@ -2526,6 +2522,8 @@ tcRnExpr hsc_env mode rdr_expr
     return (snd (normaliseType fam_envs Nominal ty))
     }
   where
+    tc_infer | inst      = tcInferRhoNC
+             | otherwise = tcInferAppHead
     -- See Note [TcRnExprMode]
     (inst, infer_mode, perhaps_disable_default_warnings) = case mode of
       TM_Inst    -> (True,  NoRestrictions, id)


=====================================
compiler/GHC/Tc/TyCl/PatSyn.hs
=====================================
@@ -149,8 +149,7 @@ tcInferPatSynDecl (PSB { psb_id = lname@(L _ name), psb_args = details
        ; let (arg_names, rec_fields, is_infix) = collectPatSynArgInfo details
        ; (tclvl, wanted, ((lpat', args), pat_ty))
             <- pushLevelAndCaptureConstraints  $
-               tcInferNoInst                   $ \ exp_ty ->
-               tcPat PatSyn lpat exp_ty        $
+               tcInferPat PatSyn lpat          $
                mapM tcLookupId arg_names
 
        ; let (ex_tvs, prov_dicts) = tcCollectEx lpat'
@@ -389,9 +388,9 @@ tcCheckPatSynDecl psb at PSB{ psb_id = lname@(L _ name), psb_args = details
        ; req_dicts <- newEvVars req_theta
        ; (tclvl, wanted, (lpat', (ex_tvs', prov_dicts, args'))) <-
            ASSERT2( equalLength arg_names arg_tys, ppr name $$ ppr arg_names $$ ppr arg_tys )
-           pushLevelAndCaptureConstraints            $
-           tcExtendTyVarEnv univ_tvs                 $
-           tcPat PatSyn lpat (mkCheckExpType pat_ty) $
+           pushLevelAndCaptureConstraints   $
+           tcExtendTyVarEnv univ_tvs        $
+           tcCheckPat PatSyn lpat pat_ty    $
            do { let in_scope    = mkInScopeSet (mkVarSet univ_tvs)
                     empty_subst = mkEmptyTCvSubst in_scope
               ; (subst, ex_tvs') <- mapAccumLM newMetaTyVarX empty_subst ex_tvs


=====================================
compiler/GHC/Tc/Utils/Monad.hs
=====================================
@@ -835,9 +835,8 @@ addLocM :: (a -> TcM b) -> Located a -> TcM b
 addLocM fn (L loc a) = setSrcSpan loc $ fn a
 
 wrapLocM :: (a -> TcM b) -> Located a -> TcM (Located b)
--- wrapLocM :: (a -> TcM b) -> Located a -> TcM (Located b)
 wrapLocM fn (L loc a) = setSrcSpan loc $ do { b <- fn a
-                                                ; return (L loc b) }
+                                            ; return (L loc b) }
 
 wrapLocFstM :: (a -> TcM (b,c)) -> Located a -> TcM (Located b, c)
 wrapLocFstM fn (L loc a) =


=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -563,13 +563,9 @@ tcSubTypeET orig ctxt (Check ty_actual) ty_expected
                            , uo_visible  = True }
 
 tcSubTypeET _ _ (Infer inf_res) ty_expected
-  = ASSERT2( not (ir_inst inf_res), ppr inf_res $$ ppr ty_expected )
-      -- An (Infer inf_res) ExpSigmaType passed into tcSubTypeET never
-      -- has the ir_inst field set.  Reason: in patterns (which is what
-      -- tcSubTypeET is used for) do not aggressively instantiate
-    do { co <- fill_infer_result ty_expected inf_res
-               -- Since ir_inst is false, we can skip fillInferResult
-               -- and go straight to fill_infer_result
+  = do { co <- fillInferResult ty_expected inf_res
+               -- In patterns we ignore the ir_inst field
+               -- and never instantatiate
 
        ; return (mkWpCastN (mkTcSymCo co)) }
 
@@ -643,7 +639,7 @@ tcSubTypeDS_NC_O :: CtOrigin   -- origin used for instantiation only
 -- ty_expected is deeply skolemised
 tcSubTypeDS_NC_O inst_orig ctxt m_thing ty_actual ty_expected
   = case ty_expected of
-      Infer inf_res -> fillInferResult inst_orig ty_actual inf_res
+      Infer inf_res -> instantiateAndFillInferResult inst_orig ty_actual inf_res
       Check ty      -> tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty
          where
            eq_orig = TypeEqOrigin { uo_actual = ty_actual, uo_expected = ty
@@ -864,7 +860,7 @@ tcWrapResultO orig rn_expr expr actual_ty res_ty
 
 {- **********************************************************************
 %*                                                                      *
-            ExpType functions: tcInfer, fillInferResult
+            ExpType functions: tcInfer, instantiateAndFillInferResult
 %*                                                                      *
 %********************************************************************* -}
 
@@ -884,24 +880,24 @@ tcInfer instantiate tc_check
        ; res_ty <- readExpType res_ty
        ; return (result, res_ty) }
 
-fillInferResult :: CtOrigin -> TcType -> InferResult -> TcM HsWrapper
--- If wrap = fillInferResult t1 t2
+instantiateAndFillInferResult :: CtOrigin -> TcType -> InferResult -> TcM HsWrapper
+-- If wrap = instantiateAndFillInferResult t1 t2
 --    => wrap :: t1 ~> t2
 -- See Note [Deep instantiation of InferResult]
-fillInferResult orig ty inf_res@(IR { ir_inst = instantiate_me })
-  | instantiate_me
+instantiateAndFillInferResult orig ty inf_res@(IR { ir_inst = instantiate_me })
+  | instantiate_me   -- This is *the* place where ir_inst is consulted
   = do { (wrap, rho) <- deeplyInstantiate orig ty
-       ; co <- fill_infer_result rho inf_res
+       ; co <- fillInferResult rho inf_res
        ; return (mkWpCastN co <.> wrap) }
 
   | otherwise
-  = do { co <- fill_infer_result ty inf_res
+  = do { co <- fillInferResult ty inf_res
        ; return (mkWpCastN co) }
 
-fill_infer_result :: TcType -> InferResult -> TcM TcCoercionN
--- If wrap = fill_infer_result t1 t2
+fillInferResult :: TcType -> InferResult -> TcM TcCoercionN
+-- If wrap = fillInferResult t1 t2
 --    => wrap :: t1 ~> t2
-fill_infer_result orig_ty (IR { ir_uniq = u, ir_lvl = res_lvl
+fillInferResult orig_ty (IR { ir_uniq = u, ir_lvl = res_lvl
                             , ir_ref = ref })
   = do { (ty_co, ty_to_fill_with) <- promoteTcType res_lvl orig_ty
 


=====================================
testsuite/tests/quantified-constraints/T17458.stderr
=====================================
@@ -1,5 +1,5 @@
 
-T17458.hs:32:27: error:
+T17458.hs:32:32: error:
     • Reduction stack overflow; size = 201
       When simplifying the following type: Typeable Void
       Use -freduction-depth=0 to disable this check


=====================================
testsuite/tests/typecheck/should_compile/T18005.hs
=====================================
@@ -27,4 +27,5 @@ unT2b' :: T2b -> S2
 unT2b' (MkT2b x) = x
 
 pattern MkT2b' :: S2 -> T2b
-pattern MkT2b' {unT2b} <- (unT2b' -> unT2b)
+-- pattern MkT2b' {unT2b} <- (unT2b' -> unT2b)
+pattern MkT2b' x <- (unT2b' -> x)


=====================================
testsuite/tests/typecheck/should_fail/T3176.stderr
=====================================
@@ -1,7 +1,8 @@
 
-T3176.hs:9:27:
-    Cannot use record selector ‘unES’ as a function due to escaped type variables
-    Probable fix: use pattern-matching syntax instead
-    In the expression: unES
-    In the second argument of ‘($)’, namely ‘unES $ f t’
-    In the expression: show $ unES $ f t
+T3176.hs:9:27: error:
+    • Cannot use record selector ‘unES’ as a function due to escaped type variables
+      Probable fix: use pattern-matching syntax instead
+    • In the second argument of ‘($)’, namely ‘unES $ f t’
+      In the expression: show $ unES $ f t
+      In an equation for ‘smallPrintES’:
+          smallPrintES f t = show $ unES $ f t



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/8531783ae7eb9f2f8bc76508e16fd6fc5d00e844

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/8531783ae7eb9f2f8bc76508e16fd6fc5d00e844
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20200409/f1b9269d/attachment-0001.html>


More information about the ghc-commits mailing list