Fix #10963 and #11975 by adding new cmds to GHCi.

See the user's guide entry or the Note [TcRnExprMode] in TcRnDriver.

Test cases: ghci/scripts/T{10963,11975}

18 files changed, 300 insertions, 82 deletions

diff --git a/compiler/main/GHC.hs b/compiler/main/GHC.hs
index 40aa7dfa01..9dc68537d9 100644
--- a/compiler/main/GHC.hs
+++ b/compiler/main/GHC.hs
@@ -116,7 +116,7 @@ module GHC (
         isModuleInterpreted,
 
         -- ** Inspecting types and kinds
-        exprType,
+        exprType, TcRnExprMode(..),
         typeKind,
 
         -- ** Looking up a Name
diff --git a/compiler/main/HscMain.hs b/compiler/main/HscMain.hs
index 7cbc6e711f..9c510df27b 100644
--- a/compiler/main/HscMain.hs
+++ b/compiler/main/HscMain.hs
@@ -65,7 +65,7 @@ module HscMain
     , hscTcRnLookupRdrName
     , hscStmt, hscStmtWithLocation, hscParsedStmt
     , hscDecls, hscDeclsWithLocation
-    , hscTcExpr, hscImport, hscKcType
+    , hscTcExpr, TcRnExprMode(..), hscImport, hscKcType
     , hscParseExpr
     , hscCompileCoreExpr
     -- * Low-level exports for hooks
@@ -1609,14 +1609,14 @@ hscImport hsc_env str = runInteractiveHsc hsc_env $ do
                      text "parse error in import declaration"
 
 -- | Typecheck an expression (but don't run it)
--- Returns its most general type
 hscTcExpr :: HscEnv
+          -> TcRnExprMode
           -> String -- ^ The expression
           -> IO Type
-hscTcExpr hsc_env0 expr = runInteractiveHsc hsc_env0 $ do
+hscTcExpr hsc_env0 mode expr = runInteractiveHsc hsc_env0 $ do
   hsc_env <- getHscEnv
   parsed_expr <- hscParseExpr expr
-  ioMsgMaybe $ tcRnExpr hsc_env parsed_expr
+  ioMsgMaybe $ tcRnExpr hsc_env mode parsed_expr
 
 -- | Find the kind of a type
 -- Currently this does *not* generalise the kinds of the type
diff --git a/compiler/main/InteractiveEval.hs b/compiler/main/InteractiveEval.hs
index 6c95dc3bcc..9877e9a0c7 100644
--- a/compiler/main/InteractiveEval.hs
+++ b/compiler/main/InteractiveEval.hs
@@ -864,10 +864,10 @@ parseThing parser dflags stmt = do
 -- Getting the type of an expression
 
 -- | Get the type of an expression
--- Returns its most general type
-exprType :: GhcMonad m => String -> m Type
-exprType expr = withSession $ \hsc_env -> do
-   ty <- liftIO $ hscTcExpr hsc_env expr
+-- Returns the type as described by 'TcRnExprMode'
+exprType :: GhcMonad m => TcRnExprMode -> String -> m Type
+exprType mode expr = withSession $ \hsc_env -> do
+   ty <- liftIO $ hscTcExpr hsc_env mode expr
    return $ tidyType emptyTidyEnv ty
 
 -- -----------------------------------------------------------------------------
diff --git a/compiler/typecheck/TcBinds.hs b/compiler/typecheck/TcBinds.hs
index 7c45ac7b59..3a931cb6f6 100644
--- a/compiler/typecheck/TcBinds.hs
+++ b/compiler/typecheck/TcBinds.hs
@@ -710,15 +710,16 @@ tcPolyInfer rec_tc prag_fn tc_sig_fn mono bind_list
              <- pushLevelAndCaptureConstraints  $
                 tcMonoBinds rec_tc tc_sig_fn LetLclBndr bind_list
 
-       ; let name_taus = [ (mbi_poly_name info, idType (mbi_mono_id info))
-                         | info <- mono_infos ]
-             sigs      = [ sig | MBI { mbi_sig = Just sig } <- mono_infos ]
+       ; let name_taus  = [ (mbi_poly_name info, idType (mbi_mono_id info))
+                          | info <- mono_infos ]
+             sigs       = [ sig | MBI { mbi_sig = Just sig } <- mono_infos ]
+             infer_mode = if mono then ApplyMR else NoRestrictions
 
        ; mapM_ (checkOverloadedSig mono) sigs
 
        ; traceTc "simplifyInfer call" (ppr tclvl $$ ppr name_taus $$ ppr wanted)
        ; (qtvs, givens, ev_binds)
-                 <- simplifyInfer tclvl mono sigs name_taus wanted
+                 <- simplifyInfer tclvl infer_mode sigs name_taus wanted
 
        ; let inferred_theta = map evVarPred givens
        ; exports <- checkNoErrs $
diff --git a/compiler/typecheck/TcExpr.hs b/compiler/typecheck/TcExpr.hs
index 0e3c655f76..bb3fef7349 100644
--- a/compiler/typecheck/TcExpr.hs
+++ b/compiler/typecheck/TcExpr.hs
@@ -29,7 +29,7 @@ import BasicTypes
 import Inst
 import TcBinds          ( chooseInferredQuantifiers, tcLocalBinds )
 import TcSigs           ( tcUserTypeSig, tcInstSig )
-import TcSimplify       ( simplifyInfer )
+import TcSimplify       ( simplifyInfer, InferMode(..) )
 import FamInst          ( tcGetFamInstEnvs, tcLookupDataFamInst )
 import FamInstEnv       ( FamInstEnvs )
 import RnEnv            ( addUsedGRE, addNameClashErrRn
@@ -1472,10 +1472,13 @@ tcExprSig expr sig@(PartialSig { psig_name = name, sig_loc = loc })
                    ; return (expr', sig_inst) }
        -- See Note [Partial expression signatures]
        ; let tau = sig_inst_tau sig_inst
-             mr  = null (sig_inst_theta sig_inst) &&
-                   isNothing (sig_inst_wcx sig_inst)
+             infer_mode | null (sig_inst_theta sig_inst)
+                        , isNothing (sig_inst_wcx sig_inst)
+                        = ApplyMR
+                        | otherwise
+                        = NoRestrictions
        ; (qtvs, givens, ev_binds)
-                 <- simplifyInfer tclvl mr [sig_inst] [(name, tau)] wanted
+                 <- simplifyInfer tclvl infer_mode [sig_inst] [(name, tau)] wanted
        ; tau <- zonkTcType tau
        ; let inferred_theta = map evVarPred givens
              tau_tvs        = tyCoVarsOfType tau
diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs
index b9a6dec0a8..e19a786b1d 100644
--- a/compiler/typecheck/TcPatSyn.hs
+++ b/compiler/typecheck/TcPatSyn.hs
@@ -81,7 +81,8 @@ tcInferPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details,
 
        ; let named_taus = (name, pat_ty) : map (\arg -> (getName arg, varType arg)) args
 
-       ; (qtvs, req_dicts, ev_binds) <- simplifyInfer tclvl False [] named_taus wanted
+       ; (qtvs, req_dicts, ev_binds) <- simplifyInfer tclvl NoRestrictions []
+                                                      named_taus wanted
 
        ; let ((ex_tvs, ex_vars), prov_dicts) = tcCollectEx lpat'
              univ_tvs   = filter (not . (`elemVarSet` ex_vars)) qtvs
diff --git a/compiler/typecheck/TcRnDriver.hs b/compiler/typecheck/TcRnDriver.hs
index 9d3bd99ab9..46d0a7b34f 100644
--- a/compiler/typecheck/TcRnDriver.hs
+++ b/compiler/typecheck/TcRnDriver.hs
@@ -13,7 +13,7 @@ https://ghc.haskell.org/trac/ghc/wiki/Commentary/Compiler/TypeChecker
 
 module TcRnDriver (
 #ifdef GHCI
-        tcRnStmt, tcRnExpr, tcRnType,
+        tcRnStmt, tcRnExpr, TcRnExprMode(..), tcRnType,
         tcRnImportDecls,
         tcRnLookupRdrName,
         getModuleInterface,
@@ -1972,13 +1972,17 @@ isGHCiMonad hsc_env ty
             Just _  -> failWithTc $ text "Ambiguous type!"
             Nothing -> failWithTc $ text ("Can't find type:" ++ ty)
 
--- tcRnExpr just finds the type of an expression
+-- | How should we infer a type? See Note [TcRnExprMode]
+data TcRnExprMode = TM_Inst    -- ^ Instantiate the type fully (:type)
+                  | TM_NoInst  -- ^ Do not instantiate the type (:type +v)
+                  | TM_Default -- ^ Default the type eagerly (:type +d)
 
+-- | tcRnExpr just finds the type of an expression
 tcRnExpr :: HscEnv
+         -> TcRnExprMode
          -> LHsExpr RdrName
          -> IO (Messages, Maybe Type)
--- Type checks the expression and returns its most general type
-tcRnExpr hsc_env rdr_expr
+tcRnExpr hsc_env mode rdr_expr
   = runTcInteractive hsc_env $
     do {
 
@@ -1993,15 +1997,15 @@ tcRnExpr hsc_env rdr_expr
     (tclvl, lie, res_ty)
           <- pushLevelAndCaptureConstraints $
              do { (_tc_expr, expr_ty) <- tcInferSigma rn_expr
-                ; (_wrap, res_ty)   <- deeplyInstantiate orig expr_ty
-                     -- See [Note Deeply instantiate in :type]
-                ; return res_ty } ;
+                ; if inst
+                  then snd <$> deeplyInstantiate orig expr_ty
+                  else return expr_ty } ;
 
     -- Generalise
     ((qtvs, dicts, _), lie_top) <- captureConstraints $
                                    {-# SCC "simplifyInfer" #-}
                                    simplifyInfer tclvl
-                                                 False {- No MR for now -}
+                                                 infer_mode
                                                  []    {- No sig vars -}
                                                  [(fresh_it, res_ty)]
                                                  lie ;
@@ -2009,7 +2013,8 @@ tcRnExpr hsc_env rdr_expr
     stWC <- tcg_static_wc <$> getGblEnv >>= readTcRef ;
 
     -- Ignore the dictionary bindings
-    _ <- simplifyInteractive (andWC stWC lie_top) ;
+    _ <- perhaps_disable_default_warnings $
+         simplifyInteractive (andWC stWC lie_top) ;
 
     let { all_expr_ty = mkInvForAllTys qtvs (mkLamTypes dicts res_ty) } ;
     ty <- zonkTcType all_expr_ty ;
@@ -2022,6 +2027,12 @@ tcRnExpr hsc_env rdr_expr
     -- irrelevant
     return (snd (normaliseType fam_envs Nominal ty))
     }
+  where
+    -- See Note [Deeply instantiate in :type]
+    (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)
 
 --------------------------
 tcRnImportDecls :: HscEnv
@@ -2038,7 +2049,6 @@ tcRnImportDecls hsc_env import_decls
     zap_rdr_env gbl_env = gbl_env { tcg_rdr_env = emptyGlobalRdrEnv }
 
 -- tcRnType just finds the kind of a type
-
 tcRnType :: HscEnv
          -> Bool        -- Normalise the returned type
          -> LHsType RdrName
@@ -2073,20 +2083,63 @@ tcRnType hsc_env normalise rdr_type
 
        ; return (ty', mkInvForAllTys kvs (typeKind ty')) }
 
-{- Note [Deeply instantiate in :type]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Suppose (Trac #11376)
-  bar :: forall a b. Show a => a -> b -> a
-What should `:t bar @Int` show?
-
- 1. forall b. Show Int => Int -> b -> Int
- 2. forall b. Int -> b -> Int
- 3. forall {b}. Int -> b -> Int
- 4. Int -> b -> Int
-
-We choose (3), which is the effect of deeply instantiating and
-re-generalising.  All the others seem deeply confusing.  That is
-why we deeply instantiate here.
+{- Note [TcRnExprMode]
+~~~~~~~~~~~~~~~~~~~~~~
+How should we infer a type when a user asks for the type of an expression e
+at the GHCi prompt? We offer 3 different possibilities, described below. Each
+considers this example, with -fprint-explicit-foralls enabled:
+
+  foo :: forall a f b. (Show a, Num b, Foldable f) => a -> f b -> String
+  :type{,-spec,-def} foo @Int
+
+:type / TM_Inst
+
+  In this mode, we report the type that would be inferred if a variable
+  were assigned to expression e, without applying the monomorphism restriction.
+  This means we deeply instantiate the type and then regeneralize, as discussed
+  in #11376.
+
+  > :type foo @Int
+  forall {b} {f :: * -> *}. (Foldable f, Num b) => Int -> f b -> String
+
+  Note that the variables and constraints are reordered here, because this
+  is possible during regeneralization. Also note that the variables are
+  reported as Invisible instead of Specified.
+
+:type +v / TM_NoInst
+
+  This mode is for the benefit of users using TypeApplications. It does no
+  instantiation whatsoever, sometimes meaning that class constraints are not
+  solved.
+
+  > :type +v foo @Int
+  forall f b. (Show Int, Num b, Foldable f) => Int -> f b -> String
+
+  Note that Show Int is still reported, because the solver never got a chance
+  to see it.
+
+:type +d / TM_Default
+
+  This mode is for the benefit of users who wish to see instantiations of
+  generalized types, and in particular to instantiate Foldable and Traversable.
+  In this mode, any type variable that can be defaulted is defaulted. Because
+  GHCi uses -XExtendedDefaultRules, this means that Foldable and Traversable are
+  defaulted.
+
+  > :type +d foo @Int
+  Int -> [Integer] -> String
+
+  Note that this mode can sometimes lead to a type error, if a type variable is
+  used with a defaultable class but cannot actually be defaulted:
+
+  bar :: (Num a, Monoid a) => a -> a
+  > :type +d bar
+  ** error **
+
+  The error arises because GHC tries to default a but cannot find a concrete
+  type in the defaulting list that is both Num and Monoid. (If this list is
+  modified to include an element that is both Num and Monoid, the defaulting
+  would succeed, of course.)
 
 Note [Kind-generalise in tcRnType]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs
index 594cc949b3..18adee8047 100644
--- a/compiler/typecheck/TcSimplify.hs
+++ b/compiler/typecheck/TcSimplify.hs
@@ -1,7 +1,7 @@
 {-# LANGUAGE CPP #-}
 
 module TcSimplify(
-       simplifyInfer,
+       simplifyInfer, InferMode(..),
        growThetaTyVars,
        simplifyAmbiguityCheck,
        simplifyDefault,
@@ -514,8 +514,22 @@ the let binding.
 
 -}
 
+-- | How should we choose which constraints to quantify over?
+data InferMode = ApplyMR          -- ^ Apply the monomorphism restriction,
+                                  -- never quantifying over any constraints
+               | EagerDefaulting  -- ^ See Note [TcRnExprMode] in TcRnDriver,
+                                  -- the :type +d case; this mode refuses
+                                  -- to quantify over any defaultable constraint
+               | NoRestrictions   -- ^ Quantify over any constraint that
+                                  -- satisfies TcType.pickQuantifiablePreds
+
+instance Outputable InferMode where
+  ppr ApplyMR         = text "ApplyMR"
+  ppr EagerDefaulting = text "EagerDefaulting"
+  ppr NoRestrictions  = text "NoRestrictions"
+
 simplifyInfer :: TcLevel               -- Used when generating the constraints
-              -> Bool                  -- Apply monomorphism restriction
+              -> InferMode
               -> [TcIdSigInst]         -- Any signatures (possibly partial)
               -> [(Name, TcTauType)]   -- Variables to be generalised,
                                        -- and their tau-types
@@ -523,7 +537,7 @@ simplifyInfer :: TcLevel               -- Used when generating the constraints
               -> TcM ([TcTyVar],    -- Quantify over these type variables
                       [EvVar],      -- ... and these constraints (fully zonked)
                       TcEvBinds)    -- ... binding these evidence variables
-simplifyInfer rhs_tclvl apply_mr sigs name_taus wanteds
+simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
   | isEmptyWC wanteds
   = do { gbl_tvs <- tcGetGlobalTyCoVars
        ; dep_vars <- zonkTcTypesAndSplitDepVars (map snd name_taus)
@@ -536,7 +550,7 @@ simplifyInfer rhs_tclvl apply_mr sigs name_taus wanteds
              [ text "sigs =" <+> ppr sigs
              , text "binds =" <+> ppr name_taus
              , text "rhs_tclvl =" <+> ppr rhs_tclvl
-             , text "apply_mr =" <+> ppr apply_mr
+             , text "infer_mode =" <+> ppr infer_mode
              , text "(unzonked) wanted =" <+> ppr wanteds
              ]
 
@@ -616,7 +630,7 @@ simplifyInfer rhs_tclvl apply_mr sigs name_taus wanteds
        -- Decide what type variables and constraints to quantify
        -- NB: bound_theta are constraints we want to quantify over,
        --     /apart from/ the psig_theta, which we always quantify over
-       ; (qtvs, bound_theta) <- decideQuantification apply_mr name_taus psig_theta
+       ; (qtvs, bound_theta) <- decideQuantification infer_mode name_taus psig_theta
                                                      quant_pred_candidates
 
          -- Promote any type variables that are free in the inferred type
@@ -763,23 +777,31 @@ including all covars -- and the quantified constraints are empty/insoluble.
 -}
 
 decideQuantification
-  :: Bool                  -- try the MR restriction?
+  :: InferMode
   -> [(Name, TcTauType)]   -- Variables to be generalised
   -> [PredType]            -- All annotated constraints from signatures
   -> [PredType]            -- Candidate theta
   -> TcM ( [TcTyVar]       -- Quantify over these (skolems)
          , [PredType] )    -- and this context (fully zonked)
 -- See Note [Deciding quantification]
-decideQuantification apply_mr name_taus psig_theta candidates
+decideQuantification infer_mode name_taus psig_theta candidates
   = do { gbl_tvs <- tcGetGlobalTyCoVars
        ; zonked_taus <- mapM TcM.zonkTcType (psig_theta ++ taus)
                         -- psig_theta: see Note [Quantification and partial signatures]
-       ; let DV { dv_kvs = zkvs, dv_tvs = ztvs} = splitDepVarsOfTypes zonked_taus
+       ; ovl_strings <- xoptM LangExt.OverloadedStrings
+       ; let DV {dv_kvs = zkvs, dv_tvs = ztvs} = splitDepVarsOfTypes zonked_taus
              (gbl_cand, quant_cand)  -- gbl_cand   = do not quantify me
-                = case apply_mr of   -- quant_cand = try to quantify me
-                    True  -> (candidates, [])
-                    False -> ([], candidates)
-             zonked_tkvs     = dVarSetToVarSet zkvs `unionVarSet` dVarSetToVarSet ztvs
+                = case infer_mode of   -- quant_cand = try to quantify me
+                    ApplyMR         -> (candidates, [])
+                    NoRestrictions  -> ([], candidates)
+                    EagerDefaulting -> partition is_interactive_ct candidates
+                      where
+                        is_interactive_ct ct
+                          | Just (cls, _) <- getClassPredTys_maybe ct
+                          = isInteractiveClass ovl_strings cls
+                          | otherwise
+                          = False
+
              eq_constraints  = filter isEqPred quant_cand
              constrained_tvs = tyCoVarsOfTypes gbl_cand
              mono_tvs        = growThetaTyVars eq_constraints $
@@ -804,7 +826,10 @@ decideQuantification apply_mr name_taus psig_theta candidates
 
            -- Warn about the monomorphism restriction
        ; warn_mono <- woptM Opt_WarnMonomorphism
-       ; let mr_bites = constrained_tvs `intersectsVarSet` zonked_tkvs
+       ; let mr_bites | ApplyMR <- infer_mode
+                      = constrained_tvs `intersectsVarSet` tcDepVarSet dvs_plus
+                      | otherwise
+                      = False
        ; warnTc (Reason Opt_WarnMonomorphism) (warn_mono && mr_bites) $
          hang (text "The Monomorphism Restriction applies to the binding"
                <> plural bndrs <+> text "for" <+> pp_bndrs)
@@ -812,8 +837,9 @@ decideQuantification apply_mr name_taus psig_theta candidates
                 <+> if isSingleton bndrs then pp_bndrs
                                          else text "these binders")
 
-       ; traceTc "decideQuantification 2"
-           (vcat [ text "gbl_cand:"     <+> ppr gbl_cand
+       ; traceTc "decideQuantification"
+           (vcat [ text "infer_mode:"   <+> ppr infer_mode
+                 , text "gbl_cand:"     <+> ppr gbl_cand
                  , text "quant_cand:"   <+> ppr quant_cand
                  , text "gbl_tvs:"      <+> ppr gbl_tvs
                  , text "mono_tvs:"     <+> ppr mono_tvs
@@ -1676,7 +1702,7 @@ approximateWC to produce a list of candidate constraints.  Then we MUST
      approximateWC, to restore invariant (MetaTvInv) described in
      Note [TcLevel and untouchable type variables] in TcType.
 
-  b) Default the kind of any meta-tyyvars that are not mentioned in
+  b) Default the kind of any meta-tyvars that are not mentioned in
      in the environment.
 
 To see (b), suppose the constraint is (C ((a :: OpenKind) -> Int)), and we
@@ -1994,22 +2020,13 @@ findDefaultableGroups (default_tys, (ovl_strings, extended_defaults)) wanteds
           in b1 && b2
 
     defaultable_classes clss
-        | extended_defaults = any isInteractiveClass clss
-        | otherwise         = all is_std_class clss && (any is_num_class clss)
-
-    -- In interactive mode, or with -XExtendedDefaultRules,
-    -- we default Show a to Show () to avoid graututious errors on "show []"
-    isInteractiveClass cls
-        = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey
-                                                   , ordClassKey, foldableClassKey
-                                                   , traversableClassKey])
-
-    is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
-    -- is_num_class adds IsString to the standard numeric classes,
-    -- when -foverloaded-strings is enabled
+        | extended_defaults = any (isInteractiveClass ovl_strings) clss
+        | otherwise         = all is_std_class clss && (any (isNumClass ovl_strings) clss)
 
-    is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
-    -- Similarly is_std_class
+    -- is_std_class adds IsString to the standard numeric classes,
+    -- when -foverloaded-strings is enabled
+    is_std_class cls = isStandardClass cls ||
+                       (ovl_strings && (cls `hasKey` isStringClassKey))
 
 ------------------------------
 disambigGroup :: [Type]            -- The default types
@@ -2061,6 +2078,20 @@ disambigGroup (default_ty:default_tys) group@(the_tv, wanteds)
       -- With the addition of polykinded defaulting we also want to reject
       -- ill-kinded defaulting attempts like (Eq []) or (Foldable Int) here.
 
+-- In interactive mode, or with -XExtendedDefaultRules,
+-- we default Show a to Show () to avoid graututious errors on "show []"
+isInteractiveClass :: Bool   -- -XOverloadedStrings?
+                   -> Class -> Bool
+isInteractiveClass ovl_strings cls
+    = isNumClass ovl_strings cls || (classKey cls `elem` interactiveClassKeys)
+
+    -- isNumClass adds IsString to the standard numeric classes,
+    -- when -foverloaded-strings is enabled
+isNumClass :: Bool   -- -XOverloadedStrings?
+           -> Class -> Bool
+isNumClass ovl_strings cls
+  = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
+
 
 {-
 Note [Avoiding spurious errors]
diff --git a/docs/users_guide/ghci.rst b/docs/users_guide/ghci.rst
index 5404701898..783059fe17 100644
--- a/docs/users_guide/ghci.rst
+++ b/docs/users_guide/ghci.rst
@@ -977,6 +977,10 @@ Type defaulting in GHCi
    single: Type defaulting; in GHCi
    single: Show class
 
+.. ghc-flag:: -XExtendedDefaultRules
+
+    Allow defaulting to take place for more than just numeric classes.
+
 Consider this GHCi session:
 
 .. code-block:: none
@@ -1014,7 +1018,7 @@ is given, the following additional differences apply:
    single-parameter type classes.
 
 -  Rule 3 above is relaxed this: At least one of the classes ``Ci`` is
-   numeric, or is ``Show``, ``Eq``, ``Ord``, ``Foldable`` or ``Traversable``.
+   an *interactive class* (defined below).
 
 -  The unit type ``()`` and the list type ``[]`` are added to the start of
    the standard list of types which are tried when doing type defaulting.
@@ -1044,6 +1048,38 @@ printf.
 See also :ref:`actions-at-prompt` for how the monad of a computational
 expression defaults to ``IO`` if possible.
 
+Interactive classes
+^^^^^^^^^^^^^^^^^^^
+
+.. index::
+   single: Interactive classes
+
+The interactive classes (only relevant when :ghc-flag:`-XExtendedDefaultRules`
+is in effect) are: any numeric class, ``Show``, ``Eq``, ``Ord``,
+``Foldable`` or ``Traversable``.
+
+As long as a type variable is constrained by one of these classes, defaulting
+will occur, as outlined above.
+
+Extended rules around ``default`` declarations
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+.. index::
+   single: default declarations
+
+Since the rules for defaulting are relaxed under
+:ghc-flag:`-XExtendedDefaultRules`, the rules for ``default`` declarations
+are also relaxed. According to Section 4.3.4 of the Haskell 2010 Report,
+a ``default`` declaration looks like ``default (t1, ..., tn)`` where, for
+each ``ti``, ``Num ti`` must hold. This is relaxed to say that for each
+``ti``, there must exist an interactive class ``C`` such that ``C ti`` holds.
+This means that type *constructors* can be allowed in these lists.
+For example, the following works if you wish your ``Foldable`` constraints
+to default to ``Maybe`` but your ``Num`` constraints to still default
+to ``Integer`` or ``Double``: ::
+
+    default (Maybe, Integer, Double)
+
 .. _ghci-interactive-print:
 
 Using a custom interactive printing function
@@ -2625,10 +2661,48 @@ commonly used commands.
 .. ghci-cmd:: :type; ⟨expression⟩
 
     Infers and prints the type of ⟨expression⟩, including explicit
-    forall quantifiers for polymorphic types. The monomorphism
-    restriction is *not* applied to the expression during type
-    inference.
+    forall quantifiers for polymorphic types.
+    The type reported is the type that would be inferred
+    for a variable assigned to the expression, but without the
+    monomorphism restriction applied.
+
+    .. code-block:: none
+
+	*X> :type length
+	length :: Foldable t => t a -> Int
+
+.. ghci-cmd:: :type +v ⟨expression⟩
+
+    Infers and prints the type of ⟨expression⟩, but without fiddling
+    with type variables or class constraints. This is useful when you
+    are using :ghc-flag:`-XTypeApplications` and care about the distinction
+    between specified type variables (available for type application)
+    and inferred type variables (not available). This mode sometimes prints
+    constraints (such as ``Show Int``) that could readily be solved, but
+    solving these constraints may affect the type variables, so GHC refrains.
+
+    .. code-block:: none
+
+	*X> :set -fprint-explicit-foralls
+	*X> :type +v length
+	length :: forall (t :: * -> *). Foldable t => forall a. t a -> Int
+    
+.. ghci-cmd:: :type +d ⟨expression⟩
+
+    Infers and prints the type of ⟨expression⟩, defaulting type variables
+    if possible. In this mode, if the inferred type is constrained by
+    any interactive class (``Num``, ``Show``, ``Eq``, ``Ord``, ``Foldable``,
+    or ``Traversable``), the constrained type variable(s) are defaulted
+    according to the rules described under :ghc-flag:`-XExtendedDefaultRules`.
+    This mode is quite useful when the inferred type is quite general (such
+    as for ``foldr``) and it may be helpful to see a more concrete
+    instantiation.
+
+    .. code-block:: none
 
+	*X> :type +d length
+	length :: [a] -> Int
+	      
 .. ghci-cmd:: :type-at; ⟨module⟩ ⟨line⟩ ⟨col⟩ ⟨end-line⟩ ⟨end-col⟩ [⟨name⟩]
 
     Reports the inferred type at the given span/position in the module, e.g.:
diff --git a/ghc/GHCi/UI.hs b/ghc/GHCi/UI.hs
index c04bf2d194..1e27c7a861 100644
--- a/ghc/GHCi/UI.hs
+++ b/ghc/GHCi/UI.hs
@@ -299,6 +299,8 @@ defFullHelpText =
   "   :run function [<arguments> ...] run the function with the given arguments\n" ++
   "   :script <file>              run the script <file>\n" ++
   "   :type <expr>                show the type of <expr>\n" ++
+  "   :type +d <expr>             show the type of <expr>, defaulting type variables\n" ++
+  "   :type +v <expr>             show the type of <expr>, with its specified tyvars\n" ++
   "   :undef <cmd>                undefine user-defined command :<cmd>\n" ++
   "   :!<command>                 run the shell command <command>\n" ++
   "\n" ++
@@ -1811,12 +1813,16 @@ exceptT :: Applicative m => Either e a -> ExceptT e m a
 exceptT = ExceptT . pure
 
 -----------------------------------------------------------------------------
--- | @:type@ command
+-- | @:type@ command. See also Note [TcRnExprMode] in TcRnDriver.
 
 typeOfExpr :: String -> InputT GHCi ()
 typeOfExpr str = handleSourceError GHC.printException $ do
-    ty <- GHC.exprType str
-    printForUser $ sep [text str, nest 2 (dcolon <+> pprTypeForUser ty)]
+    let (mode, expr_str) = case break isSpace str of
+          ("+d", rest) -> (GHC.TM_Default, dropWhile isSpace rest)
+          ("+v", rest) -> (GHC.TM_NoInst,  dropWhile isSpace rest)
+          _            -> (GHC.TM_Inst,    str)
+    ty <- GHC.exprType mode expr_str
+    printForUser $ sep [text expr_str, nest 2 (dcolon <+> pprTypeForUser ty)]
 
 -----------------------------------------------------------------------------
 -- | @:type-at@ command
diff --git a/ghc/GHCi/UI/Info.hs b/ghc/GHCi/UI/Info.hs
index 2c44e3f8e2..ef5e9ef207 100644
--- a/ghc/GHCi/UI/Info.hs
+++ b/ghc/GHCi/UI/Info.hs
@@ -215,7 +215,7 @@ findType infos span0 string = do
              MaybeT $ pure $ M.lookup name infos
 
     case resolveType (modinfoSpans info) (spanInfoFromRealSrcSpan' span0) of
-        Nothing -> (,) info <$> lift (exprType string)
+        Nothing -> (,) info <$> lift (exprType TM_Inst string)
         Just ty -> return (info, ty)
   where
     -- | Try to resolve the type display from the given span.
diff --git a/testsuite/tests/ghc-api/T8639_api.hs b/testsuite/tests/ghc-api/T8639_api.hs
index 36458b8eca..2b0bc7d4c6 100644
--- a/testsuite/tests/ghc-api/T8639_api.hs
+++ b/testsuite/tests/ghc-api/T8639_api.hs
@@ -22,6 +22,6 @@ main
            execStmt "putStrLn (show 3)" execOptions
            execStmt "hFlush stdout" execOptions
 
-           ty <- exprType "T8639_api_a.it"
+           ty <- exprType TM_Inst "T8639_api_a.it"
            liftIO (putStrLn (showPpr flags ty))
        ; hFlush stdout }
diff --git a/testsuite/tests/ghci/scripts/T10963.script b/testsuite/tests/ghci/scripts/T10963.script
new file mode 100644
index 0000000000..357d1256ba
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T10963.script
@@ -0,0 +1,7 @@
+:type mapM
+:type +d mapM
+:t +d length
+let foo :: (Num a, Monoid a) => a -> a; foo = undefined
+:t +d foo
+instance Monoid Double where mempty = 0; mappend = (+)
+:t +d foo
diff --git a/testsuite/tests/ghci/scripts/T10963.stderr b/testsuite/tests/ghci/scripts/T10963.stderr
new file mode 100644
index 0000000000..e20f792773
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T10963.stderr
@@ -0,0 +1,12 @@
+
+<interactive>:1:1: error:
+    Ambiguous type variable ‘a0’ arising from a use of ‘foo’
+    prevents the constraint ‘(Num a0)’ from being solved.
+    Probable fix: use a type annotation to specify what ‘a0’ should be.
+    These potential instances exist:
+      instance Num Integer -- Defined in ‘GHC.Num’
+      instance Num Double -- Defined in ‘GHC.Float’
+      instance Num Float -- Defined in ‘GHC.Float’
+      ...plus two others
+      ...plus five instances involving out-of-scope types
+      (use -fprint-potential-instances to see them all)
diff --git a/testsuite/tests/ghci/scripts/T10963.stdout b/testsuite/tests/ghci/scripts/T10963.stdout
new file mode 100644
index 0000000000..bf639a8aa5
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T10963.stdout
@@ -0,0 +1,4 @@
+mapM :: (Monad m, Traversable t) => (a -> m b) -> t a -> m (t b)
+mapM :: Monad m => (a -> m b) -> [a] -> m [b]
+length :: [a] -> Int
+foo :: Double -> Double
diff --git a/testsuite/tests/ghci/scripts/T11975.script b/testsuite/tests/ghci/scripts/T11975.script
new file mode 100644
index 0000000000..80061ef97b
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T11975.script
@@ -0,0 +1,9 @@
+:set -fprint-explicit-foralls
+:type mapM
+:type +v mapM
+:t +v mapM
+let foo :: (Show a, Num b) => a -> b; foo = undefined
+:set -XTypeApplications
+:type foo @Int
+:type +v foo @Int
+:t +v foo @Int
diff --git a/testsuite/tests/ghci/scripts/T11975.stdout b/testsuite/tests/ghci/scripts/T11975.stdout
new file mode 100644
index 0000000000..23adaf02db
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T11975.stdout
@@ -0,0 +1,15 @@
+mapM
+  :: forall {t :: * -> *} {b} {m :: * -> *} {a}.
+     (Monad m, Traversable t) =>
+     (a -> m b) -> t a -> m (t b)
+mapM
+  :: forall (t :: * -> *).
+     Traversable t =>
+     forall (m :: * -> *) a b. Monad m => (a -> m b) -> t a -> m (t b)
+mapM
+  :: forall (t :: * -> *).
+     Traversable t =>
+     forall (m :: * -> *) a b. Monad m => (a -> m b) -> t a -> m (t b)
+foo @Int :: forall {b}. Num b => Int -> b
+foo @Int :: forall b. (Show Int, Num b) => Int -> b
+foo @Int :: forall b. (Show Int, Num b) => Int -> b
diff --git a/testsuite/tests/ghci/scripts/all.T b/testsuite/tests/ghci/scripts/all.T
index dfedb39ea7..b2ea302f42 100755
--- a/testsuite/tests/ghci/scripts/all.T
+++ b/testsuite/tests/ghci/scripts/all.T
@@ -254,3 +254,5 @@ test('TypeAppData', normal, ghci_script, ['TypeAppData.script'])
 test('T11728', normal, ghci_script, ['T11728.script'])
 test('T11376', normal, ghci_script, ['T11376.script'])
 test('T12007', normal, ghci_script, ['T12007.script'])
+test('T11975', normal, ghci_script, ['T11975.script'])
+test('T10963', normal, ghci_script, ['T10963.script'])