[Git][ghc/ghc][wip/marge_bot_batch_merge_job] 4 commits: Introduce `dataToTagSmall#` primop (closes #21710)

Marge Bot (@marge-bot) gitlab at gitlab.haskell.org
Mon Dec 11 19:14:56 UTC 2023



Marge Bot pushed to branch wip/marge_bot_batch_merge_job at Glasgow Haskell Compiler / GHC


Commits:
297c93b0 by Matthew Craven at 2023-12-11T14:14:28-05:00
Introduce `dataToTagSmall#` primop (closes #21710)

...and use it to generate slightly better code when dataToTag#
is used at a "small data type" where there is no need to mess
with "is_too_big_tag" or potentially look at an info table.

Metric Decrease:
    T18304

- - - - -
f80e4e70 by Matthew Craven at 2023-12-11T14:14:28-05:00
Fix formatting of Note [alg-alt heap check]

- - - - -
baa76a83 by Oleg Grenrus at 2023-12-11T14:14:29-05:00
Allow untyped brackets in typed splices and vice versa.

Resolves #24190

Apparently the check was essentially always (as far as I can trace back: d0d47ba76f8f0501cf3c4966bc83966ab38cac27),
and while it does catch some mismatches, the type-checker will catch
them too. OTOH, it prevents writing completely reasonable programs.

- - - - -
1f21c8b3 by Vladislav Zavialov at 2023-12-11T14:14:29-05:00
docs: update information on RequiredTypeArguments

Update the User's Guide and Release Notes to account for the recent
progress in the implementation of RequiredTypeArguments.

- - - - -


26 changed files:

- compiler/GHC/Builtin/PrimOps.hs
- compiler/GHC/Builtin/primops.txt.pp
- compiler/GHC/Core/Lint.hs
- compiler/GHC/Core/Opt/ConstantFold.hs
- compiler/GHC/Rename/Splice.hs
- compiler/GHC/Stg/InferTags/Rewrite.hs
- compiler/GHC/StgToCmm/Expr.hs
- compiler/GHC/StgToCmm/Prim.hs
- compiler/GHC/StgToJS/Prim.hs
- compiler/GHC/Tc/Instance/Class.hs
- docs/users_guide/9.10.1-notes.rst
- docs/users_guide/exts/required_type_arguments.rst
- docs/users_guide/using-warnings.rst
- libraries/base/src/GHC/Base.hs
- libraries/base/src/GHC/Exts.hs
- testsuite/tests/codeGen/should_compile/T21710a.stderr
- testsuite/tests/linters/notes.stdout
- testsuite/tests/simplCore/should_compile/T22375.hs
- testsuite/tests/simplCore/should_compile/T22375.stderr
- testsuite/tests/simplCore/should_compile/T22375DataFamily.hs
- testsuite/tests/simplCore/should_compile/T22375DataFamily.stderr
- + testsuite/tests/th/T24190.hs
- + testsuite/tests/th/T24190.stdout
- testsuite/tests/th/TH_NestedSplicesFail3.stderr
- testsuite/tests/th/TH_NestedSplicesFail4.stderr
- testsuite/tests/th/all.T


Changes:

=====================================
compiler/GHC/Builtin/PrimOps.hs
=====================================
@@ -921,5 +921,6 @@ instance Outputable PrimCall where
 primOpIsReallyInline :: PrimOp -> Bool
 primOpIsReallyInline = \case
   SeqOp       -> False
-  DataToTagOp -> False
+  DataToTagSmallOp -> False
+  DataToTagLargeOp -> False
   p           -> not (primOpOutOfLine p)


=====================================
compiler/GHC/Builtin/primops.txt.pp
=====================================
@@ -3689,7 +3689,27 @@ section "Tag to enum stuff"
         and small integers.}
 ------------------------------------------------------------------------
 
-primop  DataToTagOp "dataToTagLarge#" GenPrimOp
+primop  DataToTagSmallOp "dataToTagSmall#" GenPrimOp
+   a_levpoly -> Int#
+   { Used internally to implement @dataToTag#@: Use that function instead!
+     This one normally offers /no advantage/ and comes with no stability
+     guarantees: it may change its type, its name, or its behavior
+     with /no warning/ between compiler releases.
+
+     It is expected that this function will be un-exposed in a future
+     release of ghc.
+
+     For more details, look at @Note [DataToTag overview]@
+     in GHC.Tc.Instance.Class in the source code for
+     /the specific compiler version you are using./
+   }
+   with
+   deprecated_msg = { Use dataToTag# from \"GHC.Magic\" instead. }
+   strictness = { \ _arity -> mkClosedDmdSig [evalDmd] topDiv }
+   effect = ThrowsException
+   cheap = True
+
+primop  DataToTagLargeOp "dataToTagLarge#" GenPrimOp
    a_levpoly -> Int#
    { Used internally to implement @dataToTag#@: Use that function instead!
      This one offers /no advantage/ and comes with no stability


=====================================
compiler/GHC/Core/Lint.hs
=====================================
@@ -1131,23 +1131,29 @@ checkTypeDataConOcc what dc
     (text "type data constructor found in a" <+> text what <> colon <+> ppr dc)
 
 {-
--- | Check that a use of dataToTagLarge# satisfies condition DTT2
--- from Note [DataToTag overview] in GHC.Tc.Instance.Class
+-- | Check that a use of a dataToTag# primop satisfies conditions DTT2
+-- and DTT3 from Note [DataToTag overview] in GHC.Tc.Instance.Class
 --
--- Ignores applications not headed by dataToTagLarge#.
+-- Ignores applications not headed by dataToTag# primops.
 
 -- Commented out because GHC.PrimopWrappers doesn't respect this condition yet.
+-- See wrinkle DTW7 in Note [DataToTag overview].
 checkDataToTagPrimOpTyCon
   :: CoreExpr   -- ^ the function (head of the application) we are checking
   -> [CoreArg]  -- ^ The arguments to the application
   -> LintM ()
 checkDataToTagPrimOpTyCon (Var fun_id) args
-  | Just DataToTagOp <- isPrimOpId_maybe fun_id
+  | Just op <- isPrimOpId_maybe fun_id
+  , op == DataToTagSmallOp || op == DataToTagLargeOp
   = case args of
       Type _levity : Type dty : _rest
         | Just (tc, _) <- splitTyConApp_maybe dty
         , isValidDTT2TyCon tc
-          -> pure ()
+          -> do  platform <- getPlatform
+                 let  numConstrs = tyConFamilySize tc
+                      isSmallOp = op == DataToTagSmallOp
+                 checkL (isSmallFamily platform numConstrs == isSmallOp) $
+                   text "dataToTag# primop-size/tycon-family-size mismatch"
         | otherwise -> failWithL $ text "dataToTagLarge# used at non-ADT type:"
                                    <+> ppr dty
       _ -> failWithL $ text "dataToTagLarge# needs two type arguments but has args:"


=====================================
compiler/GHC/Core/Opt/ConstantFold.hs
=====================================
@@ -102,7 +102,8 @@ That is why these rules are built in here.
 primOpRules ::  Name -> PrimOp -> Maybe CoreRule
 primOpRules nm = \case
    TagToEnumOp -> mkPrimOpRule nm 2 [ tagToEnumRule ]
-   DataToTagOp -> mkPrimOpRule nm 3 [ dataToTagRule ]
+   DataToTagSmallOp -> mkPrimOpRule nm 3 [ dataToTagRule ]
+   DataToTagLargeOp -> mkPrimOpRule nm 3 [ dataToTagRule ]
 
    -- Int8 operations
    Int8AddOp   -> mkPrimOpRule nm 2 [ binaryLit (int8Op2 (+))
@@ -1985,7 +1986,9 @@ tagToEnumRule = do
 
 ------------------------------
 dataToTagRule :: RuleM CoreExpr
--- See Note [DataToTag overview] in GHC.Tc.Instance.Class.
+-- Used for both dataToTagSmall# and dataToTagLarge#.
+-- See Note [DataToTag overview] in GHC.Tc.Instance.Class,
+-- particularly wrinkle DTW5.
 dataToTagRule = a `mplus` b
   where
     -- dataToTag (tagToEnum x)   ==>   x
@@ -3374,7 +3377,8 @@ caseRules platform (App (App (Var f) type_arg) v)
 
 -- See Note [caseRules for dataToTag]
 caseRules _ (Var f `App` Type lev `App` Type ty `App` v) -- dataToTag x
-  | Just DataToTagOp <- isPrimOpId_maybe f
+  | Just op <- isPrimOpId_maybe f
+  , op == DataToTagSmallOp || op == DataToTagLargeOp
   = case splitTyConApp_maybe ty of
       Just (tc, _) | isValidDTT2TyCon tc
         -> Just (v, tx_con_dtt tc
@@ -3382,9 +3386,9 @@ caseRules _ (Var f `App` Type lev `App` Type ty `App` v) -- dataToTag x
       _ -> pprTraceUserWarning warnMsg Nothing
   where
     warnMsg = vcat $ map text
-      [ "Found dataToTag primop applied to a non-ADT type. This"
-      , "could be a future bug in GHC, or it may be caused by an"
-      , "unsupported use of the ghc-internal primop dataToTagLarge#."
+      [ "Found dataToTag primop applied to a non-ADT type. This could"
+      , "be a future bug in GHC, or it may be caused by an unsupported"
+      , "use of the ghc-internal primops dataToTagSmall# and dataToTagLarge#."
       , "In either case, the GHC developers would like to know about it!"
       , "Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug"
       ]
@@ -3554,7 +3558,7 @@ Note [caseRules for dataToTag]
 See also Note [DataToTag overview] in GHC.Tc.Instance.Class.
 
 We want to transform
-  case dataToTagLarge# x of
+  case dataToTagSmall# x of
     DEFAULT -> e1
     1# -> e2
 into
@@ -3569,12 +3573,17 @@ case-flattening and case-of-known-constructor and can be very
 important for code using derived Eq instances.
 
 We can apply this transformation only when we can easily get the
-constructors from the type at which dataToTagLarge# is used.  And we
+constructors from the type at which dataToTagSmall# is used.  And we
 cannot apply this transformation at "type data"-related types without
 breaking invariant I1 from Note [Type data declarations] in
 GHC.Rename.Module.  That leaves exactly the types satisfying condition
 DTT2 from Note [DataToTag overview] in GHC.Tc.Instance.Class.
 
+All of the above applies identically for `dataToTagLarge#`.  And
+thanks to wrinkle DTW5, there is no need to worry about large-tag
+arguments for `dataToTagSmall#`; those cause undefined behavior anyway.
+
+
 Note [Unreachable caseRules alternatives]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Take care if we see something like


=====================================
compiler/GHC/Rename/Splice.hs
=====================================
@@ -85,6 +85,38 @@ checkForTemplateHaskellQuotes e =
   unlessXOptM LangExt.TemplateHaskellQuotes $
     failWith $ thSyntaxError $ IllegalTHQuotes e
 
+{-
+
+Note [Untyped quotes in typed splices and vice versa]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider this typed splice
+   $$(f [| x |])
+
+Is there anything wrong with that /typed/ splice containing an /untyped/
+quote [| x |]?   One could ask the same about an /untyped/ slice containing a
+/typed/ quote.
+
+In fact, both are fine (#24190). Presumably f's type looks something like:
+   f :: Q Expr -> Code Q Int
+
+It is pretty hard for `f` to use its (untyped code) argument to build a typed
+syntax tree, but not impossible:
+* `f` could use `unsafeCodeCoerce :: Q Exp -> Code Q a`
+* `f` could just perform case analysis on the tree
+
+But in the end all that matters is that in $$( e ), the expression `e` has the
+right type.  It doesn't matter how `e` is built.  To put it another way, the
+untyped quote `[| x |]` could also be written `varE 'x`, which is an ordinary
+expression.
+
+Moreover the ticked variable, 'x :: Name, is itself treated as an untyped quote;
+but it is a perfectly fine sub-expression to have in a typed splice.
+
+(Historical note: GHC used to unnecessarily  check that a typed quote only
+occurred in a typed splice: #24190.)
+
+-}
+
 rnTypedBracket :: HsExpr GhcPs -> LHsExpr GhcPs -> RnM (HsExpr GhcRn, FreeVars)
 rnTypedBracket e br_body
   = addErrCtxt (typedQuotationCtxtDoc br_body) $
@@ -93,9 +125,8 @@ rnTypedBracket e br_body
          -- Check for nested brackets
        ; cur_stage <- getStage
        ; case cur_stage of
-           { Splice Typed   -> return ()
-           ; Splice Untyped -> failWithTc $ thSyntaxError
-                                          $ MismatchedSpliceType Untyped IsBracket
+           { Splice _       -> return ()
+               -- See Note [Untyped quotes in typed splices and vice versa]
            ; RunSplice _    ->
                -- See Note [RunSplice ThLevel] in GHC.Tc.Types.
                pprPanic "rnTypedBracket: Renaming typed bracket when running a splice"
@@ -123,9 +154,8 @@ rnUntypedBracket e br_body
          -- Check for nested brackets
        ; cur_stage <- getStage
        ; case cur_stage of
-           { Splice Typed   -> failWithTc $ thSyntaxError
-                                          $ MismatchedSpliceType Typed IsBracket
-           ; Splice Untyped -> return ()
+           { Splice _       -> return ()
+               -- See Note [Untyped quotes in typed splices and vice versa]
            ; RunSplice _    ->
                -- See Note [RunSplice ThLevel] in GHC.Tc.Types.
                pprPanic "rnUntypedBracket: Renaming untyped bracket when running a splice"


=====================================
compiler/GHC/Stg/InferTags/Rewrite.hs
=====================================
@@ -495,10 +495,9 @@ occurrence of `x` and `y` to record whether it is evaluated and
 properly tagged. For the vast majority of primops that's a waste of
 time: the argument is an `Int#` or something.
 
-But code generation for `seq#` and `dataToTagLarge#` /does/ consult that
-tag, to statically avoid generating an eval:
-* `seq#`: uses `getCallMethod` on its first argument, which looks at the `tagSig`
-* `dataToTagLarge#`: checks `tagSig` directly in the `DataToTagOp` case of `cgExpr`.
+But code generation for `seq#` and the `dataToTag#` ops /does/ consult that
+tag, to statically avoid generating an eval.  All three do so via `cgIdApp`,
+which in turn uses `getCallMethod` which looks at the `tagSig`.
 
 So for these we should call `rewriteArgs`.
 
@@ -507,7 +506,7 @@ So for these we should call `rewriteArgs`.
 rewriteOpApp :: InferStgExpr -> RM TgStgExpr
 rewriteOpApp (StgOpApp op args res_ty) = case op of
   op@(StgPrimOp primOp)
-    | primOp == SeqOp || primOp == DataToTagOp
+    | primOp == SeqOp || primOp == DataToTagSmallOp || primOp == DataToTagLargeOp
     -- see Note [Rewriting primop arguments]
     -> (StgOpApp op) <$!> rewriteArgs args <*> pure res_ty
   _ -> pure $! StgOpApp op args res_ty


=====================================
compiler/GHC/StgToCmm/Expr.hs
=====================================
@@ -37,7 +37,7 @@ import GHC.Cmm.Graph
 import GHC.Cmm.BlockId
 import GHC.Cmm hiding ( succ )
 import GHC.Cmm.Info
-import GHC.Cmm.Utils ( zeroExpr, cmmTagMask, mkWordCLit, mAX_PTR_TAG )
+import GHC.Cmm.Utils ( cmmTagMask, mkWordCLit, mAX_PTR_TAG )
 import GHC.Core
 import GHC.Core.DataCon
 import GHC.Types.ForeignCall
@@ -73,55 +73,51 @@ cgExpr (StgApp fun args)     = cgIdApp fun args
 cgExpr (StgOpApp (StgPrimOp SeqOp) [StgVarArg a, _] _res_ty) =
   cgIdApp a []
 
+-- dataToTagSmall# :: a_levpoly -> Int#
+-- See Note [DataToTag overview] in GHC.Tc.Instance.Class,
+-- particularly wrinkles H3 and DTW4
+cgExpr (StgOpApp (StgPrimOp DataToTagSmallOp) [StgVarArg a] _res_ty) = do
+  platform <- getPlatform
+  emitComment (mkFastString "dataToTagSmall#")
+
+  a_eval_reg <- newTemp (bWord platform)
+  _ <- withSequel (AssignTo [a_eval_reg] False) (cgIdApp a [])
+  let a_eval_expr = CmmReg (CmmLocal a_eval_reg)
+      tag1 = cmmConstrTag1 platform a_eval_expr
+
+  -- subtract 1 because we need to return a zero-indexed tag
+  emitReturn [cmmSubWord platform tag1 (CmmLit $ mkWordCLit platform 1)]
+
 -- dataToTagLarge# :: a_levpoly -> Int#
--- See Note [DataToTag overview] in GHC.Tc.Instance.Class
--- TODO: There are some more optimization ideas for this code path
--- in #21710
-cgExpr (StgOpApp (StgPrimOp DataToTagOp) [StgVarArg a] _res_ty) = do
+-- See Note [DataToTag overview] in GHC.Tc.Instance.Class,
+-- particularly wrinkles H3 and DTW4
+cgExpr (StgOpApp (StgPrimOp DataToTagLargeOp) [StgVarArg a] _res_ty) = do
   platform <- getPlatform
   emitComment (mkFastString "dataToTagLarge#")
-  info <- getCgIdInfo a
-  let amode = idInfoToAmode info
-  tag_reg <- assignTemp $ cmmConstrTag1 platform amode
+
+  a_eval_reg <- newTemp (bWord platform)
+  _ <- withSequel (AssignTo [a_eval_reg] False) (cgIdApp a [])
+  let a_eval_expr = CmmReg (CmmLocal a_eval_reg)
+
+  tag1_reg <- assignTemp $ cmmConstrTag1 platform a_eval_expr
   result_reg <- newTemp (bWord platform)
-  let tag = CmmReg $ CmmLocal tag_reg
-      is_tagged = cmmNeWord platform tag (zeroExpr platform)
-      is_too_big_tag = cmmEqWord platform tag (cmmTagMask platform)
-  -- Here we will first check the tag bits of the pointer we were given;
-  -- if this doesn't work then enter the closure and use the info table
-  -- to determine the constructor. Note that all tag bits set means that
-  -- the constructor index is too large to fit in the pointer and therefore
-  -- we must look in the info table. See Note [Tagging big families].
-
-  (fast_path :: CmmAGraph) <- getCode $ do
-      -- Return the constructor index from the pointer tag
-      return_ptr_tag <- getCode $ do
-          emitAssign (CmmLocal result_reg)
-            $ cmmSubWord platform tag (CmmLit $ mkWordCLit platform 1)
-      -- Return the constructor index recorded in the info table
-      return_info_tag <- getCode $ do
-          profile     <- getProfile
-          align_check <- stgToCmmAlignCheck <$> getStgToCmmConfig
-          emitAssign (CmmLocal result_reg)
-            $ getConstrTag profile align_check (cmmUntag platform amode)
-
-      emit =<< mkCmmIfThenElse' is_too_big_tag return_info_tag return_ptr_tag (Just False)
-  -- If we know the argument is already tagged there is no need to generate code to evaluate it
-  -- so we skip straight to the fast path. If we don't know if there is a tag we take the slow
-  -- path which evaluates the argument before fetching the tag.
-  case (idTagSig_maybe a) of
-    Just sig
-      | isTaggedSig sig
-      -> emit fast_path
-    _ -> do
-          slow_path <- getCode $ do
-              tmp <- newTemp (bWord platform)
-              _ <- withSequel (AssignTo [tmp] False) (cgIdApp a [])
-              profile     <- getProfile
-              align_check <- stgToCmmAlignCheck <$> getStgToCmmConfig
-              emitAssign (CmmLocal result_reg)
-                $ getConstrTag profile align_check (cmmUntag platform (CmmReg (CmmLocal tmp)))
-          emit =<< mkCmmIfThenElse' is_tagged fast_path slow_path (Just True)
+  let tag1_expr = CmmReg $ CmmLocal tag1_reg
+      is_too_big_tag = cmmEqWord platform tag1_expr (cmmTagMask platform)
+
+  -- Return the constructor index from the pointer tag
+  -- (Used if pointer tag is small enough to be unambiguous)
+  return_ptr_tag <- getCode $ do
+    emitAssign (CmmLocal result_reg)
+      $ cmmSubWord platform tag1_expr (CmmLit $ mkWordCLit platform 1)
+
+  -- Return the constructor index recorded in the info table
+  return_info_tag <- getCode $ do
+    profile     <- getProfile
+    align_check <- stgToCmmAlignCheck <$> getStgToCmmConfig
+    emitAssign (CmmLocal result_reg)
+      $ getConstrTag profile align_check (cmmUntag platform a_eval_expr)
+
+  emit =<< mkCmmIfThenElse' is_too_big_tag return_info_tag return_ptr_tag (Just False)
   emitReturn [CmmReg $ CmmLocal result_reg]
 
 
@@ -666,9 +662,10 @@ isSimpleScrut _                    _         = return False
 isSimpleOp :: StgOp -> [StgArg] -> FCode Bool
 -- True iff the op cannot block or allocate
 isSimpleOp (StgFCallOp (CCall (CCallSpec _ _ safe)) _) _ = return $! not (playSafe safe)
--- dataToTagLarge# evaluates its argument;
+-- dataToTagSmall#/dataToTagLarge# evaluate an argument;
 -- see Note [DataToTag overview] in GHC.Tc.Instance.Class
-isSimpleOp (StgPrimOp DataToTagOp) _ = return False
+isSimpleOp (StgPrimOp DataToTagSmallOp) _ = return False
+isSimpleOp (StgPrimOp DataToTagLargeOp) _ = return False
 isSimpleOp (StgPrimOp op) stg_args                  = do
     arg_exprs <- getNonVoidArgAmodes stg_args
     cfg       <- getStgToCmmConfig
@@ -879,6 +876,7 @@ cgAlts _ _ _ _ = panic "cgAlts"
 
 
 -- Note [alg-alt heap check]
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~
 --
 -- In an algebraic case with more than one alternative, we will have
 -- code like


=====================================
compiler/GHC/StgToCmm/Prim.hs
=====================================
@@ -1640,7 +1640,8 @@ emitPrimOp cfg primop =
   SeqOp -> alwaysExternal
   GetSparkOp -> alwaysExternal
   NumSparks -> alwaysExternal
-  DataToTagOp -> alwaysExternal
+  DataToTagSmallOp -> alwaysExternal
+  DataToTagLargeOp -> alwaysExternal
   MkApUpd0_Op -> alwaysExternal
   NewBCOOp -> alwaysExternal
   UnpackClosureOp -> alwaysExternal


=====================================
compiler/GHC/StgToJS/Prim.hs
=====================================
@@ -967,7 +967,11 @@ genPrim prof bound ty op = case op of
 
 ------------------------------ Tag to enum stuff --------------------------------
 
-  DataToTagOp -> \[_r] [d] -> pure $ PRPrimCall $ mconcat
+  DataToTagSmallOp -> \[_r] [d] -> pure $ PRPrimCall $ mconcat
+      [ stack .! PreInc sp |= var "h$dataToTag_e"
+      , returnS (app "h$e" [d])
+      ]
+  DataToTagLargeOp -> \[_r] [d] -> pure $ PRPrimCall $ mconcat
       [ stack .! PreInc sp |= var "h$dataToTag_e"
       , returnS (app "h$e" [d])
       ]


=====================================
compiler/GHC/Tc/Instance/Class.hs
=====================================
@@ -50,6 +50,8 @@ import GHC.Core.Class
 
 import GHC.Core ( Expr(..) )
 
+import GHC.StgToCmm.Closure ( isSmallFamily )
+
 import GHC.Utils.Outputable
 import GHC.Utils.Panic
 import GHC.Utils.Misc( splitAtList, fstOf3 )
@@ -671,15 +673,17 @@ But, to avoid all this boilerplate code, and improve optimisation opportunities,
 GHC generates instances like this:
 
    instance DataToTag [a] where
-     dataToTag# = dataToTagLarge#
+     dataToTag# = dataToTagSmall#
 
-using a (temporarily strangely-named) primop `dataToTagLarge#`. The
-primop has the following over-polymorphic type
+using one of two dedicated primops: `dataToTagSmall#` and `dataToTagLarge#`.
+(Why two primops? What's the difference? See wrinkles DTW4 and DTW5.)
+Both primops have the following over-polymorphic type:
 
   dataToTagLarge# :: forall {l::levity} (a::TYPE (BoxedRep l)). a -> Int#
 
-Every call to (dataToTagLarge# @{lev} @ty) that we generate should
-satisfy these conditions:
+Every call to either primop that we generate should look like
+(dataToTagSmall# @{lev} @ty) with two type arguments that satisfy
+these conditions:
 
 (DTT1) `lev` is concrete (either lifted or unlifted), not polymorphic.
    This is an invariant--we must satisfy this or Core Lint will complain.
@@ -698,25 +702,36 @@ satisfy these conditions:
    GHC.Rename.Module.  See Note [caseRules for dataToTag] in
    GHC.Core.Opt.ConstantFold for why this matters.
 
-   While the dataToTagLarge# primop remains exposed from GHC.Prim
-   (and abused in GHC.PrimopWrappers), this cannot be a true invariant.
-   But with a little effort we can ensure that every `dataToTagLarge#`
+   While wrinkle DTW7 is unresolved, this cannot be a true invariant.
+   But with a little effort we can ensure that every primop
    call we generate in a DataToTag instance satisfies this condition.
 
-The `dataToTagLarge#` primop has special handling in several parts of
+(DTT3) If the TyCon in wrinkle DTT2 is a "large data type" with more
+   constructors than fit in pointer tags on the target, then the
+   primop must be dataToTagLarge# and not dataToTagSmall#.
+   Otherwise, the primop must be dataToTagSmall# and not dataToTagLarge#.
+   (See wrinkles DTW4 and DTW5.)
+
+These two primops have special handling in several parts of
 the compiler:
 
-- It has a couple of built-in rewrite rules, implemented in
-  GHC.Core.Opt.ConstantFold.dataToTagRule
+H1. They have a couple of built-in rewrite rules, implemented in
+    GHC.Core.Opt.ConstantFold.dataToTagRule
 
-- The simplifier rewrites most case expressions scrutinizing its result.
-  See Note [caseRules for dataToTag] in GHC.Core.Opt.ConstantFold.
+H2. The simplifier rewrites most case expressions scrutinizing their results.
+    See Note [caseRules for dataToTag] in GHC.Core.Opt.ConstantFold.
 
-- It evaluates its argument; this is implemented via a special case in
-  GHC.StgToCmm.Expr.cgExpr.
+H3. Each evaluates its argument.  But we want to omit this eval when the
+    actual argument is already evaluated and properly tagged.  To do this,
 
-- Additionally, a special case in GHC.Stg.InferTags.Rewrite.rewriteExpr ensures
-  that that any inferred tag information on the argument is retained until then.
+    * We have a special case in GHC.Stg.InferTags.Rewrite.rewriteOpApp
+      ensuring that any inferred tag information on the argument is
+      retained until code generation.
+
+    * We generate code via special cases in GHC.StgToCmm.Expr.cgExpr
+      instead of with the other primops in GHC.StgToCmm.Prim.emitPrimOp;
+      tag info is not readily available in the latter function.
+      (Wrinkle DTW4 describes what we generate after the eval.)
 
 Wrinkles:
 
@@ -727,12 +742,12 @@ Wrinkles:
      [W] DataToTag (D (Either t1 t2))
   GHC uses the built-in instance
      instance DataToTag (D (Either p q)) where
-        dataToTag# x = dataToTagLarge# @Lifted @(R:DEither p q)
+        dataToTag# x = dataToTagSmall# @Lifted @(R:DEither p q)
                                        (x |> sym (ax:DEither p q))
   where `ax:DEither` is the axiom arising from the `data instance`:
     ax:DEither p q :: D (Either p q) ~ R:DEither p q
 
-  Notice that we cast `x` before giving it to `dataToTagLarge#`, so
+  Notice that we cast `x` before giving it to `dataToTagSmall#`, so
   that (DTT2) is satisfied.
 
 (DTW2) Suppose we have module A (T(..)) where { data T = TCon }
@@ -747,7 +762,7 @@ Wrinkles:
 (DTW3) Similar to DTW2, consider this example:
 
     {-# LANGUAGE MagicHash #-}
-    module A (X(X2, X3), f) where
+    module A (X(X2, X3), g) where
     -- see also testsuite/tests/warnings/should_compile/DataToTagWarnings.hs
     import GHC.Exts (dataToTag#, Int#)
     data X = X1 | X2 | X3 | X4
@@ -774,23 +789,93 @@ Wrinkles:
   keepAlive on the constructor names.
   (Contrast with Note [Unused name reporting and HasField].)
 
-(DTW4) It is expected that in the future some instances may select more
-  efficient specialised implementations; for example we may use a
-  separate `dataToTagSmall#` primop for a type with only a few
-  constructors; see #17079 and #21710.
-
-(DTW5) We make no promises about the primops used to implement
+(DTW4) Why have two primops, `dataToTagSmall#` and `dataToTagLarge#`?
+  The way tag information is stored at runtime is described in
+  Note [Tagging big families] in GHC.StgToCmm.Expr.  In particular,
+  for "big data types" we must consult the heap object's info table at
+  least in the mAX_PTR_TAG case, while for "small data types" we can
+  always just examine the tag bits on the pointer itself. So:
+
+  * dataToTagSmall# consults the tag bits in the pointer, ignoring the
+    info table.  It should, therefore, be used only for data type with
+    few enough contructors that the tag always fits in the pointer.
+
+  * dataToTagLarge# also consults the tag bits in the pointer, but
+    must fall back to examining the info table whenever those tag
+    bits are equal to mAX_PTR_TAG.
+
+  One could imagine having one primop with a small/large tag, or just
+  the data type width, but the PrimOp data type is not currently set
+  up for that.  Looking at the type information on the argument during
+  code generation is also possible, but would be less reliable.
+  Remember: type information is not always preserved in STG.
+
+(DTW5) How do the two primops differ in their semantics?  We consider
+  a call `dataToTagSmall# x` to result in undefined behavior whenever
+  the target supports pointer tagging but the actual constructor index
+  for `x` is too large to fit in the pointer's tag bits.  Otherwise,
+  `dataToTagSmall#` behaves identically to `dataToTagLarge#`.
+
+  This allows the rewrites performed in GHC.Core.Opt.ConstantFold to
+  safely treat `dataToTagSmall#` identically to `dataToTagLarge#`:
+  the allowed program behaviors for the former is always a superset of
+  the allowed program behaviors for the latter.
+
+  This undefined behavior is only observable if a user writes a
+  wrongly-sized primop call.  The calls we generate are properly-sized
+  (condition DTT3 above) so that the type system protects us.
+
+(DTW6) We make no promises about the primops used to implement
   DataToTag instances.  Changes to GHC's representation of algebraic
   data types at runtime may force us to redesign these primops.
   Indeed, accommodating such changes without breaking users of the
   original (no longer existing) "dataToTag#" primop is one of the
   main reasons the DataToTag class exists!
 
-  We can currently get away with using the same primop for every
-  DataToTag instance because every Haskell-land data constructor use
-  gets translated to its own "real" heap or static data object at
-  runtime and the index of that constructor is always exposed via
-  pointer tagging and via the object's info table.
+  In particular, our current two primop implementations (as described
+  in wrinkle DTW4) are adequate for every DataToTag instance only
+  because every Haskell-land data constructor use gets translated to
+  its own "real" heap or static data object at runtime and the index
+  of that constructor is always exposed via pointer tagging and via
+  the object's info table.
+
+(DTW7) Currently, the generated module GHC.PrimopWrappers in ghc-prim
+  contains the following non-sense definitions:
+
+    {-# NOINLINE dataToTagSmall# #-}
+    dataToTagSmall# :: a_levpoly -> Int#
+    dataToTagSmall# a1 = GHC.Prim.dataToTagSmall# a1
+    {-# NOINLINE dataToTagLarge# #-}
+    dataToTagLarge# :: a_levpoly -> Int#
+    dataToTagLarge# a1 = GHC.Prim.dataToTagLarge# a1
+
+  Why do these exist? GHCi uses these symbols for... something.  There
+  is on-going work to get rid of them.  See also #24169, #20155, and !6245.
+  Their continued existence makes it difficult to do several nice things:
+
+   * As explained in DTW6, the dataToTag# primops are very internal.
+     We would like to hide them from GHC.Prim entirely to prevent
+     their mis-use, but doing so would cause GHC.PrimopWrappers to
+     fail to compile.
+
+   * The primops are applied at the (confusingly monomorphic) type
+     variable `a_levpoly` in the above definitions.  In particular,
+     they do not satisfy conditions DTT2 and DTT3 above.  We would
+     very much like these conditions to be invariants, but while
+     GHC.PrimopWrappers breaks them we cannot do so.  (The code that
+     would check these invariants in Core Lint exists but remains
+     commented out for now.)
+
+   * This in turn means that `GHC.Core.Opt.ConstantFold.caseRules`
+     must check for condition DTT2 before doing the work described in
+     Note [caseRules for dataToTag].
+
+   * Likewise, wrinkle DTW5 is only necessary because condition DTT3
+     is not an invariant.  Otherwise, invoking the currently-specified
+     undefined behavior of `dataToTagSmall# @ty` would require passing it
+     an argument which will not really have type `ty` at runtime.  And
+     evaluating such an expression is always undefined behavior anyway!
+
 
 
 Historical note:
@@ -816,6 +901,7 @@ matchDataToTag :: Class -> [Type] -> TcM ClsInstResult
 matchDataToTag dataToTagClass [levity, dty] = do
   famEnvs <- tcGetFamInstEnvs
   (gbl_env, _lcl_env) <- getEnvs
+  platform <- getPlatform
   if | isConcreteType levity -- condition C3
      , Just (rawTyCon, rawTyConArgs) <- tcSplitTyConApp_maybe dty
      , let (repTyCon, repArgs, repCo)
@@ -828,13 +914,14 @@ matchDataToTag dataToTagClass [levity, dty] = do
      , let  rdr_env = tcg_rdr_env gbl_env
             inScope con = isJust $ lookupGRE_Name rdr_env $ dataConName con
      , all inScope constrs -- condition C2
+
      , let  repTy = mkTyConApp repTyCon repArgs
-            whichOp
-              -- TODO: More optimized implementations for:
-              --    * small constructor families
-              --    * Bool/Int/Float/etc. on JS backend
+            numConstrs = tyConFamilySize repTyCon
+            !whichOp -- see wrinkle DTW4
+              | isSmallFamily platform numConstrs
+                = primOpId DataToTagSmallOp
               | otherwise
-                = primOpId DataToTagOp
+                = primOpId DataToTagLargeOp
 
             -- See wrinkle DTW1; we must apply the underlying
             -- operation at the representation type and cast it


=====================================
docs/users_guide/9.10.1-notes.rst
=====================================
@@ -6,17 +6,33 @@ Version 9.10.1
 Language
 ~~~~~~~~
 
-- Part 1 of GHC Proposal `#281
-  <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0281-visible-forall.rst>`_
-  "Visible forall in types of terms" has been implemented.
+- GHC Proposal `#281 <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0281-visible-forall.rst>`_
+  "Visible forall in types of terms" has been partially implemented.
   The following code is now accepted by GHC::
 
-    idv :: forall a -> a -> a
-    idv (type a) (x :: a) = x
+    {-# LANGUAGE RequiredTypeArguments #-}
 
-    x = idv (type Int) 42
+    vshow :: forall a -> Show a => a -> String
+    vshow t x = show (x :: t)
 
-  This feature is guarded behind :extension:`RequiredTypeArguments` and :extension:`ExplicitNamespaces`.
+    s1 = vshow Int    42      -- "42"
+    s2 = vshow Double 42      -- "42.0"
+
+  The use of ``forall a ->`` instead of ``forall a.`` indicates a *required* type
+  argument. A required type argument is visually indistinguishable from a value
+  argument but does not exist at runtime.
+
+  This feature is guarded behind :extension:`RequiredTypeArguments`.
+
+- The :extension:`ExplicitNamespaces` extension can now be used in conjunction
+  with :extension:`RequiredTypeArguments` to select the type namespace in a
+  required type argument::
+
+    data T = T               -- the name `T` is ambiguous
+    f :: forall a -> ...     -- `f` expects a required type argument
+
+    x1 = f T         -- refers to the /data/ constructor `T`
+    x2 = f (type T)  -- refers to the /type/ constructor `T`
 
 - Due to an oversight, previous GHC releases (starting from 9.4) allowed the use
   of promoted data types in kinds, even when :extension:`DataKinds` was not


=====================================
docs/users_guide/exts/required_type_arguments.rst
=====================================
@@ -19,42 +19,94 @@ dependent quantification in types of terms::
   id     :: forall a.   a -> a         -- invisible dependent quantification
   id_vdq :: forall a -> a -> a         --   visible dependent quantification
 
-Note that the arrow in ``forall a ->`` is part of the syntax and not a function
-arrow, just like the dot in ``forall a.`` is not a type operator. The essence of
-a ``forall`` is the same regardless of whether it is followed by a dot or an
-arrow: it introduces a type variable. But the way we bind and specify this type
-variable at the term level differs.
+The arrow in ``forall a ->`` is part of the syntax and not a function arrow,
+just like the dot in ``forall a.`` is not a type operator.
 
-When we define ``id``, we can use a lambda to bind a variable that stands for
-the function argument::
+The choice between ``forall a.`` and ``forall a ->`` does not have any effect on
+program execution. Both quantifiers introduce type variables, which are erased
+during compilation. Rather, the main difference is in the syntax used at call
+sites::
 
-  -- For reference: id :: forall a. a -> a
-  id = \x -> x
+  x1 = id       True     -- invisible forall, the type argument is inferred by GHC
+  x2 = id @Bool True     -- invisible forall, the type argument is supplied by the programmer
 
-At the same time, there is no mention of ``a`` in this definition at all. It is
-bound by the compiler behind the scenes, and that is why we call the ordinary
-``forall a.`` an *invisible* quantifier. Compare that to ``forall a ->``, which
-is considered *visible*::
+  x3 = id_vdq _    True  --   visible forall, the type argument is inferred by GHC
+  x4 = id_vdq Bool True  --   visible forall, the type argument is supplied by the programmer
 
-  -- For reference: id_vdq :: forall a -> a -> a
-  id_vdq = \(type t) x -> x
+.. _dependent-quantifier:
 
-This time we have two binders in the lambda:
-* ``type t``, corresponding to ``forall a ->`` in the signature
-* ``x``, corresponding to ``a ->`` in the signature
+Terminology: Dependent quantifier
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Both ``forall a.`` and ``forall a ->`` are said to be "dependent" because the
+result type depends on the supplied type argument: ::
+
+  id @Integer :: Integer -> Integer
+  id @String  :: String  -> String
+
+  id_vdq Integer :: Integer -> Integer
+  id_vdq String  :: String  -> String
+
+Notice how the RHS of the signature is influenced by the LHS.
+
+This is in contrast to the function arrow ``->``, which is a non-dependent
+quantifier::
+
+  putStrLn "Hello" :: IO ()
+  putStrLn "World" :: IO ()
+
+The type of ``putStrLn`` is ``String -> IO ()``. No matter what string we pass
+as input, the result type ``IO ()`` does not depend on it.
+
+This notion of dependence is weaker than the one used in dependently-typed
+languages (see :ref:`pi-types`).
+
+Terminology: Visible quantifier
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+We say that ``forall a.`` is an *invisible* quantifier and ``forall a ->`` is a
+*visible* quantifier. This notion of "visibility" is unrelated to implicit
+quantification, which happens when the quantifier is omitted: ::
 
-And of course, now we also have the option of using the bound ``t`` in a
-subsequent pattern, as well as on the right-hand side of the lambda::
+  id     ::             a -> a    -- implicit quantification, invisible forall
+  id     :: forall a.   a -> a    -- explicit quantification, invisible forall
+  id_vdq :: forall a -> a -> a    -- explicit quantification,   visible forall
 
-  -- For reference: id_vdq :: forall a -> a -> a
-  id_vdq = \(type t) (x :: t) -> x :: t
-  --              ↑        ↑          ↑
-  --            bound     used       used
+The property of "visibility" actually describes whether the corresponding type
+argument is visible at the definition site and at call sites: ::
 
-At use sites, we also instantiate this type variable explicitly::
+  -- Invisible quantification
+  id :: forall a. a -> a
+  id x = x                -- defn site: `a` is not mentioned
+  call_id = id True       -- call site: `a` is invisibly instantiated to `Bool`
 
-  n = id_vdq (type Integer) 42
-  s = id_vdq (type String)  "Hello"
+  -- Visible quantification
+  id_vdq :: forall a -> a -> a
+  id_vdq t x = x                  -- defn site: `a` is visibly bound to `t`
+  call_id_vdq = id_vdq Bool True  -- call site: `a` is visibly instantiated to `Bool`
+
+In the equation for ``id`` there is just one binder on the LHS, ``x``, and it
+corresponds to the value argument, not to the type argument. Compare that with
+the definition of ``id_vdq``::
+
+  id_vdq :: forall a -> a -> a
+  id_vdq t x = x
+
+This time we have two binders on the LHS:
+
+* ``t``, corresponding to ``forall a ->`` in the signature
+* ``x``, corresponding to ``a ->`` in the signature
+
+The bound ``t`` can be used in subsequent patterns, as well as on the right-hand
+side of the equation::
+
+  id_vdq :: forall a -> a -> a
+  id_vdq t (x :: t) = x :: t
+  --     ↑       ↑         ↑
+  --   bound    used      used
+
+We use the terms "visible type argument" and "required type argument"
+interchangeably.
 
 Relation to :extension:`TypeApplications`
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -70,12 +122,12 @@ not reflected syntactically in the expression, it is invisible unless we use a
 Required type arguments are compulsory. They must appear syntactically at call
 sites::
 
-  x1 = id_vdq (type Bool) True    -- OK
-  x2 = id_vdq             True    -- not OK
+  x1 = id_vdq Bool True    -- OK
+  x2 = id_vdq      True    -- not OK
 
 You may use an underscore to infer a required type argument::
 
-  x3 = id_vdq (type _) True       -- OK
+  x3 = id_vdq _ True       -- OK
 
 That is, it is mostly a matter of syntax whether to use ``forall a.`` with type
 applications or ``forall a ->``. One advantage of required type arguments is that
@@ -92,20 +144,265 @@ With :extension:`RequiredTypeArguments`, we can imagine a slightly different API
 
   sizeOf :: forall a -> Storable a => Int
 
-If ``sizeOf`` had this type, we could write ``sizeOf (type Bool)`` without
+If ``sizeOf`` had this type, we could write ``sizeOf Bool`` without
 passing a dummy value.
 
+Required type arguments are erased during compilation. While the source program
+appears to bind and pass required type arguments alongside value arguments, the
+compiled program does not. There is no runtime overhead associated with required
+type arguments relative to the usual, invisible type arguments.
+
 Relation to :extension:`ExplicitNamespaces`
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-The ``type`` keyword that we used in the examples is not actually part of
-:extension:`RequiredTypeArguments`. It is guarded behind
-:extension:`ExplicitNamespaces`. As described in the proposal, required type
-arguments can be passed without a syntactic marker, making them syntactically
-indistinguishble from ordinary function arguments::
+A required type argument is syntactically indistinguishable from a value
+argument. In a function call ``f arg1 arg2 arg3``, it is impossible to tell,
+without looking at the type of ``f``, which of the three arguments are required
+type arguments, if any.
+
+At the same time, one of the design goals of GHC is to be able to perform name
+resolution (find the binding sites of identifiers) without involving the type
+system. Consider: ::
+
+  data Ty = Int | Double | String deriving Show
+  main = print Int
+
+In this example, there are two constructors named ``Int`` in scope:
+
+* The **type constructor** ``Int`` of kind ``Type`` (imported from ``Prelude``)
+* The **data constructor** ``Int`` of type ``Ty`` (defined locally)
+
+How does the compiler or someone reading the code know that ``print Int`` is
+supposed to refer to the data constructor, not the type constructor?  In GHC,
+this is resolved as follows. Each identifier is said to occur either in
+**type syntax** or **term syntax**, depending on the surrounding syntactic
+context::
+
+  -- Examples of X in type syntax
+  type T = X      -- RHS of a type synonym
+  data D = MkD X  -- field of a data constructor declaration
+  a :: X          -- RHS of a type signature
+  b = f (c :: X)  -- RHS of a type signature (in expressions)
+  f (x :: X) = x  -- RHS of a type signature (in patterns)
+
+  -- Examples of X in term syntax
+  c X = a         -- LHS of a function equation
+  c a = X         -- RHS of a function equation
+
+One could imagine the entire program "zoned" into type syntax and term syntax,
+each zone having its own rules for name resolution:
+
+* In type syntax, type constructors take precedence over data constructors.
+* In term syntax, data constructors take precedence over type constructors.
+
+This means that in the ``print Int`` example, the data constructor is selected
+solely based on the fact that the ``Int`` occurs in term syntax. This is firmly
+determined before GHC attempts to type-check the expression, so the type of
+``print`` does not influence which of the two ``Int``\s is passed to it.
+
+This may not be the desired behavior in a required type argument. Consider::
+
+  vshow :: forall a -> Show a => a -> String
+  vshow t x = show (x :: t)
+
+  s1 = vshow Int    42      -- "42"
+  s2 = vshow Double 42      -- "42.0"
+
+The function calls ``vshow Int 42`` and ``vshow Double 42`` are written in
+*term* syntax, while the intended referents of ``Int`` and ``Double`` are the
+respective *type* constructors. As long as there are no data constructors named
+``Int`` or ``Double`` in scope, the example works as intended. However, if such
+clashing constructor names are introduced, they may disrupt name resolution::
+
+  data Ty = Int | Double | String
+
+  vshow :: forall a -> Show a => a -> String
+  vshow t x = show (x :: t)
+
+  s1 = vshow Int    42      -- error: Expected a type, but ‘Int’ has kind ‘Ty’
+  s2 = vshow Double 42      -- error: Expected a type, but ‘Double’ has kind ‘Ty’
+
+In this example the intent was to refer to ``Int`` and ``Double`` as types, but
+the names were resolved in favor of data constructors, resulting in type errors.
+
+The example can be fixed with the help of :extension:`ExplicitNamespaces`, which
+allows embedding type syntax into term syntax using the ``type`` keyword::
+
+  s1 = vshow (type Int)    42
+  s2 = vshow (type Double) 42
+
+A similar problem occurs with list and tuple syntax. In type syntax, ``[a]`` is
+the type of a list, i.e. ``Data.List.List a``. In term syntax, ``[a]`` is a
+singleton list, i.e. ``a : []``. A naive attempt to use the list type as a
+required type argument will result in a type error::
+
+  s3 = vshow [Int] [1,2,3]  -- error: Expected a type, but ‘[Int]’ has kind ‘[Type]’
+
+The problem is that GHC assumes ``[Int]`` to stand for ``Int : []`` instead of
+the intended ``Data.List.List Int``. This, too, can be solved using the ``type`` keyword::
+
+  s3 = vshow (type [Int]) [1,2,3]
+
+Since the ``type`` keyword is merely a namespace disambiguation mechanism, it
+need not apply to the entire type argument. Using it to disambiguate only a part
+of the type argument is also valid::
+
+  f :: forall a -> ...   -- `f`` is a function that expects a required type argument
+
+  r1 = f (type (Either () Int))           -- `type` applied to the entire type argument
+  r2 = f (Either (type ()) Int)           -- `type` applied to one part of it
+  r3 = f (Either (type ()) (type Int))    -- `type` applied to multiple parts
+
+That is, the expression ``Either (type ()) (type Int)`` does *not* indicate that
+``Either`` is applied to two type arguments; rather, the entire expression is a
+single type argument and ``type`` is used to disambiguate parts of it.
+
+Outside a required type argument, it is illegal to use ``type``:
+::
+
+  r4 = type Int  -- illegal use of ‘type’
+
+Finally, there are types that require the ``type`` keyword only due to
+limitations of the current implementation::
+
+  a1 = f (type (Int -> Bool))                       -- function type
+  a2 = f (type (Read T => T))                       -- constrained type
+  a3 = f (type (forall a. a))                       -- universally quantified type
+  a4 = f (type (forall a. Read a => String -> a))   -- a combination of the above
+
+This restriction will be relaxed in a future release of GHC.
+
+Effect on implicit quantification
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Implicit quantification is said to occur when GHC inserts an implicit ``forall``
+to bind type variables::
+
+  const :: a -> b -> a               -- implicit quantification
+  const :: forall a b. a -> b -> a   -- explicit quantification
+
+Normally, implicit quantification is unaffected by term variables in scope:
+::
+  f a = ...  -- the LHS binds `a`
+    where const :: a -> b -> a
+             -- implicit quantification over `a` takes place
+             -- despite the `a` bound on the LHS of `f`
+
+When :extension:`RequiredTypeArguments` is in effect, names bound in term syntax
+are not implicitly quantified. This allows us to accept the following example: ::
+
+  readshow :: forall a -> (Read a, Show a) => String -> String
+  readshow t s = show (read s :: t)
+
+  s1 = readshow Int    "42"      -- "42"
+  s2 = readshow Double "42"      -- "42.0"
+
+Note how ``t`` is bound on the LHS of a function equation (term syntax), and
+then used in a type annotation (type syntax). Under the usual rules for implicit
+quantification, the ``t`` would have been implicitly quantified: ::
+
+  -- RequiredTypeArguments
+  readshow t s = show (read s :: t)   -- the `t` is captured
+  --       ↑                     ↑
+  --      bound                 used
+
+  -- NoRequiredTypeArguments
+  readshow t s = show (read s :: t)   -- the `t` is implicitly quantified as follows:
+  readshow t s = show (read s :: forall t. t)
+  --       ↑                            ↑  ↑
+  --      bound                      bound used
+
+On the one hand, taking the current scope into account allows us to accept
+programs like the one above. On the other hand, some existing programs will no
+longer compile: ::
+
+  a = 42
+  f :: a -> a    -- RequiredTypeArguments: the top-level `a` is captured
+
+Because of that, merely enabling :extension:`RequiredTypeArguments` might lead
+to type errors of this form::
+
+  Term variable ‘a’ cannot be used here
+    (term variables cannot be promoted)
+
+There are two possible ways to fix this error::
+
+  a = 42
+  f1 :: b -> b              -- (1) use a different variable name
+  f2 :: forall a. a -> a    -- (2) use an explicit forall
+
+If you are converting a large codebase to be compatible with
+:extension:`RequiredTypeArguments`, consider using
+:ghc-flag:`-Wterm-variable-capture` during the migration. It is a warning that
+detects instances of implicit quantification incompatible with
+:extension:`RequiredTypeArguments`: ::
+
+  The type variable ‘a’ is implicitly quantified,
+  even though another variable of the same name is in scope:
+    ‘a’ defined at ...
+
+.. _pi-types:
+
+Relation to Π-types
+~~~~~~~~~~~~~~~~~~~
+
+Both ``forall a.`` and ``forall a ->`` are dependent quantifiers in the narrow
+sense defined in :ref:`dependent-quantifier`. However, neither of them
+constitutes a dependent function type (Π-type) that might be familiar to users
+coming from dependently-typed languages or proof assistants.
+
+* Haskell has always had functions whose result *value* depends on
+  the argument *value*::
+
+    not True  = False   -- argument value: True;  result value: False
+    (*2) 5    = 10      -- argument value: 5;     result value: 10
+
+  This captures the usual idea of a function, denoted ``a -> b``.
+
+* Haskell also has functions whose result *type* depends on the argument *type*:
+  ::
+
+    id    @Int  :: Int  -> Int    -- argument type: Int;  result type: Int  -> Int
+    id_vdq Bool :: Bool -> Bool   -- argument type: Bool; result type: Bool -> Bool
+
+  This captures the idea of parametric polymorphism, denoted ``forall a. b`` or
+  ``forall a -> b``.
+
+* Furthermore, Haskell has functions whose result *value* depends on the
+  argument *type*::
+
+    maxBound @Int8   = 127    -- argument type: Int8;  result value: 127
+    maxBound @Int16  = 32767  -- argument type: Int16; result value: 32767
+
+  This captures the idea of ad-hoc (class-based) polymorphism,
+  denoted ``C a => b``.
+
+* However, Haskell does **not** have direct support for functions whose result
+  *type* depends on the argument *value*. In the literature, these are often
+  called "dependent functions", or "Π-types".
+
+  Consider: ::
+
+    type F :: Bool -> Bool
+    type family F b where
+      F True  = ...
+      F False = ...
+
+    f :: Bool -> Bool
+    f True  = ...
+    f False = ...
+
+  In this example, we define a type family ``F`` to pattern-match on ``b`` at
+  the type level; and a function ``f`` to pattern-match on ``b`` at the term
+  level. However, it is impossible to quantify over ``b`` in such a way that
+  both ``F`` and ``f`` could be applied to it::
+
+    depfun :: forall (b :: Bool) -> F b  -- Allowed
+    depfun b = ... (f b) ...             -- Not allowed
 
-  n = id_vdq Integer 42
+  It is illegal to pass ``b`` to ``f`` because ``b`` does not exist at runtime.
+  Types and type arguments are erased before runtime.
 
-In this example we pass ``Integer`` as opposed to ``(type Integer)``.
-This means that :extension:`RequiredTypeArguments` is not tied to the ``type``
-syntax, which belongs to :extension:`ExplicitNamespaces`.
\ No newline at end of file
+The :extension:`RequiredTypeArguments` extension does not add dependent
+functions, which would be a much bigger step. Rather :extension:`RequiredTypeArguments`
+just makes it possible for the type arguments of a function to be compulsory.
\ No newline at end of file


=====================================
docs/users_guide/using-warnings.rst
=====================================
@@ -2440,8 +2440,8 @@ of ``-W(no-)*``.
     For example: ::
 
        a = 15
-       f :: a -> a    -- Does ‘a’ refer to the term-level binding
-                      -- or is it implicitly quantified?
+       f :: a -> a    -- NoRequiredTypeArguments: The ‘a’ is implicitly quantified
+                      -- RequiredTypeArguments:   The ‘a’ refers to the term-level binding
 
     When :ghc-flag:`-Wterm-variable-capture` is enabled, GHC warns against implicit quantification
     that would stop working under :extension:`RequiredTypeArguments`.


=====================================
libraries/base/src/GHC/Base.hs
=====================================
@@ -117,8 +117,8 @@ import GHC.Classes
 import GHC.CString
 import GHC.Magic
 import GHC.Magic.Dict
-import GHC.Prim hiding (dataToTagLarge#)
-  -- Hide dataToTagLarge# because it is expected to break for
+import GHC.Prim hiding (dataToTagSmall#, dataToTagLarge#)
+  -- Hide dataToTag# ops because they are expected to break for
   -- GHC-internal reasons in the near future, and shouldn't
   -- be exposed from base (not even GHC.Exts)
 


=====================================
libraries/base/src/GHC/Exts.hs
=====================================
@@ -133,8 +133,8 @@ module GHC.Exts
         maxTupleSize,
        ) where
 
-import GHC.Prim hiding ( coerce, dataToTagLarge# )
-  -- Hide dataToTagLarge# because it is expected to break for
+import GHC.Prim hiding ( coerce, dataToTagSmall#, dataToTagLarge# )
+  -- Hide dataToTag# ops because they are expected to break for
   -- GHC-internal reasons in the near future, and shouldn't
   -- be exposed from base (not even GHC.Exts)
 


=====================================
testsuite/tests/codeGen/should_compile/T21710a.stderr
=====================================
@@ -1,117 +1,44 @@
 
-==================== Output Cmm ====================
-[section ""cstring" . M.$tc'E2_bytes" {
-     M.$tc'E2_bytes:
-         I8[] "'E"
- }]
-
-
-
-==================== Output Cmm ====================
-[section ""cstring" . M.$tc'D2_bytes" {
-     M.$tc'D2_bytes:
-         I8[] "'D"
- }]
-
-
-
-==================== Output Cmm ====================
-[section ""cstring" . M.$tc'C2_bytes" {
-     M.$tc'C2_bytes:
-         I8[] "'C"
- }]
-
-
-
-==================== Output Cmm ====================
-[section ""cstring" . M.$tc'B2_bytes" {
-     M.$tc'B2_bytes:
-         I8[] "'B"
- }]
-
-
-
-==================== Output Cmm ====================
-[section ""cstring" . M.$tc'A3_bytes" {
-     M.$tc'A3_bytes:
-         I8[] "'A"
- }]
-
-
-
-==================== Output Cmm ====================
-[section ""cstring" . M.$tcE2_bytes" {
-     M.$tcE2_bytes:
-         I8[] "E"
- }]
-
-
-
-==================== Output Cmm ====================
-[section ""cstring" . M.$trModule2_bytes" {
-     M.$trModule2_bytes:
-         I8[] "M"
- }]
-
-
-
-==================== Output Cmm ====================
-[section ""cstring" . M.$trModule4_bytes" {
-     M.$trModule4_bytes:
-         I8[] "main"
- }]
-
-
-
 ==================== Output Cmm ====================
 [M.foo_entry() { //  [R2]
-         { info_tbls: [(cBa,
-                        label: block_cBa_info
+         { info_tbls: [(cCU,
+                        label: block_cCU_info
                         rep: StackRep []
                         srt: Nothing),
-                       (cBi,
+                       (cD2,
                         label: M.foo_info
                         rep: HeapRep static { Fun {arity: 1 fun_type: ArgSpec 5} }
                         srt: Nothing)]
            stack_info: arg_space: 8
          }
      {offset
-       cBi: // global
-           if ((Sp + -8) < SpLim) (likely: False) goto cBj; else goto cBk;   // CmmCondBranch
-       cBj: // global
+       cD2: // global
+           if ((Sp + -8) < SpLim) (likely: False) goto cD3; else goto cD4;   // CmmCondBranch
+       cD3: // global
            R1 = M.foo_closure;   // CmmAssign
            call (stg_gc_fun)(R2, R1) args: 8, res: 0, upd: 8;   // CmmCall
-       cBk: // global
-           I64[Sp - 8] = cBa;   // CmmStore
+       cD4: // global
+           I64[Sp - 8] = cCU;   // CmmStore
            R1 = R2;   // CmmAssign
            Sp = Sp - 8;   // CmmAssign
-           if (R1 & 7 != 0) goto cBa; else goto cBb;   // CmmCondBranch
-       cBb: // global
-           call (I64[R1])(R1) returns to cBa, args: 8, res: 8, upd: 8;   // CmmCall
-       cBa: // global
-           _cBh::P64 = R1 & 7;   // CmmAssign
-           if (_cBh::P64 != 1) goto uBz; else goto cBf;   // CmmCondBranch
-       uBz: // global
-           if (_cBh::P64 != 2) goto cBe; else goto cBg;   // CmmCondBranch
-       cBe: // global
-           // dataToTag#
-           _cBn::P64 = R1 & 7;   // CmmAssign
-           if (_cBn::P64 == 7) (likely: False) goto cBs; else goto cBr;   // CmmCondBranch
-       cBs: // global
-           _cBo::I64 = %MO_UU_Conv_W32_W64(I32[I64[R1 & (-8)] - 4]);   // CmmAssign
-           goto cBq;   // CmmBranch
-       cBr: // global
-           _cBo::I64 = _cBn::P64 - 1;   // CmmAssign
-           goto cBq;   // CmmBranch
-       cBq: // global
-           R1 = _cBo::I64;   // CmmAssign
+           if (R1 & 7 != 0) goto cCU; else goto cCV;   // CmmCondBranch
+       cCV: // global
+           call (I64[R1])(R1) returns to cCU, args: 8, res: 8, upd: 8;   // CmmCall
+       cCU: // global
+           _cD1::P64 = R1 & 7;   // CmmAssign
+           if (_cD1::P64 != 1) goto uDf; else goto cCZ;   // CmmCondBranch
+       uDf: // global
+           if (_cD1::P64 != 2) goto cCY; else goto cD0;   // CmmCondBranch
+       cCY: // global
+           // dataToTagSmall#
+           R1 = R1 & 7 - 1;   // CmmAssign
            Sp = Sp + 8;   // CmmAssign
            call (P64[Sp])(R1) args: 8, res: 0, upd: 8;   // CmmCall
-       cBg: // global
+       cD0: // global
            R1 = 42;   // CmmAssign
            Sp = Sp + 8;   // CmmAssign
            call (P64[Sp])(R1) args: 8, res: 0, upd: 8;   // CmmCall
-       cBf: // global
+       cCZ: // global
            R1 = 2;   // CmmAssign
            Sp = Sp + 8;   // CmmAssign
            call (P64[Sp])(R1) args: 8, res: 0, upd: 8;   // CmmCall
@@ -124,190 +51,6 @@
 
 
 
-==================== Output Cmm ====================
-[section ""data" . M.$trModule3_closure" {
-     M.$trModule3_closure:
-         const GHC.Types.TrNameS_con_info;
-         const M.$trModule4_bytes;
- }]
-
-
-
-==================== Output Cmm ====================
-[section ""data" . M.$trModule1_closure" {
-     M.$trModule1_closure:
-         const GHC.Types.TrNameS_con_info;
-         const M.$trModule2_bytes;
- }]
-
-
-
-==================== Output Cmm ====================
-[section ""data" . M.$trModule_closure" {
-     M.$trModule_closure:
-         const GHC.Types.Module_con_info;
-         const M.$trModule3_closure+1;
-         const M.$trModule1_closure+1;
-         const 3;
- }]
-
-
-
-==================== Output Cmm ====================
-[section ""data" . M.$tcE1_closure" {
-     M.$tcE1_closure:
-         const GHC.Types.TrNameS_con_info;
-         const M.$tcE2_bytes;
- }]
-
-
-
-==================== Output Cmm ====================
-[section ""data" . M.$tcE_closure" {
-     M.$tcE_closure:
-         const GHC.Types.TyCon_con_info;
-         const M.$trModule_closure+1;
-         const M.$tcE1_closure+1;
-         const GHC.Types.krep$*_closure+5;
-         const 10475418246443540865;
-         const 12461417314693222409;
-         const 0;
-         const 3;
- }]
-
-
-
-==================== Output Cmm ====================
-[section ""data" . M.$tc'A1_closure" {
-     M.$tc'A1_closure:
-         const GHC.Types.KindRepTyConApp_con_info;
-         const M.$tcE_closure+1;
-         const GHC.Types.[]_closure+1;
-         const 3;
- }]
-
-
-
-==================== Output Cmm ====================
-[section ""data" . M.$tc'A2_closure" {
-     M.$tc'A2_closure:
-         const GHC.Types.TrNameS_con_info;
-         const M.$tc'A3_bytes;
- }]
-
-
-
-==================== Output Cmm ====================
-[section ""data" . M.$tc'A_closure" {
-     M.$tc'A_closure:
-         const GHC.Types.TyCon_con_info;
-         const M.$trModule_closure+1;
-         const M.$tc'A2_closure+1;
-         const M.$tc'A1_closure+1;
-         const 10991425535368257265;
-         const 3459663971500179679;
-         const 0;
-         const 3;
- }]
-
-
-
-==================== Output Cmm ====================
-[section ""data" . M.$tc'B1_closure" {
-     M.$tc'B1_closure:
-         const GHC.Types.TrNameS_con_info;
-         const M.$tc'B2_bytes;
- }]
-
-
-
-==================== Output Cmm ====================
-[section ""data" . M.$tc'B_closure" {
-     M.$tc'B_closure:
-         const GHC.Types.TyCon_con_info;
-         const M.$trModule_closure+1;
-         const M.$tc'B1_closure+1;
-         const M.$tc'A1_closure+1;
-         const 13038863156169552918;
-         const 13430333535161531545;
-         const 0;
-         const 3;
- }]
-
-
-
-==================== Output Cmm ====================
-[section ""data" . M.$tc'C1_closure" {
-     M.$tc'C1_closure:
-         const GHC.Types.TrNameS_con_info;
-         const M.$tc'C2_bytes;
- }]
-
-
-
-==================== Output Cmm ====================
-[section ""data" . M.$tc'C_closure" {
-     M.$tc'C_closure:
-         const GHC.Types.TyCon_con_info;
-         const M.$trModule_closure+1;
-         const M.$tc'C1_closure+1;
-         const M.$tc'A1_closure+1;
-         const 8482817676735632621;
-         const 8146597712321241387;
-         const 0;
-         const 3;
- }]
-
-
-
-==================== Output Cmm ====================
-[section ""data" . M.$tc'D1_closure" {
-     M.$tc'D1_closure:
-         const GHC.Types.TrNameS_con_info;
-         const M.$tc'D2_bytes;
- }]
-
-
-
-==================== Output Cmm ====================
-[section ""data" . M.$tc'D_closure" {
-     M.$tc'D_closure:
-         const GHC.Types.TyCon_con_info;
-         const M.$trModule_closure+1;
-         const M.$tc'D1_closure+1;
-         const M.$tc'A1_closure+1;
-         const 7525207739284160575;
-         const 13746130127476219356;
-         const 0;
-         const 3;
- }]
-
-
-
-==================== Output Cmm ====================
-[section ""data" . M.$tc'E1_closure" {
-     M.$tc'E1_closure:
-         const GHC.Types.TrNameS_con_info;
-         const M.$tc'E2_bytes;
- }]
-
-
-
-==================== Output Cmm ====================
-[section ""data" . M.$tc'E_closure" {
-     M.$tc'E_closure:
-         const GHC.Types.TyCon_con_info;
-         const M.$trModule_closure+1;
-         const M.$tc'E1_closure+1;
-         const M.$tc'A1_closure+1;
-         const 6748545530683684316;
-         const 10193016702094081137;
-         const 0;
-         const 3;
- }]
-
-
-
 ==================== Output Cmm ====================
 [section ""data" . M.A_closure" {
      M.A_closure:
@@ -362,14 +105,14 @@
 
 ==================== Output Cmm ====================
 [M.A_con_entry() { //  []
-         { info_tbls: [(cC5,
+         { info_tbls: [(cDt,
                         label: M.A_con_info
                         rep: HeapRep 1 nonptrs { Con {tag: 0 descr:"main:M.A"} }
                         srt: Nothing)]
            stack_info: arg_space: 8
          }
      {offset
-       cC5: // global
+       cDt: // global
            R1 = R1 + 1;   // CmmAssign
            call (P64[Sp])(R1) args: 8, res: 0, upd: 8;   // CmmCall
      }
@@ -379,14 +122,14 @@
 
 ==================== Output Cmm ====================
 [M.B_con_entry() { //  []
-         { info_tbls: [(cCa,
+         { info_tbls: [(cDy,
                         label: M.B_con_info
                         rep: HeapRep 1 nonptrs { Con {tag: 1 descr:"main:M.B"} }
                         srt: Nothing)]
            stack_info: arg_space: 8
          }
      {offset
-       cCa: // global
+       cDy: // global
            R1 = R1 + 2;   // CmmAssign
            call (P64[Sp])(R1) args: 8, res: 0, upd: 8;   // CmmCall
      }
@@ -396,14 +139,14 @@
 
 ==================== Output Cmm ====================
 [M.C_con_entry() { //  []
-         { info_tbls: [(cCf,
+         { info_tbls: [(cDD,
                         label: M.C_con_info
                         rep: HeapRep 1 nonptrs { Con {tag: 2 descr:"main:M.C"} }
                         srt: Nothing)]
            stack_info: arg_space: 8
          }
      {offset
-       cCf: // global
+       cDD: // global
            R1 = R1 + 3;   // CmmAssign
            call (P64[Sp])(R1) args: 8, res: 0, upd: 8;   // CmmCall
      }
@@ -413,14 +156,14 @@
 
 ==================== Output Cmm ====================
 [M.D_con_entry() { //  []
-         { info_tbls: [(cCk,
+         { info_tbls: [(cDI,
                         label: M.D_con_info
                         rep: HeapRep 1 nonptrs { Con {tag: 3 descr:"main:M.D"} }
                         srt: Nothing)]
            stack_info: arg_space: 8
          }
      {offset
-       cCk: // global
+       cDI: // global
            R1 = R1 + 4;   // CmmAssign
            call (P64[Sp])(R1) args: 8, res: 0, upd: 8;   // CmmCall
      }
@@ -430,14 +173,14 @@
 
 ==================== Output Cmm ====================
 [M.E_con_entry() { //  []
-         { info_tbls: [(cCp,
+         { info_tbls: [(cDN,
                         label: M.E_con_info
                         rep: HeapRep 1 nonptrs { Con {tag: 4 descr:"main:M.E"} }
                         srt: Nothing)]
            stack_info: arg_space: 8
          }
      {offset
-       cCp: // global
+       cDN: // global
            R1 = R1 + 5;   // CmmAssign
            call (P64[Sp])(R1) args: 8, res: 0, upd: 8;   // CmmCall
      }


=====================================
testsuite/tests/linters/notes.stdout
=====================================
@@ -1,41 +1,40 @@
-ref    compiler/GHC/Core/Coercion/Axiom.hs:463:2:     Note [RoughMap and rm_empty]
-ref    compiler/GHC/Core/Opt/OccurAnal.hs:983:7:     Note [Loop breaking]
-ref    compiler/GHC/Core/Opt/SetLevels.hs:1574:30:     Note [Top level scope]
-ref    compiler/GHC/Core/Opt/Simplify/Iteration.hs:2826:13:     Note [Case binder next]
-ref    compiler/GHC/Core/Opt/Simplify/Iteration.hs:4018:8:     Note [Lambda-bound unfoldings]
-ref    compiler/GHC/Core/Opt/Simplify/Utils.hs:1343:37:     Note [Gentle mode]
-ref    compiler/GHC/Core/Opt/Specialise.hs:1765:29:     Note [Arity decrease]
-ref    compiler/GHC/Core/TyCo/Rep.hs:1565:31:     Note [What prevents a constraint from floating]
-ref    compiler/GHC/Driver/DynFlags.hs:1245:49:     Note [Eta-reduction in -O0]
-ref    compiler/GHC/Driver/Main.hs:1762:34:     Note [simpleTidyPgm - mkBootModDetailsTc]
-ref    compiler/GHC/Hs/Expr.hs:194:63:     Note [Pending Splices]
-ref    compiler/GHC/Hs/Expr.hs:1738:87:     Note [Lifecycle of a splice]
-ref    compiler/GHC/Hs/Expr.hs:1774:7:     Note [Pending Splices]
-ref    compiler/GHC/Hs/Extension.hs:146:5:     Note [Strict argument type constraints]
-ref    compiler/GHC/Hs/Pat.hs:143:74:     Note [Lifecycle of a splice]
-ref    compiler/GHC/HsToCore/Pmc/Solver.hs:858:20:     Note [COMPLETE sets on data families]
-ref    compiler/GHC/HsToCore/Quote.hs:1476:7:     Note [How brackets and nested splices are handled]
-ref    compiler/GHC/Stg/Unarise.hs:442:32:     Note [Renaming during unarisation]
-ref    compiler/GHC/StgToCmm/Expr.hs:585:4:     Note [case on bool]
-ref    compiler/GHC/StgToCmm/Expr.hs:853:3:     Note [alg-alt heap check]
+ref    compiler/GHC/Core/Coercion/Axiom.hs:472:2:     Note [RoughMap and rm_empty]
+ref    compiler/GHC/Core/Opt/OccurAnal.hs:1157:7:     Note [Loop breaking]
+ref    compiler/GHC/Core/Opt/SetLevels.hs:1586:30:     Note [Top level scope]
+ref    compiler/GHC/Core/Opt/Simplify/Iteration.hs:2832:13:     Note [Case binder next]
+ref    compiler/GHC/Core/Opt/Simplify/Iteration.hs:4023:8:     Note [Lambda-bound unfoldings]
+ref    compiler/GHC/Core/Opt/Simplify/Utils.hs:1342:37:     Note [Gentle mode]
+ref    compiler/GHC/Core/Opt/Specialise.hs:1763:29:     Note [Arity decrease]
+ref    compiler/GHC/Core/TyCo/Rep.hs:1652:31:     Note [What prevents a constraint from floating]
+ref    compiler/GHC/Driver/DynFlags.hs:1251:52:     Note [Eta-reduction in -O0]
+ref    compiler/GHC/Driver/Main.hs:1749:34:     Note [simpleTidyPgm - mkBootModDetailsTc]
+ref    compiler/GHC/Hs/Expr.hs:191:63:     Note [Pending Splices]
+ref    compiler/GHC/Hs/Expr.hs:1727:87:     Note [Lifecycle of a splice]
+ref    compiler/GHC/Hs/Expr.hs:1763:7:     Note [Pending Splices]
+ref    compiler/GHC/Hs/Extension.hs:147:5:     Note [Strict argument type constraints]
+ref    compiler/GHC/Hs/Pat.hs:141:74:     Note [Lifecycle of a splice]
+ref    compiler/GHC/HsToCore/Pmc/Solver.hs:856:20:     Note [COMPLETE sets on data families]
+ref    compiler/GHC/HsToCore/Quote.hs:1487:7:     Note [How brackets and nested splices are handled]
+ref    compiler/GHC/Stg/Unarise.hs:438:32:     Note [Renaming during unarisation]
+ref    compiler/GHC/StgToCmm/Expr.hs:578:4:     Note [case on bool]
 ref    compiler/GHC/Tc/Gen/HsType.hs:556:56:     Note [Skolem escape prevention]
-ref    compiler/GHC/Tc/Gen/HsType.hs:2621:7:     Note [Matching a kind signature with a declaration]
-ref    compiler/GHC/Tc/Gen/Pat.hs:176:20:     Note [Typing patterns in pattern bindings]
-ref    compiler/GHC/Tc/Gen/Pat.hs:1127:7:     Note [Matching polytyped patterns]
-ref    compiler/GHC/Tc/Gen/Sig.hs:81:10:     Note [Overview of type signatures]
-ref    compiler/GHC/Tc/Gen/Splice.hs:356:16:     Note [How brackets and nested splices are handled]
-ref    compiler/GHC/Tc/Gen/Splice.hs:531:35:     Note [PendingRnSplice]
-ref    compiler/GHC/Tc/Gen/Splice.hs:655:7:     Note [How brackets and nested splices are handled]
-ref    compiler/GHC/Tc/Gen/Splice.hs:888:11:     Note [How brackets and nested splices are handled]
-ref    compiler/GHC/Tc/Instance/Family.hs:474:35:     Note [Constrained family instances]
-ref    compiler/GHC/Tc/Solver/Rewrite.hs:1009:7:     Note [Stability of rewriting]
-ref    compiler/GHC/Tc/TyCl.hs:1130:6:     Note [Unification variables need fresh Names]
-ref    compiler/GHC/Tc/Types/Constraint.hs:226:34:     Note [NonCanonical Semantics]
-ref    compiler/GHC/Types/Demand.hs:302:25:     Note [Preserving Boxity of results is rarely a win]
-ref    compiler/GHC/Unit/Module/Deps.hs:81:13:     Note [Structure of dep_boot_mods]
+ref    compiler/GHC/Tc/Gen/HsType.hs:2676:7:     Note [Matching a kind signature with a declaration]
+ref    compiler/GHC/Tc/Gen/Pat.hs:174:20:     Note [Typing patterns in pattern bindings]
+ref    compiler/GHC/Tc/Gen/Pat.hs:1163:7:     Note [Matching polytyped patterns]
+ref    compiler/GHC/Tc/Gen/Sig.hs:80:10:     Note [Overview of type signatures]
+ref    compiler/GHC/Tc/Gen/Splice.hs:358:16:     Note [How brackets and nested splices are handled]
+ref    compiler/GHC/Tc/Gen/Splice.hs:533:35:     Note [PendingRnSplice]
+ref    compiler/GHC/Tc/Gen/Splice.hs:657:7:     Note [How brackets and nested splices are handled]
+ref    compiler/GHC/Tc/Gen/Splice.hs:891:11:     Note [How brackets and nested splices are handled]
+ref    compiler/GHC/Tc/Instance/Family.hs:406:35:     Note [Constrained family instances]
+ref    compiler/GHC/Tc/Solver/Rewrite.hs:1010:7:     Note [Stability of rewriting]
+ref    compiler/GHC/Tc/TyCl.hs:1316:6:     Note [Unification variables need fresh Names]
+ref    compiler/GHC/Tc/Types/Constraint.hs:206:38:     Note [NonCanonical Semantics]
+ref    compiler/GHC/Types/Demand.hs:301:25:     Note [Preserving Boxity of results is rarely a win]
+ref    compiler/GHC/Unit/Module/Deps.hs:83:13:     Note [Structure of dep_boot_mods]
 ref    compiler/GHC/Utils/Monad.hs:410:34:     Note [multiShotIO]
 ref    compiler/Language/Haskell/Syntax/Binds.hs:200:31:     Note [fun_id in Match]
-ref    configure.ac:210:10:     Note [Linking ghc-bin against threaded stage0 RTS]
+ref    configure.ac:203:10:     Note [Linking ghc-bin against threaded stage0 RTS]
 ref    docs/core-spec/core-spec.mng:177:6:     Note [TyBinders]
 ref    hadrian/src/Expression.hs:145:30:     Note [Linking ghc-bin against threaded stage0 RTS]
 ref    linters/lint-notes/Notes.hs:32:29:     Note [" <> T.unpack x <> "]


=====================================
testsuite/tests/simplCore/should_compile/T22375.hs
=====================================
@@ -1,12 +1,19 @@
 module T22375 where
 
-data X = A | B | C | D | E
+data X
+  = A | B | C | D | E
+  | F | G | H | I | J
   deriving Eq
 
 f :: X -> Int -> Int
 f x v
-  | x == A = 1 + v
-  | x == B = 2 + v
-  | x == C = 3 + v
-  | x == D = 4 + v
-  | otherwise = 5 + v
+  | x == A = v + 1
+  | x == B = v + 2
+  | x == C = v + 3
+  | x == D = v + 4
+  | x == E = v + 5
+  | x == F = v + 6
+  | x == G = v + 7
+  | x == H = v + 8
+  | x == I = v + 9
+  | otherwise = v + 10


=====================================
testsuite/tests/simplCore/should_compile/T22375.stderr
=====================================
@@ -1,7 +1,7 @@
 
 ==================== Tidy Core ====================
 Result size of Tidy Core
-  = {terms: 76, types: 41, coercions: 0, joins: 0/0}
+  = {terms: 96, types: 41, coercions: 0, joins: 0/0}
 
 -- RHS size: {terms: 14, types: 9, coercions: 0, joins: 0/0}
 T22375.$fEqX_$c== :: X -> X -> Bool
@@ -50,22 +50,27 @@ T22375.$fEqX [InlPrag=CONLIKE] :: Eq X
 T22375.$fEqX
   = GHC.Classes.C:Eq @X T22375.$fEqX_$c== T22375.$fEqX_$c/=
 
--- RHS size: {terms: 24, types: 3, coercions: 0, joins: 0/0}
+-- RHS size: {terms: 44, types: 3, coercions: 0, joins: 0/0}
 T22375.$wf [InlPrag=[2]] :: X -> GHC.Prim.Int# -> GHC.Prim.Int#
 [GblId[StrictWorker([!])],
  Arity=2,
  Str=<1L><L>,
  Unf=Unf{Src=<vanilla>, TopLvl=True,
          Value=True, ConLike=True, WorkFree=True, Expandable=True,
-         Guidance=IF_ARGS [64 0] 55 0}]
+         Guidance=IF_ARGS [119 0] 110 0}]
 T22375.$wf
   = \ (x :: X) (ww :: GHC.Prim.Int#) ->
       case x of {
-        A -> GHC.Prim.+# 1# ww;
-        B -> GHC.Prim.+# 2# ww;
-        C -> GHC.Prim.+# 3# ww;
-        D -> GHC.Prim.+# 4# ww;
-        E -> GHC.Prim.+# 5# ww
+        A -> GHC.Prim.+# ww 1#;
+        B -> GHC.Prim.+# ww 2#;
+        C -> GHC.Prim.+# ww 3#;
+        D -> GHC.Prim.+# ww 4#;
+        E -> GHC.Prim.+# ww 5#;
+        F -> GHC.Prim.+# ww 6#;
+        G -> GHC.Prim.+# ww 7#;
+        H -> GHC.Prim.+# ww 8#;
+        I -> GHC.Prim.+# ww 9#;
+        J -> GHC.Prim.+# ww 10#
       }
 
 -- RHS size: {terms: 12, types: 5, coercions: 0, joins: 0/0}


=====================================
testsuite/tests/simplCore/should_compile/T22375DataFamily.hs
=====================================
@@ -6,13 +6,20 @@ import Data.Kind
 
 type X :: Type -> Type
 data family X a
-data instance X () = A | B | C | D | E
+data instance X ()
+  = A | B | C | D | E
+  | F | G | H | I | J
   deriving Eq
 
 f :: X () -> Int -> Int
 f x v
-  | x == A = 1 + v
-  | x == B = 2 + v
-  | x == C = 3 + v
-  | x == D = 4 + v
-  | otherwise = 5 + v
+  | x == A = v + 1
+  | x == B = v + 2
+  | x == C = v + 3
+  | x == D = v + 4
+  | x == E = v + 5
+  | x == F = v + 6
+  | x == G = v + 7
+  | x == H = v + 8
+  | x == I = v + 9
+  | otherwise = v + 10


=====================================
testsuite/tests/simplCore/should_compile/T22375DataFamily.stderr
=====================================
@@ -1,7 +1,7 @@
 
 ==================== Tidy Core ====================
 Result size of Tidy Core
-  = {terms: 86, types: 65, coercions: 15, joins: 0/0}
+  = {terms: 116, types: 75, coercions: 25, joins: 0/0}
 
 -- RHS size: {terms: 1, types: 0, coercions: 2, joins: 0/0}
 T22375DataFamily.$WA [InlPrag=INLINE[final] CONLIKE] :: X ()
@@ -58,6 +58,61 @@ T22375DataFamily.$WE
     `cast` (Sym (T22375DataFamily.D:R:XUnit0[0])
             :: T22375DataFamily.R:XUnit ~R# X ())
 
+-- RHS size: {terms: 1, types: 0, coercions: 2, joins: 0/0}
+T22375DataFamily.$WF [InlPrag=INLINE[final] CONLIKE] :: X ()
+[GblId[DataConWrapper],
+ Unf=Unf{Src=StableSystem, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=False)}]
+T22375DataFamily.$WF
+  = T22375DataFamily.F
+    `cast` (Sym (T22375DataFamily.D:R:XUnit0[0])
+            :: T22375DataFamily.R:XUnit ~R# X ())
+
+-- RHS size: {terms: 1, types: 0, coercions: 2, joins: 0/0}
+T22375DataFamily.$WG [InlPrag=INLINE[final] CONLIKE] :: X ()
+[GblId[DataConWrapper],
+ Unf=Unf{Src=StableSystem, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=False)}]
+T22375DataFamily.$WG
+  = T22375DataFamily.G
+    `cast` (Sym (T22375DataFamily.D:R:XUnit0[0])
+            :: T22375DataFamily.R:XUnit ~R# X ())
+
+-- RHS size: {terms: 1, types: 0, coercions: 2, joins: 0/0}
+T22375DataFamily.$WH [InlPrag=INLINE[final] CONLIKE] :: X ()
+[GblId[DataConWrapper],
+ Unf=Unf{Src=StableSystem, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=False)}]
+T22375DataFamily.$WH
+  = T22375DataFamily.H
+    `cast` (Sym (T22375DataFamily.D:R:XUnit0[0])
+            :: T22375DataFamily.R:XUnit ~R# X ())
+
+-- RHS size: {terms: 1, types: 0, coercions: 2, joins: 0/0}
+T22375DataFamily.$WI [InlPrag=INLINE[final] CONLIKE] :: X ()
+[GblId[DataConWrapper],
+ Unf=Unf{Src=StableSystem, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=False)}]
+T22375DataFamily.$WI
+  = T22375DataFamily.I
+    `cast` (Sym (T22375DataFamily.D:R:XUnit0[0])
+            :: T22375DataFamily.R:XUnit ~R# X ())
+
+-- RHS size: {terms: 1, types: 0, coercions: 2, joins: 0/0}
+T22375DataFamily.$WJ [InlPrag=INLINE[final] CONLIKE] :: X ()
+[GblId[DataConWrapper],
+ Unf=Unf{Src=StableSystem, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=False)}]
+T22375DataFamily.$WJ
+  = T22375DataFamily.J
+    `cast` (Sym (T22375DataFamily.D:R:XUnit0[0])
+            :: T22375DataFamily.R:XUnit ~R# X ())
+
 -- RHS size: {terms: 14, types: 11, coercions: 2, joins: 0/0}
 T22375DataFamily.$fEqX_$c== :: X () -> X () -> Bool
 [GblId,
@@ -133,7 +188,7 @@ T22375DataFamily.$fEqX
   = GHC.Classes.C:Eq
       @(X ()) T22375DataFamily.$fEqX_$c== T22375DataFamily.$fEqX_$c/=
 
--- RHS size: {terms: 24, types: 4, coercions: 1, joins: 0/0}
+-- RHS size: {terms: 44, types: 4, coercions: 1, joins: 0/0}
 T22375DataFamily.$wf [InlPrag=[2]]
   :: X () -> GHC.Prim.Int# -> GHC.Prim.Int#
 [GblId[StrictWorker([!])],
@@ -141,18 +196,23 @@ T22375DataFamily.$wf [InlPrag=[2]]
  Str=<1L><L>,
  Unf=Unf{Src=<vanilla>, TopLvl=True,
          Value=True, ConLike=True, WorkFree=True, Expandable=True,
-         Guidance=IF_ARGS [64 0] 55 0}]
+         Guidance=IF_ARGS [119 0] 110 0}]
 T22375DataFamily.$wf
   = \ (x :: X ()) (ww :: GHC.Prim.Int#) ->
       case x
            `cast` (T22375DataFamily.D:R:XUnit0[0]
                    :: X () ~R# T22375DataFamily.R:XUnit)
       of {
-        A -> GHC.Prim.+# 1# ww;
-        B -> GHC.Prim.+# 2# ww;
-        C -> GHC.Prim.+# 3# ww;
-        D -> GHC.Prim.+# 4# ww;
-        E -> GHC.Prim.+# 5# ww
+        A -> GHC.Prim.+# ww 1#;
+        B -> GHC.Prim.+# ww 2#;
+        C -> GHC.Prim.+# ww 3#;
+        D -> GHC.Prim.+# ww 4#;
+        E -> GHC.Prim.+# ww 5#;
+        F -> GHC.Prim.+# ww 6#;
+        G -> GHC.Prim.+# ww 7#;
+        H -> GHC.Prim.+# ww 8#;
+        I -> GHC.Prim.+# ww 9#;
+        J -> GHC.Prim.+# ww 10#
       }
 
 -- RHS size: {terms: 12, types: 6, coercions: 0, joins: 0/0}


=====================================
testsuite/tests/th/T24190.hs
=====================================
@@ -0,0 +1,11 @@
+module Main (main) where
+
+import Language.Haskell.TH
+
+main :: IO ()
+main = do
+    -- type annotations are needed so the monad is not ambiguous.
+    -- we also highlight that the monad can be different:
+    -- brackets are "just" syntax.
+    print $$(const [|| 'x' ||] ([| 'y' |]  :: IO Exp))
+    print $( const  [| 'x' |] ([|| 'y' ||] :: Code IO Char))


=====================================
testsuite/tests/th/T24190.stdout
=====================================
@@ -0,0 +1,2 @@
+'x'
+'x'


=====================================
testsuite/tests/th/TH_NestedSplicesFail3.stderr
=====================================
@@ -1,5 +1,8 @@
 
-TH_NestedSplicesFail3.hs:4:12: error: [GHC-45108]
-    • Untyped brackets may not appear in typed splices.
-    • In the Template Haskell quotation [| 'x' |]
-      In the typed splice: $$([| 'x' |])
+TH_NestedSplicesFail3.hs:4:12: error: [GHC-39999]
+    • No instance for ‘Language.Haskell.TH.Syntax.Quote
+                         (Language.Haskell.TH.Syntax.Code Language.Haskell.TH.Syntax.Q)’
+        arising from a quotation bracket
+    • In the expression: [| 'x' |]
+      In the Template Haskell splice $$([| 'x' |])
+      In the expression: $$([| 'x' |])


=====================================
testsuite/tests/th/TH_NestedSplicesFail4.stderr
=====================================
@@ -1,5 +1,9 @@
 
-TH_NestedSplicesFail4.hs:4:11: error: [GHC-45108]
-    • Typed brackets may not appear in untyped splices.
-    • In the Template Haskell typed quotation [|| 'y' ||]
+TH_NestedSplicesFail4.hs:4:11: error: [GHC-83865]
+    • Couldn't match type: Language.Haskell.TH.Syntax.Code m0 Char
+                     with: Language.Haskell.TH.Syntax.Q Language.Haskell.TH.Syntax.Exp
+      Expected: Language.Haskell.TH.Lib.Internal.ExpQ
+        Actual: Language.Haskell.TH.Syntax.Code m0 Char
+    • In the Template Haskell quotation [|| 'y' ||]
+      In the expression: [|| 'y' ||]
       In the untyped splice: $([|| 'y' ||])


=====================================
testsuite/tests/th/all.T
=====================================
@@ -599,3 +599,4 @@ test('T23971', normal, compile_and_run, [''])
 test('T23986', normal, compile_and_run, [''])
 test('T24111', normal, compile_and_run, [''])
 test('T23719', normal, compile_fail, [''])
+test('T24190', normal, compile_and_run, [''])



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/4062551ae94d3d787a8fc1bcba9c2ac3e5b1d70b...1f21c8b3b047e706323adb965a779fd2640cdd74

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/4062551ae94d3d787a8fc1bcba9c2ac3e5b1d70b...1f21c8b3b047e706323adb965a779fd2640cdd74
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20231211/fc150f33/attachment-0001.html>


More information about the ghc-commits mailing list