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

[Adam Chlipala]

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.

Here's the idiomatic way to do it:

(* --- *)

fun id [a] (x: a): a = x

type assertion = transaction xbody

datatype test = Test of assertion | TestList of list test

(* class *)
structure Testable : sig
     class testable
     val mkTestable : t ::: Type -> (t -> test) -> testable t
     val testIt : t ::: Type -> testable t -> t -> test
end = struct
     type testable t = t -> test
     fun mkTestable [t] (f : t -> test) = f
     fun testIt [t] (f : testable t) = f
end

open Testable

(* instances *)
val testable_test: testable test = mkTestable id

val testable_testList [t] (_: testable t): testable (list t) =
      let
           fun testIt' (t1: list t): test =
                TestList (List.mp testIt t1)
      in mkTestable testIt'
      end

(* --- *)

On 01/19/2015 08:05 AM, Gabriel Riba wrote:
> (* --- *)
>
> fun id [a] (x: a): a = x
>
> type assertion = transaction xbody
>
> datatype test = Test of assertion | TestList of (list test)
>
> (* class *)
> con testable t = {TestIt: t -> test}
> fun mkTestable [t] (f: t -> test): testable t = {TestIt = f}
> val testIt [t] (r: testable t): (t -> test) = r.TestIt
>
> (* instances *)
> val testable_test: testable test = mkTestable id
>
> val testable_testList [t] (_: testable t): testable (list t) =
>       let
>            fun testIt' (t1: list t): test =
>                 TestList (List.mp testIt t1)    (* line with error *)
>       in mkTestable testIt'
>       end
>
> (* --- *)