Fix #15787 by squashing a coercion hole.

In type-incorrect code, we can sometimes let a coercion
hole make it through the zonker. If this coercion hole then
ends up in the environment (e.g., in the type of a data
constructor), then it causes trouble later.

This patch avoids trouble by substituting the coercion hole
for its representative CoVar. Really, any coercion would do,
but the CoVar was very handy.

test case: polykinds/T15787

3 files changed, 26 insertions, 0 deletions

diff --git a/testsuite/tests/polykinds/T15787.hs b/testsuite/tests/polykinds/T15787.hs
new file mode 100644
index 0000000000..85e737a479
--- /dev/null
+++ b/testsuite/tests/polykinds/T15787.hs
@@ -0,0 +1,19 @@
+{-# Language RankNTypes #-}
+{-# Language TypeApplications #-}
+{-# Language DataKinds        #-}
+{-# Language PolyKinds        #-}
+{-# Language GADTs            #-}
+{-# Language TypeFamilies     #-}
+
+import Data.Kind
+
+class Ríki (ob :: Type) where
+ type Hom :: ob -> ob -> Type
+
+data
+  Kl_kind :: forall ob . (ob -> ob) -> ob -> Type where
+  Kl      :: k -> Kl_kind (m :: ob -> ob) k
+
+type family
+  UnKl (kl :: Kl_kind m k) = (res :: k) where
+  UnKl (Kl a) = a
diff --git a/testsuite/tests/polykinds/T15787.stderr b/testsuite/tests/polykinds/T15787.stderr
new file mode 100644
index 0000000000..6d368d5218
--- /dev/null
+++ b/testsuite/tests/polykinds/T15787.stderr
@@ -0,0 +1,6 @@
+
+T15787.hs:15:43: error:
+    • Expected kind ‘ob’, but ‘k’ has kind ‘*’
+    • In the second argument of ‘Kl_kind’, namely ‘k’
+      In the type ‘Kl_kind (m :: ob -> ob) k’
+      In the definition of data constructor ‘Kl’
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 010d0ac703..371fbf249a 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -194,3 +194,4 @@ test('T15170', normal, compile, [''])
 test('T14939', normal, compile, ['-O'])
 test('T15577', normal, compile_fail, ['-O'])
 test('T15592', normal, compile, [''])
+test('T15787', normal, compile_fail, [''])