Bug or feature?

[Iavor Diatchki]

Hello,

I've encountered some odd behavior related to quantification and type families,
but I am not sure if it is a bug or by design.

Here is an example which works fine:

> {-# Language ExistentialQuantification, RankNTypes, TypeFamilies #-}
>
> data T a b = T a
>
> t :: T Bool a
> t = T True
>
> data Q1 = forall a. Q1 (forall b. T a b)
>
> q1 :: Q1
> q1 = Q1 t

Now, suppose we wanted to constraint the universally quantified type of
the field.  This also works fine:

> data Q2 = forall a. Q2 (forall b. (b ~ Int) => T a b)
>
> q2 :: Q2
> q2 = Q2 t

However, things break down if the restriction involves a type family:

> type family F a
>
> data Q3 = forall a. Q3 (forall b. (F b ~ Int) => T a b)
>
> q3 :: Q3
> q3 = Q3 t

This causes some complaints about *a*, resulting from checking ambiguity.
If we `AllowAmbiguousTypes`, then the definition of `Q3` is accepted, but
`q3` fails with a similar error, complaining that GHC cannot match `a`
with `Bool` because it is "untouchable".

This seems confusing---I would have thought that when we use the `Q3`
constructor we are providing the value for `a` (e.g., it is `Bool`),
so I am not sure why GHC is trying
to match anything.

Any ideas?

-Iavor