Agda ee45333 (recent master) mis-compiles this code:
open import Agda.Builtin.Float open import Agda.Builtin.Nat open import Agda.Builtin.Int open import Agda.Builtin.Maybe default-to-0 : Maybe Int → Nat default-to-0 (just (pos x)) = x default-to-0 _ = 0 x : Nat -- mis-compiled to a JS number x = default-to-0 (primFloatRound 1234.5) y : Nat y = x + x -- OK at JS load-time (number + number) z : Nat z = x + 4 -- crashes at JS load-time (number + BigInt)
The implementation is here:
primFloatRound : Float → Maybe Int {-# COMPILE JS primFloatRound = function(x) { x = agdaRTS._primFloatRound(x); if (x === null) { return z_jAgda_Agda_Builtin_Maybe["Maybe"]["nothing"]; } else { return z_jAgda_Agda_Builtin_Maybe["Maybe"]["just"](x); } }; exports._primFloatRound = function(x) { if (exports.primFloatIsNaN(x) || exports.primFloatIsInfinite(x)) { return null; } else { return Math.round(x); } };Math.round() returns a floating-point JS number, which never gets converted to the JS BigInt that the type of primFloatRound advertises.
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