Ex.hs

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE RankNTypes                #-}

data Ex = forall a. Ex a

type State i o a = i -> (a, o)

-- enforce independence of types i and a:
newtype Filt a = Filt { unFilt :: forall i. i -> (a, Ex) }

-- generate a copy to subject to Filt
dup :: State i o a -> (State i o a, State i Ex a)
dup m = (m, \i -> let (x, j) = m i in (x, Ex j))

x :: State i i ()
x = \i -> ((), i)

test1 :: State i i ()
test1 = let (a, b) = dup x
            _      = Filt b
        in a

y :: State i () i
y = \i -> (i, ())

--test2 = let (a, b) = dup y
--            _      = Filt b
--        in a
-- => rigid type variable error

-- but seems it's impossible to get the relevant pattern into a function
-- test m = let (a, b) = dup m
--             _      = Filt b
--         in a