Use eqType, not tcEqType, in metavar kind check

Close #20356.

See addendum to Note [coreView vs tcView] in GHC.Core.Type
for the details.

Also killed old Note about metaTyVarUpdateOK, which has been
gone for some time.

test case: typecheck/should_fail/T20356

8 files changed, 61 insertions, 41 deletions

diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs
index f162ab6fd4..b2d12c7f35 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/compiler/GHC/Core/Type.hs
@@ -388,6 +388,31 @@ idea is to have roles in kind coercions, but that has yet to be implemented.
 See also "A Role for Dependent Types in Haskell", ICFP 2019, which describes
 how roles in kinds might work out.
 
+One annoying consequence of this inconsistency is that we can get ill-kinded
+updates to metavariables. #20356 is a case in point. Simplifying somewhat,
+we end up with
+  [W] (alpha :: Constraint)  ~  (Int :: Type)
+This is heterogeneous, so we produce
+  [W] co :: (Constraint ~ Type)
+and transform our original wanted to become
+  [W] alpha ~ Int |> sym co
+in accordance with Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Canonical.
+Our transformed wanted is now homogeneous (both sides have kind Constraint)
+and so we unify alpha := Int |> sym co.
+
+However, it's not so easy: when we build the cast (Int |> sym co), we actually
+just get Int back. This is because we forbid reflexive casts (invariant (EQ2) of
+Note [Respecting definitional equality] in GHC.Core.TyCo.Rep), and co looks
+reflexive: it relates Type and Constraint, even though these are considered
+identical in Core. Above, when we tried to say alpha := Int |> sym co, we
+really ended up doing alpha := Int -- even though alpha :: Constraint and
+Int :: Type have different kinds. Nothing has really gone wrong, though:
+we still emitted [W] co :: (Constraint ~ Type), which will be insoluble
+and lead to a decent error message. We simply need not to fall over at the
+moment of unification, because all will be OK in the end. We thus use the
+Core eqType, not the Haskell tcEqType, in the kind check for a meta-tyvar
+unification in GHC.Tc.Utils.TcMType.writeMetaTyVarRef.
+
 -}
 
 -- | Gives the typechecker view of a type. This unwraps synonyms but
diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index dd31ef586d..10a8953d29 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -4094,10 +4094,11 @@ more.  So I use a HACK:
   ordinary tuples we don't have the same limit as for constraint
   tuples (which need selectors and an associated class).
 
-* Because it is ill-kinded, it trips an assert in writeMetaTyVar,
-  so now I disable the assertion if we are writing a type of
-  kind Constraint.  (That seldom/never normally happens so we aren't
-  losing much.)
+* Because it is ill-kinded (unifying something of kind Constraint with
+  something of kind Type), it should trip an assert in writeMetaTyVarRef.
+  However, writeMetaTyVarRef uses eqType, not tcEqType, to avoid falling
+  over in this scenario (and another scenario, as detailed in
+  Note [coreView vs tcView] in GHC.Core.Type).
 
 Result works fine, but it may eventually bite us.
 
