Uninferrable type variable in type family

Hello everyone. I have this code (I use ghc-9.2.4)

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}

module Main where

import Data.Proxy
import Data.Kind
import Data.Type.Equality
import qualified GHC.TypeLits as TL
import qualified Data.Type.Bool as TB

type Undefined :: k
type family Undefined where {}

type LoT :: Type -> Type
data LoT k where
  LoT0 :: LoT Type
  (:&&:) :: k -> LoT ks -> LoT (k -> ks)

type HeadLoT :: forall k k'. LoT (k -> k') -> k
type family HeadLoT tys where
  HeadLoT (a ':&&: _) = a

type TailLoT :: forall k k'. LoT (k -> k') -> LoT k'
type family TailLoT tys where
  TailLoT (_ ':&&: as) = as

type (:@@:) :: forall k. k -> LoT k -> Type
type family f :@@: tys where
  f :@@: _  = f
  f :@@: as = f (HeadLoT as) :@@: TailLoT as

type (~>) :: forall k1 k2. k1 -> k2 -> Type
type (~>) f g = Proxy f -> Proxy g -> Type

type Eval :: forall as f g. (f ~> g) -> f :@@: as -> g :@@: as
type family Eval nat t

-- >>> :k Eval
-- Eval :: forall {k} (as :: LoT k) (f :: k) (g :: k).
--         (f ~> g) -> (f :@@: as) -> g :@@: as

type Exp_ :: forall k. k -> Type
type Exp_ a = () ~> a

type Eval_ :: forall k. Exp_ k -> k
type Eval_ (e :: Exp_ a) = Eval e '()

And I got this error

    • Uninferrable type variable (as0 :: LoT (*)) in
      the type synonym right-hand side: Eval @{*} @as0 @() @k e '()
    • In the type declaration for 'Eval_'
   |
   | type Eval_ (e :: Exp_ a) = Eval e '()

In ghc-8.10.7 it’s ok, and compile, but Eval has different kind

-- >>> :kind Eval
-- Eval :: forall k (as :: LoT k) (f :: k) (g :: k).
--         (f ~> g) -> (f :@@: as) -> g :@@: as