summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSimon Peyton Jones <simonpj@microsoft.com>2018-11-09 18:11:25 +0000
committerSimon Peyton Jones <simonpj@microsoft.com>2018-11-26 09:44:12 +0000
commit326f87a2028b6254dd0fd0f722564740e99cf108 (patch)
tree2e100ee8537068149036c0255b6ed05927bddd7b
parent99802578f8a900a102bf20c1e812c4b899dc556a (diff)
downloadhaskell-326f87a2028b6254dd0fd0f722564740e99cf108.tar.gz
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)
-rw-r--r--compiler/typecheck/TcHsType.hs49
-rw-r--r--compiler/typecheck/TcMType.hs18
2 files changed, 29 insertions, 38 deletions
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 99bc57e39d..7b1e414fbb 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -230,19 +230,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
@@ -1468,20 +1464,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]
@@ -2004,7 +1986,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 6d9f3cae4c..a1cdf2425c 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