While writing the the dep-t package, I encountered what I think is a known limitation of the GHC inliner.
dep-t provides a small variation over ReaderT which I believe offers some advantages for performing “dependency injection”:
type DepT ::
((Type -> Type) -> Type) ->
(Type -> Type) ->
Type ->
Type
newtype DepT env m r = DepT {toReaderT :: ReaderT (env (DepT env m)) m r}
The difference with vanilla ReaderT is that DepT's environment is parameterized with DepT itself.
One function which makes sense to define for DepT is one that transforms an environment so that the functions inside it require a “bigger” environment:
zoomEnv ::
forall small big m a.
Monad m =>
-- | rank-2 map function that changes the environment's monad
( forall p q.
(forall x. p x -> q x) ->
small p ->
small q
) ->
-- | function that changes the environment
(forall t. big t -> small t) ->
small (DepT small m) ->
small (DepT big m)
But trying to compile the implementation of this function fails, as can be reproduced with this reduced example.
$ ghc -O1 Main.hs
[1 of 1] Compiling Main ( Main.hs, Main.o )
Simplifier ticks exhausted
When trying UnfoldingDone ds_s1ze
To increase the limit, use -fsimpl-tick-factor=N (default 100).
If you need to increase the limit substantially, please file a
bug report and indicate the factor you needed.
If GHC was unable to complete compilation even with a very large factor
(a thousand or more), please consult the "Known bugs or infelicities"
section in the Users Guide before filing a report. There are a
few situations unlikely to occur in practical programs for which
simplifier non-termination has been judged acceptable.
Well, I didn’t expect that! Let’s look in that “Known bugs and infelicities” section. It says that
GHC’s inliner can be persuaded into non-termination using the standard way to encode recursion via a data type:
data U = MkU (U -> Bool)
russel :: U -> Bool
russel u@(MkU p) = not $ p ux :: Bool
x = russel (MkU russel)We have never found another class of programs, other than this contrived one, that makes GHC diverge, and fixing the problem would impose an extra overhead on every compilation. So the bug remains un-fixed. There is more background in Secrets of the GHC inliner.
Is DepT an example of that contrived kind of program? I’m non 100% sure, but it looks like it. Because DepT takes an environment, and that environment contains other DepTs in “positive position”. So it’s not unlike data U = MkU (U -> Bool) … I guess there’s also a correspondence between russel and zoomEnv, but it’s less clear to me.
In any case, slapping a NOINLINE pragma onto zoomEnv makes the program compile.
Edit: I’ve opened a GHC issue.
