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.