[Ur] Polymorphic variants and JSON

[Adam Chlipala]

Edward Z. Yang wrote:
> (And even that's not enough, since something like $(map json ts) 
> counts as a typeclass witness too--so what is a witness, anyway?)

Yes, records built by mapping over type classes are also witnesses. :)

> Yeah, here is the ambiguity thing, since there exists a destr2R but
> it doesn't have the right signature here.
>
> map2 is useful.  With it, I get here:
>
>      {ToJson = fn r =>  let val jsts = @map2 [json] [fn _ =>  string] [fn x =>  json x * string]
>                                       (fn [t] (js : json t) (t : string) =>  (js, t)) fl jss names
>                        in @Variant.destrR [ident] [fn x =>  json x * string]
>                            (fn [p] (v : p) (js : json p, t : string) =>  "something") fl r jsts
>                        end
>
> I can't get this to unify:
>
>      /home/ezyang/Dev/logitext/meta/json.ur:273:26-273:83: Unification failure
>      Expression:
>      fn p ::: Type =>
>       fn v : p =>
>        fn $x : {1 : json p, 2 : string} =>
>         case $x of {1 = js, 2 = t} =>  "something"
>        Have con:
>      p ::: Type ->
>       (p ->
>         ({1 :
>            {ToJson : (p ->  string),
>              FromJson : (string ->  {1 : p, 2 : string})}, 2 : Basis.string}
>           ->  Basis.string))
>        Need con:
>      p :: Type ->
>       (p ->
>         ({1 :
>            {ToJson : (p ->  string),
>              FromJson : (string ->  {1 : p, 2 : string})}, 2 : Basis.string}
>           ->  <UNIF:U1048::Type+1>))
>      Differing constructor function explicitness
>      Have:
>      p ::: Type ->
>       (p ->
>         ({1 :
>            {ToJson : (p ->  string),
>              FromJson : (string ->  {1 : p, 2 : string})}, 2 : Basis.string}
>           ->  Basis.string))
>      Need:
>      p :: Type ->
>       (p ->
>         ({1 :
>            {ToJson : (p ->  string),
>              FromJson : (string ->  {1 : p, 2 : string})}, 2 : Basis.string}
>           ->  <UNIF:U1048::Type+1>))

I think this error message is actually pretty good!  In the expression 
quoted, you need to change the binder of [p] to mark it as explicit, not 
implicit.  The easy way to do that is to change [[p]] to [[p ::_]] (note 
no space between [::] and [_]).