Identity optimisation not kicking in

[gallais]

In the following minimal example, erase should be detected as an identity function
(and, importantly, we should be able to state our intent that it is) however it is not.

import Data.Vect

erase : Vect n a -> List a
erase [] = []
erase (x :: xs) = x :: erase xs

main : IO ()
main = putStrLn $ pack $ erase $ fromList $ unpack "Hello world"

In both the scheme and javascript backends you can find it remaining in the codegen:

(define Main-erase
  (lambda (arg-2)
    (if (null? arg-2) '()
        (let ((e-3 (car arg-2)))
        (let ((e-4 (cdr arg-2)))
        (cons e-3 (Main-erase e-4)))))))

/* Main.erase : Vect n a -> List a */
function Main_erase($0) {
 switch($0.h) {
  case 0: /* nil */ return {h: 0};
  case undefined: /* cons */ return {a1: $0.a1, a2: Main_erase($0.a2)};
 }
}

[Z-snails]

Some backends ignore the ConInfo information and backends can also ignore the constructor tag and only use the name (this is the case in my GRIN backend - although I haven't used that in a very long time). This means Vect and List are genuinely distinct on some backends, so the identity optimsation can't optimise erase.
One possible solution would be to use a different name for constructors with some ConInfo, eg any constructor with ConInfo of NIL would have the tag 0 and name _BUILTIN.NIL, and CONS would have tag 1 and name _BUILTIN.CONS.
This shouldn't be too difficult to do, and this change alone should make the identity optimisation work in this case.

In order to give users more control over optimisations, it might be better to implement this paper: https://trendsfp.github.io/abstracts/paper-019.pdf - although I expect that would be a much bigger and more tricky change.

I also agree it would be good to be able to assert a function is the identity function - perhaps a %identity modifier before the function declaration would work for that.

[Z-snails]

One possible solution would be to use a different name for constructors with some ConInfo, eg any constructor with ConInfo of NIL would have the tag 0 and name _BUILTIN.NIL, and CONS would have tag 1 and name _BUILTIN.CONS. This shouldn't be too difficult to do, and this change alone should make the identity optimisation work in this case.

This worked. I will test it properly and make a PR later.