[Git][ghc/ghc][wip/int-index/t2t-expr] T2T in Expressions (#23738)

Vladislav Zavialov (@int-index) gitlab at gitlab.haskell.org
Wed Nov 1 20:50:08 UTC 2023



Vladislav Zavialov pushed to branch wip/int-index/t2t-expr at Glasgow Haskell Compiler / GHC


Commits:
0fdb0d1c by Vladislav Zavialov at 2023-11-01T23:49:32+03:00
T2T in Expressions (#23738)

This patch implements the T2T (term-to-type) transformation in
expressions. Given a function with a required type argument
	vfun :: forall a -> ...

the user can now call it as
	vfun (Maybe Int)

instead of
	vfun (type (Maybe Int))

The Maybe Int argument is parsed and renamed as a term (HsExpr), but then
undergoes a conversion to a type (HsType).
See the new function expr_to_type in compiler/GHC/Tc/Gen/App.hs
and Note [RequiredTypeArguments and the T2T mapping]

Left as future work: checking for puns.

- - - - -


27 changed files:

- compiler/GHC/Hs/Expr.hs
- compiler/GHC/Tc/Errors/Ppr.hs
- compiler/GHC/Tc/Errors/Types.hs
- compiler/GHC/Tc/Gen/App.hs
- compiler/GHC/Types/Error/Codes.hs
- compiler/GHC/Types/Hint.hs
- compiler/GHC/Types/Hint/Ppr.hs
- compiler/GHC/Types/Name/Occurrence.hs
- docs/users_guide/exts/required_type_arguments.rst
- testsuite/tests/diagnostic-codes/codes.stdout
- testsuite/tests/vdq-rta/should_compile/T22326_idv.hs
- + testsuite/tests/vdq-rta/should_compile/T23738_basic.hs
- + testsuite/tests/vdq-rta/should_compile/T23738_nested.hs
- + testsuite/tests/vdq-rta/should_compile/T23738_overlit.hs
- + testsuite/tests/vdq-rta/should_compile/T23738_sigforall.hs
- + testsuite/tests/vdq-rta/should_compile/T23738_th.hs
- + testsuite/tests/vdq-rta/should_compile/T23738_tyvar.hs
- + testsuite/tests/vdq-rta/should_compile/T23738_wild.hs
- testsuite/tests/vdq-rta/should_compile/all.T
- testsuite/tests/vdq-rta/should_fail/T22326_fail_raw_arg.stderr
- + testsuite/tests/vdq-rta/should_fail/T23738_fail_implicit_tv.hs
- + testsuite/tests/vdq-rta/should_fail/T23738_fail_implicit_tv.stderr
- + testsuite/tests/vdq-rta/should_fail/T23738_fail_var.hs
- + testsuite/tests/vdq-rta/should_fail/T23738_fail_var.stderr
- + testsuite/tests/vdq-rta/should_fail/T23738_fail_wild.hs
- + testsuite/tests/vdq-rta/should_fail/T23738_fail_wild.stderr
- testsuite/tests/vdq-rta/should_fail/all.T


Changes:

=====================================
compiler/GHC/Hs/Expr.hs
=====================================
@@ -208,8 +208,6 @@ data EpAnnUnboundVar = EpAnnUnboundVar
      , hsUnboundHole       :: EpaLocation
      } deriving Data
 
-type instance XVar           (GhcPass _) = NoExtField
-
 -- Record selectors at parse time are HsVar; they convert to HsRecSel
 -- on renaming.
 type instance XRecSel              GhcPs = DataConCantHappen
@@ -430,6 +428,13 @@ tupArgPresent :: HsTupArg (GhcPass p) -> Bool
 tupArgPresent (Present {}) = True
 tupArgPresent (Missing {}) = False
 
+tupArgPresent_maybe :: HsTupArg (GhcPass p) -> Maybe (LHsExpr (GhcPass p))
+tupArgPresent_maybe (Present _ e) = Just e
+tupArgPresent_maybe (Missing {})  = Nothing
+
+tupArgsPresent_maybe :: [HsTupArg (GhcPass p)] -> Maybe [LHsExpr (GhcPass p)]
+tupArgsPresent_maybe = traverse tupArgPresent_maybe
+
 
 {- *********************************************************************
 *                                                                      *


=====================================
compiler/GHC/Tc/Errors/Ppr.hs
=====================================
@@ -277,6 +277,14 @@ instance Diagnostic TcRnMessage where
         sole_msg =
           vcat [ text "except as the sole constraint"
                , nest 2 (text "e.g., deriving instance _ => Eq (Foo a)") ]
+    TcRnIllegalNamedWildcardInTypeArgument rdr
+      -> mkSimpleDecorated $
+           hang (text "Illegal named wildcard in a required type argument:")
+                2 (quotes (ppr rdr))
+    TcRnIllegalImplicitTyVarInTypeArgument rdr
+      -> mkSimpleDecorated $
+            hang (text "Illegal implicitly quantified type variable in a required type argument:")
+                2 (quotes (ppr rdr))
     TcRnDuplicateFieldName fld_part dups
       -> mkSimpleDecorated $
            hsep [ text "Duplicate field name"
@@ -1254,9 +1262,7 @@ instance Diagnostic TcRnMessage where
           text "A type pattern must be checked against a visible forall."
     TcRnIllformedTypeArgument e
       -> mkSimpleDecorated $
-          hang (text "Ill-formed type argument:") 2 (ppr e) $$
-          text "Expected a type expression introduced with the"
-            <+> quotes (text "type") <+> text "keyword."
+          hang (text "Ill-formed type argument:") 2 (ppr e)
     TcRnIllegalTypeExpr
       -> mkSimpleDecorated $
           text "Illegal type expression." $$
@@ -1944,6 +1950,10 @@ instance Diagnostic TcRnMessage where
       -> ErrorWithoutFlag
     TcRnIllegalWildcardInType{}
       -> ErrorWithoutFlag
+    TcRnIllegalNamedWildcardInTypeArgument{}
+      -> ErrorWithoutFlag
+    TcRnIllegalImplicitTyVarInTypeArgument{}
+      -> ErrorWithoutFlag
     TcRnDuplicateFieldName{}
       -> ErrorWithoutFlag
     TcRnIllegalViewPattern{}
@@ -2555,6 +2565,10 @@ instance Diagnostic TcRnMessage where
       -> [suggestExtension LangExt.RecordWildCards]
     TcRnIllegalWildcardInType{}
       -> noHints
+    TcRnIllegalNamedWildcardInTypeArgument{}
+      -> [SuggestAnonymousWildcard]
+    TcRnIllegalImplicitTyVarInTypeArgument tv
+      -> [SuggestExplicitQuantification tv]
     TcRnDuplicateFieldName{}
       -> noHints
     TcRnIllegalViewPattern{}


=====================================
compiler/GHC/Tc/Errors/Types.hs
=====================================
@@ -712,6 +712,37 @@ data TcRnMessage where
     -> !BadAnonWildcardContext
     -> TcRnMessage
 
+  {-| TcRnIllegalNamedWildcardInTypeArgument is an error that occurs
+      when a named wildcard is used in a required type argument.
+
+      Example:
+
+        vfun :: forall (a :: k) -> ()
+        x = vfun _nwc
+        --       ^^^^
+        -- named wildcards not allowed in type arguments
+
+      Test cases:
+        T23738_fail_wild
+  -}
+  TcRnIllegalNamedWildcardInTypeArgument
+    :: RdrName
+    -> TcRnMessage
+
+  {- TcRnIllegalImplicitTyVarInTypeArgument is an error raised
+     when a type variable is implicitly quantified in a required type argument.
+
+     Example:
+       vfun :: forall (a :: k) -> ()
+       x = vfun (Nothing :: Maybe a)
+       --                        ^^^
+       -- implicit quantification not allowed in type arguments
+
+  -}
+  TcRnIllegalImplicitTyVarInTypeArgument
+    :: RdrName
+    -> TcRnMessage
+
   {-| TcRnDuplicateFieldName is an error that occurs whenever
       there are duplicate field names in a single record.
 
@@ -4112,16 +4143,12 @@ data TcRnMessage where
       that specifies a required type argument (instantiates a visible forall)
       does not have a form that can be interpreted as a type argument.
 
-      At the moment, only expressions constructed using the @type@ keyword
-      are considered well-formed, but this restriction will be relaxed
-      when part 2 of GHC Proposal #281 is implemented.
-
       Example:
 
         vfun :: forall (a :: k) -> ()
-        x = vfun Int
-        --       ^^^
-        --  expected `type Int` instead of `Int`
+        x = vfun (\_ -> _)
+        --       ^^^^^^^^^
+        -- lambdas not allowed in type arguments
 
       Test cases:
         T22326_fail_raw_arg


=====================================
compiler/GHC/Tc/Gen/App.hs
=====================================
@@ -23,6 +23,7 @@ import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcPolyExpr )
 import GHC.Types.Var
 import GHC.Builtin.Types ( multiplicityTy )
 import GHC.Tc.Gen.Head
+import Language.Haskell.Syntax.Basic
 import GHC.Hs
 import GHC.Tc.Errors.Types
 import GHC.Tc.Utils.Monad
@@ -51,8 +52,10 @@ import GHC.Builtin.Names
 import GHC.Driver.DynFlags
 import GHC.Types.Name
 import GHC.Types.Name.Env
+import GHC.Types.Name.Reader
 import GHC.Types.SrcLoc
 import GHC.Types.Var.Env  ( emptyTidyEnv, mkInScopeSet )
+import GHC.Types.SourceText
 import GHC.Data.Maybe
 import GHC.Utils.Misc
 import GHC.Utils.Outputable as Outputable
@@ -806,10 +809,210 @@ tcVDQ :: ConcreteTyVars              -- See Note [Representation-polymorphism ch
       -> LHsExpr GhcRn               -- Argument type
       -> TcM (TcType, TcType)
 tcVDQ conc_tvs (tvb, inner_ty) arg
-  = do { hs_ty <- case stripParensLHsExpr arg of
-           L _ (HsEmbTy _ _ hs_ty) -> return hs_ty
-           e -> failWith $ TcRnIllformedTypeArgument e
-       ; tc_inst_forall_arg conc_tvs (tvb, inner_ty) hs_ty }
+  = do { hs_wc_ty <- expr_to_type (stripParensLHsExpr arg)
+       ; tc_inst_forall_arg conc_tvs (tvb, inner_ty) hs_wc_ty }
+
+-- Convert a HsExpr into the equivalent HsType.
+-- See [RequiredTypeArguments and the T2T mapping]
+expr_to_type :: LHsExpr GhcRn -> TcM (LHsWcType GhcRn)
+expr_to_type earg =
+  case stripParensLHsExpr earg of
+    L _ (HsEmbTy _ _ hs_ty) ->
+      -- The entire type argument is guarded with the `type` herald,
+      -- e.g. `vfun (type (Maybe Int))`. This special case supports
+      -- named wildcards. See Note [Wildcards in the T2T translation]
+      return hs_ty
+    e ->
+      -- The type argument is not guarded with the `type` herald, or perhaps
+      -- only parts of it are, e.g. `vfun (Maybe Int)` or `vfun (Maybe (type Int))`.
+      -- Apply a recursive T2T transformation.
+      HsWC [] <$> go e
+  where
+    go :: LHsExpr GhcRn -> TcM (LHsType GhcRn)
+    go (L _ (HsEmbTy _ _ t)) =
+      -- HsEmbTy means there is an explicit `type` herald, e.g. vfun :: forall a -> blah
+      -- and the call   vfun (type Int)
+      --           or   vfun (Int -> type Int)
+      -- The T2T transformation can simply discard the herald and use the embedded type.
+      unwrap_wc t
+    go (L l (HsVar _ lname)) =
+      -- as per #281: variables and constructors (regardless of their namespace)
+      -- are mapped directly, without modification.
+      return (L l (HsTyVar noAnn NotPromoted lname))
+    go (L l (HsApp _ lhs rhs)) =
+      do { lhs' <- go lhs
+         ; rhs' <- go rhs
+         ; return (L l (HsAppTy noExtField lhs' rhs')) }
+    go (L l (HsAppType _ lhs at rhs)) =
+      do { lhs' <- go lhs
+         ; rhs' <- unwrap_wc rhs
+         ; return (L l (HsAppKindTy noExtField lhs' at rhs')) }
+    go (L l e@(OpApp _ lhs op rhs)) =
+      do { lhs' <- go lhs
+         ; op'  <- go op
+         ; rhs' <- go rhs
+         ; op_id <- unwrap_op_tv op'
+         ; return (L l (HsOpTy noAnn NotPromoted lhs' op_id rhs')) }
+      where
+        unwrap_op_tv (L _ (HsTyVar _ _ op_id)) = return op_id
+        unwrap_op_tv _ = failWith $ TcRnIllformedTypeArgument (L l e)
+    go (L l e@(HsOverLit _ lit)) =
+      do { tylit <- case ol_val lit of
+             HsIntegral   n -> return $ HsNumTy NoSourceText (il_value n)
+             HsIsString _ s -> return $ HsStrTy NoSourceText s
+             HsFractional _ -> failWith $ TcRnIllformedTypeArgument (L l e)
+         ; return (L l (HsTyLit noExtField tylit)) }
+    go (L l e@(HsLit _ lit)) =
+      do { tylit <- case lit of
+             HsChar   _ c -> return $ HsCharTy NoSourceText c
+             HsString _ s -> return $ HsStrTy  NoSourceText s
+             _ -> failWith $ TcRnIllformedTypeArgument (L l e)
+         ; return (L l (HsTyLit noExtField tylit)) }
+    go (L l (ExplicitTuple _ tup_args boxity))
+      -- Neither unboxed tuples (#e1,e2#) nor tuple sections (e1,,e2,) can be promoted
+      | isBoxed boxity
+      , Just es <- tupArgsPresent_maybe tup_args
+      = do { ts <- traverse go es
+           ; return (L l (HsExplicitTupleTy noExtField ts)) }
+    go (L l (ExplicitList _ es)) =
+      do { ts <- traverse go es
+         ; return (L l (HsExplicitListTy noExtField NotPromoted ts)) }
+    go (L l (ExprWithTySig _ e sig_ty)) =
+      do { t <- go e
+         ; sig_ki <- (unwrap_sig <=< unwrap_wc) sig_ty
+         ; return (L l (HsKindSig noAnn t sig_ki)) }
+      where
+        unwrap_sig :: LHsSigType GhcRn -> TcM (LHsType GhcRn)
+        unwrap_sig (L _ (HsSig _ HsOuterImplicit{hso_ximplicit=bndrs} body))
+          | null bndrs = return body
+          | otherwise  = illegal_implicit_tvs bndrs
+        unwrap_sig (L l (HsSig _ HsOuterExplicit{hso_bndrs=bndrs} body)) =
+          return $ L l (HsForAllTy noExtField (HsForAllInvis noAnn bndrs) body)
+    go (L l (HsPar _ _ e _)) =
+      do { t <- go e
+         ; return (L l (HsParTy noAnn t)) }
+    go (L l (HsUntypedSplice splice_result splice))
+      | HsUntypedSpliceTop finalizers e <- splice_result
+      = do { t <- go (L l e)
+           ; let splice_result' = HsUntypedSpliceTop finalizers t
+           ; return (L l (HsSpliceTy splice_result' splice)) }
+    go (L l (HsUnboundVar _ rdr))
+      | isUnderscore occ = return (L l (HsWildCardTy noExtField))
+      | startsWithUnderscore occ =
+          -- See Note [Wildcards in the T2T translation]
+          do { wildcards_enabled <- xoptM LangExt.NamedWildCards
+             ; if wildcards_enabled
+               then illegal_wc rdr
+               else not_in_scope }
+      | otherwise = not_in_scope
+      where occ = occName rdr
+            not_in_scope = failWith $ mkTcRnNotInScope rdr NotInScope
+    go (L l (XExpr (HsExpanded orig _))) =
+      -- Use the original, user-written expression (before expansion).
+      -- Example. Say we have   vfun :: forall a -> blah
+      --          and the call  vfun (Maybe [1,2,3])
+      --          expanded to   vfun (Maybe (fromListN 3 [1,2,3]))
+      -- (This happens when OverloadedLists is enabled).
+      -- The expanded expression can't be promoted, as there is no type-level
+      -- equivalent of fromListN, so we must use the original.
+      go (L l orig)
+    go e = failWith $ TcRnIllformedTypeArgument e
+
+    unwrap_wc :: HsWildCardBndrs GhcRn t -> TcM t
+    unwrap_wc (HsWC wcs t)
+      = do { mapM_ (illegal_wc . nameRdrName) wcs
+           ; return t }
+
+    illegal_wc :: RdrName -> TcM t
+    illegal_wc rdr = failWith $ TcRnIllegalNamedWildcardInTypeArgument rdr
+
+    illegal_implicit_tvs :: [Name] -> TcM t
+    illegal_implicit_tvs tvs
+      = do { mapM_ (addErr . TcRnIllegalImplicitTyVarInTypeArgument . nameRdrName) tvs
+           ; failM }
+
+{- Note [RequiredTypeArguments and the T2T mapping]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The "T2T-Mapping" section of GHC Proposal #281 introduces a term-to-type transformation
+that comes into play when we typecheck function applications to required type arguments.
+Say we have a function that expects a required type argument, vfun :: forall a -> ...
+then it is possible to call it as follows:
+
+  vfun (Maybe Int)
+
+The Maybe Int argument is parsed and renamed as a term. There is no syntactic marker
+to tell GHC that it is actually a type argument.  We only discover this by the time
+we get to type checking, where we know that f's type has a visible forall at the front,
+so we are expecting a type argument. More precisely, this happens in tcVDQ in GHC/Tc/Gen/App.hs:
+
+  tcVDQ :: ConcreteTyVars              -- See Note [Representation-polymorphism checking built-ins]
+        -> (ForAllTyBinder, TcType)    -- Function type
+        -> LHsExpr GhcRn               -- Argument type
+        -> TcM (TcType, TcType)
+
+What we want is a type to instantiate the forall-bound variable. But what we have is an HsExpr,
+and we need to convert it to an HsType in order to reuse the same code paths as we use for
+checking f @ty (see tc_inst_forall_arg).
+
+  f (Maybe Int)
+  -- ^^^^^^^^^
+  -- parsed and renamed as:   HsApp   (HsVar   "Maybe") (HsVar   "Int")  ::  HsExpr GhcRn
+  -- must be converted to:    HsTyApp (HsTyVar "Maybe") (HsTyVar "Int")  ::  HsType GhcRn
+
+We do this using a helper function:
+
+  expr_to_type :: LHsExpr GhcRn -> TcM (LHsWcType GhcRn)
+
+This conversion is in the TcM monad because
+* It can fail, if the expression is not convertible to a type.
+      vfun [x | x <- xs]     Can't convert list comprehension to a type
+      vfun (\x -> x)         Can't convert a lambda to a type
+* It needs to check for LangExt.NamedWildCards to generate an appropriate
+  error message for HsUnboundVar.
+     vfun _a    Not in scope: ‘_a’
+                   (NamedWildCards disabled)
+     vfun _a    Illegal named wildcard in a required type argument: ‘_a’
+                   (NamedWildCards enabled)
+
+Note [Wildcards in the T2T translation]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose f1 :: forall a b. blah
+        f2 :: forall a b -> blah
+
+Consider the terms
+  f1 @_ @(Either _ _)
+  f2 (type _) (type (Either _ _))
+Those `_` wildcards are type wildcards, each standing for a monotype.
+All good.
+
+Now consider this, with -XNamedWildCards:
+  f1 @_a @(Either _a _a)
+  f2 (type _a) (type (Either _a _a))
+Those `_a` are "named wildcards", specified by the user manual like this: "All
+occurrences of the same named wildcard within one type signature will unify to
+the same type".  Note "within one signature".  So each type argument is considered
+separately, and the examples mean the same as:
+  f1 @_a1 @(Either _a2 _a2)
+  f2 (type _a1) (type (Either _a2 _a2))
+The repeated `_a2` ensures that the two arguments of `Either` are the same type;
+but there is no connection with `_a1`.  (NB: `_a1` and `_a2` only scope within
+their respective type, no further.)
+
+Now, consider the T2T translation for
+   f2 _ (Either _ _)
+This is fine: the term wildcard `_` is translated to a type wildcard, so we get
+the same as if we had written
+   f2 (type _) (type (Either _ _))
+
+But what about /named/ wildcards?
+   f2 _a (Either _a _a)
+Now we are in difficulties.  The renamer looks for a /term/ variable `_a` in scope,
+and won't find one.  Even if it did, the three `_a`'s would not be renamed separately
+as above.
+
+Conclusion: we treat a named wildcard in the T2T translation as an error.  If you
+want that, use a `(type ty)` argument instead.
+-}
 
 tc_inst_forall_arg :: ConcreteTyVars            -- See Note [Representation-polymorphism checking built-ins]
                    -> (ForAllTyBinder, TcType)  -- Function type
@@ -890,7 +1093,7 @@ At a call site we may have calls looking like this
     fs             True  -- Specified: type argument omitted
     fs      @Bool  True  -- Specified: type argument supplied
     fr (type Bool) True  -- Required: type argument is compulsory, `type` qualifier used
-    fr       Bool  True  -- Required: type argument is compulsory, `type` qualifier omitted (NB: not implemented)
+    fr       Bool  True  -- Required: type argument is compulsory, `type` qualifier omitted
 
 At definition sites we may have type /patterns/ to abstract over type variables
    fi           x       = rhs   -- Inferred: no type pattern
@@ -953,8 +1156,8 @@ Syntax of applications in HsExpr
 
   Why the difference?  Because we /also/ need to express these /nested/ uses of `type`:
 
-      g (Maybe (type Int))               -- valid for g :: forall (a :: Type) -> t     (NB. not implemented)
-      g (Either (type Int) (type Bool))  -- valid for g :: forall (a :: Type) -> t     (NB. not implemented)
+      g (Maybe (type Int))               -- valid for g :: forall (a :: Type) -> t
+      g (Either (type Int) (type Bool))  -- valid for g :: forall (a :: Type) -> t
 
   This nesting makes `type` rather different from `@`. Remember, the HsEmbTy mainly just
   switches namespace, and is subject to the term-to-type transformation.
@@ -993,7 +1196,7 @@ rnExpr delegates renaming of type arguments to rnHsWcType if possible:
     f (type t)  -- HsApp and HsEmbTy, t is renamed with rnHsWcType
 
 But what about:
-    f t         -- HsApp, no HsEmbTy      (NB. not implemented)
+    f t         -- HsApp, no HsEmbTy
 We simply rename `t` as a term using a recursive call to rnExpr; in particular,
 the type of `f` does not affect name resolution (Lexical Scoping Principle).
 We will later convert `t` from a `HsExpr` to a `Type`, see "Typechecking type
@@ -1057,7 +1260,7 @@ This is done by tcVTA (if Specified) and tcVDQ (if Required).
 tcVDQ unwraps the HsEmbTy and uses the type contained within it.  Crucially, in
 tcVDQ we know that we are expecting a type argument.  This means that we can
 support
-    f (Maybe Int)   -- HsApp, no HsEmbTy      (NB. not implemented)
+    f (Maybe Int)   -- HsApp, no HsEmbTy
 The type argument (Maybe Int) is represented as an HsExpr, but tcVDQ can easily
 convert it to HsType.  This conversion is called the "T2T-Mapping" in GHC
 Proposal #281.


=====================================
compiler/GHC/Types/Error/Codes.hs
=====================================
@@ -369,6 +369,8 @@ type family GhcDiagnosticCode c = n | n -> c where
   GhcDiagnosticCode "TcRnIllegalFieldPunning"                       = 44287
   GhcDiagnosticCode "TcRnIllegalWildcardsInRecord"                  = 37132
   GhcDiagnosticCode "TcRnIllegalWildcardInType"                     = 65507
+  GhcDiagnosticCode "TcRnIllegalNamedWildcardInTypeArgument"        = 93411
+  GhcDiagnosticCode "TcRnIllegalImplicitTyVarInTypeArgument"        = 80557
   GhcDiagnosticCode "TcRnDuplicateFieldName"                        = 85524
   GhcDiagnosticCode "TcRnIllegalViewPattern"                        = 22406
   GhcDiagnosticCode "TcRnCharLiteralOutOfRange"                     = 17268


=====================================
compiler/GHC/Types/Hint.hs
=====================================
@@ -474,6 +474,12 @@ data GhcHint
   -}
   | SuggestBindTyVarOnLhs RdrName
 
+  {-| Suggest using an anonymous wildcard instead of a named wildcard -}
+  | SuggestAnonymousWildcard
+
+  {-| Suggest explicitly quantifying a type variable instead of relying on implicit quantification -}
+  | SuggestExplicitQuantification RdrName
+
 -- | An 'InstantiationSuggestion' for a '.hsig' file. This is generated
 -- by GHC in case of a 'DriverUnexpectedSignature' and suggests a way
 -- to instantiate a particular signature, where the first argument is


=====================================
compiler/GHC/Types/Hint/Ppr.hs
=====================================
@@ -266,6 +266,11 @@ instance Outputable GhcHint where
             ppr_r = quotes $ ppr r
     SuggestBindTyVarOnLhs tv
       -> text "Bind" <+> quotes (ppr tv) <+> text "on the LHS of the type declaration"
+    SuggestAnonymousWildcard
+      -> text "Use an anonymous wildcard" <+> quotes (text "_")
+    SuggestExplicitQuantification tv
+      -> hsep [ text "Use an explicit", quotes (text "forall")
+              , text "to quantify over", quotes (ppr tv) ]
 
 perhapsAsPat :: SDoc
 perhapsAsPat = text "Perhaps you meant an as-pattern, which must not be surrounded by whitespace"


=====================================
compiler/GHC/Types/Name/Occurrence.hs
=====================================
@@ -80,7 +80,7 @@ module GHC.Types.Name.Occurrence (
 
         isVarOcc, isTvOcc, isTcOcc, isDataOcc, isDataSymOcc, isSymOcc, isValOcc,
         isFieldOcc, fieldOcc_maybe,
-        parenSymOcc, startsWithUnderscore,
+        parenSymOcc, startsWithUnderscore, isUnderscore,
 
         isTcClsNameSpace, isTvNameSpace, isDataConNameSpace, isVarNameSpace, isValNameSpace,
         isFieldNameSpace, isTermVarOrFieldNameSpace,
@@ -912,6 +912,9 @@ startsWithUnderscore occ = case unpackFS (occNameFS occ) of
   '_':_ -> True
   _     -> False
 
+isUnderscore :: OccName -> Bool
+isUnderscore occ = occNameFS occ == fsLit "_"
+
 {-
 ************************************************************************
 *                                                                      *


=====================================
docs/users_guide/exts/required_type_arguments.rst
=====================================
@@ -107,7 +107,5 @@ indistinguishble from ordinary function arguments::
   n = id_vdq Integer 42
 
 In this example we pass ``Integer`` as opposed to ``(type Integer)``.
-**This is not currently implemented**, but it demonstrates how
-:extension:`RequiredTypeArguments` is not tied to the ``type`` syntax.
-For this reason, using the ``type`` syntax requires enabling the
-:extension:`ExplicitNamespaces` extension separately.
\ No newline at end of file
+This means that :extension:`RequiredTypeArguments` is not tied to the ``type``
+syntax, which belongs to :extension:`ExplicitNamespaces`.
\ No newline at end of file


=====================================
testsuite/tests/diagnostic-codes/codes.stdout
=====================================
@@ -65,7 +65,6 @@
 [GHC-85337] is untested (constructor = TcRnSpecialiseNotVisible)
 [GHC-91382] is untested (constructor = TcRnIllegalKindSignature)
 [GHC-72520] is untested (constructor = TcRnIgnoreSpecialisePragmaOnDefMethod)
-[GHC-10969] is untested (constructor = TcRnTyThingUsedWrong)
 [GHC-61072] is untested (constructor = TcRnGADTDataContext)
 [GHC-16409] is untested (constructor = TcRnMultipleConForNewtype)
 [GHC-54478] is untested (constructor = TcRnRedundantSourceImport)


=====================================
testsuite/tests/vdq-rta/should_compile/T22326_idv.hs
=====================================
@@ -1,6 +1,7 @@
 {-# LANGUAGE ExplicitNamespaces #-}
 {-# LANGUAGE RequiredTypeArguments #-}
 {-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE NamedWildCards #-}
 
 module T22326_idv where
 
@@ -38,4 +39,8 @@ idv_wild (type _) x = x
 
 -- Usage (using a wildcard)
 rBool'   = idv (type _) True
-rChar'   = idv (type _) 'x'
\ No newline at end of file
+rChar'   = idv (type _) 'x'
+
+-- Usage (using named wildcards)
+rMaybeX         = idv (type (Maybe _a)) Nothing
+rEitherCharChar = idv (type (Either _a _a)) (Left 'x')
\ No newline at end of file


=====================================
testsuite/tests/vdq-rta/should_compile/T23738_basic.hs
=====================================
@@ -0,0 +1,19 @@
+{-# LANGUAGE RequiredTypeArguments #-}
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE DataKinds #-}
+
+-- Overloaded string literals checked in T23738_overlit.
+{-# LANGUAGE NoOverloadedStrings #-}
+
+module T23738_basic where
+
+type (:+:) = Either
+
+checkEq :: forall a b -> (a ~ b) => ()
+checkEq (type _) (type _) = ()
+
+result :: ()
+result =
+  checkEq
+  {- type syntax: -} (type '(Maybe Int, String :+: Int, 10, "Hello", 'x' :: Char, '[] @Bool, '[10], [1, 2]))
+  {- term syntax: -}        (Maybe Int, String :+: Int, 10, "Hello", 'x' :: Char,  [] @Bool,  [10], [1, 2])
\ No newline at end of file


=====================================
testsuite/tests/vdq-rta/should_compile/T23738_nested.hs
=====================================
@@ -0,0 +1,14 @@
+{-# LANGUAGE RequiredTypeArguments #-}
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE DataKinds #-}
+
+module T23738_nested where
+
+checkEq :: forall a b -> (a ~ b) => ()
+checkEq (type _) (type _) = ()
+
+result :: ()
+result =
+  checkEq
+    (type (Either Int Bool))
+    (Either (type Int) (type Bool))
\ No newline at end of file


=====================================
testsuite/tests/vdq-rta/should_compile/T23738_overlit.hs
=====================================
@@ -0,0 +1,20 @@
+{-# LANGUAGE RequiredTypeArguments #-}
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE DataKinds #-}
+
+-- Non-overloaded string literals checked in T23738_basic.
+{-# LANGUAGE OverloadedStrings #-}
+
+-- Non-overloaded lists are checked in T23738_basic.
+{-# LANGUAGE OverloadedLists #-}
+
+module T23738_overlit where
+
+checkEq :: forall a b -> (a ~ b) => ()
+checkEq (type _) (type _) = ()
+
+result :: ()
+result =
+  checkEq
+  {- type syntax: -} (type '("Hello", [1, 2, 3]))
+  {- term syntax: -}        ("Hello", [1, 2, 3])
\ No newline at end of file


=====================================
testsuite/tests/vdq-rta/should_compile/T23738_sigforall.hs
=====================================
@@ -0,0 +1,28 @@
+{-# LANGUAGE RequiredTypeArguments #-}
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE DataKinds #-}
+
+module T23738_sigforall where
+
+import Data.Kind (Type)
+
+checkEq :: forall a b -> (a ~ b) => ()
+checkEq (type _) (type _) = ()
+
+r1 :: ()
+r1 =
+  checkEq
+  {- type syntax: -} (type (Left :: forall a b. a -> Either a b))
+  {- term syntax: -}       (Left :: forall a b. a -> Either a b)
+
+r2 :: ()
+r2 =
+  checkEq
+  {- type syntax: -} (type (Left :: forall a. forall b. a -> Either a b))
+  {- term syntax: -}       (Left :: forall a. forall b. a -> Either a b)
+
+r3 :: ()
+r3 =
+  checkEq
+  {- type syntax: -} (type (Left :: forall. forall a. forall b. a -> Either a b))
+  {- term syntax: -}       (Left :: forall. forall a. forall b. a -> Either a b)
\ No newline at end of file


=====================================
testsuite/tests/vdq-rta/should_compile/T23738_th.hs
=====================================
@@ -0,0 +1,17 @@
+{-# LANGUAGE RequiredTypeArguments #-}
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TemplateHaskell #-}
+
+module T23738_th where
+
+type (:+:) = Either
+
+checkEq :: forall a b -> (a ~ b) => ()
+checkEq (type _) (type _) = ()
+
+result :: ()
+result =
+  checkEq
+  {- type syntax: -} (type $[t| '(Maybe Int, String :+: Int, 10, "Hello", 'x' :: Char, '[] @Bool, '[10], [1, 2]) |])
+  {- term syntax: -}       $[e|  (Maybe Int, String :+: Int, 10, "Hello", 'x' :: Char,  [] @Bool,  [10], [1, 2]) |]
\ No newline at end of file


=====================================
testsuite/tests/vdq-rta/should_compile/T23738_tyvar.hs
=====================================
@@ -0,0 +1,15 @@
+{-# LANGUAGE RequiredTypeArguments #-}
+{-# LANGUAGE ExplicitNamespaces #-}
+
+module T23738_tyvar where
+
+import Data.Kind (Type)
+
+checkEq :: forall a b -> (a ~ b) => ()
+checkEq (type _) (type _) = ()
+
+result :: forall k. forall (f :: k -> Type) (t :: k) -> ()
+result (type f) (type t) =
+  checkEq
+  {- type syntax: -} (type (f t))
+  {- term syntax: -}       (f t)
\ No newline at end of file


=====================================
testsuite/tests/vdq-rta/should_compile/T23738_wild.hs
=====================================
@@ -0,0 +1,14 @@
+{-# LANGUAGE RequiredTypeArguments #-}
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE NamedWildCards #-}
+
+module T23738_wild where
+
+idv :: forall a -> a -> a
+idv (type t) (x :: t) = x
+
+rBool = idv _ True
+rChar = idv _ 'x'
+
+rMaybeBool = idv (Maybe _) (Just True)
+rMaybeChar = idv (Maybe _) (Just 'x')
\ No newline at end of file


=====================================
testsuite/tests/vdq-rta/should_compile/all.T
=====================================
@@ -10,6 +10,13 @@ test('T22326_sig', normal, compile, [''])
 test('T17792_vdq', normal, compile, [''])
 test('T14158_vdq', normal, compile, [''])
 test('WithSpineVDQ_LintErr', normal, compile, [''])
+test('T23738_basic', normal, compile, [''])
+test('T23738_tyvar', normal, compile, [''])
+test('T23738_overlit', normal, compile, [''])
+test('T23738_nested', normal, compile, [''])
+test('T23738_wild', normal, compile, [''])
+test('T23738_sigforall', normal, compile, [''])
 
 test('T22326_th_dump1', req_th, compile, ['-v0 -ddump-splices -dsuppress-uniques'])
-test('T22326_th_pprint1', req_th, compile, [''])
\ No newline at end of file
+test('T22326_th_pprint1', req_th, compile, [''])
+test('T23738_th', req_th, compile, [''])
\ No newline at end of file


=====================================
testsuite/tests/vdq-rta/should_fail/T22326_fail_raw_arg.stderr
=====================================
@@ -1,6 +1,5 @@
 
 T22326_fail_raw_arg.hs:9:5: error: [GHC-29092]
     • Ill-formed type argument: \ _ -> _
-      Expected a type expression introduced with the ‘type’ keyword.
     • In the expression: f (\ _ -> _)
       In an equation for ‘x’: x = f (\ _ -> _)


=====================================
testsuite/tests/vdq-rta/should_fail/T23738_fail_implicit_tv.hs
=====================================
@@ -0,0 +1,11 @@
+{-# LANGUAGE RequiredTypeArguments #-}
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE DataKinds #-}
+
+module T23738_fail_implicit_tv where
+
+vfun :: forall (a :: k) -> ()
+vfun (type _) = ()
+
+rNothing = vfun (Nothing :: Maybe a)
+rLeft = vfun (Left :: a -> Either a b)
\ No newline at end of file


=====================================
testsuite/tests/vdq-rta/should_fail/T23738_fail_implicit_tv.stderr
=====================================
@@ -0,0 +1,21 @@
+
+T23738_fail_implicit_tv.hs:10:12: error: [GHC-80557]
+    • Illegal implicitly quantified type variable in a required type argument:
+        ‘a’
+    • In the expression: vfun (Nothing :: Maybe a)
+      In an equation for ‘rNothing’: rNothing = vfun (Nothing :: Maybe a)
+    Suggested fix: Use an explicit ‘forall’ to quantify over ‘a’
+
+T23738_fail_implicit_tv.hs:11:9: error: [GHC-80557]
+    • Illegal implicitly quantified type variable in a required type argument:
+        ‘b’
+    • In the expression: vfun (Left :: a -> Either a b)
+      In an equation for ‘rLeft’: rLeft = vfun (Left :: a -> Either a b)
+    Suggested fix: Use an explicit ‘forall’ to quantify over ‘b’
+
+T23738_fail_implicit_tv.hs:11:9: error: [GHC-80557]
+    • Illegal implicitly quantified type variable in a required type argument:
+        ‘a’
+    • In the expression: vfun (Left :: a -> Either a b)
+      In an equation for ‘rLeft’: rLeft = vfun (Left :: a -> Either a b)
+    Suggested fix: Use an explicit ‘forall’ to quantify over ‘a’


=====================================
testsuite/tests/vdq-rta/should_fail/T23738_fail_var.hs
=====================================
@@ -0,0 +1,11 @@
+{-# LANGUAGE RequiredTypeArguments #-}
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE TypeAbstractions #-}
+
+module T23738_fail_var where
+
+vfun :: forall (a :: k) -> ()
+vfun (type _) = ()
+
+f :: Int -> ()
+f a = vfun a
\ No newline at end of file


=====================================
testsuite/tests/vdq-rta/should_fail/T23738_fail_var.stderr
=====================================
@@ -0,0 +1,6 @@
+
+T23738_fail_var.hs:11:12: error: [GHC-10969]
+    • Local identifier ‘a’ used as a type
+    • In the type ‘a’
+      In the expression: vfun a
+      In an equation for ‘f’: f a = vfun a


=====================================
testsuite/tests/vdq-rta/should_fail/T23738_fail_wild.hs
=====================================
@@ -0,0 +1,14 @@
+{-# LANGUAGE RequiredTypeArguments #-}
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE NamedWildCards #-}
+
+module T23738_fail_wild where
+
+idv :: forall a -> a -> a
+idv (type t) (x :: t) = x
+
+rBool' = idv _w True
+rChar' = idv _w 'x'
+
+rMaybeBool' = idv (Maybe _w) (Just True)
+rMaybeChar' = idv (Maybe _w) (Just 'x')
\ No newline at end of file


=====================================
testsuite/tests/vdq-rta/should_fail/T23738_fail_wild.stderr
=====================================
@@ -0,0 +1,26 @@
+
+T23738_fail_wild.hs:10:10: error: [GHC-93411]
+    • Illegal named wildcard in a required type argument: ‘_w’
+    • In the expression: idv _w True
+      In an equation for ‘rBool'’: rBool' = idv _w True
+    Suggested fix: Use an anonymous wildcard ‘_’
+
+T23738_fail_wild.hs:11:10: error: [GHC-93411]
+    • Illegal named wildcard in a required type argument: ‘_w’
+    • In the expression: idv _w 'x'
+      In an equation for ‘rChar'’: rChar' = idv _w 'x'
+    Suggested fix: Use an anonymous wildcard ‘_’
+
+T23738_fail_wild.hs:13:15: error: [GHC-93411]
+    • Illegal named wildcard in a required type argument: ‘_w’
+    • In the expression: idv (Maybe _w) (Just True)
+      In an equation for ‘rMaybeBool'’:
+          rMaybeBool' = idv (Maybe _w) (Just True)
+    Suggested fix: Use an anonymous wildcard ‘_’
+
+T23738_fail_wild.hs:14:15: error: [GHC-93411]
+    • Illegal named wildcard in a required type argument: ‘_w’
+    • In the expression: idv (Maybe _w) (Just 'x')
+      In an equation for ‘rMaybeChar'’:
+          rMaybeChar' = idv (Maybe _w) (Just 'x')
+    Suggested fix: Use an anonymous wildcard ‘_’


=====================================
testsuite/tests/vdq-rta/should_fail/all.T
=====================================
@@ -11,4 +11,7 @@ test('T22326_fail_caseof', normal, compile_fail, [''])
 test('T22326_fail_ado', normal, compile_fail, [''])
 test('T22326_fail_n_args', normal, compile_fail, [''])
 test('T22326_fail_patsyn', normal, compile_fail, [''])
-test('T22326_fail_match', normal, compile_fail, [''])
\ No newline at end of file
+test('T22326_fail_match', normal, compile_fail, [''])
+test('T23738_fail_wild', normal, compile_fail, [''])
+test('T23738_fail_implicit_tv', normal, compile_fail, [''])
+test('T23738_fail_var', normal, compile_fail, [''])
\ No newline at end of file



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/0fdb0d1cf14ccff09f76030c2eab90bd251f8d75

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/0fdb0d1cf14ccff09f76030c2eab90bd251f8d75
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/20231101/0b9791f4/attachment-0001.html>


More information about the ghc-commits mailing list