The JS backend does not reduce constructor type signatures

[nad]

The following code is not compiled correctly by the JS backend:

open import Agda.Builtin.IO
open import Agda.Builtin.String
open import Agda.Builtin.Unit

postulate
  putStr : String → IO ⊤

{-# COMPILE JS putStr =
    function (x) {
      return function(cb) {
        process.stdout.write(x); cb(0); }; } #-}

F : Set → Set
F A = A → A

data D : Set where
  c₀ : D
  c₁ : F D

f : D → String
f c₀     = "OK\n"
f (c₁ x) = f x

main = putStr (f (c₁ c₀))

$ NODE_PATH=. nodejs jAgda.Bug.js
[…]/jAgda.Bug.js:10
exports["D"]["c₁"] = a => a["c₁"]();
                                 ^

TypeError: a.c₁ is not a function
    at Object.exports.D.c₁.a [as c₁] ([…]/jAgda.Bug.js:10:34)
    at Object.<anonymous> ([…]/jAgda.Bug.js:18:25)
    at Module._compile (module.js:652:30)
    at Object.Module._extensions..js (module.js:663:10)
    at Module.load (module.js:565:32)
    at tryModuleLoad (module.js:505:12)
    at Function.Module._load (module.js:497:3)
    at Function.Module.runMain (module.js:693:10)
    at startup (bootstrap_node.js:188:16)
    at bootstrap_node.js:609:3

The code is compiled successfully if F D is replaced by D → D.

I constructed the test case above after seeing the following code:

agda/src/full/Agda/Compiler/JS/Compiler.hs

Lines 473 to 474 in d281ede

	Constructor{conData = p, conPars = nc} -> do
	let np = arity t - nc

Note the documentation of arity:

agda/src/full/Agda/Syntax/Internal.hs

Lines 956 to 957 in d281ede

	-- | Doesn't do any reduction.
	arity :: Type -> Nat