Explicit type not correctly handled

[GoogleCodeExporter]

The following query succeeds whereas it should not.
(X : int -> A) = (Z : int -> A) 3.

Notice that if you replace A by a constant then it correctly fails.

Fabien

Original issue reported on code.google.com by fafounet@gmail.com on 1 Feb 2013 at 4:05

[GoogleCodeExporter]

I guess that this is the same problem causing the following behavior:
?- (X : A -> int) (Z : A -> int).
Error: expecting query term of type: o
    encountered term: X Z
    of type: int

However, I am not sure what kind of message I would like to read.

Original comment by fafounet@gmail.com on 1 Feb 2013 at 4:30

[GoogleCodeExporter]

I think this example illustrates a bug in Teyjus's treatment of type variables. 
 I believe that in the query
    (X : int -> A) = (Z : int -> A) 3.
all occurrences of the A type variable should be the same.  If X occurred 
twice, we would have two occurrences of the *same* variable.  What seems to be 
happening in with query is that the two occurrences to A are treated as two 
occurrences to *different* variables.

If you want to have different variables, you could simply write 
    (X : int -> A) = (Z : int -> B) 3.
instead.  Notice that the same thing happens when we compile clauses.  For 
example, a module containing 

test :- (X : int -> A) = (Z : int -> A) 3.

compiles and executes (it should generate a typing error instead).

  -Dale

Original comment by dale.a.m...@gmail.com on 7 Feb 2013 at 4:33

[GoogleCodeExporter]

[deleted comment]

[GoogleCodeExporter]

All occurrences of a variable in a query are now the same.

Fixed by commit 1123

Original comment by fafounet@gmail.com on 21 Aug 2013 at 8:29

• Changed state: Fixed