UlfNorell
commented
10 years ago From andreas....@gmail.com on November 11, 2013 15:40:24
Fixed. For a test case see fail/ Issue949 .
Tue Nov 12 00:38:33 CET 2013 Andreas Abel andreas.abel@ifi.lmu.de
- [ issue 951 ] Hidden function types cannot be printed as {A} -> B, only as {x : A} -> B.
Status: Fixed
Owner: andreas....@gmail.com
From andreas....@gmail.com on November 11, 2013 22:52:54
See test/fail/ Issue949 postulate S : Set F : {A : Set} → Set ok : F {A = S} err : F {B = S}
-- Function does not accept argument {B = _} -- when checking that {B = S} are valid arguments to a function of -- type {Set} → Set
The type {A : Set} → Set is printed incorrectly as {Set} → Set. This is not a valid Agda type. In this case, it quite obscures the error message.
Original issue: http://code.google.com/p/agda/issues/detail?id=951