diff --git a/compiler/GHC/Tc/Solver/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs
index e49ead9824..e583861196 100644
--- a/compiler/GHC/Tc/Solver/Interact.hs
+++ b/compiler/GHC/Tc/Solver/Interact.hs
@@ -1573,7 +1573,7 @@ interactEq inerts workItem@(CEqCan { cc_lhs = lhs
 interactEq _ wi = pprPanic "interactEq" (ppr wi)
 
 ----------------------
--- We have a meta-tyvar on the left, and metaTyVarUpateOK has said "yes"
+-- We have a meta-tyvar on the left, and metaTyVarUpdateOK has said "yes"
 -- So try to solve by unifying.
 -- Three reasons why not:
 --    Skolem escape
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index a4769bc759..1a008bbff0 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -987,10 +987,10 @@ writeMetaTyVarRef tyvar ref ty
              zonked_ty_lvl  = tcTypeLevel zonked_ty
              level_check_ok  = not (zonked_ty_lvl `strictlyDeeperThan` tv_lvl)
              level_check_msg = ppr zonked_ty_lvl $$ ppr tv_lvl $$ ppr tyvar $$ ppr ty
-             kind_check_ok = tcIsConstraintKind zonked_tv_kind
-                          || tcEqKind zonked_ty_kind zonked_tv_kind
-             -- Hack alert! tcIsConstraintKind: see GHC.Tc.Gen.HsType
-             -- Note [Extra-constraint holes in partial type signatures]
+             kind_check_ok = zonked_ty_kind `eqType` zonked_tv_kind
+             -- Hack alert! eqType, not tcEqType. see:
+             -- Note [coreView vs tcView] in GHC.Core.Type
+             -- Note [Extra-constraint holes in partial type signatures] in GHC.Tc.Gen.HsType
 
              kind_msg = hang (text "Ill-kinded update to meta tyvar")
                            2 (    ppr tyvar <+> text "::" <+> (ppr tv_kind $$ ppr zonked_tv_kind)
diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs
index 7b8920f555..dc1fd382d2 100644
--- a/compiler/GHC/Tc/Utils/Unify.hs
+++ b/compiler/GHC/Tc/Utils/Unify.hs
@@ -1764,38 +1764,6 @@ better in practice.
 Revisited in Nov '20, along with removing flattening variables. Problem
 is still present, and the solution is still the same.
 
-Note [Refactoring hazard: metaTyVarUpdateOK]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-I (Richard E.) have a sad story about refactoring this code, retained here
-to prevent others (or a future me!) from falling into the same traps.
-
-It all started with #11407, which was caused by the fact that the TyVarTy
-case of defer_me didn't look in the kind. But it seemed reasonable to
-simply remove the defer_me check instead.
-
-It referred to two Notes (since removed) that were out of date, and the
-fast_check code in occurCheckExpand seemed to do just about the same thing as
-defer_me. The one piece that defer_me did that wasn't repeated by
-occurCheckExpand was the type-family check. (See Note [Prevent unification
-with type families].) So I checked the result of occurCheckExpand for any
-type family occurrences and deferred if there were any. This was done
-in commit e9bf7bb5cc9fb3f87dd05111aa23da76b86a8967 .
-
-This approach turned out not to be performant, because the expanded
-type was bigger than the original type, and tyConsOfType (needed to
-see if there are any type family occurrences) looks through type
-synonyms. So it then struck me that we could dispense with the
-defer_me check entirely. This simplified the code nicely, and it cut
-the allocations in T5030 by half. But, as documented in Note [Prevent
-unification with type families], this destroyed performance in
-T3064. Regardless, I missed this regression and the change was
-committed as 3f5d1a13f112f34d992f6b74656d64d95a3f506d .
-
-Bottom lines:
- * defer_me is back, but now fixed w.r.t. #11407.
- * Tread carefully before you start to refactor here. There can be
-   lots of hard-to-predict consequences.
-
 Note [Type synonyms and the occur check]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Generally speaking we try to update a variable with type synonyms not
diff --git a/testsuite/tests/typecheck/should_fail/T20356.hs b/testsuite/tests/typecheck/should_fail/T20356.hs
new file mode 100644
index 0000000000..6a847cb22a
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T20356.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE TypeFamilies, PolyKinds, ConstraintKinds #-}
+
+module T20356 where
+
+import GHC.Types
+
+type family Id (a :: k -> Constraint) :: l -> Constraint
+type instance Id f = f
+
+type T :: Constraint -> Constraint
+type T = Id Eq
+
+data Proxy p = MkProxy
+
+id' :: f a -> f a
+id' x = x
+
+z = id' (MkProxy @T)
diff --git a/testsuite/tests/typecheck/should_fail/T20356.stderr b/testsuite/tests/typecheck/should_fail/T20356.stderr
new file mode 100644
index 0000000000..476b71a385
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T20356.stderr
@@ -0,0 +1,7 @@
+
+T20356.hs:18:10: error:
+    • Couldn't match kind ‘*’ with ‘Constraint’
+      When matching the kind of ‘Eq’
+    • In the first argument of ‘id'’, namely ‘(MkProxy @T)’
+      In the expression: id' (MkProxy @T)
+      In an equation for ‘z’: z = id' (MkProxy @T)
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 1d308d7529..20b30d3deb 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -617,6 +617,7 @@ test('TyAppPat_ScopedTyVarConflict', normal, compile_fail, [''])
 test('TyAppPat_TooMany', normal, compile_fail, [''])
 test('T12178a', normal, compile_fail, [''])
 test('T18869', normal, compile_fail, [''])
+test('T20356', normal, compile_fail, [''])
 test('T19142', normal, compile_fail, [''])
 test('T19346', normal, compile_fail, ['-fprint-typechecker-elaboration'])
 test('T19364', normal, compile_fail, [''])