Might you have more success with a Reynolds style defunctionalization pass
for the polymorphic recursion you can't eliminate?
Then you wouldn't have to rule out things like
data Complete a = S (Complete (a,a)) | Z a
which don't pass that test.
-Edward
On Thu, Jun 19, 2014 at 3:28 PM, Conal
Thanks, Ed. It hadn't occurred to me that defunctionalization might be
useful for monomorphization. Do you know of a connection?
I'm using a perfect leaf tree type similar to the one you mentioned but
indexed by depth:
data Tree :: (* - *) - Nat - * - * where
L :: a - Tree k 0 a
B :: Tree
I think the first time I saw a connection to polymorphic recursion was in
Neil Mitchell's supero, which used it as a catch-all fallback plan.
http://community.haskell.org/~ndm/downloads/slides-haskell_with_go_faster_stripes-30_nov_2006.pdf
-Edward
On Thu, Jun 19, 2014 at 4:49 PM, Conal Elliott