Weird problem involving untouchable type variables

[Vladislav Zavialov]

I can reproduce this on GHC 8.2.1 and GHC HEAD as well.

This looks like a bug in the ambiguity checker. Disabling it with
-XAllowAmbiguousTypes, as GHC suggests, makes the error go away.
Report it on GHC Trac [1]. As a work-around you could enable
-XAllowAmbiguousTypes — it should be safe as it merely disables
ambiguity checking, which is not necessary to ensure well-typedness.

[1] https://ghc.haskell.org/trac/ghc/

On Fri, May 5, 2017 at 1:11 PM, Wolfgang Jeltsch
<g9ks157k at acme.softbase.org> wrote:
> 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
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs