Fix #12919 by making the flattener homegeneous.

This changes a key invariant of the flattener. Previously,
flattening a type meant flattening its kind as well. But now,
flattening is always homogeneous -- that is, the kind of the
flattened type is the same as the kind of the input type.
This is achieved by various wizardry in the TcFlatten.flatten_many
function, as described in Note [flatten_many].

There are several knock-on effects, including some refactoring
in the canonicalizer to take proper advantage of the flattener's
changed behavior. In particular, the tyvar case of can_eq_nc' no
longer needs to take casts into account.

Another effect is that flattening a tyconapp might change it
into a casted tyconapp. This might happen if the result kind
of the tycon contains a variable, and that variable changes
during flattening. Because the flattener is homogeneous, it tacks
on a cast to keep the tyconapp kind the same. However, this
is problematic when flattening CFunEqCans, which need to have
an uncasted tyconapp on the LHS and must remain homogeneous.
The solution is a more involved canCFunEqCan, described in
Note [canCFunEqCan].

This patch fixes #13643 (as tested in typecheck/should_compile/T13643)
and the panic in typecheck/should_compile/T13822 (as reported in #14024).
Actually, there were two bugs in T13822: the first was just some
incorrect logic in tryFill (part of the unflattener) -- also fixed
in this patch -- and the other was the main bug fixed in this ticket.

The changes in this patch exposed a long-standing flaw in OptCoercion,
in that breaking apart an AppCo sometimes has unexpected effects on
kinds. See new Note [EtaAppCo] in OptCoercion, which explains the
problem and fix.

Also here is a reversion of the major change in
09bf135ace55ce2572bf4168124d631e386c64bb, affecting ctEvCoercion.
It turns out that making the flattener homogeneous changes the
invariants on the algorithm, making the change in that patch
no longer necessary.

This patch also fixes:
  #14038 (dependent/should_compile/T14038)
  #13910 (dependent/should_compile/T13910)
  #13938 (dependent/should_compile/T13938)
  #14441 (typecheck/should_compile/T14441)
  #14556 (dependent/should_compile/T14556)
  #14720 (dependent/should_compile/T14720)
  #14749 (typecheck/should_compile/T14749)

Sadly, this patch negatively affects performance of type-family-
heavy code. The following patch fixes these performance degradations.
However, the performance fixes are somewhat invasive and so I've
kept them as a separate patch, labeling this one as [skip ci] so
that validation doesn't fail on the performance cases.

12 files changed, 230 insertions, 25 deletions

diff --git a/testsuite/tests/dependent/should_compile/T14556.hs b/testsuite/tests/dependent/should_compile/T14556.hs
new file mode 100644
index 0000000000..eebbdca888
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T14556.hs
@@ -0,0 +1,38 @@
+{-# Language UndecidableInstances, DataKinds, TypeOperators, KindSignatures, PolyKinds, TypeInType, TypeFamilies, GADTs, LambdaCase, ScopedTypeVariables #-}
+
+module T14556 where
+
+import Data.Kind
+import Data.Proxy
+
+data Fn a b where
+  IdSym :: Fn Type Type
+
+type family
+  (@@) (f::Fn k k') (a::k)::k' where
+  IdSym @@ a = a
+
+data KIND = X | FNARR KIND KIND
+
+data TY :: KIND -> Type where
+  ID    :: TY (FNARR X X)
+  FNAPP :: TY (FNARR k k') -> TY k -> TY k'
+
+data TyRep (kind::KIND) :: TY kind -> Type where
+  TID    :: TyRep (FNARR X X)  ID
+  TFnApp :: TyRep (FNARR k k') f
+         -> TyRep k            a
+         -> TyRep k'           (FNAPP f a)
+
+type family
+  IK (kind::KIND) :: Type where
+  IK X            = Type
+  IK (FNARR k k') = Fn (IK k) (IK k')
+
+type family
+  IT (ty::TY kind) :: IK kind where
+  IT ID          = IdSym
+  IT (FNAPP f x) = IT f @@ IT x
+
+zero :: TyRep X a -> IT a
+zero = undefined
diff --git a/testsuite/tests/dependent/should_compile/T14720.hs b/testsuite/tests/dependent/should_compile/T14720.hs
new file mode 100644
index 0000000000..c26a184689
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T14720.hs
@@ -0,0 +1,44 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+module T14720 where
+
+import Data.Kind (Type)
+import Data.Type.Equality ((:~:)(..), sym, trans)
+import Data.Void
+
+data family Sing (z :: k)
+
+class Generic (a :: Type) where
+    type Rep a :: Type
+    from :: a -> Rep a
+    to :: Rep a -> a
+
+class PGeneric (a :: Type) where
+  type PFrom (x :: a)     :: Rep a
+  type PTo   (x :: Rep a) :: a
+
+class SGeneric k where
+  sFrom :: forall (a :: k).     Sing a -> Sing (PFrom a)
+  sTo   :: forall (a :: Rep k). Sing a -> Sing (PTo a :: k)
+
+class (PGeneric k, SGeneric k) => VGeneric k where
+  sTof  :: forall (a :: k).     Sing a -> PTo (PFrom a) :~: a
+  sFot  :: forall (a :: Rep k). Sing a -> PFrom (PTo a :: k) :~: a
+
+data Decision a = Proved a
+                | Disproved (a -> Void)
+
+class SDecide k where
+  (%~) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)
+  default (%~) :: forall (a :: k) (b :: k). (VGeneric k, SDecide (Rep k))
+               => Sing a -> Sing b -> Decision (a :~: b)
+  s1 %~ s2 = case sFrom s1 %~ sFrom s2 of
+    Proved (Refl :: PFrom a :~: PFrom b) ->
+      case (sTof s1, sTof s2) of
+          (Refl, Refl) -> Proved Refl
+    Disproved contra -> Disproved (\Refl -> contra Refl)
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index 684602cc94..ab7ab3c8df 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -25,7 +25,9 @@ test('T11966', normal, compile, [''])
 test('T12442', normal, compile, [''])
 test('T13538', normal, compile, [''])
 test('T12176', normal, compile, [''])
-test('T14038', expect_broken(14038), compile, [''])
+test('T14038', normal, compile, [''])
 test('T12742', normal, compile, [''])
-test('T13910', expect_broken(13910), compile, [''])
-test('T13938', expect_broken(13938), compile, [''])
+test('T13910', normal, compile, [''])
+test('T13938', normal, compile, [''])
+test('T14556', normal, compile, [''])
+test('T14720', normal, compile, [''])
diff --git a/testsuite/tests/dependent/should_fail/RAE_T32a.stderr b/testsuite/tests/dependent/should_fail/RAE_T32a.stderr
index cb94dd2854..046a1e1aa4 100644
--- a/testsuite/tests/dependent/should_fail/RAE_T32a.stderr
+++ b/testsuite/tests/dependent/should_fail/RAE_T32a.stderr
@@ -1,19 +1,18 @@
 
 RAE_T32a.hs:28:1: error:
-    Too many parameters to Sing:
-      x is unexpected;
-      expected only two parameters
-    In the data instance declaration for ‘Sing’
+    • Expected kind ‘k0 -> *’,
+        but ‘Sing Sigma (Sigma p r)’ has kind ‘*’
+    • In the data instance declaration for ‘Sing’
 
 RAE_T32a.hs:28:20: error:
-    Expecting two more arguments to ‘Sigma’
-    Expected a type, but
-    ‘Sigma’ has kind
-    ‘forall p -> TyPi p (MkStar p) -> *’
-    In the first argument of ‘Sing’, namely ‘Sigma’
-    In the data instance declaration for ‘Sing’
+    • Expecting two more arguments to ‘Sigma’
+      Expected a type, but
+      ‘Sigma’ has kind
+      ‘forall p -> TyPi p (MkStar p) -> *’
+    • In the first argument of ‘Sing’, namely ‘Sigma’
+      In the data instance declaration for ‘Sing’
 
 RAE_T32a.hs:28:27: error:
-    Expected kind ‘Sigma’, but ‘Sigma p r’ has kind ‘*’
-    In the second argument of ‘Sing’, namely ‘(Sigma p r)’
-    In the data instance declaration for ‘Sing’
+    • Expected kind ‘Sigma’, but ‘Sigma p r’ has kind ‘*’
+    • In the second argument of ‘Sing’, namely ‘(Sigma p r)’
+      In the data instance declaration for ‘Sing’
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index 4eb426419d..e28b2df5cd 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -1,5 +1,5 @@
 test('DepFail1', normal, compile_fail, [''])
-test('RAE_T32a', expect_broken(12919), compile_fail, [''])
+test('RAE_T32a', normal, compile_fail, [''])
 test('TypeSkolEscape', normal, compile_fail, [''])
 test('BadTelescope', normal, compile_fail, [''])
 test('BadTelescope2', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_compile/SplitWD.hs b/testsuite/tests/typecheck/should_compile/SplitWD.hs
new file mode 100644
index 0000000000..370b077b6e
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/SplitWD.hs
@@ -0,0 +1,55 @@
+{-# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators,
+             TypeFamilies, GADTs, StandaloneDeriving #-}
+
+module SplitWD where
+
+import Data.Kind ( Type )
+
+data Nat = Zero | Succ Nat
+
+type family a + b where
+  Zero + b = b
+  Succ a + b = Succ (a + b)
+infixl 6 +
+
+data Vec :: Type -> Nat -> Type where
+  VNil :: Vec a Zero
+  (:>) :: a -> Vec a n -> Vec a (Succ n)
+infixr 5 :>
+
+type family (xs :: Vec a n) +++ (ys :: Vec a m) :: Vec a (n + m) where
+  VNil +++ ys = ys
+  (x :> xs) +++ ys = x :> (xs +++ ys)
+infixr 5 +++
+
+data Exp :: Vec Type n -> Type -> Type where
+  Var :: Elem xs x -> Exp xs x
+
+data Elem :: forall a n. Vec a n -> a -> Type where
+  Here :: Elem (x :> xs) x
+  There :: Elem xs x -> Elem (y :> xs) x
+
+-- | @Length xs@ is a runtime witness for how long a vector @xs@ is.
+-- @LZ :: Length xs@ says that @xs@ is empty.
+-- @LS len :: Length xs@ tells you that @xs@ has one more element
+-- than @len@ says.
+-- A term of type @Length xs@ also serves as a proxy for @xs@.
+data Length :: forall a n. Vec a n -> Type where
+  LZ :: Length VNil
+  LS :: Length xs -> Length (x :> xs)
+
+deriving instance Show (Length xs)
+
+-- | Convert an expression typed in one context to one typed in a larger
+-- context. Operationally, this amounts to de Bruijn index shifting.
+-- As a proposition, this is the weakening lemma.
+shift :: forall ts2 t ty. Exp ts2 ty -> Exp (t :> ts2) ty
+shift = go LZ
+  where
+    go :: forall ts1 ty. Length ts1 -> Exp (ts1 +++ ts2) ty -> Exp (ts1 +++ t :> ts2) ty
+    go l_ts1 (Var v)          = Var (shift_elem l_ts1 v)
+
+    shift_elem :: Length ts1 -> Elem (ts1 +++ ts2) x
+               -> Elem (ts1 +++ t :> ts2) x
+    shift_elem = undefined
+
diff --git a/testsuite/tests/typecheck/should_compile/T13643.hs b/testsuite/tests/typecheck/should_compile/T13643.hs
new file mode 100644
index 0000000000..d7cf1342c8
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T13643.hs
@@ -0,0 +1,22 @@
+{-# Language TypeFamilyDependencies #-}
+{-# Language RankNTypes             #-}
+{-# Language KindSignatures         #-}
+{-# Language DataKinds              #-}
+{-# Language TypeInType             #-}
+{-# Language GADTs                  #-}
+
+import Data.Kind (Type)
+
+data Code = I
+
+type family
+  Interp (a :: Code) = (res :: Type) | res -> a where
+  Interp I = Bool
+
+data T :: forall a. Interp a -> Type where
+  MkNat :: T False
+
+instance Show (T a) where show _ = "MkNat"
+
+main = do
+  print MkNat
diff --git a/testsuite/tests/typecheck/should_compile/T14441.hs b/testsuite/tests/typecheck/should_compile/T14441.hs
new file mode 100644
index 0000000000..047de1659f
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T14441.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+module T14441 where
+
+import Data.Kind
+
+type family Demote (k :: Type) :: Type
+type family DemoteX (a :: k) :: Demote k
+
+data Prox (a :: k) = P
+
+type instance Demote (Prox (a :: k)) = Prox (DemoteX a)
+$(return [])
+type instance DemoteX P = P
diff --git a/testsuite/tests/typecheck/should_compile/T14749.hs b/testsuite/tests/typecheck/should_compile/T14749.hs
new file mode 100644
index 0000000000..79bcce66ff
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T14749.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE GADTs, TypeOperators, DataKinds, TypeFamilies, TypeInType #-}
+
+module T14749 where
+
+import Data.Kind
+
+data KIND = STAR | KIND :> KIND
+
+data Ty :: KIND -> Type where
+  TMaybe :: Ty (STAR :> STAR)
+  TApp   :: Ty (a :> b) -> (Ty a -> Ty b)
+
+type family IK (k :: KIND) = (res :: Type) where
+  IK STAR   = Type
+  IK (a:>b) = IK a -> IK b
+
+type family I (t :: Ty k) = (res :: IK k)  where
+  I TMaybe     = Maybe
+  I (TApp f a) = (I f) (I a)
+
+data TyRep (k :: KIND) (t :: Ty k) where
+  TyMaybe :: TyRep (STAR:>STAR) TMaybe
+  TyApp   :: TyRep (a:>b) f -> TyRep a x -> TyRep b (TApp f x)
+
+zero :: TyRep STAR a -> I a
+zero x = case x of
+            TyApp TyMaybe _ -> Nothing
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 9a2ce73263..f4b7fe6aeb 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -536,7 +536,7 @@ test('T12797', normal, compile, [''])
 test('T12850', normal, compile, [''])
 test('T12911', normal, compile, [''])
 test('T12925', normal, compile, [''])
-test('T12919', expect_broken(12919), compile, [''])
+test('T12919', normal, compile, [''])
 test('T12936', normal, compile, [''])
 test('T13050', normal, compile, ['-fdefer-type-errors -fno-max-valid-substitutions'])
 test('T13083', normal, compile, [''])
@@ -568,7 +568,7 @@ test('T13651a', normal, compile, [''])
 test('T13680', normal, compile, [''])
 test('T13785', normal, compile, [''])
 test('T13804', normal, compile, [''])
-test('T13822', expect_broken(14749), compile, [''])
+test('T13822', normal, compile, [''])
 test('T13848', normal, compile, [''])
 test('T13871', normal, compile, [''])
 test('T13879', normal, compile, [''])
@@ -599,3 +599,7 @@ test('T14763', normal, compile, [''])
 test('T14811', normal, compile, [''])
 test('T14934', [extra_files(['T14934.hs', 'T14934a.hs'])], run_command,
                ['$MAKE -s --no-print-directory T14934'])
+test('T13643', normal, compile, [''])
+test('SplitWD', expect_broken(14119), compile, [''])
+test('T14441', normal, compile, [''])
+test('T14749', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T12373.stderr b/testsuite/tests/typecheck/should_fail/T12373.stderr
index d3a4bb5e65..a2568d75f9 100644
--- a/testsuite/tests/typecheck/should_fail/T12373.stderr
+++ b/testsuite/tests/typecheck/should_fail/T12373.stderr
@@ -2,10 +2,10 @@
 T12373.hs:10:19: error:
     • Couldn't match a lifted type with an unlifted type
       When matching types
-        a1 :: *
-        MVar# RealWorld a0 :: TYPE 'UnliftedRep
-      Expected type: (# State# RealWorld, a1 #)
-        Actual type: (# State# RealWorld, MVar# RealWorld a0 #)
+        a0 :: *
+        MVar# RealWorld a1 :: TYPE 'UnliftedRep
+      Expected type: (# State# RealWorld, a0 #)
+        Actual type: (# State# RealWorld, MVar# RealWorld a1 #)
     • In the expression: newMVar# rw
       In the first argument of ‘IO’, namely ‘(\ rw -> newMVar# rw)’
       In the first argument of ‘(>>)’, namely ‘IO (\ rw -> newMVar# rw)’
diff --git a/testsuite/tests/typecheck/should_run/Typeable1.stderr b/testsuite/tests/typecheck/should_run/Typeable1.stderr
index 65f6fd4645..63f02dbeb6 100644
--- a/testsuite/tests/typecheck/should_run/Typeable1.stderr
+++ b/testsuite/tests/typecheck/should_run/Typeable1.stderr
@@ -1,7 +1,6 @@
 
 Typeable1.hs:22:5: error:
-    • Couldn't match kind ‘* -> (* -> *) -> (* -> *) -> * -> *’
-                     with ‘forall k. (* -> *) -> (k -> *) -> k -> *’
+    • Couldn't match type ‘ComposeK’ with ‘a3 b3’
       Inaccessible code in
         a pattern with pattern synonym:
           App :: forall k2 (t :: k2).