anoma / juvix

A language for intent-centric and declarative decentralised applications
https://docs.juvix.org
GNU General Public License v3.0
442 stars 54 forks source link

Juvix typecheck runs into an infinite loop #2866

Open heueristik opened 3 days ago

heueristik commented 3 days ago

Description

The juvix typechecker freezes when

Systemn

To Reproduce

  1. Remove the square brackets

    create (self : KeyPair) (tokenLabel : Label) (amount : Nat) (receiver : PublicKey) : Transaction :=
    let
    myself : PublicKey := KeyPair.pubKey self;
    in
    Internal.mkTransaction
      (KeyPair.privKey self)
    ---   [(Internal.mkToken true amount tokenLabel mkData@{owner := myself; previousOwner := myself})]
    +++   (Internal.mkToken true amount tokenLabel mkData@{owner := myself; previousOwner := myself})
      [(Internal.mkToken false amount tokenLabel mkData@{owner := receiver; previousOwner := myself})];

    in https://github.com/anoma/anoma-apps/blob/9cfc2011d0706ddc81f69da38d4ecfd1250df1d8/Token/Token.juvix#L19.

  2. Run the typechecker with juvix typecheck Token.juvix.

  3. See the terminal not terminating.

    [133 of 134] Compiling /Users/michaelheuer/Projects/Anoma/apps/anoma-apps/Token/Internal.juvix             
    [134 of 134] Compiling /Users/michaelheuer/Projects/Anoma/apps/anoma-apps/Token/Token.juvix

The bug can be reproduced by making the following change to the code https://github.com/anoma/anoma-apps/blob/9cfc2011d0706ddc81f69da38d4ecfd1250df1d8/Token/Token.juvix#L25

--- createKudos (self : KeyPair) (amount : Nat) (receiver : PublicKey) : Transaction :=
+++ createKudos (self : KeyPair) (amount : Nat) (receiver : PublicKey) : Maybe Transaction :=
     create self (mkKudosLabel (KeyPair.pubKey self)) amount receiver;

Expected behavior

The typechecker should throw a type error demanding List Nat instead of Nat as a function argument.

Screenshots

Bildschirmfoto 2024-06-28 um 10 42 37