Interaction between associated type families and quantified constraints

Question

Why is it that the following code:

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`

produces the error:

    • 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))

but the following seemingly trivial modification to 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

makes the compiler happy?

Shouldn't the two snippets be equivalent? All I'm doing is aliasing TheFamily t as some other temporary type variable using an equality constraint.

Ooze

does this answer your question #56471100 – Ladyship

@Li-yaoXia If there's an answer to my question in there, I can't see it. As far as I can tell the setting of the two problems is different, because I have a constraint-valued type family applied to a naked type parameter (with no type-valued type families involved), whereas in the other question they are using a standard class applied to the result of a type-valued type family. Maybe this is a red herring though, i don't really know. – Ooze

I see, yes, that seems like a different situation, though the take away ends up the same: quantified constraints and type families don't mix; some indirection is necessary. I think your specific question (explaining this behavior) can only be answered by someone who understands the implementation, so you're better off asking on the mailing lists or on GHC's issue tracker. – Ladyship

Please update your GHC: quantified constraints are a new feature and lots of fixes are being applied. The issue is actually just that forall x y. (TheFamily t x, TheFamily t y) => TheFamily t (t x y) isn't allowed in the first place, so it doesn't matter that it doesn't work properly. GHC 8.10.1 complains "Quantified predicate must have a class or type variable head". Your GHC seems to lack this check. I'm voting to close. – Aerology

Actually, it looks like 8.10.1 rejects foo with that error but accepts foo'. – Dividivi