diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs index d23ae2326922e04f49abe8a87caf3bf9be4fc60b..2b2b64b909cf014ec29c5dccc3f091fed9ef2ff1 100644 --- a/compiler/typecheck/TcHsType.hs +++ b/compiler/typecheck/TcHsType.hs @@ -1571,7 +1571,7 @@ kcLHsQTyVars name flav cusk -- fully settled down by this point, and so this check will get -- a false positive. ; when (not_associated && not (null meta_tvs)) $ - report_non_cusk_tvs (qkvs ++ tc_tvs) + report_non_cusk_tvs (qkvs ++ tc_tvs) res_kind -- If any of the scoped_kvs aren't actually mentioned in a binder's -- kind (or the return kind), then we're in the CUSK case from @@ -1643,7 +1643,7 @@ kcLHsQTyVars name flav cusk | otherwise = mkAnonTyConBinder tv - report_non_cusk_tvs all_tvs + report_non_cusk_tvs all_tvs res_kind = do { all_tvs <- mapM zonkTyCoVarKind all_tvs ; let (_, tidy_tvs) = tidyOpenTyCoVars emptyTidyEnv all_tvs (meta_tvs, other_tvs) = partition isMetaTyVar tidy_tvs @@ -1654,8 +1654,14 @@ kcLHsQTyVars name flav cusk isOrAre meta_tvs <+> text "undetermined:") 2 (vcat (map pp_tv meta_tvs)) , text "Perhaps add a kind signature." - , hang (text "Inferred kinds of user-written variables:") - 2 (vcat (map pp_tv other_tvs)) ] } + , ppUnless (null other_tvs) $ + hang (text "Inferred kinds of user-written variables:") + 2 (vcat (map pp_tv other_tvs)) + -- It's possible that the result kind contains + -- underdetermined, forall-bound variables which weren't + -- reported earier (see #13777). + , hang (text "Inferred result kind:") + 2 (ppr res_kind) ] } where pp_tv tv = ppr tv <+> dcolon <+> ppr (tyVarKind tv) kcLHsQTyVars _ _ _ (XLHsQTyVars _) _ = panic "kcLHsQTyVars" diff --git a/testsuite/tests/indexed-types/should_fail/T13777.hs b/testsuite/tests/indexed-types/should_fail/T13777.hs new file mode 100644 index 0000000000000000000000000000000000000000..bd6e85981aa262e9e23664b82d2575866ae2043b --- /dev/null +++ b/testsuite/tests/indexed-types/should_fail/T13777.hs @@ -0,0 +1,14 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeInType #-} +module T13777 where + +import Data.Kind +import Data.Proxy + +data S :: forall k. Proxy k -> Type where + MkS :: S ('Proxy :: Proxy Maybe) + +data T (a :: b) :: forall c (d :: Type) e. + (forall f. Proxy f) -> Proxy c -> Proxy d -> Proxy e + -> Type where diff --git a/testsuite/tests/indexed-types/should_fail/T13777.stderr b/testsuite/tests/indexed-types/should_fail/T13777.stderr new file mode 100644 index 0000000000000000000000000000000000000000..b920991d4b427f3ae18b4f7388b7914fd8f6a9ae --- /dev/null +++ b/testsuite/tests/indexed-types/should_fail/T13777.stderr @@ -0,0 +1,20 @@ + +T13777.hs:9:1: error: + You have written a *complete user-suppled kind signature*, + but the following variable is undetermined: k0 :: * + Perhaps add a kind signature. + Inferred result kind: forall (k :: k0). Proxy k -> * + +T13777.hs:12:1: error: + You have written a *complete user-suppled kind signature*, + but the following variables are undetermined: + k0 :: * + k1 :: * + k2 :: * + Perhaps add a kind signature. + Inferred kinds of user-written variables: + b :: * + a :: b + Inferred result kind: + forall (c :: k2) d (e :: k1). + (forall (f :: k0). Proxy f) -> Proxy c -> Proxy d -> Proxy e -> * diff --git a/testsuite/tests/indexed-types/should_fail/all.T b/testsuite/tests/indexed-types/should_fail/all.T index ef5eee2e8bd7abce7a53e4d8e51f73146812fe97..f69bce80bd4bd2548f80d46a3dfa75c69a363d31 100644 --- a/testsuite/tests/indexed-types/should_fail/all.T +++ b/testsuite/tests/indexed-types/should_fail/all.T @@ -134,6 +134,7 @@ test('T7102', [ expect_broken(7102) ], ghci_script, ['T7102.script']) test('T7102a', normal, ghci_script, ['T7102a.script']) test('T13271', normal, compile_fail, ['']) test('T13674', normal, compile_fail, ['']) +test('T13777', normal, compile_fail, ['']) test('T13784', normal, compile_fail, ['']) test('T13877', normal, compile_fail, ['']) test('T13972', normal, compile_fail, ['']) diff --git a/testsuite/tests/polykinds/T11648b.stderr b/testsuite/tests/polykinds/T11648b.stderr index e709e006b025c34c9d0f1e23cf6c7bed92226c23..cbe926394995dee89137e7eb89854e36591ad6e3 100644 --- a/testsuite/tests/polykinds/T11648b.stderr +++ b/testsuite/tests/polykinds/T11648b.stderr @@ -6,3 +6,4 @@ T11648b.hs:7:1: error: Inferred kinds of user-written variables: k :: k0 a :: Proxy k + Inferred result kind: * diff --git a/testsuite/tests/typecheck/should_fail/T14904a.stderr b/testsuite/tests/typecheck/should_fail/T14904a.stderr index 61be519d6a766f0d8387663d41bad65c8fad2371..603ecb5ec00e59535655db1d858afe984f73adb8 100644 --- a/testsuite/tests/typecheck/should_fail/T14904a.stderr +++ b/testsuite/tests/typecheck/should_fail/T14904a.stderr @@ -6,6 +6,7 @@ T14904a.hs:8:1: error: Inferred kinds of user-written variables: g :: k0 -> * f :: forall (a :: k0). g a + Inferred result kind: * T14904a.hs:9:6: error: • Expected kind ‘forall (a :: k1). g a’, but ‘f’ has kind ‘k0’