Hi!
Today I encountered for the first time the notion of an “untouchable”
type variable. I have no clue what this is supposed to mean. 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.
Why does the type checker even introduce a type variable c0?
All the best,
Wolfgang
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
