From ffde234854f49dba9ec4735aad74b30fd2deee29 Mon Sep 17 00:00:00 2001
From: Simon Peyton Jones <simonpj@microsoft.com>
Date: Wed, 8 Apr 2020 23:08:12 +0100
Subject: Do eager instantation in terms

This patch implements eager instantiation, a small but critical change
to the type inference engine, #17173.  The main change is this:

  When inferring types, always return an instantiated type
  (for now, deeply instantiated; in future shallowly instantiated)

There is more discussion in
https://www.tweag.io/posts/2020-04-02-lazy-eager-instantiation.html

There is quite a bit of refactoring in this patch:

* The ir_inst field of GHC.Tc.Utils.TcType.InferResultk
  has entirely gone.  So tcInferInst and tcInferNoInst have collapsed
  into tcInfer.

* Type inference of applications, via tcInferApp and
  tcInferAppHead, are substantially refactored, preparing
  the way for Quick Look impredicativity.

* New pure function GHC.Tc.Gen.Expr.collectHsArgs and applyHsArgs
  are beatifully dual.  We can see the zipper!

* GHC.Tc.Gen.Expr.tcArgs is now much nicer; no longer needs to return
  a wrapper

* In HsExpr, HsTypeApp now contains the the actual type argument,
  and is used in desugaring, rather than putting it in a mysterious
  wrapper.

* I struggled a bit with good error reporting in
  Unify.matchActualFunTysPart. It's a little bit simpler than before,
  but still not great.

Some smaller things

* Rename tcPolyExpr --> tcCheckExpr
         tcMonoExpr --> tcLExpr
* tcPatSig moves from GHC.Tc.Gen.HsType to GHC.Tc.Gen.Pat

Metric Decrease:
    T9961

Reduction of 1.6% in comiler allocation on T9961, I think.
---
 compiler/GHC/Tc/Module.hs | 38 ++++++++++++++++++++++++++++----------
 1 file changed, 28 insertions(+), 10 deletions(-)

(limited to 'compiler/GHC/Tc/Module.hs')

diff --git a/compiler/GHC/Tc/Module.hs b/compiler/GHC/Tc/Module.hs
index 17f2dd69d5..cc3bf4a2cc 100644
--- a/compiler/GHC/Tc/Module.hs
+++ b/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
@@ -1785,8 +1784,8 @@ check_main dflags tcg_env explicit_mod_hdr export_ies
         ; (ev_binds, main_expr)
                <- checkConstraints skol_info [] [] $
                   addErrCtxt mainCtxt    $
-                  tcMonoExpr (L loc (HsVar noExtField (L loc main_name)))
-                             (mkCheckExpType io_ty)
+                  tcLExpr (L loc (HsVar noExtField (L loc main_name)))
+                          (mkCheckExpType io_ty)
 
                 -- See Note [Root-main Id]
                 -- Construct the binding
@@ -2491,15 +2490,11 @@ 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 } ;
-    ((tclvl, res_ty), lie)
+    let { fresh_it  = itName uniq (getLoc rdr_expr) } ;
+    ((tclvl, (_tc_expr, 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 } ;
+             tc_infer rn_expr ;
 
     -- Generalise
     (qtvs, dicts, _, residual, _)
@@ -2525,12 +2520,35 @@ tcRnExpr hsc_env mode rdr_expr
     return (snd (normaliseType fam_envs Nominal ty))
     }
   where
+    tc_infer expr | inst      = tcInferRho expr
+                  | otherwise = tcInferSigma expr
+                  -- tcInferSigma: see Note [Implementing :type]
+
     -- See Note [TcRnExprMode]
     (inst, infer_mode, perhaps_disable_default_warnings) = case mode of
       TM_Inst    -> (True,  NoRestrictions, id)
       TM_NoInst  -> (False, NoRestrictions, id)
       TM_Default -> (True,  EagerDefaulting, unsetWOptM Opt_WarnTypeDefaults)
 
+{- Note [Implementing :type]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider   :type const
+
+We want    forall a b. a -> b -> a
+and not    forall {a}{b}. a -> b -> a
+
+The latter is what we'd get if we eagerly instantiated and then
+re-generalised with Inferred binders.  It makes a difference, because
+it tells us we where we can use Visible Type Application (VTA).
+
+And also for   :type const @Int
+we want        forall b. Int -> b -> Int
+and not        forall {b}. Int -> b -> Int
+
+Solution: use tcInferSigma, which in turn uses tcInferApp, which
+has a special case for application chains.
+-}
+
 --------------------------
 tcRnImportDecls :: HscEnv
                 -> [LImportDecl GhcPs]
-- 
cgit v1.2.1