blob: 8a0c3d989fc04002012a3ad176733a6a7776e816 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
|
{-# LANGUAGE TypeApplications, ImpredicativeTypes, ScopedTypeVariables,
QuantifiedConstraints, StandaloneDeriving, GeneralizedNewtypeDeriving #-}
module T15290 where
import Prelude hiding ( Monad(..) )
import Data.Coerce ( Coercible, coerce )
class Monad m where
join :: m (m a) -> m a
newtype StateT s m a = StateT { runStateT :: s -> m (s, a) }
newtype IntStateT m a = IntStateT { runIntStateT :: StateT Int m a }
instance Monad m => Monad (StateT s m) where
join = error "urk"
instance (Monad m, forall p q. Coercible p q => Coercible (m p) (m q))
=> Monad (IntStateT m) where
-- Fails with the impredicative instantiation of coerce, succeeds without
-- Impredicative version (fails)
-- join = coerce
-- @(forall a. StateT Int m (StateT Int m a) -> StateT Int m a)
-- @(forall a. IntStateT m (IntStateT m a) -> IntStateT m a)
-- join
-- Predicative version (succeeds)
join = (coerce
@(StateT Int m (StateT Int m a) -> StateT Int m a)
@(IntStateT m (IntStateT m a) -> IntStateT m a)
join) :: forall a. IntStateT m (IntStateT m a) -> IntStateT m a
|
