Revert "Remove unnecessary isTyVar tests in TcType"

Summary:
This reverts commit a0899b2f66a4102a7cf21569889381446ce63833. This is because
removing these checks prompts panics in at least two different programs
reported in #12785.

Test Plan: ./validate

Reviewers: simonpj, goldfire, bgamari, austin

Subscribers: thomie

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

GHC Trac Issues: #12785

5 files changed, 77 insertions, 0 deletions

diff --git a/testsuite/tests/typecheck/should_compile/T12785a.hs b/testsuite/tests/typecheck/should_compile/T12785a.hs
new file mode 100644
index 0000000000..1e4d6a1b64
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T12785a.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeFamilies #-}
+module T12785a where
+
+import Data.Kind (Type)
+
+foo :: forall (dk :: Type) (c :: Type -> Type) (t :: dk -> Type) (a :: Type).
+       (dk ~ Type)
+    => (forall (d :: dk). c (t d)) -> Maybe (c a)
+foo _ = Nothing
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 465d8acf9d..d322cc0e00 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -559,6 +559,7 @@ test('T12507', normal, compile, [''])
 test('T12734', normal, compile, [''])
 test('T12734a', normal, compile_fail, [''])
 test('T12763', normal, compile, [''])
+test('T12785a', normal, compile, [''])
 test('T12797', normal, compile, [''])
 test('T12911', normal, compile, [''])
 test('T12925', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T12785b.hs b/testsuite/tests/typecheck/should_fail/T12785b.hs
new file mode 100644
index 0000000000..4188e3e67c
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T12785b.hs
@@ -0,0 +1,38 @@
+{-# LANGUAGE RankNTypes, TypeInType, TypeOperators, KindSignatures, ViewPatterns #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE DataKinds, GADTs #-}
+
+module T12785b where
+
+import Data.Kind
+
+data Peano = Z | S Peano
+
+data HTree n a where
+  Point :: a -> HTree Z a
+  Leaf :: HTree (S n) a
+  Branch :: a -> HTree n (HTree (S n) a) -> HTree (S n) a
+
+data STree n :: forall a . (a -> *) -> HTree n a -> * where
+  SPoint :: f a -> STree Z f (Point a)
+  SLeaf :: STree (S n) f Leaf
+  SBranch :: f a -> STree n (STree (S n) f) stru -> STree (S n) f (a `Branch` stru)
+  SBranchX :: (Payload (S n) (Payload n stru) ~ a)
+          => f a -> STree n (STree (S n) f) stru -> STree (S n) f (a `Branch` stru)
+
+data Hidden :: Peano -> (a -> *) -> * where
+  Hide :: STree n f s -> Hidden n f
+
+nest :: HTree m (Hidden (S m) f) -> Hidden m (STree ('S m) f)
+nest (Point (Hide st)) = Hide (SPoint st)
+nest Leaf = Hide SLeaf
+nest (Hide a `Branch` (nest . hmap nest -> Hide tr)) = Hide $ a `SBranchX` tr
+
+hmap :: (x -> y) -> HTree n x -> HTree n y
+hmap f (Point a) = Point (f a)
+hmap f Leaf = Leaf
+hmap f (a `Branch` tr) = f a `Branch` hmap (hmap f) tr
+
+type family Payload (n :: Peano) (s :: HTree n x) where
+  Payload Z (Point a) = a
+  Payload (S n) (a `Branch` stru) = a
diff --git a/testsuite/tests/typecheck/should_fail/T12785b.stderr b/testsuite/tests/typecheck/should_fail/T12785b.stderr
new file mode 100644
index 0000000000..0290cfe4dd
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T12785b.stderr
@@ -0,0 +1,26 @@
+
+T12785b.hs:29:63: error:
+    • Could not deduce: Payload ('S n1) (Payload n1 s1) ~ s
+        arising from a use of ‘SBranchX’
+      from the context: m1 ~ 'S n1
+        bound by a pattern with constructor:
+                   Branch :: forall a (n :: Peano).
+                             a -> HTree n (HTree ('S n) a) -> HTree ('S n) a,
+                 in an equation for ‘nest’
+        at T12785b.hs:29:7-51
+    • In the second argument of ‘($)’, namely ‘a `SBranchX` tr’
+      In the expression: Hide $ a `SBranchX` tr
+      In an equation for ‘nest’:
+          nest (Hide a `Branch` (nest . hmap nest -> Hide tr))
+            = Hide $ a `SBranchX` tr
+    • Relevant bindings include
+        tr :: STree
+                n1
+                (HTree ('S n1) (HTree ('S ('S n1)) a))
+                (STree ('S n1) (HTree ('S ('S n1)) a) (STree ('S ('S n1)) a f))
+                s1
+          (bound at T12785b.hs:29:49)
+        a :: STree ('S m1) a f s (bound at T12785b.hs:29:12)
+        nest :: HTree m1 (Hidden ('S m1) f)
+                -> Hidden m1 (STree ('S m1) a f)
+          (bound at T12785b.hs:27:1)
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 9931037e4e..f4db8bac4e 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -428,6 +428,7 @@ test('T12124', normal, compile_fail, [''])
 test('T12589', normal, compile_fail, [''])
 test('T12529', normal, compile_fail, [''])
 test('T12729', normal, compile_fail, [''])
+test('T12785b', normal, compile_fail, [''])
 test('T12803', normal, compile_fail, [''])
 test('T12042', extra_clean(['T12042a.hi', 'T12042a.o', 'T12042.hi-boot', 'T12042.o-boot']), multimod_compile_fail, ['T12042', ''])
 test('T12966', normal, compile_fail, [''])