[PVS-Help] Typechecking problem

[Aditya Kanade <aditya@cse.iitb.ac.in>]

hi,

I'm getting a typechecking error where I atmost expect a
TCC. Following is the scenario:

T1[t:type+]:theory
begin
  t1:type = [# a: set[t], b:set[[(a),(a)]] #]
end T1

T2:theory
begin
  importing T1[list[real]]

  e:t1 = (# a := (: 1 :), b := (: (1,1) :) #)
end T2

The typechecking error is:

Incompatible types for (: (1, 1) :)
     Found: (list_adt[[real, real]].cons?)
  Expected: sets
                [[(singleton[(cons?[real])]((: 1 :))),
                  (singleton[(cons?[real])]((: 1 :)))]].set

Now, AFAIK, PVS should have applied the list2set conversion to 
the list (: (1,1) :). I think it does that for a := (: 1 :). If I
explicitly write list2set((: (1,1) :)), then it gives the same error,
this time for the list2set conversion!

At least conceptually, what I'm trying to do should work. Can anyone
please explain the problem? And any solution to this?

Regards,
Aditya.