Provide a better error message for unpromotable data constructor contexts

Trac #14845 brought to light a corner case where a data
constructor could not be promoted (even with `-XTypeInType`) due to
an unpromotable constraint in its context. However, the error message
was less than helpful, so this patch adds an additional check to
`tcTyVar` catch unpromotable data constructors like these //before//
they're promoted, and to give a sensible error message in such cases.

Test Plan: make test TEST="T13895 T14845"

Reviewers: simonpj, goldfire, bgamari

Reviewed By: bgamari

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #13895, #14845

Differential Revision: https://phabricator.haskell.org/D4728

12 files changed, 104 insertions, 3 deletions

diff --git a/testsuite/tests/dependent/should_compile/T14845_compile.hs b/testsuite/tests/dependent/should_compile/T14845_compile.hs
new file mode 100644
index 0000000000..04f50189b8
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T14845_compile.hs
@@ -0,0 +1,16 @@
+{-# Language PolyKinds, DataKinds, KindSignatures, GADTs, TypeInType, ConstraintKinds #-}
+{-# Language FlexibleContexts #-}
+{-# Language RankNTypes #-}
+{-# Language TypeOperators #-}
+module T14845 where
+
+import Data.Kind
+import Data.Type.Equality
+
+data A :: Type -> Type where
+  MkA1 :: a ~  Int => A a
+  MkA2 :: a ~~ Int => A a
+
+data SA :: forall a. A a -> Type where
+  SMkA1 :: SA MkA1
+  SMkA2 :: SA MkA2
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index 2865351ff5..64782c0276 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -47,6 +47,7 @@ test('T14556', normal, compile, [''])
 test('T14720', normal, compile, [''])
 test('T14066a', normal, compile, [''])
 test('T14749', normal, compile, [''])
+test('T14845_compile', normal, compile, [''])
 test('T14991', normal, compile, [''])
 test('T15264', normal, compile, [''])
-test('DkNameRes', normal, compile, [''])
\ No newline at end of file
+test('DkNameRes', normal, compile, [''])
diff --git a/testsuite/tests/dependent/should_fail/PromotedClass.stderr b/testsuite/tests/dependent/should_fail/PromotedClass.stderr
index f0683309bc..4da1a32fca 100644
--- a/testsuite/tests/dependent/should_fail/PromotedClass.stderr
+++ b/testsuite/tests/dependent/should_fail/PromotedClass.stderr
@@ -1,5 +1,6 @@
 
 PromotedClass.hs:10:15: error:
-    • Illegal constraint in a type: Show a0
+    • Data constructor ‘MkX’ cannot be used here
+        (it has an unpromotable context ‘Show a’)
     • In the first argument of ‘Proxy’, namely ‘( 'MkX  'True)’
       In the type signature: foo :: Proxy ( 'MkX  'True)
diff --git a/testsuite/tests/dependent/should_fail/T13895.hs b/testsuite/tests/dependent/should_fail/T13895.hs
new file mode 100644
index 0000000000..5897cd8149
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T13895.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeInType #-}
+module T13895 where
+
+import Data.Data (Data, Typeable)
+import Data.Kind
+
+dataCast1 :: forall (a :: Type).
+             Data a
+          => forall (c :: Type -> Type)
+                    (t :: forall (k :: Type). Typeable k => k -> Type).
+             Typeable t
+          => (forall d. Data d => c (t d))
+          -> Maybe (c a)
+dataCast1 _ = undefined
diff --git a/testsuite/tests/dependent/should_fail/T13895.stderr b/testsuite/tests/dependent/should_fail/T13895.stderr
new file mode 100644
index 0000000000..0ae1710bf0
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T13895.stderr
@@ -0,0 +1,20 @@
+
+T13895.hs:12:23: error:
+    • Illegal constraint in a kind: Typeable k0
+    • In the first argument of ‘Typeable’, namely ‘t’
+      In the type signature:
+        dataCast1 :: forall (a :: Type).
+                     Data a =>
+                     forall (c :: Type -> Type)
+                            (t :: forall (k :: Type). Typeable k => k -> Type).
+                     Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)
+
+T13895.hs:13:38: error:
+    • Illegal constraint in a kind: Typeable k0
+    • In the first argument of ‘c’, namely ‘(t d)’
+      In the type signature:
+        dataCast1 :: forall (a :: Type).
+                     Data a =>
+                     forall (c :: Type -> Type)
+                            (t :: forall (k :: Type). Typeable k => k -> Type).
+                     Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)
diff --git a/testsuite/tests/dependent/should_fail/T14845.stderr b/testsuite/tests/dependent/should_fail/T14845.stderr
new file mode 100644
index 0000000000..3c11d15195
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14845.stderr
@@ -0,0 +1,7 @@
+
+T14845.hs:19:16: error:
+    • Data constructor ‘MkA3’ cannot be used here
+        (it has an unpromotable context ‘Coercible a Int’)
+    • In the first argument of ‘SA’, namely ‘(MkA3 :: A Int)’
+      In the type ‘SA (MkA3 :: A Int)’
+      In the definition of data constructor ‘SMkA3’
diff --git a/testsuite/tests/dependent/should_fail/T14845_fail1.hs b/testsuite/tests/dependent/should_fail/T14845_fail1.hs
new file mode 100644
index 0000000000..46c1351027
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14845_fail1.hs
@@ -0,0 +1,10 @@
+{-# Language PolyKinds, DataKinds, KindSignatures, GADTs, TypeInType, ConstraintKinds #-}
+module T14845_fail1 where
+
+import Data.Kind
+
+data Struct :: (k -> Constraint) -> (k -> Type) where
+  S :: cls a => Struct cls a
+
+data Foo a where
+  F :: Foo (S::Struct Eq a)
diff --git a/testsuite/tests/dependent/should_fail/T14845_fail1.stderr b/testsuite/tests/dependent/should_fail/T14845_fail1.stderr
new file mode 100644
index 0000000000..c1f1c8605d
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14845_fail1.stderr
@@ -0,0 +1,7 @@
+
+T14845_fail1.hs:10:13: error:
+    • Data constructor ‘S’ cannot be used here
+        (it has an unpromotable context ‘cls a’)
+    • In the first argument of ‘Foo’, namely ‘(S :: Struct Eq a)’
+      In the type ‘Foo (S :: Struct Eq a)’
+      In the definition of data constructor ‘F’
diff --git a/testsuite/tests/dependent/should_fail/T14845_fail2.hs b/testsuite/tests/dependent/should_fail/T14845_fail2.hs
new file mode 100644
index 0000000000..4c5dac730f
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14845_fail2.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeInType #-}
+module T14845_fail2 where
+
+import Data.Coerce
+import Data.Kind
+
+data A :: Type -> Type where
+  MkA :: Coercible a Int => A a
+
+data SA :: forall a. A a -> Type where
+  SMkA :: SA MkA
diff --git a/testsuite/tests/dependent/should_fail/T14845_fail2.stderr b/testsuite/tests/dependent/should_fail/T14845_fail2.stderr
new file mode 100644
index 0000000000..9fe733f374
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14845_fail2.stderr
@@ -0,0 +1,7 @@
+
+T14845_fail2.hs:14:14: error:
+    • Data constructor ‘MkA’ cannot be used here
+        (it has an unpromotable context ‘Coercible a Int’)
+    • In the first argument of ‘SA’, namely ‘MkA’
+      In the type ‘SA MkA’
+      In the definition of data constructor ‘SMkA’
diff --git a/testsuite/tests/dependent/should_fail/T15215.stderr b/testsuite/tests/dependent/should_fail/T15215.stderr
index 80181b44bd..53aff765a3 100644
--- a/testsuite/tests/dependent/should_fail/T15215.stderr
+++ b/testsuite/tests/dependent/should_fail/T15215.stderr
@@ -6,7 +6,7 @@ T15215.hs:9:3: error:
       In the data type declaration for ‘A’
 
 T15215.hs:12:14: error:
-    • Illegal constraint in a type: Show (Maybe a0)
+    • Illegal constraint in a kind: Show (Maybe a0)
     • In the first argument of ‘SA’, namely ‘MkA’
       In the type ‘SA MkA’
       In the definition of data constructor ‘SMkA’
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index 8e5185f1ae..2bfc39a6b8 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -19,6 +19,7 @@ test('T13601', normal, compile_fail, [''])
 test('T13780a', normal, compile_fail, [''])
 test('T13780c', [extra_files(['T13780b.hs'])],
                 multimod_compile_fail, ['T13780c', ''])
+test('T13895', normal, compile_fail, [''])
 test('T14066', normal, compile_fail, [''])
 test('T14066c', normal, compile_fail, [''])
 test('T14066d', normal, compile_fail, [''])
@@ -26,6 +27,8 @@ test('T14066e', normal, compile_fail, [''])
 test('T14066f', normal, compile_fail, [''])
 test('T14066g', normal, compile_fail, [''])
 test('T14066h', normal, compile_fail, [''])
+test('T14845_fail1', normal, compile_fail, [''])
+test('T14845_fail2', normal, compile_fail, [''])
 test('InferDependency', normal, compile_fail, [''])
 test('T15245', normal, compile_fail, [''])
 test('T15215', normal, compile_fail, [''])