Slow chez startup times depending on case ordering in function

[alexhumphreys]

Self contained gist

Steps to Reproduce

run idris2 CodeGen.idr --client ':di someFunc' | wc -c for the following file (sorry it's still a bit long):

data Value
  = VLambda
  | VHLam
  | VPi
  | VHPi String Value (Value -> Value)
  | VEquivalent Value Value
  | VAssert Value
  | VConst
  | VBool
  | VBoolLit
  | VInteger
  | VListFold Value Value Value Value Value
  | VText
  | VTextLit
  | VOptional Value
  | VRecord Value
  | VRecordLit Value
  | VUnion (Maybe Value)
  | VInject (Maybe Value) (Maybe Value)
  | VPrimVar

someFunc : List a -> Value -> Value -> Either String Value
-- someFunc xs _ (VListFold y z w v s) = Right VBool -- $ idris2 CodeGen.idr --client ':di someFunc' | wc -c # 9037
someFunc xs VPi VLambda = Right VBool
someFunc xs VInteger VHLam = Right VBool
someFunc xs VPi VPi = Right VBool
someFunc xs VBool (VHPi y z f) = Right VBool
someFunc xs VBool (VEquivalent y z) = Right VBool
someFunc xs VPi (VAssert y) = Right VBool
someFunc xs VTextLit VConst = Right VBool
someFunc xs VPrimVar VBool = Right VBool
someFunc xs VPi VBoolLit = Right VBool
someFunc xs VPi (VOptional y) = Right VBool
someFunc xs VPrimVar (VUnion a) = Right VBool
-- someFunc xs VPi (VListFold y z w v s) = Right VBool -- $ idris2 CodeGen.idr --client ':di someFunc' | wc -c # 8977
someFunc xs _ (VListFold y z w v s) = Right VBool -- $ idris2 CodeGen.idr --client ':di someFunc' | wc -c # 34987
someFunc xs VBool VTextLit = Right VBool
someFunc xs VPi (VInject x y) = Right VBool
someFunc xs VPrimVar (VOptional y) = Right VBool
someFunc xs VText (VUnion y) = Right VBool
someFunc xs VPi VText = Right VBool
someFunc xs VText VTextLit = Right VBool
someFunc xs VBool (VOptional y) = Right VBool
someFunc xs VPi (VRecord y) = Right VBool
someFunc xs VPrimVar (VRecordLit y) = Right VBool
someFunc xs VPi (VUnion y) = Right VBool
someFunc xs x (VInject y z) = Right VBool
someFunc xs x VPrimVar = Right VBool
-- someFunc xs _ (VListFold y z w v s) = Right VBool -- $ idris2 CodeGen.idr --client ':di someFunc' | wc -c # 10423
someFunc xs _ _ = Left "whatever"

There are 4 cases someFunc xs _ (VListFold y z w v s) in someFunc, one at the start, one at the middle and one at the end. Uncomment each one in turn and run idris2 CodeGen.idr --client ':di someFunc' | wc -c for each.

Expected Behavior

Similar sized chez output.

Observed Behavior

When the someFunc xs _ (VListFold y z w v s) is in the middle of the function, the outputted chez size increases by a factor of about 4 compared to if that case is at the start or the end. It seems to be caused by the _ match, because when an actual Value is matched on it goes back to similar values to the others.

Notes

This is a contrived example, and output size isn't the metric I care about, but I ran into in the wild this PR, where my tests slowed down from 15s to 40s based on where the case was in a function. There's more details at the PR, but the tests once they were running seemed just as fast, so it looks like the chez startup time increased as a result of the much larger output sizes.

Since this example is small it won't show the slow startup times, hence why I concentrated on output size, but the example at the certainly PR exhibits this behaviour.

[gallais]

The case tree generated by Idris directly depends on the order in which the patterns are spelt out. If you spell out stricter patterns first that may lead to a lot of duplicated code in the "catchall" branches.

These RHS should perhaps be let-bound first so that the code can be shared.

[alexhumphreys]

Not sure I understand what you mean: Is let binding on RHS something I can do, or would that be a change to how the idris compiler handles pattern matching?

[gallais]

No, I mean in the generated code: when the same RHS is used for multiple branches of the case generated tree, we may want to introduce them as separate auxiliary definitions to avoid code duplication.