Add check for number of type variables in type signature (#512)

* Fix tvar string generation

* Add check for number of tvars in a single type signature

The number of tvars is limited by serialization (u8) to 255

* Added a comment in CHANGELOG

* Docs fixes

* Adding docs about the limitation on number of tvars

* Limit is 256, not 255

* Update CHANGELOG.md

Co-authored-by: Gaith Hallak <gaithhallak@gmail.com>

---------

Co-authored-by: Gaith Hallak <gaithhallak@gmail.com>

CHANGELOG.md

@@ -6,6 +6,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [Unreleased]
 ### Added
+- Added a check for number of type variables in a type signature; it is serialized using 8 bits,
+  so the upper limit is 256.
 ### Changed
 ### Removed
 

docs/sophia_features.md

@@ -295,6 +295,11 @@ of `A`.
 - When a user-defined type `t('a)` is invariant in `'a`, then `t(A)` can never be
 a subtype of `t(B)`.
 
+#### Type variable limitation
+
+Because of how FATE represents types as values there is a fixed upper limit (256)
+of type variables that can be used in a single type signature.
+
 ## Mutable state
 
 Sophia does not have arbitrary mutable state, but only a limited form of state

docs/sophia_syntax.md

@@ -267,11 +267,11 @@ UnOp  ::= '-' | '!' | 'bnot'
 | Operators | Type
 | --- | ---
 | `-` `+` `*` `/` `mod` `^` | arithmetic operators
-| `!` `&&` `||` | logical operators
+| `!` `&&` `\|\|` | logical operators
 | `band` `bor` `bxor` `bnot` `<<` `>>` | bitwise operators
 | `==` `!=` `<` `>` `=<` `>=` | comparison operators
 | `::` `++` | list operators
-| `|>` | functional operators
+| `\|>` | functional operators
 
 ## Operator precedence
 
@@ -291,5 +291,5 @@ In order of highest to lowest precedence.
 | `bxor` | left
 | `bor` | left
 | `&&` | right
-| `||` | right
-| `|>` | left
+| `\|\|` | right
+| `\|>` | left

src/aeso_ast_infer_types.erl

@@ -1760,8 +1760,27 @@ desugar_clauses(Ann, Fun, {type_sig, _, _, _, ArgTypes, RetType}, Clauses) ->
     end.
 
 print_typesig({Name, TypeSig}) ->
+    assert_tvars(Name, TypeSig),
     ?PRINT_TYPES("Inferred ~s : ~s\n", [Name, pp(TypeSig)]).
 
+assert_tvars(Name, TS) ->
+    TVars = assert_tvars_(TS, #{}),
+    case maps:size(TVars) > 256 of
+        true ->
+            type_error({too_many_tvars, Name, TS});
+        false ->
+            ok
+    end.
+
+assert_tvars_({tvar, _, TV}, TVars) ->
+    TVars#{TV => ok};
+assert_tvars_(T, TVars) when is_tuple(T) ->
+    assert_tvars_(tuple_to_list(T), TVars);
+assert_tvars_(Ts, TVars) when is_list(Ts) ->
+    lists:foldl(fun(T, TVars1) -> assert_tvars_(T, TVars1) end, TVars, Ts);
+assert_tvars_(_, TVars) ->
+    TVars.
+
 arg_type(ArgAnn, {id, Ann, "_"}) ->
     case aeso_syntax:get_ann(origin, Ann, user) of
         system -> fresh_uvar(ArgAnn);
@@ -3389,7 +3408,7 @@ instantiate1(X) ->
 integer_to_tvar(X) when X < 26 ->
     [$a + X];
 integer_to_tvar(X) ->
-    [integer_to_tvar(X div 26)] ++ [$a + (X rem 26)].
+    integer_to_tvar(X div 26 - 1) ++ [$a + (X rem 26)].
 
 %% Warnings
 
@@ -3776,6 +3795,9 @@ mk_error({type_decl, _, {id, Pos, Name}, _}) ->
     Msg = io_lib:format("Empty type declarations are not supported. Type `~s` lacks a definition",
                         [Name]),
     mk_t_err(pos(Pos), Msg);
+mk_error({too_many_tvars, Name, {type_sig, Pos, _, _, _, _}}) ->
+    Msg = io_lib:format("Too many type variables (max 256) in definition of `~s`", [Name]),
+    mk_t_err(pos(Pos), Msg);
 mk_error({stateful_not_allowed, Id, Fun}) ->
     Msg = io_lib:format("Cannot reference stateful function `~s` in the definition of non-stateful function `~s`.",
                         [pp(Id), pp(Fun)]),

test/aeso_compiler_tests.erl

@@ -1302,6 +1302,10 @@ failing_contracts() ->
                    <<?Pos(3,9)
                      "The name of the compile-time constant cannot have pattern matching">>
                   ])
+    , ?TYPE_ERROR(too_many_tvars,
+                  [<<?Pos(2,3)
+                     "Too many type variables (max 256) in definition of `too_many`">>
+                  ])
     ].
 
 validation_test_() ->

test/contracts/too_many_tvars.aes

@@ -0,0 +1,60 @@
+contract C =
+  entrypoint too_many(
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _, _, _, _, _),
+
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _, _, _, _, _),
+
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _, _, _, _, _)) = 0
+
+  entrypoint not_too_many(
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _, _, _, _, _),
+
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _, _, _, _, _),
+
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _, _, _, _, _),
+      (_, _, _, _, _, _)) = 0