Juvix compiler crash: permutation should have at least one element

[lukaszcz]

Compiling

module Interpreter;

import Stdlib.Prelude open;

type Expression :=
  -- Put both of these into a Const type
  | Const Nat
  | Str String
  | Var String
  | Lam String Expression
  | App Expression Expression;

axiom undefined : {A : Type} -> A;

Environment : Type := List (Pair String Expression) ;

type Return :=
  | RNatural Nat
  | RString String;


eval (env : Environment) : Expression -> Maybe Return
  | (Const x) := RNatural x          |> just
  | (Str str) := RString str         |> just
  | (Lam n e) := RString "Function"  |> just
  | (App f x) := eval-lookup env f x
  | (Var var) := lookup-var env var
  | _ := undefined;

eval-lookup (env : Environment) (f : Expression) (x : Expression) : Maybe Return :=
  let recursive : _ -- Expression -> Return
      | (Lam variable body) := eval ((variable , x) :: env) body
      | _ := undefined;
  in recursive f;

lookup-var (env : Environment) (to-lookup : String) : Maybe Return
  := find \{ x := x == to-lookup } env >>= eval env;

foo : Nat := 888;

results in

juvix: The permutation should have one element at least!
CallStack (from HasCallStack):
  error, called at src/Juvix/Prelude/Base/Foundation.hs:484:9 in juvix-0.6.6-8nbo1zrgYROKfeHQOHuYy0:Juvix.Prelude.Base.Foundation
  error, called at src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Termination/LexOrder.hs:156:17 in juvix-0.6.6-8nbo1zrgYROKfeHQOHuYy0:Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.LexOrder