This week Vlad and I created individual tickets for all remaining parts of GHC Proposal #425 “Invisible binders in type declarations”:
 #23501 “Wildcard binders in type declarations”
 #23502 “Kind inference for invisible binders in type declarations”
 #23515 “Type/data instances: require that the instantiation is determined by the LHS alone”
 #23512 “Type/data instances: require that variables on the RHS are mentioned on the LHS”

#23510 “Implement the
Wimplicitrhsquantification
warning”  #23514 “Remove arity inference in type declarations”
And immediately began to solve them resulting in the following merge requests:
 !10644 “Type/data instances: require that variables on the RHS are mentioned on the LHS”

!10638 “Implement the
Wimplicitrhsquantification
warning”  !10660 “Remove arity inference in type declarations”
One of those issues turned out to be more difficult to solve because it involves modifying the type checker (#23515). I’m currently in the process of debugging a compiler crash caused by my changes
No skolem info  we could not find the origin of the following variables
[(UnkSkol (please report this as a bug)
Call stack:
CallStack (from HasCallStack):
unkSkolAnon, called at compiler/GHC/Tc/Types/Origin.hs:315:42 in ghc9.7inplace:GHC.Tc.Types.Origin
unkSkol, called at compiler/GHC/Tc/Utils/TcType.hs:583:31 in ghc9.7inplace:GHC.Tc.Utils.TcType
vanillaSkolemTvUnk, called at compiler/GHC/Types/Var.hs:1094:56 in ghc9.7inplace:GHC.Types.Var,
[k3])]
This should not happen, please report it as a bug following the instructions at:
https://gitlab.haskell.org/ghc/ghc/wikis/reportabug
Here is a summary of the changes implemented in the submitted merge requests:

Type synonym definitions that rely on outermost kind signatures to bring variables into scope must be rewritten with
@k
binders:type T1 :: forall a . Maybe a type T1 = 'Nothing :: Maybe a  old type T1 @a = 'Nothing :: Maybe a  new
To help users identify the code that needs to change a new warning was implemented:
Wimplicitrhsquantification

Type and data family instances that rely on outermost kind signatures to bring variables into scope now require either an explicit
forall
or mentioning the variables on the lefthand side.The following example is now rejected with an outofscope error:
type family F1 a :: k type instance F1 Int = Any :: j > j
T23512a.hs:6:31: error: [GHC76037] Not in scope: type variable ‘j’ T23512a.hs:6:36: error: [GHC76037] Not in scope: type variable ‘j’
And here are the ways to fix it:
type family F2 a :: k type instance F2 @(j > j) Int = Any :: j > j type family F3 a :: k type instance forall j. F3 Int = Any :: j > j
Notably those are not
@k
binders, but ordinary type applications, so you don’t have to wait for 9.8 to fix such code. Because of this there is no warning. 
The subtle and fragile arity inference algorithm was removed. Now GHC infers the smallest possible arity making examples like this possible:
data T (f :: forall r . (TYPE r) > Type) = MkT (f Int) (f Int#) tcodeq :: T CodeQ tcodeq = MkT [5] [5#]
GHC used to reject this because it assigned
arity = 1
toCodeQ
based on its definition:type CodeQ :: TYPE r > Kind.Type type CodeQ = Code Q
The new simple approach assigns
arity = 0
to this type synonym. But it also means that the following code is now rejected:type F :: Type > forall k. Maybe k type family F x where F Int @Type = Just Bool F Int = Just Either
It can be fixed using
@k
binders:type family F x @k where
Finally, my fix for Wtermvariablecapture
was reviewed by Ryan (thank you!) and merged in commit b84a2900.
This work is funded by Serokell