有没有办法让这种类型的家庭成为主观的？

Question

以下类型系列

type family ListVariadic (as :: [Type]) (b :: Type) = (f :: Type) where  
  ListVariadic (a ': as) b = a -> ListVariadic as b
  ListVariadic '[]       b = b

显然不是单射的,例如ListVariadic '[] (a -> a) ~ ListVariadic '[a] a.
然而,使用injectivity帮助类型推断是非常方便的,我不打算使用ListVariadic其第二个参数作为函数类型.
我提出了两个解决方法,两者都非常令人不满意:

选项1:传递与ListVariadic(通过类型类)相反的左侧类型族.

type family Arguments (f :: Type) :: [Type] where
  Arguments (a -> b) = a ': Arguments b
  Arguments b        = '[]
type family Return (f :: Type) :: Type where
  Return (a -> b) = Return b
  Return b        = b

class    ( f ~ ListVariadic (Arguments f) (Return f) ) => VariadicIsInjective f where
instance ( f ~ ListVariadic (Arguments f) (Return f) ) => VariadicIsInjective f where

对我来说,这最终引入了太多的复杂性,不得不贯穿这些辅助类型类.

选项2.在可变参数类型系列的定义中,明确列出将要使用的所有非函数类型:

type family ListVariadic (as :: [Type]) (b :: Type) = (f :: Type) | f -> as b where  
  ListVariadic (a ': as) b = a -> ListVariadic as b
  ListVariadic '[] ()     = ()
  ListVariadic '[] Bool   = Bool
  ListVariadic '[] Word   = Word 
  ListVariadic '[] Int    = Int 
  ListVariadic '[] Float  = Float
  ListVariadic '[] Double = Double
  ... ... ...
  ListVariadic '[] (a,b) = (a,b)
  ListVariadic '[] (a,b,c) = (a,b,c)
  ... ... ...
  ListVariadic '[] [a] = [a]
  ... ... ...

然后可以使用注入性注释并按预期工作.它显然非常有限......并且最终仍然a ~ ListVariadic '[] a需要传递形式的约束.

---

我希望有一种方式来编写ListVariadic类型族(或实现相同目的的东西),表明它的第二个参数不是函数,并允许注入性注释.
我知道我遇到了麻烦,因为在提供的第一个定义中ListVariadic,第二个等式在右侧有一个裸型变量.在检查注入性时通常不允许这样做...但也许有一些聪明的技巧使用类型同义词可以解决这个问题？