Quantified constraint should be accepted in RHS of type family equation

This is rejected, but it shouldn't be:

{-# LANGUAGE QuantifiedConstraints, DataKinds, TypeFamilies #-}

module Bug4 where

import Data.Kind

newtype Phant p = MkPhant Int
  deriving Eq

f1 :: forall p. (forall x. Eq (p x)) => p Char -> p Double -> Bool
f1 p1 p2 = p1 == p1 && p2 == p2

type ForallEq p = forall x. Eq (p x)

f2 :: ForallEq p => p Char -> p Double -> Bool
f2 p1 p2 = p1 == p1 && p2 == p2

type ForallEqs :: [Type -> Type] -> Constraint
type family ForallEqs ps where
  ForallEqs '[] = ()
  ForallEqs (p : ps) = (ForallEq p, ForallEqs ps)

The forall in a quantified constraint is really a different forall than the one used in normal types, and it should be acceptable in the RHS of a type family equation.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information