Hi! My inquiry on the users mailing list about untouchable types did not get a reply. Maybe it is better to ask my question here. Today I encountered for the first time the notion of an untouchable type variable. I have no clue what this is supposed to mean. The error message that talked about a type variable being untouchable is unfounded in my opinion. 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. Apparently, c is not related to the type family F at all. Why does the type checker even introduce a type variable c0? All the best, Wolfgang