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