Am Sonntag, den 18.06.2017, 12:02 -0700 schrieb wren romano:
{-# LANGUAGE Rank2Types, TypeFamilies #-}
import GHC.Exts (Constraint)
type family F a b :: Constraint
data T b c = T
f :: (forall b . F a b => T b c) -> a f _ = undefined
FWIW, the error comes specifically from the fact that @F@ is a family. If you use a plain old type class, or if you use a type alias (via -XConstraintKinds) then it typechecks just fine. So it's something about how the arguments to @F@ are indices rather than parameters.
I have a few guesses about why the families don't work here, but I'm not finding any of them particularly convincing. Really, imo, @c@ should be held abstract within the type of the argument, since it's universally quantified from outside. Whatever @F a b@ evaluates to can't possibly have an impact on @c@. I'd file a bug report. If it's just an implementation defect, then the GHC devs will want to know. And if there's actually a type theoretic reason I missed, it'd be good to have that documented somewhere.
I already filed a bug report: https://ghc.haskell.org/trac/ghc/ticket/13655 In a comment, Simon says that this behavior is according to the rules. I am just not sure whether the rules have to be as they are. All the best, Wolfgang