Idiom brackets does not support correctly leftmost {integer, double, char, string} literal

[buzden]

Context

We can use whatever we want as the only thing in idiom brackets, say a Nat or String:

ff : List Nat
ff = let x = 4 in [| x |]

We even can go fancy and use strange coding of function that is acting inside an idiom bracket:

fromString : String -> (Nat -> Nat -> Nat)      
fromString "haha" = (*)      
fromString _      = (+)      
      
fh' : List Nat -> List Nat -> List Nat      
fh' a b = let x = "haha" in [| x a b |]

fh'' : List Nat -> List Nat -> List Nat
fh'' a b = [| (let x = "haha" in x) a b |]

fh''' : List Nat -> List Nat -> List Nat
fh''' a b = [| (let x = () in "haha") a b |]

All above typecheks fine.

Steps to Reproduce

Use an integer or string (or whatever redefinable) literal as a leftmost expression directly inside the idiom bracket:

fg : List Nat
fg = [| 4 |]

fs : List String
fs = [| "" |]

fh : List Nat -> List Nat -> List Nat
fh a b = [| "haha" a b |]

Expected Behavior

I'd expect "inlining" the lets to work the same as the uninlined let versions above.

Observed Behavior

Error: While processing right hand side of fg. When unifying:
    List Nat
and:
    List Nat
When unifying:
    Integer
and:
    List Integer
Mismatch between: Integer and List Integer.

....:5:9--5:10
 1 | ff : List Nat
 2 | ff = let x = 4 in [| x |]
 3 | 
 4 | fg : List Nat
 5 | fg = [| 4 |]
             ^

Error: While processing right hand side of fs. When unifying:
    List String
and:
    List String
When unifying:
    String
and:
    List String
Mismatch between: String and List String.

....:8:9--8:11
 4 | fg : List Nat
 5 | fg = [| 4 |]
 6 | 
 7 | fs : List String
 8 | fs = [| "" |]
             ^^

Error: While processing right hand side of fh. When unifying:
    String
and:
    List ?a
Mismatch between: String and List ?a.

....:15:14--15:18
 11 | fromString "haha" = (*)
 12 | fromString _      = (+)
 13 |     
 14 | fh : List Nat -> List Nat -> List Nat
 15 | fh a b = [| "haha" a b |]

Discussion

When looking at the logs, it turns out that [| 4 |] desugars to pure fromInteger <*> 4, not to pure (fromInteger 4), which is understandable when you consider 4 to be literally fromInteger 4.

This happens because Idris.Desugar.idiomise function works upon already desugared terms (RawImp) and desugaring treats, say, integer term as an application of fromInteger to an integer term, so idiomise does not have any information to distinguish between real function application and function application from literal desugaring.

Anyway, this is rather miserable bug, I think mostly affecting those who like styling their code like this

f ... = [| 0 |]
f ... = [| g ... ... |]

just giving a strange error and easy (not so stylish) workarounds.

Maybe, this can be fixed by idiomise returning IAlternative when leftmost application is a from* literal-reading function.

[gallais]

I wonder whether we shouldn't instead run idiomise on PTerm rather and RawImp. And then run desugarB on the result rather than before it.

[buzden]

It seems that only PPair and PDPair should be managed additionally in PTerm-based idiomise because it seems that they are only stuff that produces IApp additionally to PApp while desugaring. So, it looks feasible.

[dunhamsteve]

Also POp needs to be handled. The desugaring for that one collects tokens, runs shunting yard to get a Tree and then desugarTree to get a bunch of IApp. The desugarTree step makes me a little nervous - if we reproduce it for PApp then we have two copies of the same logic that need to be kept in sync.