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 |
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 |
Free forum by Nabble | Edit this page |