Typechecker gets stuck in infinite loop on recursive type definition using Set

[heueristik]

The typechecker hangs (persumably because of an infinite loop) when checking the following recursive type definition.
MWE.juvix

module MWE;

import Data.Set as Set open using {Set};

type Foo :=
  | Bar
  | Baz (Set Foo);

Note that | Baz (List Foo); or | Baz Foo; works.

I am using Juvix v0.6.6-e4559bb and the following Package.juvix

module Package;

import PackageDescription.V2 open;

package : Package :=
  defaultPackage@?{
    dependencies :=
      [github "anoma" "juvix-stdlib" "v0.7.0"; github "anoma" "juvix-containers" "v0.15.0"]
  };

Steps to reproduce.

1. Create a project directory with MWE.juvix and Package.juvix inside.
2. Run juvix clean --global && juvix clean && juvix dependencies update
3. Run juvix typecheck MWE.juvix
4. Observe the command not terminating

 juvix typecheck MWE.juvix                                        
[Dependency stdlib 0.0.1] [1 of 54] Compiling Stdlib.Trait.DivMod
[Dependency stdlib 0.0.1] [2 of 54] Compiling Stdlib.Data.Fixity
[Dependency stdlib 0.0.1] [3 of 54] Compiling Stdlib.Data.Maybe.Base
[Dependency stdlib 0.0.1] [4 of 54] Compiling Stdlib.Data.Nat.Base
[Dependency stdlib 0.0.1] [5 of 54] Compiling Stdlib.Data.Pair.Base
[Dependency stdlib 0.0.1] [6 of 54] Compiling Stdlib.Data.Bool.Base
[Dependency stdlib 0.0.1] [7 of 54] Compiling Stdlib.System.IO.Base
[Dependency stdlib 0.0.1] [8 of 54] Compiling Stdlib.Trait.FromNatural
[Dependency stdlib 0.0.1] [9 of 54] Compiling Stdlib.Trait.Natural
[Dependency stdlib 0.0.1] [10 of 54] Compiling Stdlib.Data.Int.Base
[Dependency stdlib 0.0.1] [11 of 54] Compiling Stdlib.Data.Byte.Base
[Dependency stdlib 0.0.1] [12 of 54] Compiling Stdlib.Trait.Eq
[Dependency stdlib 0.0.1] [13 of 54] Compiling Stdlib.Trait.Ord
[Dependency stdlib 0.0.1] [14 of 54] Compiling Stdlib.Function
[Dependency stdlib 0.0.1] [15 of 54] Compiling Stdlib.Data.Nat.Ord
[Dependency stdlib 0.0.1] [16 of 54] Compiling Stdlib.Trait.Integral
[Dependency stdlib 0.0.1] [17 of 54] Compiling Stdlib.Data.Field.Base
[Dependency stdlib 0.0.1] [18 of 54] Compiling Stdlib.Data.Int.Ord
[Dependency stdlib 0.0.1] [19 of 54] Compiling Stdlib.Trait.Numeric
[Dependency stdlib 0.0.1] [20 of 54] Compiling Stdlib.Data.List.Base
[Dependency stdlib 0.0.1] [21 of 54] Compiling Stdlib.Trait.Foldable.Polymorphic
[Dependency stdlib 0.0.1] [22 of 54] Compiling Stdlib.Data.Result.Base
[Dependency stdlib 0.0.1] [23 of 54] Compiling Stdlib.Trait.Foldable.Monomorphic
[Dependency stdlib 0.0.1] [24 of 54] Compiling Stdlib.Trait.Foldable
[Dependency stdlib 0.0.1] [25 of 54] Compiling Stdlib.Data.String.Base
[Dependency stdlib 0.0.1] [26 of 54] Compiling Stdlib.Trait.Show
[Dependency stdlib 0.0.1] [27 of 54] Compiling Stdlib.Debug.Fail
[Dependency stdlib 0.0.1] [28 of 54] Compiling Stdlib.Data.Nat
[Dependency stdlib 0.0.1] [29 of 54] Compiling Stdlib.Data.Unit.Base
[Dependency stdlib 0.0.1] [30 of 54] Compiling Stdlib.Data.Bool
[Dependency stdlib 0.0.1] [31 of 54] Compiling Stdlib.Data.Pair
[Dependency stdlib 0.0.1] [32 of 54] Compiling Stdlib.Trait.Partial
[Dependency stdlib 0.0.1] [33 of 54] Compiling Stdlib.Data.Unit
[Dependency stdlib 0.0.1] [34 of 54] Compiling Stdlib.Data.Field
[Dependency stdlib 0.0.1] [35 of 54] Compiling Stdlib.Data.Byte
[Dependency stdlib 0.0.1] [36 of 54] Compiling Stdlib.Data.Range
[Dependency stdlib 0.0.1] [37 of 54] Compiling Stdlib.Data.String.Ord
[Dependency stdlib 0.0.1] [38 of 54] Compiling Stdlib.Data.String
[Dependency stdlib 0.0.1] [39 of 54] Compiling Stdlib.System.IO.String
[Dependency stdlib 0.0.1] [40 of 54] Compiling Stdlib.Data.Int
[Dependency stdlib 0.0.1] [41 of 54] Compiling Stdlib.System.IO.Nat
[Dependency stdlib 0.0.1] [42 of 54] Compiling Stdlib.System.IO.Bool
[Dependency stdlib 0.0.1] [43 of 54] Compiling Stdlib.Trait.Functor.Polymorphic
[Dependency stdlib 0.0.1] [44 of 54] Compiling Stdlib.System.IO.Int
[Dependency stdlib 0.0.1] [45 of 54] Compiling Stdlib.System.IO
[Dependency stdlib 0.0.1] [46 of 54] Compiling Stdlib.Trait.Functor.Monomorphic
[Dependency stdlib 0.0.1] [47 of 54] Compiling Stdlib.Trait.Functor
[Dependency stdlib 0.0.1] [48 of 54] Compiling Stdlib.Trait.Applicative
[Dependency stdlib 0.0.1] [49 of 54] Compiling Stdlib.Trait.Monad
[Dependency stdlib 0.0.1] [50 of 54] Compiling Stdlib.Trait
[Dependency stdlib 0.0.1] [51 of 54] Compiling Stdlib.Data.Maybe
[Dependency stdlib 0.0.1] [52 of 54] Compiling Stdlib.Data.List
[Dependency stdlib 0.0.1] [53 of 54] Compiling Stdlib.Data.Result
[Dependency stdlib 0.0.1] [54 of 54] Compiling Stdlib.Prelude
[Dependency containers 0.15.0] [1 of 4] Compiling Data.Tmp
[Dependency containers 0.15.0] [2 of 4] Compiling Data.Tree
[Dependency containers 0.15.0] [3 of 4] Compiling Data.Set.AVL
[Dependency containers 0.15.0] [4 of 4] Compiling Data.Set
[1 of 1] Compiling MWE

