#15470: Record projections with ambiguous types -------------------------------------+------------------------------------- Reporter: sweirich | Owner: (none) Type: feature | Status: new request | Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- The following code fails {{{ {-# LANGUAGE DataKinds, KindSignatures, PolyKinds, TypeFamilies, RankNTypes, AllowAmbiguousTypes #-} module TypeLambda where data Fun a b type family App (f :: Fun t k) (x :: t) :: k data MONAD m = MONAD { return :: forall a. a -> App m a , (>>=) :: forall a b. App m a -> (a -> App m b) -> App m b } }}} with the error message {{{ TypeLambda.hs:12:5: error: • Couldn't match type ‘App m b0’ with ‘App m b’ Expected type: App m a -> (a -> App m b) -> App m b Actual type: App m a -> (a -> App m b0) -> App m b0 NB: ‘App’ is a non-injective type family The type variable ‘b0’ is ambiguous • In the expression: (>>=) In an equation for ‘TypeLambda.>>=’: (TypeLambda.>>=) MONAD {>>= = (>>=)} = (>>=) • Relevant bindings include (>>=) :: forall a b. App m a -> (a -> App m b) -> App m b (bound at TypeLambda.hs:12:5) | 12 | , (>>=) :: forall a b. App m a -> (a -> App m b) -> App m b | ^^^^^ Failed, no modules loaded. }}} However, with ScopedTypeVariables and TypeApplications, it is possible to define the projections: {{{ data MONAD2 m = MONAD2 (forall a. a -> App m a) (forall a b. App m a -> (a -> App m b) -> App m b) bind :: forall b a m. MONAD2 m -> App m a -> (a -> App m b) -> App m b bind (MONAD2 _ b) = b @a @b }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15470 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler