Weird problem involving untouchable type variables

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
2 messages Options
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Weird problem involving untouchable type variables

Wolfgang Jeltsch-2
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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: 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
<[hidden email]> 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
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Loading...