Add a missing zonk (fixes #16902)

In the eager unifier, when unifying (tv1 ~ tv2),
when we decide to swap them over, to unify (tv2 ~ tv1),
I'd forgotten to ensure that tv1's kind was fully zonked,
which is an invariant of uUnfilledTyVar2.

That could lead us to build an infinite kind, or (in the
case of #16902) update the same unification variable twice.

Yikes.

Now we get an error message rather than non-termination,
which is much better.  The error message is not great,
but it's a very strange program, and I can't see an easy way
to improve it, so for now I'm just committing this fix.

Here's the decl
 data F (a :: k) :: (a ~~ k) => Type where
    MkF :: F a

and the rather error message of which I am not proud

  T16902.hs:11:10: error:
    • Expected a type, but found something with kind ‘a1’
    • In the type ‘F a’

compiler/typecheck/TcUnify.hs

@@ -1388,7 +1388,7 @@ uType t_or_k origin orig_ty1 orig_ty2
       = do { co_tys <- uType t_or_k origin t1 t2
            ; return (mkCoherenceRightCo Nominal t2 co2 co_tys) }
 
-        -- Variables; go for uVar
+        -- Variables; go for uUnfilledVar
         -- Note that we pass in *original* (before synonym expansion),
         -- so that type variables tend to get filled in with
         -- the most informative version of the type
@@ -1576,11 +1576,11 @@ improve error messages.
 
 ************************************************************************
 *                                                                      *
-                 uVar and friends
+                 uUnfilledVar and friends
 *                                                                      *
 ************************************************************************
 
-@uVar@ is called when at least one of the types being unified is a
+@uunfilledVar@ is called when at least one of the types being unified is a
 variable.  It does {\em not} assume that the variable is a fixed point
 of the substitution; rather, notice that @uVar@ (defined below) nips
 back into @uTys@ if it turns out that the variable is already bound.
@@ -1590,7 +1590,8 @@ back into @uTys@ if it turns out that the variable is already bound.
 uUnfilledVar :: CtOrigin
              -> TypeOrKind
              -> SwapFlag
-             -> TcTyVar        -- Tyvar 1
+             -> TcTyVar        -- Tyvar 1: not necessarily a meta-tyvar
+                               --    definitely not a /filled/ meta-tyvar
              -> TcTauType      -- Type 2
              -> TcM Coercion
 -- "Unfilled" means that the variable is definitely not a filled-in meta tyvar
@@ -1608,7 +1609,8 @@ uUnfilledVar origin t_or_k swapped tv1 ty2
 uUnfilledVar1 :: CtOrigin
               -> TypeOrKind
               -> SwapFlag
-              -> TcTyVar        -- Tyvar 1
+              -> TcTyVar        -- Tyvar 1: not necessarily a meta-tyvar
+                                --    definitely not a /filled/ meta-tyvar
               -> TcTauType      -- Type 2, zonked
               -> TcM Coercion
 uUnfilledVar1 origin t_or_k swapped tv1 ty2
@@ -1621,12 +1623,19 @@ uUnfilledVar1 origin t_or_k swapped tv1 ty2
   where
     -- 'go' handles the case where both are
     -- tyvars so we might want to swap
+    -- E.g. maybe tv2 is a meta-tyvar and tv1 is not
     go tv2 | tv1 == tv2  -- Same type variable => no-op
            = return (mkNomReflCo (mkTyVarTy tv1))
 
            | swapOverTyVars tv1 tv2   -- Distinct type variables
-           = uUnfilledVar2 origin t_or_k (flipSwap swapped)
-                           tv2 (mkTyVarTy tv1)
+               -- Swap meta tyvar to the left if poss
+           = do { tv1 <- zonkTyCoVarKind tv1
+                     -- We must zonk tv1's kind because that might
+                     -- not have happened yet, and it's an invariant of
+                     -- uUnfilledTyVar2 that ty2 is fully zonked
+                     -- Omitting this caused #16902
+                ; uUnfilledVar2 origin t_or_k (flipSwap swapped)
+                           tv2 (mkTyVarTy tv1) }
 
            | otherwise
            = uUnfilledVar2 origin t_or_k swapped tv1 ty2
@@ -1635,7 +1644,8 @@ uUnfilledVar1 origin t_or_k swapped tv1 ty2
 uUnfilledVar2 :: CtOrigin
               -> TypeOrKind
               -> SwapFlag
-              -> TcTyVar        -- Tyvar 1
+              -> TcTyVar        -- Tyvar 1: not necessarily a meta-tyvar
+                                --    definitely not a /filled/ meta-tyvar
               -> TcTauType      -- Type 2, zonked
               -> TcM Coercion
 uUnfilledVar2 origin t_or_k swapped tv1 ty2
@@ -1652,8 +1662,10 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2
                   , ppr ty2 <+> dcolon <+> ppr (tcTypeKind  ty2)
                   , ppr (isTcReflCo co_k), ppr co_k ]
 
-           ; if isTcReflCo co_k  -- only proceed if the kinds matched.
-
+           ; if isTcReflCo co_k
+               -- Only proceed if the kinds match
+               -- NB: tv1 should still be unfilled, despite the kind unification
+               --     because tv1 is not free in ty2 (or, hence, in its kind)
              then do { writeMetaTyVar tv1 ty2'
                      ; return (mkTcNomReflCo ty2') }
 

testsuite/tests/polykinds/T16902.hs

+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeOperators #-}
+module Bug where
+
+import Data.Kind
+import Data.Type.Equality
+
+data F (a :: k) :: (a ~~ k) => Type where
+  MkF :: F a

testsuite/tests/polykinds/T16902.stderr

+
+T16902.hs:11:10: error:
+    • Expected a type, but found something with kind ‘a1’
+    • In the type ‘F a’
+      In the definition of data constructor ‘MkF’
+      In the data declaration for ‘F’

testsuite/tests/polykinds/all.T

@@ -211,3 +211,4 @@ test('T16221', normal, compile, [''])
 test('T16221a', normal, compile_fail, [''])
 test('T16342', normal, compile, [''])
 test('T16263', normal, compile_fail, [''])
+test('T16902', normal, compile_fail, [''])