具有GADT的内射型家族

Question

我尝试了一个涉及内射型家庭的非常简单的例子,但我不能让它起作用.

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilyDependencies #-}

type family F c = result | result -> c

data G b where
  G :: G b -> G (F b)

foo :: G (F a) -> G a
foo (G a) = a

这会导致编译错误

Inject.hs:10:13: error:
    • Could not deduce: b ~ a
      from the context: F a ~ F b
        bound by a pattern with constructor: G :: forall b. G b -> G (F b),
                 in an equation for ‘foo’
        at Inject.hs:10:6-8
      ‘b’ is a rigid type variable bound by
        a pattern with constructor: G :: forall b. G b -> G (F b),
        in an equation for ‘foo’
        at Inject.hs:10:6
      ‘a’ is a rigid type variable bound by
        the type signature for:
          foo :: forall a. G (F a) -> G a
        at Inject.hs:9:8
      Expected type: G a
        Actual type: G b
    • In the expression: a
      In an equation for ‘foo’: foo (G a) = a
    • Relevant bindings include
        a :: G b (bound at Inject.hs:10:8)
        foo :: G (F a) -> G a (bound at Inject.hs:10:1)

如果我使用非内射/普通类型的家庭,这是同样的错误F.是什么赋予了？