Reported by @plt-amy in #7156 (comment)
open import Agda.Builtin.Nat
record T : Set where
field
f : Nat → Nat
foo : T
foo .T.f = suc
test : Nat
test = foo 123
Agda 2.5.3 said (good):
T should be a function type, but it isn't
when checking that 123 is a valid argument to a function of type T
Since 2.5.4 Agda says (bad):
T !=< Nat of type Set
when checking that the inferred type of an application
T
matches the expected type
Nat
@plt-amy wrote:
I suspect that this would be fixable by checking that length tel >= sArgsLen in Application.hs.
It seems that telViewUpTo' here is not sufficient, correct would be a "telViewExactly" that asks for exactly sArgsLen visible arguments:
So, yes, we need to check
length tel >= sArgsLen
otherwise the target type is bogus and checking it is moot.
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4