Better error message for misspelled name in hidden argument application

[UlfNorell]

From andreas....@gmail.com on November 08, 2013 22:49:09

postulate S : Set F : {A : Set} → Set ok : F {A = S} err : F {B = S}

-- Error message could be clearer:

-- Set should be a function type, but it isn't -- when checking that {B = S} are valid arguments to a function of -- type Set

Error message could be instead

F does not take a hidden argument with name B when checking...

Original issue: http://code.google.com/p/agda/issues/detail?id=949

[UlfNorell]

From andreas....@gmail.com on November 11, 2013 13:49:19

Mon Nov 11 22:47:01 CET 2013 Andreas Abel andreas.abel@ifi.lmu.de

• [ issue 949 ] Better error message for wrong named argument. Refactored checkArguments to make that work.

-- New error:

-- Function does not accept argument {B = _} -- when checking that {B = S} are valid arguments to a function of -- type {Set} → Set

Status: Fixed