Case tree is not strict enough, hard crash on scheme eval

[gallais]

I haven't tested it with yaffle (wrong laptop atm) but this is concerning:

%default total

boom : Nat === List () -> List ()
boom = \ eq => (replace {p = id} eq 3) ++ [()]

The compile time case tree for replace is to just return its 5th argument. And so boom reduces to \eq => 3 ++ [()] at compile time and, even worse, evaluating boom after :set eval scheme will lead to a crash:

Exception in vector-ref: 4 is not a valid index for #(1 1016 () #(1 1016 () #(1 1016 () #(...))))

To be safe evaluation in open contexts does need to be strict on some runtime irrelevant values and get stuck on them. In this instance the compile time case tree for replace should be strict on the equality proof.

[gallais]

I tried to play the same game with Acc but luckily in that case the tree is strict and so we don't end up with an infinite loop when typechecking test (Refl is correctly rejected).

%default total

data Acc : (a -> a -> Type) -> a -> Type where
  MkAcc : ((y : a) -> lt y x -> Acc lt y) -> Acc lt x

data LT : Nat -> Nat -> Type where
  Z : LT Z (S n)
  S : LT m n -> LT (S m) (S n)

ltS : (m : Nat) -> LT m (S m)
ltS Z = Z
ltS (S m) = S (ltS m)

oops : (m : Nat) -> (0 _ : Acc (flip LT) m) -> Nat
oops m (MkAcc f) = oops (S m) (f (S m) (ltS m))

test : (lie : Acc (flip LT) Z) -> Z === oops Z lie
test lie = Refl

[CodingCellist]

Seems to partially repro on the latest Yaffle:

$ yaffle Issue3023.yaff
[...] Version 0.8.0-5b89c7ed6

1/1: Building Issue3023 (Issue3023.yaff)

Issue3023> boom
\eq => 3 ++ [()]

Issue3023> :set showtypes
Issue3023> boom (believe_me 3)
3 ++ [()] : List ()

I say "partially" because:

Issue3023> :set eval scheme
[scheme] Issue3023> boom
Scheme evaluator not implemented

Debug info

Issue3023> :di boom
Issue3023.boom
Compile time tree: \eq => replace eq 3 ++ [()]
Detaggable arg types: [0]
Compiled: \ eq => Prelude.Types.List.tailRecAppend
3
(Prelude.Basics.(::) {tag = 1} [cons]
(Builtin.MkUnit {tag = 0} [unit])
(Prelude.Basics.Nil {tag = 0} [nil]))
Refers to: Prelude.Basics.id, Prelude.Basics.Nil, Prelude.Basics.List, Prelude.Basics.(::), Builtin.replace, Builtin.Unit, Builtin.MkUnit, Builtin.Equal, Prelude.Types.Z, Prelude.Types.S, Prelude.Types.Nat, Prelude.Types.List.(++)
Refers to (runtime): Prelude.Basics.Nil, Prelude.Basics.(::), Builtin.MkUnit, Prelude.Types.List.tailRecAppend
Flags: total
Size change: Prelude.Types.List.(++): [Nothing, Nothing, Nothing], Builtin.replace: [Nothing, Nothing, Nothing, Nothing, Just (0, Same), Nothing], Prelude.Basics.id: [Nothing, Nothing]