compiler/GHC/Core/Ppr.hs

@@ -123,11 +123,13 @@ ppr_binding ann (val_bdr, expr)
          , pp_bind
          ]
   where
+    pp_val_bdr = pprPrefixOcc val_bdr
+
     pp_bind = case bndrIsJoin_maybe val_bdr of
                 Nothing -> pp_normal_bind
                 Just ar -> pp_join_bind ar
 
-    pp_normal_bind = hang (ppr val_bdr) 2 (equals <+> pprCoreExpr expr)
+    pp_normal_bind = hang pp_val_bdr 2 (equals <+> pprCoreExpr expr)
 
       -- For a join point of join arity n, we want to print j = \x1 ... xn -> e
       -- as "j x1 ... xn = e" to differentiate when a join point returns a
@@ -135,7 +137,7 @@ ppr_binding ann (val_bdr, expr)
       -- an n-argument function).
     pp_join_bind join_arity
       | bndrs `lengthAtLeast` join_arity
-      = hang (ppr val_bdr <+> sep (map (pprBndr LambdaBind) lhs_bndrs))
+      = hang (pp_val_bdr <+> sep (map (pprBndr LambdaBind) lhs_bndrs))
            2 (equals <+> pprCoreExpr rhs)
       | otherwise -- Yikes!  A join-binding with too few lambda
                   -- Lint will complain, but we don't want to crash
@@ -164,8 +166,10 @@ ppr_expr :: OutputableBndr b => (SDoc -> SDoc) -> Expr b -> SDoc
         -- an atomic value (e.g. function args)
 
 ppr_expr add_par (Var name)
- | isJoinId name               = add_par ((text "jump") <+> ppr name)
- | otherwise                   = ppr name
+ | isJoinId name               = add_par ((text "jump") <+> pp_name)
+ | otherwise                   = pp_name
+ where
+   pp_name = pprPrefixOcc name
 ppr_expr add_par (Type ty)     = add_par (text "TYPE:" <+> ppr ty)       -- Weird
 ppr_expr add_par (Coercion co) = add_par (text "CO:" <+> ppr co)
 ppr_expr add_par (Lit lit)     = pprLiteral add_par lit
@@ -429,7 +433,7 @@ pprKindedTyVarBndr tyvar
 -- pprIdBndr does *not* print the type
 -- When printing any Id binder in debug mode, we print its inline pragma and one-shot-ness
 pprIdBndr :: Id -> SDoc
-pprIdBndr id = ppr id <+> pprIdBndrInfo (idInfo id)
+pprIdBndr id = pprPrefixOcc id <+> pprIdBndrInfo (idInfo id)
 
 pprIdBndrInfo :: IdInfo -> SDoc
 pprIdBndrInfo info

compiler/GHC/Tc/Gen/HsType.hs

