search

vehicle-lang / vehicle

A toolkit for enforcing logical specifications on neural networks
https://vehicle-lang.readthedocs.io/
Other
81 stars 7 forks source link

Improve error message for `incorrectTensorLength` test #863

Open MatthewDaggitt opened 3 days ago

MatthewDaggitt commented 3 days ago

Test: 

tensor : Vector Nat 2
tensor = [1]

We should be able to come up with a much better message than the current: 

Error in file 'incorrectTensorLength.vcl' at Line 2, Columns 10-11: unable to work out a valid type for the overloaded expression '[1]'.
          Type checking has deduced that it is of type:
            forallT {A} . Vector A 1 -> ?4 A
          but '[1]' has only the following valid types:
            forallT {A} . Vector A n -> List A
            forallT {A} . Vector A n -> (\ A -> Vector A n) A