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

_______________________________________________

Glasgow-haskell-users mailing list

[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users