Remove knot-tying bug in TcHsSyn.zonkTyVarOcc

There was a subtle knot-tying bug in TcHsSyn.zonkTyVarOcc, revealed
in Trac #15552.

I fixed it by

* Eliminating the short-circuiting optimisation in zonkTyVarOcc,
  instead adding a finite map to get sharing of zonked unification
  variables.

  See Note [Sharing when zonking to Type] in TcHsSyn

* On the way I /added/ the short-circuiting optimisation to
  TcMType.zonkTcTyVar, which has no such problem.  This turned
  out (based on non-systematic measurements) to be a modest win.

  See Note [Sharing in zonking] in TcMType

On the way I renamed some of the functions in TcHsSyn:

* Ones ending in "X" (like zonkTcTypeToTypeX) take a ZonkEnv

* Ones that do not end in "x" (like zonkTcTypeToType), don't.
  Instead they whiz up an empty ZonkEnv.

4 files changed, 68 insertions, 0 deletions

diff --git a/testsuite/tests/typecheck/should_fail/T15552.hs b/testsuite/tests/typecheck/should_fail/T15552.hs
new file mode 100644
index 0000000000..f1952cc10b
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15552.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE DataKinds, ExistentialQuantification, GADTs, PolyKinds, TypeOperators #-}
+{-# LANGUAGE TypeInType, TypeFamilies #-}
+module T15552 where
+
+import Data.Kind
+
+data Elem :: k -> [k] -> Type
+
+data EntryOfVal (v :: Type) (kvs :: [Type]) where
+  EntryOfVal :: forall (v :: Type) (kvs :: [Type]) (k :: Type).
+                Elem (k, v) kvs -> EntryOfVal v kvs
+
+type family EntryOfValKey (eov :: EntryOfVal v kvs) :: Type
+
+type family GetEntryOfVal (eov :: EntryOfVal v kvs) :: Elem (EntryOfValKey eov, v) kvs
+
+type family FirstEntryOfVal (v :: Type) (kvs :: [Type]) :: EntryOfVal v kvs where
diff --git a/testsuite/tests/typecheck/should_fail/T15552a.hs b/testsuite/tests/typecheck/should_fail/T15552a.hs
new file mode 100644
index 0000000000..86c71dc9c0
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15552a.hs
@@ -0,0 +1,28 @@
+{-# LANGUAGE DataKinds, ExistentialQuantification, GADTs, PolyKinds, TypeOperators #-}
+{-# LANGUAGE TypeInType, TypeFamilies #-}
+{-  # LANGUAGE UndecidableInstances #-}
+module T15552 where
+
+import Data.Kind
+
+data Elem :: k -> [k] -> Type where
+  Here :: Elem x (x : xs)
+  There :: Elem x xs -> Elem x (y : xs)
+
+data EntryOfVal (v :: Type) (kvs :: [Type]) where
+  EntryOfVal :: forall (v :: Type) (kvs :: [Type]) (k :: Type).
+                Elem (k, v) kvs -> EntryOfVal v kvs
+
+type family EntryOfValKey (eov :: EntryOfVal v kvs) :: Type where
+  EntryOfValKey ('EntryOfVal (_ :: Elem (k, v) kvs)) = k
+
+type family GetEntryOfVal (eov :: EntryOfVal v kvs)
+            :: Elem (EntryOfValKey eov, v) kvs
+  where
+    GetEntryOfVal ('EntryOfVal e) = e
+
+type family FirstEntryOfVal (v :: Type) (kvs :: [Type]) :: EntryOfVal v kvs
+  where FirstEntryOfVal v (_ : kvs)
+           = 'EntryOfVal (There (GetEntryOfVal (FirstEntryOfVal v kvs)))
+--type instance FirstEntryOfVal v (_ : kvs)
+--         = 'EntryOfVal ('There (GetEntryOfVal (FirstEntryOfVal v kvs)))
diff --git a/testsuite/tests/typecheck/should_fail/T15552a.stderr b/testsuite/tests/typecheck/should_fail/T15552a.stderr
new file mode 100644
index 0000000000..f24c6d1285
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15552a.stderr
@@ -0,0 +1,21 @@
+
+T15552a.hs:25:9: error:
+    • Illegal nested type family application ‘EntryOfValKey
+                                                (FirstEntryOfVal v kvs)’
+      (Use UndecidableInstances to permit this)
+    • In the equations for closed type family ‘FirstEntryOfVal’
+      In the type family declaration for ‘FirstEntryOfVal’
+
+T15552a.hs:25:9: error:
+    • Illegal nested type family application ‘EntryOfValKey
+                                                (FirstEntryOfVal v kvs)’
+      (Use UndecidableInstances to permit this)
+    • In the equations for closed type family ‘FirstEntryOfVal’
+      In the type family declaration for ‘FirstEntryOfVal’
+
+T15552a.hs:25:9: error:
+    • Illegal nested type family application ‘GetEntryOfVal
+                                                (FirstEntryOfVal v kvs)’
+      (Use UndecidableInstances to permit this)
+    • In the equations for closed type family ‘FirstEntryOfVal’
+      In the type family declaration for ‘FirstEntryOfVal’
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 9c4df89238..895721937d 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -479,3 +479,5 @@ test('T15361', normal, compile_fail, [''])
 test('T15438', normal, compile_fail, [''])
 test('T15523', normal, compile_fail, ['-O'])
 test('T15527', normal, compile_fail, [''])
+test('T15552', normal, compile, [''])
+test('T15552a', normal, compile_fail, [''])