[Ur] Implicit problem in typeclass recursive instance [testable t] -> testable (list t)

[Gabriel Riba]

Adam Chlipala <adamc <at> csail.mit.edu> writes:

> 
> It's not surprising that type-class resolution is not triggering 
> automatically in your code, because the keyword [class] doesn't appear 
> anywhere in the program!  That is, you are not declaring any particular 
> type class as existing, and the [testable] argument to 
> [testable_testList] won't be marked as generated automatically.
> 

In fact I declared it as "class" in my interface file (not shown) and the
lesson is that I cannot derive instances in the same class implementation
module (or structure in sml jargon).

I have another question about free type variables of class methods. I can
make them work by bringing them to class parameters.

(* Foldable *)

structure Foldable : sig
    class foldable :: (Type -> Type) -> Type -> Type -> Type
    val mkFoldable : t ::: (Type -> Type) -> a ::: Type -> b ::: Type ->  
                     ((a -> b -> b) -> b -> t a -> b) -> foldable t a b
    val foldr : t ::: (Type -> Type) -> a ::: Type -> b ::: Type -> 
                foldable t a b -> (a -> b -> b) -> b -> t a -> b
end = struct
    type foldable t = fn a b => (a -> b -> b) -> b -> t a -> b
    fun mkFoldable [t][a][b](f: (a -> b -> b) -> b -> t a -> b) = f
    val foldr [t][a][b] (f: foldable t a b): (a -> b -> b) -> b ->
                                             t a -> b = f
end

open Foldable

val foldable_list [a][b]: foldable list a b = mkFoldable List.foldr

(* --- *)

Is there a way to define the free type variables of methods existentially or
should I stick to the previous design?

(* --- *)

type foldable t = a :::Type -> b:::Type -> (a -> b -> b) -> b -> t a -> b

(* --- *)

I didn't succeed with it.

Thanks in advance.