Revert "Remove kind generalisation from tcRnType"
authorRichard Eisenberg <rae@cs.brynmawr.edu>
Mon, 29 Oct 2018 16:15:58 +0000 (12:15 -0400)
committerRichard Eisenberg <rae@cs.brynmawr.edu>
Mon, 29 Oct 2018 16:23:17 +0000 (12:23 -0400)
This reverts commit 3a51abd04432ea3d13e4ea3c5a592f038bd57432.

I had hit the wrong button when trying to validate the original
commit... and ended up committing it prematurely instead.
This reversion commit
also updates the comments to explain why we kind-generalise.

compiler/main/HscMain.hs
compiler/typecheck/TcRnDriver.hs

index 77bcd76..9dd7507 100644 (file)
@@ -1693,8 +1693,7 @@ hscTcExpr hsc_env0 mode expr = runInteractiveHsc hsc_env0 $ do
   parsed_expr <- hscParseExpr expr
   ioMsgMaybe $ tcRnExpr hsc_env mode parsed_expr
 
--- | Find the kind of a type
--- Currently this does *not* generalise the kinds of the type
+-- | Find the kind of a type, after generalisation
 hscKcType
   :: HscEnv
   -> Bool            -- ^ Normalise the type
index 9b4565f..4fa1723 100644 (file)
@@ -2375,7 +2375,7 @@ tcRnType :: HscEnv
          -> IO (Messages, Maybe (Type, Kind))
 tcRnType hsc_env normalise rdr_type
   = runTcInteractive hsc_env $
-    setXOptM LangExt.PolyKinds $   -- See Note [Turn on PolyKinds in tcRnType]
+    setXOptM LangExt.PolyKinds $   -- See Note [Kind-generalise in tcRnType]
     do { (HsWC { hswc_ext = wcs, hswc_body = rn_type }, _fvs)
                <- rnHsWcType GHCiCtx (mkHsWildCardBndrs rdr_type)
                   -- The type can have wild cards, but no implicit
@@ -2386,13 +2386,16 @@ tcRnType hsc_env normalise rdr_type
         -- It can have any rank or kind
         -- First bring into scope any wildcards
        ; traceTc "tcRnType" (vcat [ppr wcs, ppr rn_type])
-       ; ((ty, _), lie)  <-
+       ; ((ty, kind), lie)  <-
                        captureConstraints $
                        tcWildCardBinders wcs $ \ wcs' ->
                        do { emitWildCardHoleConstraints wcs'
                           ; tcLHsTypeUnsaturated rn_type }
        ; _ <- checkNoErrs (simplifyInteractive lie)
 
+       -- Do kind generalisation; see Note [Kind-generalise in tcRnType]
+       ; kind <- zonkTcType kind
+       ; kvs <- kindGeneralize kind
        ; ty  <- zonkTcTypeToType ty
 
        -- Do validity checking on type
@@ -2405,7 +2408,7 @@ tcRnType hsc_env normalise rdr_type
                         ; return ty' }
                 else return ty ;
 
-       ; return (ty', typeKind ty') }
+       ; return (ty', mkInvForAllTys kvs (typeKind ty')) }
 
 {- Note [TcRnExprMode]
 ~~~~~~~~~~~~~~~~~~~~~~
@@ -2465,7 +2468,7 @@ considers this example, with -fprint-explicit-foralls enabled:
   modified to include an element that is both Num and Monoid, the defaulting
   would succeed, of course.)
 
-Note [Turn on PolyKinds in tcRnType]
+Note [Kind-generalise in tcRnType]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We switch on PolyKinds when kind-checking a user type, so that we will
 kind-generalise the type, even when PolyKinds is not otherwise on.
@@ -2476,6 +2479,16 @@ anything unexpected, but the apparent *loss* of polymorphism, for
 types that you know are polymorphic, is quite surprising.  See Trac
 #7688 for a discussion.
 
+Note that the goal is to generalise the *kind of the type*, not
+the type itself! Example:
+  ghci> data SameKind :: k -> k -> Type
+  ghci> :k SameKind _
+
+We want to get `k -> Type`, not `Any -> Type`, which is what we would
+get without kind-generalisation. Note that `:k SameKind` is OK, as
+GHC will not instantiate SameKind here, and so we see its full kind
+of `forall k. k -> k -> Type`.
+
 ************************************************************************
 *                                                                      *
                  tcRnDeclsi