[GHC] #15470: Record projections with ambiguous types

[GHC]

#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