eqType, tcEqType, and foralls
See also
* https://gitlab.haskell.org/ghc/ghc/-/wikis/DH-Current-Status, and
* [GHC proposal issue #558](https://github.com/ghc-proposals/ghc-proposals/issues/558) "Apartness of visible and invisible forall".
The following program passes Core Lint on GHC 9.4 and earlier:
```hs
{-# 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
```
issue