Fix a TyVar bug in the flattener

A year ago I gave up on trying to rigorously separate TyVars
from TcTyVars, and instead allowed TyVars to appear rather more
freely in types examined by the constraint solver:

   commit 18d0bdd3848201882bae167e3b15fd797d217e93
   Author: Simon Peyton Jones <simonpj@microsoft.com>
   Date:   Wed Nov 23 16:00:00 2016 +0000

   Allow TyVars in TcTypes

See Note [TcTyVars in the typechecker] in TcType.

However, TcFlatten.flatten_tyvar1 turned out to treat
a TyVar specially, and implicitly assumed that it could
not have an equality constraint in the inert set.  Wrong!

This caused Trac #14450.  Fortunately it is easily fixed,
by deleting code.

6 files changed, 46 insertions, 7 deletions

diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs
index 3c44cde47f..c8479a6d06 100644
--- a/compiler/typecheck/TcFlatten.hs
+++ b/compiler/typecheck/TcFlatten.hs
@@ -1371,15 +1371,10 @@ flatten_tyvar1 :: TcTyVar -> FlatM FlattenTvResult
 -- See also the documentation for FlattenTvResult
 
 flatten_tyvar1 tv
-  | not (isTcTyVar tv)             -- Happens when flatten under a (forall a. ty)
-  = return FTRNotFollowed
-          -- So ty contains references to the non-TcTyVar a
-
-  | otherwise
   = do { mb_ty <- liftTcS $ isFilledMetaTyVar_maybe tv
-       ; role <- getRole
        ; case mb_ty of
            Just ty -> do { traceFlat "Following filled tyvar" (ppr tv <+> equals <+> ppr ty)
+                         ; role <- getRole
                          ; return (FTRFollowed ty (mkReflCo role ty)) } ;
            Nothing -> do { traceFlat "Unfilled tyvar" (ppr tv)
                          ; fr <- getFlavourRole
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index 5e1e4be99f..d781aec49c 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -294,6 +294,10 @@ reasons:
     solve any kind equalities in foo's signature.  So the solver
     may see free occurrences of 'k'.
 
+    See calls to tcExtendTyVarEnv for other places that ordinary
+    TyVars are bought into scope, and hence may show up in the types
+    and inds generated by TcHsType.
+
 It's convenient to simply treat these TyVars as skolem constants,
 which of course they are.  So
 
diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs
index 926db6e65b..0b2151b8e1 100644
--- a/compiler/typecheck/TcUnify.hs
+++ b/compiler/typecheck/TcUnify.hs
@@ -1814,7 +1814,7 @@ matchExpectedFunKind hs_ty = go
     go k | Just k' <- tcView k = go k'
 
     go k@(TyVarTy kvar)
-      | isTcTyVar kvar, isMetaTyVar kvar
+      | isMetaTyVar kvar
       = do { maybe_kind <- readMetaTyVar kvar
            ; case maybe_kind of
                 Indirect fun_kind -> go fun_kind
diff --git a/testsuite/tests/polykinds/T14450.hs b/testsuite/tests/polykinds/T14450.hs
new file mode 100644
index 0000000000..3b8f5b7e70
--- /dev/null
+++ b/testsuite/tests/polykinds/T14450.hs
@@ -0,0 +1,31 @@
+{-# Language KindSignatures, TypeOperators, PolyKinds, TypeOperators, ConstraintKinds, TypeFamilies, DataKinds, TypeInType, GADTs, AllowAmbiguousTypes, InstanceSigs #-}
+
+module T14450 where
+
+import Data.Kind
+
+data TyFun :: Type -> Type -> Type
+
+type a ~> b = TyFun a b -> Type
+
+type Cat ob = ob -> ob -> Type
+
+type SameKind (a :: k) (b :: k) = (() :: Constraint)
+
+type family Apply (f :: a ~> b) (x :: a) :: b where
+  Apply IddSym0 x = Idd x
+
+class Varpi (f :: i ~> j) where
+  type Dom (f :: i ~> j) :: Cat i
+  type Cod (f :: i ~> j) :: Cat j
+
+  varpa :: Dom f a a' -> Cod f (Apply f a) (Apply f a')
+
+type family Idd (a::k) :: k where
+  Idd (a::k) = a
+
+data IddSym0 :: k ~> k where
+  IddSym0KindInference :: IddSym0 l
+
+instance Varpi (IddSym0 :: k ~> k) where
+  type Dom (IddSym0 :: Type ~> Type) = (->)
diff --git a/testsuite/tests/polykinds/T14450.stderr b/testsuite/tests/polykinds/T14450.stderr
new file mode 100644
index 0000000000..c7caf04220
--- /dev/null
+++ b/testsuite/tests/polykinds/T14450.stderr
@@ -0,0 +1,8 @@
+
+T14450.hs:31:12: error:
+    • Expected kind ‘k ~> k’,
+        but ‘(IddSym0 :: Type ~> Type)’ has kind ‘* ~> *’
+    • In the first argument of ‘Dom’, namely
+        ‘(IddSym0 :: Type ~> Type)’
+      In the type instance declaration for ‘Dom’
+      In the instance declaration for ‘Varpi (IddSym0 :: k ~> k)’
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 66bd9b13df..73408e81d9 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -173,3 +173,4 @@ test('T14265', normal, compile_fail, [''])
 test('T13391', normal, compile_fail, [''])
 test('T13391a', normal, compile, [''])
 test('T14270', normal, compile, [''])
+test('T14450', normal, compile_fail, [''])