Untouchable type variables

[Wolfgang Jeltsch]

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 at . 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