Recursive instances?

[yallop]

I'd like to write something analogous to the following Haskell code

{-# LANGUAGE RankNTypes #-}

class C a where
  f :: (forall b.C b => b -> b) -> a -> a

instance C a => C [a] where
  f g [] = []
  f g (x:xs) = g x : g xs

but I don't see how to make recursive instance resolution work. I suppose it should look something like this

module rec R:
sig
  module type C =
  sig
     type a
     val f : ((implicit B:R.C) -> B.a -> B.a) -> a -> a
  end
end = R
include R

implicit functor C_list(A:C) =
struct
  type a = A.a list
  let f (g : ((implicit B:C) -> B.a -> B.a)) = function
    [] -> []
  | x :: xs -> g x :: g xs
end

but that code doesn't work, of course, because C_list is not visible in the call g xs.

Is there some way to bring the implicit C_list instance into scope within its own body?

[yallop]

The workaround for this case is to use a non-recursive functor with a recursive module as the body:

implicit functor C_list(A:C) : C with type a = A.a list =
struct
  module rec S : C with type a = A.a list =
  struct
    type a = A.a list
    let f (g : ((implicit B:C) -> B.a -> B.a)) = 
      function
        [] -> []
      | x :: xs -> g (implicit A) x :: g (implicit S) xs
  end
  include S
end

[yallop]

A slightly lighter version, without explicitly-instantiated implicit arguments:

type f_arg = (implicit B:C) -> B.a -> B.a

implicit functor C_list(A:C) : C with type a = A.a list = struct
  module rec S : C with type a = A.a list = struct
    implicit module T = S
    type a = A.a list
    let f (g : f_arg) : a -> a = function
        [] -> []
      | x :: xs -> g x :: g xs
  end
  include S
end

[lpw25]

This is an interesting case. I hadn't really considered wanting to recursively use an instance within itself.

It seems that recursive functors should provide support for this, but recursive functors are very restricted in how they can be used -- you basically can't call them from within themselves. They are also not well specified. If recursive functors were improved/fixed then I think this example would just work naturally.

So I think that this example provides a use case and some motivation for fixing recursive functors, but that we shouldn't worry about it too much as part of the implicits work.