eqType, tcEqType, and foralls

See also

• https://gitlab.haskell.org/ghc/ghc/-/wikis/DH-Current-Status, and
• GHC proposal issue #558 "Apartness of visible and invisible forall".

The following program passes Core Lint on GHC 9.4 and earlier:

{-# LANGUAGE GHC2021 #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where

import Data.Kind

type Const :: a -> b -> a
type family Const x y where
  Const x _ = x

type F :: (forall (b :: Bool) -> Const Type b) -> Type
data F f

type G :: forall (b :: Bool) -> Type
data G b

type H :: Type
type family H where
  H = F G

But fails on GHC 9.6.1-alpha1:

$ ghc-9.6.0.20230111 Bug.hs -dcore-lint -fforce-recomp
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
*** Core Lint errors : in result of TcGblEnv axioms ***
Bug.hs:20:13: warning:
    From-kind of Cast differs from kind of enclosed type
    From-kind: forall (b :: Bool) -> *
    Kind of enclosed type: forall {b :: Bool}. *
    Actual enclosed type: G
    Coercion used in cast: forall (b :: <Bool>_N).
                           Sym (D:R:Const[0] <*>_N <Bool>_N <b>_N <*>_N)
    In the coercion axiom
      axiom D:R:H
        {H = F (G |> forall (b :: <Bool>_N).
                     Sym (D:R:Const[0] <*>_N <Bool>_N <b>_N <*>_N))
           -- Defined at Bug.hs:21:3}
    Substitution: <InScope = {}
                   IdSubst   = []
                   TvSubst   = []
                   CvSubst   = []>
*** Offending Program ***
axiom D:R:Const
  {forall {a} {b} {x :: a}.
     Const x _ = x_ahb -- Defined at Bug.hs:11:3}
axiom D:R:H
  {H = F (G |> forall (b :: <Bool>_N).
               Sym (D:R:Const[0] <*>_N <Bool>_N <b>_N <*>_N))
     -- Defined at Bug.hs:21:3}
*** End of Offense ***


<no location info>: error: 
Compilation had errors



<no location info>: error: ExitFailure 1