Idris mode inferring unapplied function types

[Abhiroop]

For example,

I am attempting this basic example:

plus_commutes_Z : m = plus m 0
plus_commutes_Z {m = Z} = Refl
plus_commutes_Z {m = (S k)} = let rec = plus_commutes_Z {m = k} in
                                  rewrite sym rec in Refl

plus_commutes : (n, m : Nat) -> plus n m = plus m n
plus_commutes Z m = plus_commutes_Z
plus_commutes (S k) m = rewrite plus_commutes k m in ?plus_commutes_S

Here when I typecheck plus_commutes_S, when I expected

S (plus m k) = plus m (S k)

it is being inferred as

(\replaced => S replaced = plus m (S k)) (plus m k)

I am using Idris 1.2 and spacemacs idris layer (which I assume pulls the latest version of idris mode)

[abailly]

@Abhiroop This seems like an issue within idris itself. idris-mode itself does not know how to typecheck Idris and interacts with a background idris process. But I agree this is kind of odd...

[abailly]

When I do :t Main.hole at the command-line it shows:

 :t Main.hole
  k : Nat
  j : Nat
  _rewrite_rule : plus k j = plus j k
--------------------------------------
Main.hole : S (plus j k) = plus j (S k)

So it seems something happens in the communication between idris-mode and the idris interpreter process. When tracing communication with idris process, it definitely returns a term with unapplied function.

[Abhiroop]

The issue seems to be at the idris-load-file method (https://github.com/idris-hackers/idris-mode/blob/0a5a165a0dd7be7bbc4f5c9533dc21acfc811a4e/idris-commands.el#L177).

Because the idris-type-at-point binding returns the correct applied result as well.

[david-christiansen]

This is going to be part of the Idris IDE protocol server. It probably needs updating - the command-line REPL also used to do this.

In the meantime, you can right-click the expression and click "Normalize" to reduce it.

[abailly]

@david-christiansen I tracked this to the runIdeModeCommand function called with command Metavariables in REPL.hs which is pretty daunting. I was unable to understand why the application is not properly reduced. Should we add a call to TermNormalise on the emacs side?

[mkwatson]

Also just came across this, I've been using idris-type-at-point (C-c C-t) which displays the normalized type. I don't know why the unapplied form should ever be displayed