Assertion in "asmcomp/cmmgen.ml"

[xekoukou]

The below file triggers an assertion in 4.07.0 OCaml.

https://github.com/ocaml/ocaml/blob/4.07/asmcomp/cmmgen.ml#L1983

I was trying to add Float support.

One weird thing that I noticed was that this was acceptable :

  ( $agdaIdent8.952a3c475e16a2d6.Common.IO.return
    (global $ForeignCode $Common $IO $ioReturn)
  )

while this was not :

  ( $agdaIdent2a.2ed69e510f00fd1e.Agda.Builtin.Float.primSin
    (global $Stdlib $Float $sin)
  )

( module
  ( $agdaIdenta.2ed69e510f00fd1e.Agda.Builtin.Float.primFloatEquality
    ( lambda ($a $b) ( ==.f64 $a $b ) )
  )
  ( $agdaIdentc.2ed69e510f00fd1e.Agda.Builtin.Float.primFloatLess
    ( lambda ($a $b) ( <.f64 $a $b ) )
  )
  ( $agdaIdente.2ed69e510f00fd1e.Agda.Builtin.Float.primFloatNumericalEquality
    ( lambda ($a $b) ( ==.f64 $a $b ) )
  )
  ( $agdaIdent10.2ed69e510f00fd1e.Agda.Builtin.Float.primFloatNumericalLess
    ( lambda ($a $b) ( <.f64 $a $b ) )
  )
  ( $agdaIdent1a.2ed69e510f00fd1e.Agda.Builtin.Float.primFloatNegate
    ( lambda ($a) ( neg.f64 $a ) )
  )
  ( $agdaIdent1c.2ed69e510f00fd1e.Agda.Builtin.Float.primFloatDiv
    ( lambda ($a $b) ( /.f64 $a $b ) )
  )
  ( $agdaIdent26.2ed69e510f00fd1e.Agda.Builtin.Float.primExp
    ( lambda ($a) ( apply (global $Stdlib $Float $exp) $a ) )
  )
  ( $agdaIdent2a.2ed69e510f00fd1e.Agda.Builtin.Float.primSin
    ( lambda ($a) ( apply (global $Stdlib $Float $sin) $a ) )
  )
  ( $agdaIdent2c.2ed69e510f00fd1e.Agda.Builtin.Float.primCos
    ( lambda ($a) ( apply (global $Stdlib $Float $cos) $a ) )
  )
  ( $agdaIdent2e.2ed69e510f00fd1e.Agda.Builtin.Float.primTan
    ( lambda ($a) ( apply (global $Stdlib $Float $tan) $a ) )
  )
  ( $agdaIdent30.2ed69e510f00fd1e.Agda.Builtin.Float.primASin
    ( lambda ($a) ( apply (global $Stdlib $Float $asin) $a ) )
  )
  ( $agdaIdent32.2ed69e510f00fd1e.Agda.Builtin.Float.primACos
    ( lambda ($a) ( apply (global $Stdlib $Float $acos) $a ) )
  )
  ( $agdaIdent34.2ed69e510f00fd1e.Agda.Builtin.Float.primATan
    ( lambda ($a) ( apply (global $Stdlib $Float $atan) $a ) )
  )
  ( $agdaIdent36.2ed69e510f00fd1e.Agda.Builtin.Float.primATan2
    ( lambda ($a) ( apply (global $Stdlib $Float $atan2) $a ) )
  )
  ( $agdaIdent38.2ed69e510f00fd1e.Agda.Builtin.Float.primShowFloat
    ( lambda ($a) ( apply (global $Stdlib $Float $to_string) $a ) )
  )
  ( $agdaIdent8.952a3c475e16a2d6.Common.IO.return
    (global $ForeignCode $Common $IO $ioReturn)
  )
  ( $agdaIdent12.952a3c475e16a2d6.Common.IO._{62}{62}{61}_
    (global $ForeignCode $Common $IO $ioBind)
  )
  ( $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
    (global $ForeignCode $Common $IO $printString)
  )
  ( $agdaIdent50.952a3c475e16a2d6.Common.IO.then
    ( lambda ($v0 $v1 $v2 $v3 $v4 $v5 $world)
      ( apply ( apply $agdaIdent12.952a3c475e16a2d6.Common.IO._{62}{62}{61}_
                $v0
                $v1
                0
                0
                $v4
                ( lambda ($v6) $v5 )
              )
        $world
      )
    )
  )
  ( $agdaIdent28.d2c4f4e5116ac5f5.Floats.isZero
    ( lambda ($v0)
      ( switch $v0
        ( _ (tag _)
          ( switch ( ==.f64 $v0 0.0 ) ( 1 "pos" ) ( _ (tag _) "nonzero" ) )
        )
      )
    )
  )
  ( $agdaIdent26.d2c4f4e5116ac5f5.Floats.atan2
    $agdaIdent36.2ed69e510f00fd1e.Agda.Builtin.Float.primATan2
  )
  ( $agdaIdent24.d2c4f4e5116ac5f5.Floats.atan
    $agdaIdent34.2ed69e510f00fd1e.Agda.Builtin.Float.primATan
  )
  ( $agdaIdent22.d2c4f4e5116ac5f5.Floats.acos
    $agdaIdent32.2ed69e510f00fd1e.Agda.Builtin.Float.primACos
  )
  ( $agdaIdent20.d2c4f4e5116ac5f5.Floats.asin
    $agdaIdent30.2ed69e510f00fd1e.Agda.Builtin.Float.primASin
  )
  ( $agdaIdent1e.d2c4f4e5116ac5f5.Floats.tan
    $agdaIdent2e.2ed69e510f00fd1e.Agda.Builtin.Float.primTan
  )
  ( $agdaIdent1c.d2c4f4e5116ac5f5.Floats.cos
    $agdaIdent2c.2ed69e510f00fd1e.Agda.Builtin.Float.primCos
  )
  ( $agdaIdent1a.d2c4f4e5116ac5f5.Floats.sin
    $agdaIdent2a.2ed69e510f00fd1e.Agda.Builtin.Float.primSin
  )
  ( $agdaIdent1a.952a3c475e16a2d6.Common.IO.putStrLn
    ( lambda ($v0 $world)
      ( apply ( apply $agdaIdent12.952a3c475e16a2d6.Common.IO._{62}{62}{61}_
                0
                0
                0
                0
                ( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr $v0 )
                ( lambda ($v1)
                  ( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr "\n" )
                )
              )
        $world
      )
    )
  )
  ( $agdaIdent10.d2c4f4e5116ac5f5.Floats._{60}_
    $agdaIdentc.2ed69e510f00fd1e.Agda.Builtin.Float.primFloatLess
  )
  ( $agdaIdente.d2c4f4e5116ac5f5.Floats._{60}N_
    $agdaIdent10.2ed69e510f00fd1e.Agda.Builtin.Float.primFloatNumericalLess
  )
  ( $agdaIdentc.d2c4f4e5116ac5f5.Floats._{61}N{61}_
    $agdaIdente.2ed69e510f00fd1e.Agda.Builtin.Float.primFloatNumericalEquality
  )
  ( $agdaIdenta.d2c4f4e5116ac5f5.Floats._{61}{61}_
    $agdaIdenta.2ed69e510f00fd1e.Agda.Builtin.Float.primFloatEquality
  )
  ( $agdaIdent8.d2c4f4e5116ac5f5.Floats._{47}_
    $agdaIdent1c.2ed69e510f00fd1e.Agda.Builtin.Float.primFloatDiv
  )
  ( $agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
    ( apply $agdaIdent8.d2c4f4e5116ac5f5.Floats._{47}_ 0.0 0.0 )
  )
  ( $agdaIdent14.d2c4f4e5116ac5f5.Floats.{45}NaN
    ( apply $agdaIdent1a.2ed69e510f00fd1e.Agda.Builtin.Float.primFloatNegate
      $agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
    )
  )
  ( $agdaIdent16.d2c4f4e5116ac5f5.Floats.Inf
    ( apply $agdaIdent8.d2c4f4e5116ac5f5.Floats._{47}_ 1.0 0.0 )
  )
  ( $agdaIdent18.d2c4f4e5116ac5f5.Floats.{45}Inf
    ( apply $agdaIdent8.d2c4f4e5116ac5f5.Floats._{47}_ -1.0 0.0 )
  )
  ( $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
    ( lambda ($v0 $world)
      ( apply ( switch $v0
                ( 0
                  ( apply $agdaIdent1a.952a3c475e16a2d6.Common.IO.putStrLn "false" )
                )
                ( 1
                  ( apply $agdaIdent1a.952a3c475e16a2d6.Common.IO.putStrLn "true" )
                )
                ( _ (tag _)
                  ( apply (global $Stdlib $failwith) "__UNREACHABLE__" )
                )
              )
        $world
      )
    )
  )
  ( $agdaIdent2.d2c4f4e5116ac5f5.Floats.print
    ( lambda ($v0 $world)
      ( apply ( apply $agdaIdent1a.952a3c475e16a2d6.Common.IO.putStrLn
                ( apply $agdaIdent38.2ed69e510f00fd1e.Agda.Builtin.Float.primShowFloat
                  $v0
                )
              )
        $world
      )
    )
  )
  ( $main
    ( apply (global $ForeignCode $main_run)
      ( apply ( lambda ($world)
                ( apply ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                          0
                          0
                          0
                          0
                          ( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr "123.4 = " )
                          ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                            0
                            0
                            0
                            0
                            ( apply $agdaIdent2.d2c4f4e5116ac5f5.Floats.print 123.4 )
                            ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                              0
                              0
                              0
                              0
                              ( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr "-42.9 = " )
                              ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                0
                                0
                                0
                                0
                                ( apply $agdaIdent2.d2c4f4e5116ac5f5.Floats.print -42.9 )
                                ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                  0
                                  0
                                  0
                                  0
                                  ( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
                                    "NaN   = "
                                  )
                                  ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                    0
                                    0
                                    0
                                    0
                                    ( apply $agdaIdent2.d2c4f4e5116ac5f5.Floats.print
                                      $agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
                                    )
                                    ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                      0
                                      0
                                      0
                                      0
                                      ( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
                                        "Inf   = "
                                      )
                                      ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                        0
                                        0
                                        0
                                        0
                                        ( apply $agdaIdent2.d2c4f4e5116ac5f5.Floats.print
                                          $agdaIdent16.d2c4f4e5116ac5f5.Floats.Inf
                                        )
                                        ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                          0
                                          0
                                          0
                                          0
                                          ( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
                                            "-Inf  = "
                                          )
                                          ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                            0
                                            0
                                            0
                                            0
                                            ( apply $agdaIdent2.d2c4f4e5116ac5f5.Floats.print
                                              $agdaIdent18.d2c4f4e5116ac5f5.Floats.{45}Inf
                                            )
                                            ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                              0
                                              0
                                              0
                                              0
                                              ( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
                                                "Inf == Inf = "
                                              )
                                              ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                0
                                                0
                                                0
                                                0
                                                ( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
                                                  ( apply $agdaIdenta.d2c4f4e5116ac5f5.Floats._{61}{61}_
                                                    $agdaIdent16.d2c4f4e5116ac5f5.Floats.Inf
                                                    $agdaIdent16.d2c4f4e5116ac5f5.Floats.Inf
                                                  )
                                                )
                                                ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                  0
                                                  0
                                                  0
                                                  0
                                                  ( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
                                                    "NaN == NaN = "
                                                  )
                                                  ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                    0
                                                    0
                                                    0
                                                    0
                                                    ( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
                                                      ( apply $agdaIdenta.d2c4f4e5116ac5f5.Floats._{61}{61}_
                                                        $agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
                                                        $agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
                                                      )
                                                    )
                                                    ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                      0
                                                      0
                                                      0
                                                      0
                                                      ( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
                                                        "NaN == -NaN = "
                                                      )
                                                      ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                        0
                                                        0
                                                        0
                                                        0
                                                        ( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
                                                          ( apply $agdaIdenta.d2c4f4e5116ac5f5.Floats._{61}{61}_
                                                            $agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
                                                            ( apply $agdaIdent1a.2ed69e510f00fd1e.Agda.Builtin.Float.primFloatNegate
                                                              $agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
                                                            )
                                                          )
                                                        )
                                                        ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                          0
                                                          0
                                                          0
                                                          0
                                                          ( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
                                                            "0.0 == -0.0 = "
                                                          )
                                                          ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                            0
                                                            0
                                                            0
                                                            0
                                                            ( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
                                                              ( apply $agdaIdenta.d2c4f4e5116ac5f5.Floats._{61}{61}_
                                                                0.0
                                                                0.0
                                                              )
                                                            )
                                                            ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                              0
                                                              0
                                                              0
                                                              0
                                                              ( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
                                                                "isZero  0.0 = "
                                                              )
                                                              ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                0
                                                                0
                                                                0
                                                                0
                                                                ( apply $agdaIdent1a.952a3c475e16a2d6.Common.IO.putStrLn
                                                                  ( apply $agdaIdent28.d2c4f4e5116ac5f5.Floats.isZero
                                                                    0.0
                                                                  )
                                                                )
                                                                ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                  0
                                                                  0
                                                                  0
                                                                  0
                                                                  ( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
                                                                    "isZero -0.0 = "
                                                                  )
                                                                  ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                    0
                                                                    0
                                                                    0
                                                                    0
                                                                    ( apply $agdaIdent1a.952a3c475e16a2d6.Common.IO.putStrLn
                                                                      ( apply $agdaIdent28.d2c4f4e5116ac5f5.Floats.isZero
                                                                        0.0
                                                                      )
                                                                    )
                                                                    ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                      0
                                                                      0
                                                                      0
                                                                      0
                                                                      ( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
                                                                        "isZero  1.0 = "
                                                                      )
                                                                      ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                        0
                                                                        0
                                                                        0
                                                                        0
                                                                        ( apply $agdaIdent1a.952a3c475e16a2d6.Common.IO.putStrLn
                                                                          ( apply $agdaIdent28.d2c4f4e5116ac5f5.Floats.isZero
                                                                            1.0
                                                                          )
                                                                        )
                                                                        ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                          0
                                                                          0
                                                                          0
                                                                          0
                                                                          ( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
                                                                            "NaN =N= NaN  = "
                                                                          )
                                                                          ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                            0
                                                                            0
                                                                            0
                                                                            0
                                                                            ( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
                                                                              ( apply $agdaIdentc.d2c4f4e5116ac5f5.Floats._{61}N{61}_
                                                                                $agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
                                                                                $agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
                                                                              )
                                                                            )
                                                                            ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                              0
                                                                              0
                                                                              0
                                                                              0
                                                                              ( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
                                                                                "0.0 =N= -0.0 = "
                                                                              )
                                                                              ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                0
                                                                                0
                                                                                0
                                                                                0
                                                                                ( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
                                                                                  ( apply $agdaIdentc.d2c4f4e5116ac5f5.Floats._{61}N{61}_
                                                                                    0.0
                                                                                    0.0
                                                                                  )
                                                                                )
                                                                                ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                  0
                                                                                  0
                                                                                  0
                                                                                  0
                                                                                  ( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
                                                                                    "0.0 =N= 12.0 = "
                                                                                  )
                                                                                  ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                    0
                                                                                    0
                                                                                    0
                                                                                    0
                                                                                    ( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
                                                                                      ( apply $agdaIdentc.d2c4f4e5116ac5f5.Floats._{61}N{61}_
                                                                                        0.0
                                                                                        12.0
                                                                                      )
                                                                                    )
                                                                                    ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                      0
                                                                                      0
                                                                                      0
                                                                                      0
                                                                                      ( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
                                                                                        "NaN  < -Inf = "
                                                                                      )
                                                                                      ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                        0
                                                                                        0
                                                                                        0
                                                                                        0
                                                                                        ( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
                                                                                          ( apply $agdaIdent10.d2c4f4e5116ac5f5.Floats._{60}_
                                                                                            $agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
                                                                                            $agdaIdent18.d2c4f4e5116ac5f5.Floats.{45}Inf
                                                                                          )
                                                                                        )
                                                                                        ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                          0
                                                                                          0
                                                                                          0
                                                                                          0
                                                                                          ( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
                                                                                            "-Inf < NaN  = "
                                                                                          )
                                                                                          ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                            0
                                                                                            0
                                                                                            0
                                                                                            0
                                                                                            ( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
                                                                                              ( apply $agdaIdent10.d2c4f4e5116ac5f5.Floats._{60}_
                                                                                                $agdaIdent18.d2c4f4e5116ac5f5.Floats.{45}Inf
                                                                                                $agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
                                                                                              )
                                                                                            )
                                                                                            ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                              0
                                                                                              0
                                                                                              0
                                                                                              0
                                                                                              ( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
                                                                                                "0.0  < -0.0 = "
                                                                                              )
                                                                                              ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                                0
                                                                                                0
                                                                                                0
                                                                                                0
                                                                                                ( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
                                                                                                  ( apply $agdaIdent10.d2c4f4e5116ac5f5.Floats._{60}_
                                                                                                    0.0
                                                                                                    0.0
                                                                                                  )
                                                                                                )
                                                                                                ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                                  0
                                                                                                  0
                                                                                                  0
                                                                                                  0
                                                                                                  ( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
                                                                                                    "-0.0 < 0.0  = "
                                                                                                  )
                                                                                                  ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                                    0
                                                                                                    0
                                                                                                    0
                                                                                                    0
                                                                                                    ( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
                                                                                                      ( apply $agdaIdent10.d2c4f4e5116ac5f5.Floats._{60}_
                                                                                                        0.0
                                                                                                        0.0
                                                                                                      )
                                                                                                    )
                                                                                                    ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                                      0
                                                                                                      0
                                                                                                      0
                                                                                                      0
                                                                                                      ( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
                                                                                                        "NaN  < NaN  = "
                                                                                                      )
                                                                                                      ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                                        0
                                                                                                        0
                                                                                                        0
                                                                                                        0
                                                                                                        ( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
                                                                                                          ( apply $agdaIdent10.d2c4f4e5116ac5f5.Floats._{60}_
                                                                                                            $agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
                                                                                                            $agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
                                                                                                          )
                                                                                                        )
                                                                                                        ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                                          0
                                                                                                          0
                                                                                                          0
                                                                                                          0
                                                                                                          ( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
                                                                                                            "-NaN < -NaN = "
                                                                                                          )
                                                                                                          ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                                            0
                                                                                                            0
                                                                                                            0
                                                                                                            0
                                                                                                            ( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
                                                                                                              ( apply $agdaIdent10.d2c4f4e5116ac5f5.Floats._{60}_
                                                                                                                $agdaIdent14.d2c4f4e5116ac5f5.Floats.{45}NaN
                                                                                                                $agdaIdent14.d2c4f4e5116ac5f5.Floats.{45}NaN
                                                                                                              )
                                                                                                            )
                                                                                                            ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                                              0
                                                                                                              0
                                                                                                              0
                                                                                                              0
                                                                                                              ( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
                                                                                                                "NaN  < -NaN = "
                                                                                                              )
                                                                                                              ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                                                0
                                                                                                                0
                                                                                                                0
                                                                                                                0
                                                                                                                ( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
                                                                                                                  ( apply $agdaIdent10.d2c4f4e5116ac5f5.Floats._{60}_
                                                                                                                    $agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
                                                                                                                    $agdaIdent14.d2c4f4e5116ac5f5.Floats.{45}NaN
                                                                                                                  )
                                                                                                                )
                                                                                                                ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                                                  0
                                                                                                                  0
                                                                                                                  0
                                                                                                                  0
                                                                                                                  ( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
                                                                                                                    "-NaN < NaN  = "
                                                                                                                  )
                                                                                                                  ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                                                    0
                                                                                                                    0
                                                                                                                    0
                                                                                                                    0
                                                                                                                    ( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
                                                                                                                      ( apply $agdaIdent10.d2c4f4e5116ac5f5.Floats._{60}_
                                                                                                                        $agdaIdent14.d2c4f4e5116ac5f5.Floats.{45}NaN
                                                                                                                        $agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
                                                                                                                      )
                                                                                                                    )
                                                                                                                    ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                                                      0
                                                                                                                      0
                                                                                                                      0
                                                                                                                      0
                                                                                                                      ( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
                                                                                                                        "NaN  < -5.0 = "
                                                                                                                      )
                                                                                                                      ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                                                        0
                                                                                                                        0
                                                                                                                        0
                                                                                                                        0
                                                                                                                        ( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
                                                                                                                          ( apply $agdaIdent10.d2c4f4e5116ac5f5.Floats._{60}_
                                                                                                                            $agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
                                                                                                                            -5.0
                                                                                                                          )
                                                                                                                        )
                                                                                                                        ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                                                          0
                                                                                                                          0
                                                                                                                          0
                                                                                                                          0
                                                                                                                          ( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
                                                                                                                            "-5.0 < NaN  = "
                                                                                                                          )
                                                                                                                          ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                                                            0
                                                                                                                            0
                                                                                                                            0
                                                                                                                            0
                                                                                                                            ( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
                                                                                                                              ( apply $agdaIdent10.d2c4f4e5116ac5f5.Floats._{60}_
                                                                                                                                -5.0
                                                                                                                                $agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
                                                                                                                              )
                                                                                                                            )
                                                                                                                            ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                                                              0
                                                                                                                              0
                                                                                                                              0
                                                                                                                              0
                                                                                                                              ( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
                                                                                                                                "NaN  <N -Inf = "
                                                                                                                              )
                                                                                                                              ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                                                                0
                                                                                                                                0
                                                                                                                                0
                                                                                                                                0
                                                                                                                                ( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
                                                                                                                                  ( apply $agdaIdente.d2c4f4e5116ac5f5.Floats._{60}N_
                                                                                                                                    $agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
                                                                                                                                    $agdaIdent18.d2c4f4e5116ac5f5.Floats.{45}Inf
                                                                                                                                  )
                                                                                                                                )
                                                                                                                                ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                                                                  0
                                                                                                                                  0
                                                                                                                                  0
                                                                                                                                  0
                                                                                                                                  ( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
                                                                                                                                    "-Inf <N NaN  = "
                                                                                                                                  )
                                                                                                                                  ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                                                                    0
                                                                                                                                    0
                                                                                                                                    0
                                                                                                                                    0
                                                                                                                                    ( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
                                                                                                                                      ( apply $agdaIdente.d2c4f4e5116ac5f5.Floats._{60}N_
                                                                                                                                        $agdaIdent18.d2c4f4e5116ac5f5.Floats.{45}Inf
                                                                                                                                        $agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
                                                                                                                                      )
                                                                                                                                    )
                                                                                                                                    ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                                                                      0
                                                                                                                                      0
                                                                                                                                      0
                                                                                                                                      0
                                                                                                                                      ( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
                                                                                                                                        "0.0  <N -0.0 = "
                                                                                                                                      )
                                                                                                                                      ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                                                                        0
                                                                                                                                        0
                                                                                                                                        0
                                                                                                                                        0
                                                                                                                                        ( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
                                                                                                                                          ( apply $agdaIdente.d2c4f4e5116ac5f5.Floats._{60}N_
                                                                                                                                            0.0
                                                                                                                                            0.0
                                                                                                                                          )
                                                                                                                                        )
                                                                                                                                        ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                                                                          0
                                                                                                                                          0
                                                                                                                                          0
                                                                                                                                          0
                                                                                                                                          ( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
                                                                                                                                            "-0.0 <N 0.0  = "
                                                                                                                                          )
                                                                                                                                          ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                                                                            0
                                                                                                                                            0
                                                                                                                                            0
                                                                                                                                            0
                                                                                                                                            ( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
                                                                                                                                              ( apply $agdaIdente.d2c4f4e5116ac5f5.Floats._{60}N_
                                                                                                                                                0.0
                                                                                                                                                0.0
                                                                                                                                              )
                                                                                                                                            )
                                                                                                                                            ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                                                                              0
                                                                                                                                              0
                                                                                                                                              0
                                                                                                                                              0
                                                                                                                                              ( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
                                                                                                                                                "NaN  <N NaN  = "
                                                                                                                                              )
                                                                                                                                              ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                                                                                0
                                                                                                                                                0
                                                                                                                                                0
                                                                                                                                                0
                                                                                                                                                ( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
                                                                                                                                                  ( apply $agdaIdente.d2c4f4e5116ac5f5.Floats._{60}N_
                                                                                                                                                    $agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
                                                                                                                                                    $agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
                                                                                                                                                  )
                                                                                                                                                )
                                                                                                                                                ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                                                                                  0
                                                                                                                                                  0
                                                                                                                                                  0
                                                                                                                                                  0
                                                                                                                                                  ( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
                                                                                                                                                    "-NaN <N -NaN = "
                                                                                                                                                  )
                                                                                                                                                  ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                                                                                    0
                                                                                                                                                    0
                                                                                                                                                    0
                                                                                                                                                    0
                                                                                                                                                    ( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
                                                                                                                                                      ( apply $agdaIdente.d2c4f4e5116ac5f5.Floats._{60}N_
                                                                                                                                                        $agdaIdent14.d2c4f4e5116ac5f5.Floats.{45}NaN
                                                                                                                                                        $agdaIdent14.d2c4f4e5116ac5f5.Floats.{45}NaN
                                                                                                                                                      )
                                                                                                                                                    )
                                                                                                                                                    ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                                                                                      0
                                                                                                                                                      0
                                                                                                                                                      0
                                                                                                                                                      0
                                                                                                                                                      ( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
                                                                                                                                                        "NaN  <N -NaN = "
                                                                                                                                                      )
                                                                                                                                                      ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                                                                                        0
                                                                                                                                                        0
                                                                                                                                                        0
                                                                                                                                                        0
                                                                                                                                                        ( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
                                                                                                                                                          ( apply $agdaIdente.d2c4f4e5116ac5f5.Floats._{60}N_
                                                                                                                                                            $agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
                                                                                                                                                            $agdaIdent14.d2c4f4e5116ac5f5.Floats.{45}NaN
                                                                                                                                                          )
                                                                                                                                                        )
                                                                                                                                                        ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                                                                                          0
                                                                                                                                                          0
                                                                                                                                                          0
                                                                                                                                                          0
                                                                                                                                                          ( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
                                                                                                                                                            "-NaN <N NaN  = "
                                                                                                                                                          )
                                                                                                                                                          ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                                                                                            0
                                                                                                                                                            0
                                                                                                                                                            0
                                                                                                                                                            0
                                                                                                                                                            ( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
                                                                                                                                                              ( apply $agdaIdente.d2c4f4e5116ac5f5.Floats._{60}N_
                                                                                                                                                                $agdaIdent14.d2c4f4e5116ac5f5.Floats.{45}NaN
                                                                                                                                                                $agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
                                                                                                                                                              )
                                                                                                                                                            )
                                                                                                                                                            ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                                                                                              0
                                                                                                                                                              0
                                                                                                                                                              0
                                                                                                                                                              0
                                                                                                                                                              ( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
                                                                                                                                                                "NaN  <N -5.0 = "
                                                                                                                                                              )
                                                                                                                                                              ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                                                                                                0
                                                                                                                                                                0
                                                                                                                                                                0
                                                                                                                                                                0
                                                                                                                                                                ( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
                                                                                                                                                                  ( apply $agdaIdente.d2c4f4e5116ac5f5.Floats._{60}N_
                                                                                                                                                                    $agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
                                                                                                                                                                    -5.0
                                                                                                                                                                  )
                                                                                                                                                                )
                                                                                                                                                                ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                                                                                                  0
                                                                                                                                                                  0
                                                                                                                                                                  0
                                                                                                                                                                  0
                                                                                                                                                                  ( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
                                                                                                                                                                    "-5.0 <N NaN  = "
                                                                                                                                                                  )
                                                                                                                                                                  ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                                                                                                    0
                                                                                                                                                                    0
                                                                                                                                                                    0
                                                                                                                                                                    0
                                                                                                                                                                    ( apply $agdaIdent6.d2c4f4e5116ac5f5.Floats.printB
                                                                                                                                                                      ( apply $agdaIdente.d2c4f4e5116ac5f5.Floats._{60}N_
                                                                                                                                                                        -5.0
                                                                                                                                                                        $agdaIdent12.d2c4f4e5116ac5f5.Floats.NaN
                                                                                                                                                                      )
                                                                                                                                                                    )
                                                                                                                                                                    ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                                                                                                      0
                                                                                                                                                                      0
                                                                                                                                                                      0
                                                                                                                                                                      0
                                                                                                                                                                      ( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
                                                                                                                                                                        "e                   = "
                                                                                                                                                                      )
                                                                                                                                                                      ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                                                                                                        0
                                                                                                                                                                        0
                                                                                                                                                                        0
                                                                                                                                                                        0
                                                                                                                                                                        ( apply $agdaIdent2.d2c4f4e5116ac5f5.Floats.print
                                                                                                                                                                          ( apply $agdaIdent26.2ed69e510f00fd1e.Agda.Builtin.Float.primExp
                                                                                                                                                                            1.0
                                                                                                                                                                          )
                                                                                                                                                                        )
                                                                                                                                                                        ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                                                                                                          0
                                                                                                                                                                          0
                                                                                                                                                                          0
                                                                                                                                                                          0
                                                                                                                                                                          ( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
                                                                                                                                                                            "sin (asin 0.6)      = "
                                                                                                                                                                          )
                                                                                                                                                                          ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                                                                                                            0
                                                                                                                                                                            0
                                                                                                                                                                            0
                                                                                                                                                                            0
                                                                                                                                                                            ( apply $agdaIdent2.d2c4f4e5116ac5f5.Floats.print
                                                                                                                                                                              ( apply $agdaIdent1a.d2c4f4e5116ac5f5.Floats.sin
                                                                                                                                                                                ( apply $agdaIdent20.d2c4f4e5116ac5f5.Floats.asin
                                                                                                                                                                                  0.6
                                                                                                                                                                                )
                                                                                                                                                                              )
                                                                                                                                                                            )
                                                                                                                                                                            ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                                                                                                              0
                                                                                                                                                                              0
                                                                                                                                                                              0
                                                                                                                                                                              0
                                                                                                                                                                              ( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
                                                                                                                                                                                "cos (acos 0.6)      = "
                                                                                                                                                                              )
                                                                                                                                                                              ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                                                                                                                0
                                                                                                                                                                                0
                                                                                                                                                                                0
                                                                                                                                                                                0
                                                                                                                                                                                ( apply $agdaIdent2.d2c4f4e5116ac5f5.Floats.print
                                                                                                                                                                                  ( apply $agdaIdent1c.d2c4f4e5116ac5f5.Floats.cos
                                                                                                                                                                                    ( apply $agdaIdent22.d2c4f4e5116ac5f5.Floats.acos
                                                                                                                                                                                      0.6
                                                                                                                                                                                    )
                                                                                                                                                                                  )
                                                                                                                                                                                )
                                                                                                                                                                                ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                                                                                                                  0
                                                                                                                                                                                  0
                                                                                                                                                                                  0
                                                                                                                                                                                  0
                                                                                                                                                                                  ( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
                                                                                                                                                                                    "tan (atan 0.4)      = "
                                                                                                                                                                                  )
                                                                                                                                                                                  ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                                                                                                                    0
                                                                                                                                                                                    0
                                                                                                                                                                                    0
                                                                                                                                                                                    0
                                                                                                                                                                                    ( apply $agdaIdent2.d2c4f4e5116ac5f5.Floats.print
                                                                                                                                                                                      ( apply $agdaIdent1e.d2c4f4e5116ac5f5.Floats.tan
                                                                                                                                                                                        ( apply $agdaIdent24.d2c4f4e5116ac5f5.Floats.atan
                                                                                                                                                                                          0.4
                                                                                                                                                                                        )
                                                                                                                                                                                      )
                                                                                                                                                                                    )
                                                                                                                                                                                    ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                                                                                                                      0
                                                                                                                                                                                      0
                                                                                                                                                                                      0
                                                                                                                                                                                      0
                                                                                                                                                                                      ( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
                                                                                                                                                                                        "tan (atan2 0.4 1.0) = "
                                                                                                                                                                                      )
                                                                                                                                                                                      ( apply $agdaIdent50.952a3c475e16a2d6.Common.IO.then
                                                                                                                                                                                        0
                                                                                                                                                                                        0
                                                                                                                                                                                        0
                                                                                                                                                                                        0
                                                                                                                                                                                        ( apply $agdaIdent2.d2c4f4e5116ac5f5.Floats.print
                                                                                                                                                                                          ( apply $agdaIdent1e.d2c4f4e5116ac5f5.Floats.tan
                                                                                                                                                                                            ( apply $agdaIdent26.d2c4f4e5116ac5f5.Floats.atan2
                                                                                                                                                                                              0.4
                                                                                                                                                                                              1.0
                                                                                                                                                                                            )
                                                                                                                                                                                          )
                                                                                                                                                                                        )
                                                                                                                                                                                        ( apply $agdaIdent8.952a3c475e16a2d6.Common.IO.return
                                                                                                                                                                                          0
                                                                                                                                                                                          0
                                                                                                                                                                                          0
                                                                                                                                                                                        )
                                                                                                                                                                                      )
                                                                                                                                                                                    )
                                                                                                                                                                                  )
                                                                                                                                                                                )
                                                                                                                                                                              )
                                                                                                                                                                            )
                                                                                                                                                                          )
                                                                                                                                                                        )
                                                                                                                                                                      )
                                                                                                                                                                    )
                                                                                                                                                                  )
                                                                                                                                                                )
                                                                                                                                                              )
                                                                                                                                                            )
                                                                                                                                                          )
                                                                                                                                                        )
                                                                                                                                                      )
                                                                                                                                                    )
                                                                                                                                                  )
                                                                                                                                                )
                                                                                                                                              )
                                                                                                                                            )
                                                                                                                                          )
                                                                                                                                        )
                                                                                                                                      )
                                                                                                                                    )
                                                                                                                                  )
                                                                                                                                )
                                                                                                                              )
                                                                                                                            )
                                                                                                                          )
                                                                                                                        )
                                                                                                                      )
                                                                                                                    )
                                                                                                                  )
                                                                                                                )
                                                                                                              )
                                                                                                            )
                                                                                                          )
                                                                                                        )
                                                                                                      )
                                                                                                    )
                                                                                                  )
                                                                                                )
                                                                                              )
                                                                                            )
                                                                                          )
                                                                                        )
                                                                                      )
                                                                                    )
                                                                                  )
                                                                                )
                                                                              )
                                                                            )
                                                                          )
                                                                        )
                                                                      )
                                                                    )
                                                                  )
                                                                )
                                                              )
                                                            )
                                                          )
                                                        )
                                                      )
                                                    )
                                                  )
                                                )
                                              )
                                            )
                                          )
                                        )
                                      )
                                    )
                                  )
                                )
                              )
                            )
                          )
                        )
                  $world
                )
              )
        0
      )
    )
  )
  ( export )
)

[xekoukou]

The problem lies here:

  ( $agdaIdent36.2ed69e510f00fd1e.Agda.Builtin.Float.primATan2
    ( lambda ($a) ( apply (global $Stdlib $Float $atan2) $a ) )

atan2 is a binary operation and I have only applied it once. I am keeping the issue open in case you find it useful. Maybe add a check that looks at the arity of a function.

[stedolan]

Thanks for the report! This is definitely a bug.

In OCaml, all functions are curried. However, some basic functions are implemented as "primitives", and internally these are not curried. The compiler makes sure to expand partial applications of these when compiling, but I forgot to do this in malfunction. (So the OCaml code atan2 x compiles more like (fun a b -> atan2 a b) x, ensuring that all uses of atan2 are fully applied).