Fixed #5602.

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

@@ -34,7 +34,7 @@ import Agda.Syntax.Abstract.Name
     mnameToList, qnameName, qnameModule, nameId )
 import Agda.Syntax.Internal
   ( Name, Type
-  , arity, nameFixity, unDom )
+  , arity, nameFixity, unDom, telToList )
 import Agda.Syntax.Literal       ( Literal(..) )
 import Agda.Syntax.Treeless      ( ArgUsage(..), filterUsed )
 import qualified Agda.Syntax.Treeless as T
@@ -43,6 +43,7 @@ import Agda.TypeChecking.Monad
 import Agda.TypeChecking.Reduce ( instantiateFull )
 import Agda.TypeChecking.Substitute as TC ( TelV(..), raise, subst )
 import Agda.TypeChecking.Pretty
+import Agda.TypeChecking.Telescope ( telView )
 
 import Agda.Utils.FileName ( isNewerThan )
 import Agda.Utils.Function ( iterate' )
@@ -471,7 +472,8 @@ definition' kit q d t ls =
 
     Constructor{} | Just e <- defJSDef d -> plainJS e
     Constructor{conData = p, conPars = nc} -> do
-      let np = arity t - nc
+      TelV tel _ <- telView t
+      let np = length (telToList tel) - nc
       erased <- getErasedConArgs q
       let nargs = np - length (filter id erased)
           args = [ Local $ LocalId $ nargs - i | i <- [0 .. nargs-1] ]

test/Compiler/simple/Issue5602.agda

@@ -0,0 +1,26 @@
+open import Agda.Builtin.IO
+open import Agda.Builtin.String
+open import Agda.Builtin.Unit
+
+postulate
+  putStr : String → IO ⊤
+
+{-# FOREIGN GHC import qualified Data.Text.IO #-}
+{-# COMPILE GHC putStr = Data.Text.IO.putStr #-}
+{-# 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₀))

test/Compiler/simple/Issue5602.out

@@ -0,0 +1,5 @@
+EXECUTED_PROGRAM
+
+ret > ExitSuccess
+out > OK
+out >