[Ur] function and signature

[Gergely Buday]

> I have a function that returns
>
>         Basis.list
>                 $(<UNIF:U16369::{Type}> ++
>                    [#Here = myType,
>                      #There = myType])
>
> according to the type checker. How can I express its signature so that it
> compiles? Is it possible to express that I have these two fixed fields and
> some others?

My trial is

val computeRecordz: r ::: {Type} -> [ r ~ [Here] ] -> [ r ~ [There] ] ->  ...
                          -> Basis.list {1 : Basis.bool, 2 :
Basis.list $( r ++ [Here = myType, There = myType]) }

but it invokes some syntax error messages. What is wrong with this?

- Gergely