Type Derivation going wrong

[Bart Bogaerts]

vocabulary V{
    type T isa int
    type Q isa int

    f(T):T
    f(Q):Q

}

theory T:V{
!c[T]: f(c)=c.



}

procedure main(){
    print(T)
}

Result:

Error: Could not derive the sort of variable c. At /home/bartb/Desktop/test.idp:11:2
Error: Could not derive the sorts of function f/1.
Possibly the sorts of its subterms are not subtypes of the sorts of the function's arguments? (e.g. missing isa declaration) At /home/bartb/Desktop/test.idp:11:8

While c was quantified explicitely

[Ingmar Dasseville]

say T = {1..2} Q = {2..3}

How should IDP know you mean ! c[T]: fT,T = c with the minimal model: f[T,T] 1->1 , 2 -> 2

or ! c[T]: fQ,Q = c with the minimal model f[Q,Q] 2->2

-- AFAIK, it is not possible to disambiguate between predicates when there is a possible intersection between the types, as you can mean to quantify over the intersection of the types by using or over a whole type.

[Ingmar Dasseville]

Als T en Q een mogelijke intersectie hebben is disambiguatie niet mogelijk