Record projections with ambiguous types

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

Trac metadata

Trac field	Value
Version	8.4.3
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture