Помогите пожалуйста понять принцип работы forall с type families.
Ниже минимальный пример неработающего кода, интересует метод foo.
Особенно интересует то, что обозначает явное задание сигнатуры для 
foob в методе foo, с одной стороны FooE неинъективно и соотв компилятор не может выбрать конкретное foob, с другой a и b внесены под forall что должно быть подсказкой копилятору.
Я так понимаю данное поведение зависит от следующего, FooE это функция из a b в элементы с kind *, соотвественно если на момент определения инстанса вместо FooE a b подставляется результат вычисления FooE a b, то получается то поведение, что мы видим (тип b финкирован результатом), а 'a' не определено.
Если же редуцирования (?) не происходит, то тогда инстанс должен быть выбран.
Соответсвенно вопросы:
1. правильны ли те предположения, что я написал выше
2. куда почитать, чтобы подтвердить их или опровергнуть
3. это баг или фича

--
да, я знаю, что с data families все будет работать.


{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}

class FooC a b where
  type FooE a b
  foob :: FooE a b -> b

foo :: forall a b . FooC a b => [FooE a b] -> b
foo = map (foob :: FooE a b -> b)

вывод:
3.hs:9:8:
    Could not deduce (FooE a0 b ~ FooE a b)
    from the context (FooC a b)
      bound by the type signature for foo :: FooC a b => [FooE a b] -> b
      at 3.hs:9:8-47
    NB: ‘FooE’ is a type function, and may not be injective
    The type variable ‘a0’ is ambiguous
    Expected type: [FooE a b] -> b
      Actual type: [FooE a0 b] -> b