Weird problem involving untouchable type variables
Wolfgang Jeltsch
g9ks157k at acme.softbase.org
Fri May 5 10:11:48 UTC 2017
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
More information about the ghc-devs
mailing list