haskell - 关联类型族和量化约束之间的交互

Question

为什么是下面的代码：

class TheClass (t :: * -> * -> *)
  where
  type TheFamily t :: * -> Constraint

data Dict (c :: Constraint)
  where
  Dict :: c => Dict c

foo :: forall t a b.
  ( TheClass t
  , (forall x y. (TheFamily t x, TheFamily t y) => TheFamily t (t x y))
  , TheFamily t a
  , TheFamily t b
  ) => Dict (TheFamily t (t a b))
foo = Dict

-- NB: Only using `Dict` to assert that the relevant constraint is satisfied in the body of `foo`

产生错误：

    • Could not deduce: TheFamily t (t a b)
        arising from a use of ‘Dict’
      from the context: (TheClass t,
                         forall x y. (TheFamily t x, TheFamily t y) => TheFamily t (t x y),
                         TheFamily t a, TheFamily t b)
        bound by the type signature for:
                   foo :: forall (t :: * -> * -> *) a b.
                          (TheClass t,
                           forall x y. (TheFamily t x, TheFamily t y) => TheFamily t (t x y),
                           TheFamily t a, TheFamily t b) =>
                          Dict (TheFamily t (t a b))

但以下看似微不足道的修改foo：

foo' :: forall t a b temp.
  ( TheClass t
  , TheFamily t ~ temp
  , (forall x y. (temp x, temp y) => temp (t x y))
  , TheFamily t a
  , TheFamily t b
  ) => Dict (TheFamily t (t a b))
foo' = Dict

让编译器高兴？

这两个片段不应该是等价的吗？我所做的只是TheFamily t使用等式约束将别名作为其他一些临时类型变量。