From ac91d07399207f4e22467bea3577cafd27a937d7 Mon Sep 17 00:00:00 2001
From: Ryan Scott <ryan.gl.scott@gmail.com>
Date: Sat, 2 Jun 2018 21:16:40 -0400
Subject: [PATCH] Fix #13777 by improving the underdetermined CUSK error
 message

The error message that GHC emits from underdetermined CUSKs
is rather poor, since:

1. It may print an empty list of user-written variables if there
    are none in the declaration.
2. It may not mention any `forall`-bound, underdetermined
    variables in the result kind.

To resolve these issues, this patch:

1. Doesn't bother printing a herald about user-written
    variables if there are none.
2. Prints the result kind to advertise any
    underdetermination it may exhibit.

Test Plan: make test TEST=T13777

Reviewers: goldfire, bgamari

Reviewed By: goldfire

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #13777

Differential Revision: https://phabricator.haskell.org/D4771
---
 compiler/typecheck/TcHsType.hs                | 14 +++++++++----
 .../tests/indexed-types/should_fail/T13777.hs | 14 +++++++++++++
 .../indexed-types/should_fail/T13777.stderr   | 20 +++++++++++++++++++
 .../tests/indexed-types/should_fail/all.T     |  1 +
 testsuite/tests/polykinds/T11648b.stderr      |  1 +
 .../typecheck/should_fail/T14904a.stderr      |  1 +
 6 files changed, 47 insertions(+), 4 deletions(-)
 create mode 100644 testsuite/tests/indexed-types/should_fail/T13777.hs
 create mode 100644 testsuite/tests/indexed-types/should_fail/T13777.stderr

diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index d23ae23269..2b2b64b909 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 0000000000..bd6e85981a
--- /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 0000000000..b920991d4b
--- /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 ef5eee2e8b..f69bce80bd 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 e709e006b0..cbe9263949 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 61be519d6a..603ecb5ec0 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’
-- 
GitLab