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