Significant refactor of Lint

This refactoring of Lint was triggered by #17923, which is
fixed by this patch.

The main change is this.  Instead of
   lintType :: Type -> LintM LintedKind
we now have
   lintType :: Type -> LintM LintedType

Previously, all of typeKind was effectively duplicate in lintType.
Moreover, since we have an ambient substitution, we still had to
apply the substition here and there, sometimes more than once. It
was all very tricky, in the end, and made my head hurt.

Now, lintType returns a fully linted type, with all substitutions
performed on it.  This is much simpler.

The same thing is needed for Coercions.  Instead of
  lintCoercion :: OutCoercion
               -> LintM (LintedKind, LintedKind,
                         LintedType, LintedType, Role)
we now have
  lintCoercion :: Coercion -> LintM LintedCoercion

Much simpler!  The code is shorter and less bug-prone.

There are a lot of knock on effects.  But life is now better.

Metric Decrease:
    T1969

2 files changed, 45 insertions, 0 deletions

diff --git a/testsuite/tests/indexed-types/should_compile/T17923.hs b/testsuite/tests/indexed-types/should_compile/T17923.hs
new file mode 100644
index 0000000000..8c34024864
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T17923.hs
@@ -0,0 +1,44 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# OPTIONS_GHC -Wall #-}
+module Bug where
+
+import Data.Kind
+
+-- type SingFunction2 f = forall t1 t2. Sing t1 -> Sing t2 -> Sing (f `Apply` t1 `Apply` t2)
+type SingFunction2 f = forall t1. Sing t1 -> forall t2. Sing t2 -> Sing (f `Apply` t1 `Apply` t2)
+singFun2 :: forall f. SingFunction2 f -> Sing f
+singFun2 f = SLambda (\x -> SLambda (f x))
+
+type family Sing :: k -> Type
+data TyFun :: Type -> Type -> Type
+type a ~> b = TyFun a b -> Type
+infixr 0 ~>
+
+type family Apply (f :: a ~> b) (x :: a) :: b
+data Sym4 a
+data Sym3 a
+
+type instance Apply Sym3 _ = Sym4
+
+newtype SLambda (f :: k1 ~> k2) =
+  SLambda { applySing :: forall t. Sing t -> Sing (Apply f t) }
+type instance Sing = SLambda
+
+und :: a
+und = undefined
+
+data E
+data ShowCharSym0 :: E ~> E ~> E
+
+sShow_tuple :: SLambda Sym4
+sShow_tuple
+  = applySing (singFun2 @Sym3 und)
+          (und (singFun2 @Sym3
+                 (und (applySing (singFun2 @Sym3 und)
+                                 (applySing (singFun2 @ShowCharSym0 und) und)))))
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index 8bda294207..ccca063fd2 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -294,3 +294,4 @@ test('T16828', normal, compile, [''])
 test('T17008b', normal, compile, [''])
 test('T17056', normal, compile, [''])
 test('T17405', normal, multimod_compile, ['T17405c', '-v0'])
+test('T17923', normal, compile, [''])