Coherent Reader

coherent.hs

{-# LANGUAGE RankNTypes, ScopedTypeVariables, FlexibleContexts #-}

import Control.Monad.Reader
import Data.Reflection
import Data.Tagged
import Data.Proxy

f :: Reader String Int
f = do
  a <- ask
  return $ length a

-- coherent ask
ask' :: forall s a. Reifies s a => Tagged s a
ask' = unproxy reflect

-- coherent runReader
runReader' :: (forall s. Reifies s a => Tagged s x) -> a -> x
runReader' tx a = reify a (proxy tx)

f' :: Reifies s String => Tagged s Int
f' = do
  a <- ask'
  return $ length a

x :: Int
x = runReader f "Hello"

x' :: Int
x' = runReader' f' "Hello"