diff --git a/compiler/typecheck/TcHoleErrors.hs b/compiler/typecheck/TcHoleErrors.hs
index db47450aa1279cdbf032c1ab8cd16666af04de45..a5a4cf28d4236a0d36fa0b34e44079b789dabc76 100644
--- a/compiler/typecheck/TcHoleErrors.hs
+++ b/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 "_"
diff --git a/testsuite/tests/printer/T14343.stderr b/testsuite/tests/printer/T14343.stderr
index 5865669302a4250788e0a2488aa4891125654b61..7ffb689a7de17abe917d73bb234ee6ac43161d1f 100644
--- a/testsuite/tests/printer/T14343.stderr
+++ b/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)
diff --git a/testsuite/tests/printer/T14343b.stderr b/testsuite/tests/printer/T14343b.stderr
index 75731694149099afc6a166ce20ec4ed344d7cfa1..94e540c79ef3bfd80483e4157fc1fe50322913f5 100644
--- a/testsuite/tests/printer/T14343b.stderr
+++ b/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)
diff --git a/testsuite/tests/typecheck/should_fail/T16456.hs b/testsuite/tests/typecheck/should_fail/T16456.hs
new file mode 100644
index 0000000000000000000000000000000000000000..4257483c754fec8f2472630372bcc85b0ea71ff8
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T16456.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE PolyKinds #-}
+module T16456 where
+
+data T p = MkT
+
+foo :: T Int
+foo = _
diff --git a/testsuite/tests/typecheck/should_fail/T16456.stderr b/testsuite/tests/typecheck/should_fail/T16456.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..fbc0cc6ed57f81d0cb7e3198c2b60aece53fbaa8
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T16456.stderr
@@ -0,0 +1,11 @@
+
+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)
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index c4c5040b9bda477737cea3321fa9080f54f2d344..cbda265757fef1f617924f38238fe59be02fc1f6 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -515,4 +515,5 @@ 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, [''])