Identity optimisation not kicking in

[ohad]

Steps to Reproduce

Load this:

public export
data Tree : Type where
  Leaf : Tree
  Node : Tree -> Tree -> Tree

namespace Foo
  public export
  data Path : Type where
    Nil : Path
    ConsL : Path -> Path
    ConsR : Path -> Path


namespace Bar
  public export
  data PathIn : Tree -> Type where
    Nil : PathIn Leaf
    ConsL : PathIn lft -> PathIn (Node lft rgt)
    ConsR : PathIn rgt -> PathIn (Node lft rgt)

-- Expecting identity transformation to kick in
f : PathIn tree -> Path
f [] = []
f (ConsL t) = ConsL (f t)
f (ConsR t) = ConsR (f t)

Then at the REPL:

> :di f

Expected Behavior

Main.f
...
Compiled: \ {arg:1} => {arg:1}

Observed Behavior

Main.f
...
Compiled: \ {arg:1} => case {arg:1} of
  { Main.Bar.Nil {tag = 0} => Main.Foo.Nil {tag = 0}
  ; Main.Bar.ConsL {tag = 1} {e:2} => Main.Foo.ConsL {tag = 1} (Main.f {e:2})
  ; Main.Bar.ConsR {tag = 2} {e:5} => Main.Foo.ConsR {tag = 2} (Main.f {e:5})
  }

[ohad]

If we make Path and PathIn 2-constructor datatypes (e.g., by only going left), the Identity optimisation kicks in:

public export
data Tree : Type where
  Leaf : Tree
  Node : Tree -> Tree -> Tree

namespace Foo
  public export
  data Path : Type where
    Nil : Path
    ConsL : Path -> Path
--    ConsR : Path -> Path


namespace Bar
  public export
  data PathIn : Tree -> Type where
    Nil : PathIn Leaf
    ConsL : PathIn lft -> PathIn (Node lft rgt)
--    ConsR : PathIn rgt -> PathIn (Node lft rgt)

-- Expecting identity transformation to kick in
f : PathIn tree -> Path
f [] = []
f (ConsL t) = ConsL (f t)
--f (ConsR t) = ConsR (f t)

> :di f
Compiled: \ {arg:1} => {arg:1}

[ohad]

Good place to start is this point

[ohad]

Another example from @dunhamsteve:

data Tree = Node Int Tree Tree | Leaf
data Tree2 = Node2 Int Tree2 Tree2 | Leaf2

convert : Tree -> Tree2
convert (Node x y z) = Node2 x (convert y) (convert z)
convert Leaf = Leaf2

taking the Int out makes the optimisation kick in