Untouchable type variables

[Wolfgang Jeltsch]

Hi!

Today I encountered for the first time the notion of an “untouchable”
type variable. I have no clue what this is supposed to mean. A minimal
example that exposes my problem is the following:

> {-# 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

This results in the following error message from GHC 8.0.1:

> Untouchable.hs:9:6: error:
>     • Couldn't match type ‘c0’ with ‘c’
>         ‘c0’ is untouchable
>           inside the constraints: F a b
>           bound by the type signature for:
>                      f :: F a b => T b c0
>           at Untouchable.hs:9:6-37
>       ‘c’ is a rigid type variable bound by
>         the type signature for:
>           f :: forall a c. (forall b. F a b => T b c) -> a
>         at Untouchable.hs:9:6
>       Expected type: T b c0
>         Actual type: T b c
>     • In the ambiguity check for ‘f’
>       To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
>       In the type signature:
>         f :: (forall b. F a b => T b c) -> a

I have no idea what the problem is. The type of f looks fine to me. The
type variable c should be universally quantified at the outermost level.
Why does the type checker even introduce a type variable c0?

All the best,
Wolfgang