
#13655: Spurious untouchable type variable in connection with rank-2 type and constraint family -------------------------------------+------------------------------------- Reporter: jeltsch | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1-rc2 (Type checker) | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- The following code cannot be compiled: {{{#!hs {-# LANGUAGE ConstraintKinds, 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 }}} GHC outputs the following error message: {{{ 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 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13655 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler