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 |