In hole fits, don't show VTA for inferred variables (#16456)

We fetch the ArgFlag for every argument by using splitForAllVarBndrs
instead of splitForAllTys in unwrapTypeVars.

compiler/typecheck/TcHoleErrors.hs

@@ -516,21 +516,30 @@ pprHoleFit (HFDC sWrp sWrpVars sTy sProv sMs) hf = hang display 2 provenance
           ty = hfType hf
           matches =  hfMatches hf
           wrap = hfWrap hf
-          tyApp = sep $ map ((text "@" <>) . pprParendType) wrap
+          tyApp = sep $ zipWithEqual "pprHoleFit" pprArg vars wrap
+            where pprArg b arg = case binderArgFlag b of
+                                   Specified -> text "@" <> pprParendType arg
+                                   -- Do not print type application for inferred
+                                   -- variables (#16456)
+                                   Inferred  -> empty
+                                   Required  -> pprPanic "pprHoleFit: bad Required"
+                                                         (ppr b <+> ppr arg)
           tyAppVars = sep $ punctuate comma $
-              map (\(v,t) -> ppr v <+> text "~" <+> pprParendType t) $
-                zip vars wrap
+              zipWithEqual "pprHoleFit" (\v t -> ppr (binderVar v) <+>
+                                                 text "~" <+> pprParendType t)
+                vars wrap
+
+          vars = unwrapTypeVars ty
             where
-              vars = unwrapTypeVars ty
               -- Attempts to get all the quantified type variables in a type,
               -- e.g.
-              -- return :: forall (m :: * -> *) Monad m => (forall a . a) -> m a
+              -- return :: forall (m :: * -> *) Monad m => (forall a . a -> m a)
               -- into [m, a]
-              unwrapTypeVars :: Type -> [TyVar]
+              unwrapTypeVars :: Type -> [TyCoVarBinder]
               unwrapTypeVars t = vars ++ case splitFunTy_maybe unforalled of
                                   Just (_, unfunned) -> unwrapTypeVars unfunned
                                   _ -> []
-                where (vars, unforalled) = splitForAllTys t
+                where (vars, unforalled) = splitForAllVarBndrs t
           holeVs = sep $ map (parens . (text "_" <+> dcolon <+>) . ppr) matches
           holeDisp = if sMs then holeVs
                      else sep $ replicate (length matches) $ text "_"

testsuite/tests/printer/T14343.stderr

@@ -8,7 +8,7 @@ T14343.hs:10:9: error:
       Valid hole fits include
         test1 :: Proxy '[ 'True] (defined at T14343.hs:10:1)
         Proxy :: forall k1 (k2 :: k1). Proxy k2
-          with Proxy @[Bool] @'[ 'True]
+          with Proxy @'[ 'True]
           (defined at T14343.hs:8:16)
 
 T14343.hs:11:9: error:
@@ -20,7 +20,7 @@ T14343.hs:11:9: error:
       Valid hole fits include
         test2 :: Proxy '[ '[1]] (defined at T14343.hs:11:1)
         Proxy :: forall k1 (k2 :: k1). Proxy k2
-          with Proxy @[[GHC.Types.Nat]] @'[ '[1]]
+          with Proxy @'[ '[1]]
           (defined at T14343.hs:8:16)
 
 T14343.hs:12:9: error:
@@ -32,5 +32,5 @@ T14343.hs:12:9: error:
       Valid hole fits include
         test3 :: Proxy '[ '("Symbol", 1)] (defined at T14343.hs:12:1)
         Proxy :: forall k1 (k2 :: k1). Proxy k2
-          with Proxy @[(GHC.Types.Symbol, GHC.Types.Nat)] @'[ '("Symbol", 1)]
+          with Proxy @'[ '("Symbol", 1)]
           (defined at T14343.hs:8:16)

testsuite/tests/printer/T14343b.stderr

@@ -8,7 +8,7 @@ T14343b.hs:10:9: error:
       Valid hole fits include
         test1 :: Proxy '( 'True, 'False) (defined at T14343b.hs:10:1)
         Proxy :: forall k1 (k2 :: k1). Proxy k2
-          with Proxy @(Bool, Bool) @'( 'True, 'False)
+          with Proxy @'( 'True, 'False)
           (defined at T14343b.hs:8:16)
 
 T14343b.hs:11:9: error:
@@ -23,7 +23,7 @@ T14343b.hs:11:9: error:
         test2 :: Proxy '( '( 'True, 'False), 'False)
           (defined at T14343b.hs:11:1)
         Proxy :: forall k1 (k2 :: k1). Proxy k2
-          with Proxy @((Bool, Bool), Bool) @'( '( 'True, 'False), 'False)
+          with Proxy @'( '( 'True, 'False), 'False)
           (defined at T14343b.hs:8:16)
 
 T14343b.hs:12:9: error:
@@ -35,5 +35,5 @@ T14343b.hs:12:9: error:
       Valid hole fits include
         test3 :: Proxy '( '[1], 'False) (defined at T14343b.hs:12:1)
         Proxy :: forall k1 (k2 :: k1). Proxy k2
-          with Proxy @([GHC.Types.Nat], Bool) @'( '[1], 'False)
+          with Proxy @'( '[1], 'False)
           (defined at T14343b.hs:8:16)

testsuite/tests/typecheck/should_fail/T16456.hs

+{-# LANGUAGE PolyKinds #-}
+module T16456 where
+
+data T p = MkT
+
+foo :: T Int
+foo = _

testsuite/tests/typecheck/should_fail/T16456.stderr

+
+T16456.hs:7:7: error:
+    • Found hole: _ :: T Int
+    • In the expression: _
+      In an equation for ‘foo’: foo = _
+    • Relevant bindings include foo :: T Int (bound at T16456.hs:7:1)
+      Valid hole fits include
+        foo :: T Int (bound at T16456.hs:7:1)
+        MkT :: forall {k} (p :: k). T p
+          with MkT @Int
+          (defined at T16456.hs:4:12)

testsuite/tests/typecheck/should_fail/all.T

@@ -514,5 +514,6 @@ test('T16255', normal, compile_fail, [''])
 test('T16204c', normal, compile_fail, [''])
 test('T16394', normal, compile_fail, [''])
 test('T16414', normal, compile_fail, [''])
+test('T16456', normal, compile_fail, ['-fprint-explicit-foralls'])
 test('T16627', normal, compile_fail, [''])
 test('T502', normal, compile_fail, [''])