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

[Gabriel Riba]

Hi!

Here is the code:

(* --- *)

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

(* --- *)

It looks like testIt in the error line does not get the implicit:


urweb prova_testable
/home/gabi64/lleng/ur/dlist/proves/prova_testable.ur:17:40: (to 17:42)
Unification failure
Expression:  t1
  Have con:  list t
  Need con:  list {TestIt : <UNIF:K::Type> -> test}
Incompatible constructors
Have:  t
Need:  {TestIt : <UNIF:K::Type> -> test}
/home/gabi64/lleng/ur/dlist/proves/prova_testable.ur:17:24: (to 17:43)
Unification failure
Expression: 
List.mp [{TestIt : <UNIF:K::Type> -> test}] [<UNIF:K::Type> -> test]
 (testIt [<UNIF:K::Type>]) t1
  Have con:  list (<UNIF:K::Type> -> test)
  Need con:  list test
Incompatible constructors
Have:  <UNIF:K::Type> -> test
Need:  test