It is possible to bypass the termination checker by using instances

[janmasrovira]

Running juvix eval loop.juvix does not terminate.

module loop;

import Stdlib.Prelude open;

trait
type HasNat (A : Type) :=
  mkHasNat@{
    getNat : Nat;
  };

instance
Nat-HasNatI : HasNat Nat :=
  mkHasNat@{
    getNat : Nat := HasNat.getNat {Nat};
  };

main : Nat := HasNat.getNat {Nat};