[lukaszcz]

Strange, because it works with e.g. List instead of Set. Running even juvix dev parse MWE.juvix results in an infinite loop. However, it seems like dev parse is doing more than it should (I got it to complain about identifiers not in scope).

[janmasrovira]

I've been able to minimize the example a bit.

Typechecking the code bellow hangs. However:

1. if the import is removed, it typechecks.
2. if the node constructor definitions is changed to node (AVLTree A), it typechecks.

I'll continue investigating.

module main;

import Stdlib.Prelude;

type AVLTree (A : Type) :=
  | node (AVLTree A) (AVLTree A);

type Foo :=
 | Baz (AVLTree Foo);

[lukaszcz]

I'm not sure what's happening in our positivity checker, but it definitely should not be instantiating type variables with arbitrary available types. The running time should depend only on the types (recursively) referenced in the inductive definition.

Here is a formal specification of the positivity condition for Coq: https://coq.inria.fr/doc/V8.20.0/refman/language/core/inductive.html#well-formed-inductive-definitions

In the above example, to check positivity of Foo, one needs to check only that Foo occurs strictly positively in the types of the arguments of node for the instantiation AVLTree_Foo = AVLTree Foo. But when instantiating a recursively uniform parameter A we should actually remove it from the list of parameters of AVLTree, in contrast to what's written on the linked webpage. So you actually need to check that AVLTree_Foo -> AVLTree_Foo -> AVLTree_Foo satisfies the positivity condition for Foo which is trivially true, because Foo doesn't occur in the type.