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
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
