Remove the incredibly hairy splitTelescopeTvs.

This patch removes splitTelescopeTvs by adding information about
scoped type variables to TcTyCon. Vast simplification!

This also fixes #11821 by bringing only unzonked vars into scope.

Test case: polykinds/T11821

1 files changed, 31 insertions, 0 deletions

diff --git a/testsuite/tests/polykinds/T11821.hs b/testsuite/tests/polykinds/T11821.hs
new file mode 100644
index 0000000000..82efeb5f98
--- /dev/null
+++ b/testsuite/tests/polykinds/T11821.hs
@@ -0,0 +1,31 @@
+{-# LANGUAGE RankNTypes, DataKinds, PolyKinds, GADTs, TypeFamilies, UndecidableInstances #-}
+module NotInScope where
+
+import Data.Proxy
+
+type KindOf (a :: k) = ('KProxy :: KProxy k)
+data TyFun :: * -> * -> *
+type family Apply (f :: TyFun k1 k2 -> *) (x :: k1) :: k2
+
+data Lgo2 l1
+          l2
+          l3
+          (l4 :: b)
+          (l5 :: TyFun [a] b)
+  = forall (arg :: [a]) . KindOf (Apply (Lgo2 l1 l2 l3 l4) arg) ~ KindOf (Lgo l1 l2 l3 l4 arg) =>
+    Lgo2KindInference
+
+data Lgo1 l1
+          l2
+          l3
+          (l4 :: TyFun b (TyFun [a] b -> *))
+  = forall (arg :: b) . KindOf (Apply (Lgo1 l1 l2 l3) arg) ~ KindOf (Lgo2 l1 l2 l3 arg) =>
+    Lgo1KindInference
+
+type family Lgo f
+                z0
+                xs0
+                (a1 :: b)
+                (a2 :: [a]) :: b where
+  Lgo f z0 xs0 z '[]         = z
+  Lgo f z0 xs0 z ('(:) x xs) = Apply (Apply (Lgo1 f z0 xs0) (Apply (Apply f z) x)) xs