[commit: ghc] wip/T15809: Progress (3c9ce3e)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : wip/T15809
Link       : http://ghc.haskell.org/trac/ghc/changeset/3c9ce3e8ad62e8ae64a910f919605f7c2b05667e/ghc

>---------------------------------------------------------------

commit 3c9ce3e8ad62e8ae64a910f919605f7c2b05667e
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Fri Nov 9 18:11:25 2018 +0000

    Progress
    
    Allocate result kind outside tcImplicit in
    tc_hs_sig_type_and_gen
    
    Plus comments
    
    In flight.. may not build (but it's a wip/ branch)


>---------------------------------------------------------------

3c9ce3e8ad62e8ae64a910f919605f7c2b05667e
 compiler/typecheck/TcHsType.hs | 49 +++++++++++++++++++++---------------------
 compiler/typecheck/TcMType.hs  | 18 ++++------------
 2 files changed, 29 insertions(+), 38 deletions(-)

diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index dd2995e..7f5d4ff 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -229,19 +229,15 @@ tc_hs_sig_type_and_gen skol_info hs_sig_type ctxt_kind
   | HsIB { hsib_ext = sig_vars, hsib_body = hs_ty } <- hs_sig_type
   = do { (_inner_lvl, wanted, (tkvs, ty))
               <- pushLevelAndCaptureConstraints $
-                 tcImplicitTKBndrs skol_info sig_vars $
-                   -- tcImplicitTKBndrs does a solveLocalEqualities
-                 do { kind <- case ctxt_kind of
+                 do { -- See Note [Levels and generalisation]
+                      res_kind <- case ctxt_kind of
                         TheKind k -> return k
                         AnyKind   -> newMetaKindVar
                         OpenKind  -> newOpenTypeKind
-              -- The kind is checked by checkValidType, and isn't necessarily
-              -- of kind * in a Template Haskell quote eg [t| Maybe |]
 
-                    ; tc_lhs_type typeLevelMode hs_ty kind }
-         -- Any remaining variables (unsolved in the solveLocalEqualities
-         -- in the tcImplicitTKBndrs) should be in the global tyvars,
-         -- and therefore won't be quantified over
+                    ; tcImplicitTKBndrs skol_info sig_vars $
+                      -- tcImplicitTKBndrs does a solveLocalEqualities
+                      tc_lhs_type typeLevelMode hs_ty res_kind }
 
        ; let ty1 = mkSpecForAllTys tkvs ty
        ; kvs <- kindGeneralizeLocal wanted ty1
@@ -1467,20 +1463,6 @@ To avoid the double-zonk, we do two things:
  2. When we are generalizing:
     kindGeneralize does not require a zonked type -- it zonks as it
     gathers free variables. So this way effectively sidesteps step 3.
-
-Note [TcLevel for CUSKs]
-~~~~~~~~~~~~~~~~~~~~~~~~
-In getInitialKinds we are at level 1, busy making unification
-variables over which we will subsequently generalise.
-
-But when we find a CUSK we want to jump back to top level (0)
-because that's the right starting point for a completee,
-stand-alone kind signature.
-
-More precisely, we want to make level-1 skolems, because
-the end up as the TyConBinders of the TyCon, and are brought
-into scope when we type-check the body of the type declaration
-(in tcTyClDecl).
 -}
 
 tcWildCardBinders :: [Name]
@@ -2003,7 +1985,26 @@ kindGeneralizeLocal wanted kind_or_type
 
        ; quantifyTyVars mono_tvs dvs }
 
-{-
+{- Note [Levels and generalisation]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+  f x = e
+with no type signature. We are currently at level i.
+We must
+  * Push the level to level (i+1)
+  * Allocate a fresh alpha[i+1] for the result type
+  * Check that e :: alpha[i+1], gathering constraint WC
+  * Solve WC as far as possible
+  * Zonking the result type alpha[i+1], say to beta[i-1] -> gamma[i]
+  * Find the free variables with level > i, in this case gamma[i]
+  * Skolemise those free variables and quantify over them, giving
+       f :: forall g. beta[i-1] -> g
+  * Emit the residiual constraint wrapped in an implication for g,
+    thus   forall g. WC
+
+All of this happens for types too.  Consider
+  f :: Int -> (forall a. Proxy a -> Int)
+
 Note [Kind generalisation]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 We do kind generalisation only at the outer level of a type signature.
diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs
index 6d9f3ca..a1cdf24 100644
--- a/compiler/typecheck/TcMType.hs
+++ b/compiler/typecheck/TcMType.hs
@@ -1342,16 +1342,6 @@ to be later converted to a list in a deterministic order.
 
 For more information about deterministic sets see
 Note [Deterministic UniqFM] in UniqDFM.
-
-
---------------- Note to tidy up --------
-Can we quantify over a non-unification variable? Sadly yes (Trac #15991b)
-  class C2 (a :: Type) (b :: Proxy a) (c :: Proxy b) where
-    type T4 a c
-
-When we come to T4 we have in Inferred b; but it is a skolem
-from the (fully settled) C2.
-
 -}
 
 quantifyTyVars
@@ -1444,10 +1434,10 @@ quantifyTyVars gbl_tvs
       = return Nothing   -- this can happen for a covar that's associated with
                          -- a coercion hole. Test case: typecheck/should_compile/T2494
 
-      | not (isTcTyVar tkv)
-      = WARN( True, text "quantifying over a TyVar" <+> ppr tkv)
-        return (Just tkv)  -- For associated types, we have the class variables
-                           -- in scope, and they are TyVars not TcTyVars
+      | not (isTcTyVar tkv)  -- I don't think this can ever happen.
+                             -- Hence the assert
+      = ASSERT2( False, text "quantifying over a TyVar" <+> ppr tkv)
+        return (Just tkv)
 
       | otherwise
       = do { deflt_done <- defaultTyVar default_kind tkv