Weird problem involving untouchable type variables
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
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
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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
participants (2)
-
Vladislav Zavialov -
Wolfgang Jeltsch