@@ -732,6 +732,7 @@ tc_hs_type mode forall@(HsForAllTy { hst_fvf = fvf, hst_bndrs = hs_tvs
              m_telescope = Just (sep (map ppr hs_tvs))
 
        ; emitResidualTvConstraint skol_info m_telescope tvs' tclvl wanted
+         -- See Note [Skolem escape and forall-types]
 
        ; return (mkForAllTys bndrs ty') }
 
@@ -920,6 +921,26 @@ under these conditions.
 See related Note [Wildcards in visible type application] here and
 Note [The wildcard story for types] in GHC.Hs.Types
 
+Note [Skolem escape and forall-types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+  f :: forall a. (forall kb (b :: kb). Proxy '[a, b]) -> ()
+
+The Proxy '[a,b] forces a and b to have the same kind.  But a's
+kind must be bound outside the 'forall a', and hence escapes.
+We discover this by building an implication constraint for
+each forall.  So the inner implication constraint will look like
+    forall kb (b::kb).  kb ~ ka
+where ka is a's kind.  We can't unify these two, /even/ if ka is
+unification variable, because it would be untouchable inside
+this inner implication.
+
+That's what the pushLevelAndCaptureConstraints, plus subsequent
+emitResidualTvConstraint is all about, when kind-checking
+HsForAllTy.
+
+Note that we don't need to /simplify/ the constraints here
+because we aren't generalising. We just capture them.
 -}
 
 {- *********************************************************************
@@ -2819,10 +2840,13 @@ kindGeneralizeAll ty = do { traceTc "kindGeneralizeAll" empty
                           ; kindGeneralizeSome (const True) ty }
 
 -- | Specialized version of 'kindGeneralizeSome', but where no variables
--- can be generalized. Use this variant when it is unknowable whether metavariables
--- might later be constrained.
--- See Note [Recipe for checking a signature] for why and where this
--- function is needed.
+-- can be generalized, but perhaps some may neeed to be promoted.
+-- Use this variant when it is unknowable whether metavariables might
+-- later be constrained.
+--
+-- To see why this promotion is needed, see
+-- Note [Recipe for checking a signature], and especially
+-- Note [Promotion in signatures].
 kindGeneralizeNone :: TcType  -- needn't be zonked
                    -> TcM ()
 kindGeneralizeNone ty
@@ -3160,7 +3184,7 @@ tcHsPartialSigType ctxt sig_ty
 
                   ; return (wcs, wcx, theta, tau) }
 
-         -- No kind-generalization here:
+       -- No kind-generalization here, but perhaps some promotion
        ; kindGeneralizeNone (mkSpecForAllTys implicit_tvs $
                              mkSpecForAllTys explicit_tvs $
                              mkPhiTy theta $
@@ -3171,6 +3195,14 @@ tcHsPartialSigType ctxt sig_ty
        -- See Note [Extra-constraint holes in partial type signatures]
        ; emitNamedWildCardHoleConstraints wcs
 
+       -- Zonk, so that any nested foralls can "see" their occurrences
+       -- See Note [Checking partial type signatures], in
+       -- the bullet on Nested foralls.
+       ; implicit_tvs <- mapM zonkTcTyVarToTyVar implicit_tvs
+       ; explicit_tvs <- mapM zonkTcTyVarToTyVar explicit_tvs
+       ; theta        <- mapM zonkTcType theta
+       ; tau          <- zonkTcType tau
+
          -- We return a proper (Name,TyVar) environment, to be sure that
          -- we bring the right name into scope in the function body.
          -- Test case: partial-sigs/should_compile/LocalDefinitionBug
@@ -3179,7 +3211,7 @@ tcHsPartialSigType ctxt sig_ty
 
       -- NB: checkValidType on the final inferred type will be
       --     done later by checkInferredPolyId.  We can't do it
-      --     here because we don't have a complete tuype to check
+      --     here because we don't have a complete type to check
 
        ; traceTc "tcHsPartialSigType" (ppr tv_prs)
        ; return (wcs, wcx, tv_prs, theta, tau) }
@@ -3198,12 +3230,31 @@ tcPartialContext hs_theta
 
 {- Note [Checking partial type signatures]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-See also Note [Recipe for checking a signature]
+This Note is about tcHsPartialSigType.  See also
+Note [Recipe for checking a signature]
 
 When we have a partial signature like
-   f,g :: forall a. a -> _
+   f :: forall a. a -> _
 we do the following
 
+* tcHsPartialSigType does not make quantified type (forall a. blah)
+  and then instantiate it -- it makes no sense to instantiate a type
+  with wildcards in it.  Rather, tcHsPartialSigType just returns the
+  'a' and the 'blah' separately.
+
+  Nor, for the same reason, do we push a level in tcHsPartialSigType.
+
+* We instantiate 'a' to a unification variable, a TyVarTv, and /not/
+  a skolem; hence the "_Tv" in bindExplicitTKBndrs_Tv.  Consider
+    f :: forall a. a -> _
+    g :: forall b. _ -> b
+    f = g
+    g = f
+  They are typechecked as a recursive group, with monomorphic types,
+  so 'a' and 'b' will get unified together.  Very like kind inference
+  for mutually recursive data types (sans CUSKs or SAKS); see
+  Note [Cloning for tyvar binders] in GHC.Tc.Gen.HsType
+
 * In GHC.Tc.Gen.Sig.tcUserSigType we return a PartialSig, which (unlike
   the companion CompleteSig) contains the original, as-yet-unchecked
   source-code LHsSigWcType
@@ -3218,12 +3269,28 @@ we do the following
      g x = True
   It's really as if we'd written two distinct signatures.
 
-* Note that we don't make quantified type (forall a. blah) and then
-  instantiate it -- it makes no sense to instantiate a type with
-  wildcards in it.  Rather, tcHsPartialSigType just returns the
-  'a' and the 'blah' separately.
-
-  Nor, for the same reason, do we push a level in tcHsPartialSigType.
+* Nested foralls. Consider
+     f :: forall b. (forall a. a -> _) -> b
+  We do /not/ allow the "_" to be instantiated to 'a'; but we do
+  (as before) allow it to be instantiated to the (top level) 'b'.
+  Why not?  Because suppose
+     f x = (x True, x 'c')
+  We must instantiate that (forall a. a -> _) when typechecking
+  f's body, so we must know precisely where all the a's are; they
+  must not be hidden under (filled-in) unification variables!
+
+  We achieve this in the usual way: we push a level at a forall,
+  so now the unification variable for the "_" can't unify with
+  'a'.
+
+* Just as for ordinary signatures, we must zonk the type after
+  kind-checking it, to ensure that all the nested forall binders can
+  see their occurrenceds
+
+  Just as for ordinary signatures, this zonk also gets any Refl casts
+  out of the way of instantiation.  Example: #18008 had
+       foo :: (forall a. (Show a => blah) |> Refl) -> _
+  and that Refl cast messed things up.  See #18062.
 
 Note [Extra-constraint holes in partial type signatures]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

compiler/GHC/Tc/Module.hs

@@ -2122,7 +2122,7 @@ tcRnStmt hsc_env rdr_stmt
     }
   where
     bad_unboxed id = addErr (sep [text "GHCi can't bind a variable of unlifted type:",
-                                  nest 2 (ppr id <+> dcolon <+> ppr (idType id))])
+                                  nest 2 (pprPrefixOcc id <+> dcolon <+> ppr (idType id))])
 
 {-
 --------------------------------------------------------------------------
@@ -2903,7 +2903,7 @@ ppr_types debug type_env
              -- etc are suppressed (unless -dppr-debug),
              -- because they appear elsewhere
 
-    ppr_sig id = hang (ppr id <+> dcolon) 2 (ppr (tidyTopType (idType id)))
+    ppr_sig id = hang (pprPrefixOcc id <+> dcolon) 2 (ppr (tidyTopType (idType id)))
 
 ppr_tycons :: Bool -> [FamInst] -> TypeEnv -> SDoc
 ppr_tycons debug fam_insts type_env
@@ -2921,7 +2921,7 @@ ppr_tycons debug fam_insts type_env
                      | otherwise  = isExternalName (tyConName tycon) &&
                                     not (tycon `elem` fi_tycons)
     ppr_tc tc
-       = vcat [ hang (ppr (tyConFlavour tc) <+> ppr tc
+       = vcat [ hang (ppr (tyConFlavour tc) <+> pprPrefixOcc (tyConName tc)
                       <> braces (ppr (tyConArity tc)) <+> dcolon)
                    2 (ppr (tidyTopType (tyConKind tc)))
               , nest 2 $
@@ -2955,7 +2955,7 @@ ppr_patsyns type_env
   = ppr_things "PATTERN SYNONYMS" ppr_ps
                (typeEnvPatSyns type_env)
   where
-    ppr_ps ps = ppr ps <+> dcolon <+> pprPatSynType ps
+    ppr_ps ps = pprPrefixOcc ps <+> dcolon <+> pprPatSynType ps
 
 ppr_insts :: [ClsInst] -> SDoc
 ppr_insts ispecs

rts/ProfHeap.c

@@ -552,8 +552,6 @@ initHeapProfiling(void)
 void
 endHeapProfiling(void)
 {
-    StgDouble seconds;
-
     if (! RtsFlags.ProfFlags.doHeapProfile) {
         return;
     }
@@ -596,7 +594,10 @@ endHeapProfiling(void)
 
     stgFree(censuses);
 
-    seconds = mut_user_time();
+    RTSStats stats;
+    getRTSStats(&stats);
+    Time mut_time = stats.mutator_cpu_ns;
+    StgDouble seconds = TimeToSecondsDbl(mut_time);
     printSample(true, seconds);
     printSample(false, seconds);
     fclose(hp_file);

testsuite/tests/ghci/should_fail/T18052b.script

+:set -XMagicHash
+let (%%%) = 1#

testsuite/tests/ghci/should_fail/T18052b.stderr

+
+<interactive>:1:1: error:
+    GHCi can't bind a variable of unlifted type: (%%%) :: GHC.Prim.Int#

testsuite/tests/ghci/should_fail/all.T

@@ -3,3 +3,4 @@ test('T10549a', [], ghci_script, ['T10549a.script'])
 test('T15055', normalise_version('ghc'), ghci_script, ['T15055.script'])
 test('T16013', [], ghci_script, ['T16013.script'])
 test('T16287', [], ghci_script, ['T16287.script'])
+test('T18052b', [], ghci_script, ['T18052b.script'])

testsuite/tests/partial-sigs/should_compile/ExtraConstraints3.stderr

 TYPE SIGNATURES
-  !! :: forall {a}. [a] -> Int -> a
-  $ :: forall {a} {b}. (a -> b) -> a -> b
-  $! :: forall {a} {b}. (a -> b) -> a -> b
-  && :: Bool -> Bool -> Bool
-  * :: forall {a}. Num a => a -> a -> a
-  ** :: forall {a}. Floating a => a -> a -> a
-  + :: forall {a}. Num a => a -> a -> a
-  ++ :: forall {a}. [a] -> [a] -> [a]
-  - :: forall {a}. Num a => a -> a -> a
-  . :: forall {b} {c} {a}. (b -> c) -> (a -> b) -> a -> c
-  / :: forall {a}. Fractional a => a -> a -> a
-  /= :: forall {a}. Eq a => a -> a -> Bool
-  < :: forall {a}. Ord a => a -> a -> Bool
-  <= :: forall {a}. Ord a => a -> a -> Bool
-  =<< ::
+  (!!) :: forall {a}. [a] -> Int -> a
+  ($) :: forall {a} {b}. (a -> b) -> a -> b
+  ($!) :: forall {a} {b}. (a -> b) -> a -> b
+  (&&) :: Bool -> Bool -> Bool
+  (*) :: forall {a}. Num a => a -> a -> a
+  (**) :: forall {a}. Floating a => a -> a -> a
+  (+) :: forall {a}. Num a => a -> a -> a
+  (++) :: forall {a}. [a] -> [a] -> [a]
+  (-) :: forall {a}. Num a => a -> a -> a
+  (.) :: forall {b} {c} {a}. (b -> c) -> (a -> b) -> a -> c
+  (/) :: forall {a}. Fractional a => a -> a -> a
+  (/=) :: forall {a}. Eq a => a -> a -> Bool
+  (<) :: forall {a}. Ord a => a -> a -> Bool
+  (<=) :: forall {a}. Ord a => a -> a -> Bool
+  (=<<) ::
     forall {m :: * -> *} {a} {b}. Monad m => (a -> m b) -> m a -> m b
-  == :: forall {a}. Eq a => a -> a -> Bool
-  > :: forall {a}. Ord a => a -> a -> Bool
-  >= :: forall {a}. Ord a => a -> a -> Bool
-  >> :: forall {m :: * -> *} {a} {b}. Monad m => m a -> m b -> m b
-  >>= ::
+  (==) :: forall {a}. Eq a => a -> a -> Bool
+  (>) :: forall {a}. Ord a => a -> a -> Bool
+  (>=) :: forall {a}. Ord a => a -> a -> Bool
+  (>>) :: forall {m :: * -> *} {a} {b}. Monad m => m a -> m b -> m b
+  (>>=) ::
     forall {m :: * -> *} {a} {b}. Monad m => m a -> (a -> m b) -> m b
-  ^ :: forall {b} {a}. (Integral b, Num a) => a -> b -> a
-  ^^ :: forall {a} {b}. (Fractional a, Integral b) => a -> b -> a
+  (^) :: forall {b} {a}. (Integral b, Num a) => a -> b -> a
+  (^^) :: forall {a} {b}. (Fractional a, Integral b) => a -> b -> a
   abs :: forall {a}. Num a => a -> a
   acos :: forall {a}. Floating a => a -> a
   acosh :: forall {a}. Floating a => a -> a
@@ -234,7 +234,7 @@ TYPE SIGNATURES
   zipWith3 ::
     forall {a} {b} {c} {d}.
     (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
-  || :: Bool -> Bool -> Bool
+  (||) :: Bool -> Bool -> Bool
 Dependent modules: []
-Dependent packages: [base-4.13.0.0, ghc-prim-0.6.1,
-                     integer-gmp-1.0.2.0]
+Dependent packages: [base-4.14.0.0, ghc-prim-0.6.1,
+                     integer-gmp-1.0.3.0]

testsuite/tests/partial-sigs/should_compile/T18008.hs

+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE PartialTypeSignatures #-}
+module Bug where
+
+f :: (forall a. Show a => a -> String) -> _
+f s = s ()
+

testsuite/tests/partial-sigs/should_compile/T18008.stderr

+
+T18008.hs:5:43: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘String’
+    • In the type ‘(forall a. Show a => a -> String) -> _’
+      In the type signature: f :: (forall a. Show a => a -> String) -> _

testsuite/tests/partial-sigs/should_compile/all.T

@@ -95,3 +95,4 @@ test('T16334', normal, compile, [''])
 test('T16728', normal, compile, [''])
 test('T16728a', normal, compile, [''])
 test('T16728b', normal, compile, [''])
+test('T18008', normal, compile, [''])

testsuite/tests/printer/T18052a.hs

+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE TypeOperators #-}
+module T18052a where
+
+(+++) = (++)
+pattern x :||: y = (x,y)
+type (^^^) = Either
+data (&&&)

testsuite/tests/printer/T18052a.stderr

+TYPE SIGNATURES
+  (+++) :: forall {a}. [a] -> [a] -> [a]
+TYPE CONSTRUCTORS
+  data type (&&&){0} :: *
+  type synonym (^^^){0} :: * -> * -> *
+PATTERN SYNONYMS
+  (:||:) :: forall {a} {b}. a -> b -> (a, b)
+Dependent modules: []
+Dependent packages: [base-4.14.0.0, ghc-prim-0.6.1,
+                     integer-gmp-1.0.3.0]
+
+==================== Tidy Core ====================
+Result size of Tidy Core
+  = {terms: 18, types: 53, coercions: 0, joins: 0/0}
+
+-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
+T18052a.$b:||: :: forall {a} {b}. a -> b -> (a, b)
+[GblId, Arity=2, Unf=OtherCon []]
+T18052a.$b:||: = GHC.Tuple.(,)
+
+-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
+(+++) :: forall {a}. [a] -> [a] -> [a]
+[GblId]
+(+++) = (++)
+
+-- RHS size: {terms: 13, types: 20, coercions: 0, joins: 0/0}
+T18052a.$m:||:
+  :: forall {rep :: GHC.Types.RuntimeRep} {r :: TYPE rep} {a} {b}.
+     (a, b) -> (a -> b -> r) -> (GHC.Prim.Void# -> r) -> r
+[GblId, Arity=3, Unf=OtherCon []]
+T18052a.$m:||:
+  = \ (@(rep :: GHC.Types.RuntimeRep))
+      (@(r :: TYPE rep))
+      (@a)
+      (@b)
+      (scrut :: (a, b))
+      (cont :: a -> b -> r)
+      _ [Occ=Dead] ->
+      case scrut of { (x, y) -> cont x y }
+
+
+

testsuite/tests/printer/all.T

@@ -57,3 +57,5 @@ test('T14306', ignore_stderr, makefile_test, ['T14306'])
 test('T14343', normal, compile_fail, [''])
 test('T14343b', normal, compile_fail, [''])
 test('T15761', normal, compile_fail, [''])
+test('T18052a', normal, compile,
+     ['-ddump-simpl -ddump-types -dno-typeable-binds -dsuppress-uniques'])