Add constraints to typechecker, fix old tests, add new ones

priv/stdlib/List.aes

@@ -29,9 +29,11 @@ namespace List =
     []   => abort("drop_last_unsafe: list empty")
 
 
-  function contains(e : 'a, l : list('a)) = switch(l)
+  function
-    []   => false
+    contains : 'a is eq; ('a, list('a)) => bool
-    h::t => h == e || contains(e, t)
+    contains(e, l) = switch(l)
+      []   => false
+      h::t => h == e || contains(e, t)
 
 /** Finds first element of `l` fulfilling predicate `p` as `Some` or `None`
  * if no such element exists.

priv/stdlib/Option.aes

@@ -30,7 +30,9 @@ namespace Option =
     None    => abort(err)
     Some(x) => x
 
-  function contains(e : 'a, o : option('a)) = o == Some(e)
+  function
+    contains : 'a is eq; ('a, option('a)) => bool
+    contains(e, o) = o == Some(e)
 
   function on_elem(o : option('a), f : 'a => unit) : unit = match((), f, o)
 

priv/stdlib/String.aes

@@ -90,6 +90,7 @@ namespace String =
           Some(ix)
 
   private function
+    is_prefix : (list(char), list(char)) => option(list(char))
     is_prefix([], ys) = Some(ys)
     is_prefix(_, [])  = None
     is_prefix(x :: xs, y :: ys) =

src/aeso_ast_infer_types.erl

@@ -818,6 +818,12 @@ infer(Contracts, Options) ->
         ets_new(defined_contracts, [bag]),
         ets_new(type_vars, [set]),
         ets_new(warnings, [bag]),
+
+        %% Set the constraints for the builtin types
+        ets_new(ord_constraint_types, [set]),
+        OrdTypes = [ {"int"}, {"bool"}, {"bits"}, {"char"}, {"string"}, {"list"}, {"option"} ],
+        ets_insert(ord_constraint_types, OrdTypes),
+
         when_warning(warn_unused_functions, fun() -> create_unused_functions() end),
         check_modifiers(Env, Contracts),
         create_type_errors(),
@@ -1177,6 +1183,15 @@ check_modifiers1(What, Decl) when element(1, Decl) == letfun; element(1, Decl) =
     ok;
 check_modifiers1(_, _) -> ok.
 
+-spec extract_typevars(utype()) -> [aeso_syntax:tvar()].
+extract_typevars(Type) ->
+    case Type of
+        TVar = {tvar, _, _}    -> [TVar];
+        Tup when is_tuple(Tup) -> extract_typevars(tuple_to_list(Tup));
+        [H | T]                -> extract_typevars(H) ++ extract_typevars(T);
+        _                      -> []
+    end.
+
 -spec check_type(env(), aeso_syntax:type()) -> aeso_syntax:type().
 check_type(Env, T) ->
     check_type(Env, T, 0).
@@ -1219,6 +1234,13 @@ check_type(Env, Type = {fun_t, Ann, NamedArgs, Args, Ret}, Arity) ->
 check_type(_Env, Type = {uvar, _, _}, Arity) ->
     ensure_base_type(Type, Arity),
     Type;
+check_type(Env, {constrained_t, Ann, Constraints, Type}, Arity) ->
+    when_warning(warn_duplicated_constraints, fun() -> warn_duplicated_constraints(Constraints) end),
+    TVars = [ Name || {tvar, _, Name} <- extract_typevars(Type) ],
+    [ type_error({unused_constraint, C}) || C = {constraint, _, {tvar, _, Name}, _} <- Constraints,
+                                            not lists:member(Name, TVars) ],
+
+    {constrained_t, Ann, Constraints, check_type(Env, Type, Arity)};
 check_type(_Env, {args_t, Ann, Ts}, _) ->
     type_error({new_tuple_syntax, Ann, Ts}),
     {tuple_t, Ann, Ts}.
@@ -1398,7 +1420,7 @@ infer_letfun(Env = #env{ namespace = Namespace }, LetFun = {letfun, Ann, Fun, _,
     {{Name, Sig}, Clause} = infer_letfun1(Env, LetFun),
     {{Name, Sig}, desugar_clauses(Ann, Fun, Sig, [Clause])}.
 
-infer_letfun1(Env0 = #env{ namespace = NS }, {letfun, Attrib, Fun = {id, NameAttrib, Name}, Args, What,  GuardedBodies}) ->
+infer_letfun1(Env0 = #env{ namespace = NS }, {letfun, Attrib, Fun = {id, NameAttrib, Name}, Args, What, GuardedBodies}) ->
     Env = Env0#env{ stateful = aeso_syntax:get_ann(stateful, Attrib, false),
                     current_function = Fun },
     {NewEnv, {typed, _, {tuple, _, TypedArgs}, {tuple_t, _, ArgTypes}}} = infer_pattern(Env, {tuple, [{origin, system} | NameAttrib], Args}),
@@ -1943,10 +1965,16 @@ infer_infix({IntOp, As})
     Int = {id, As, "int"},
     {fun_t, As, [], [Int, Int], Int};
 infer_infix({RelOp, As})
-  when RelOp == '=='; RelOp == '!=';
+  when RelOp == '=='; RelOp == '!=' ->
-       RelOp == '<';  RelOp == '>';
+    T = fresh_uvar(As),
+    add_constraint({is_eq, T}),
+    Bool = {id, As, "bool"},
+    {fun_t, As, [], [T, T], Bool};
+infer_infix({RelOp, As})
+  when RelOp == '<';  RelOp == '>';
        RelOp == '<='; RelOp == '=<'; RelOp == '>=' ->
-    T = fresh_uvar(As),     %% allow any type here, check in the backend that we have comparison for it
+    T = fresh_uvar(As),
+    add_constraint({is_ord, T}),
     Bool = {id, As, "bool"},
     {fun_t, As, [], [T, T], Bool};
 infer_infix({'..', As}) ->
@@ -2016,7 +2044,8 @@ next_count() ->
 
 ets_tables() ->
     [options, type_vars, constraints, freshen_tvars, type_errors,
-     defined_contracts, warnings, function_calls, all_functions].
+     defined_contracts, warnings, function_calls, all_functions,
+     ord_constraint_types].
 
 clean_up_ets() ->
     [ catch ets_delete(Tab) || Tab <- ets_tables() ],
@@ -2178,11 +2207,16 @@ destroy_and_report_unsolved_constraints(Env) ->
                            (#named_argument_constraint{}) -> true;
                            (_)                            -> false
                         end, OtherCs2),
-    {BytesCs, []} =
+    {BytesCs, OtherCs4} =
         lists:partition(fun({is_bytes, _})              -> true;
                            ({add_bytes, _, _, _, _, _}) -> true;
                            (_)                          -> false
                         end, OtherCs3),
+    {TVarsCs, []} =
+        lists:partition(fun({is_eq, _})              -> true;
+                           ({is_ord, _}) -> true;
+                           (_)                          -> false
+                        end, OtherCs4),
 
     Unsolved = [ S || S <- [ solve_constraint(Env, dereference_deep(C)) || C <- NamedArgCs ],
                       S == unsolved ],
@@ -2200,6 +2234,7 @@ destroy_and_report_unsolved_constraints(Env) ->
     check_record_create_constraints(Env, CreateCs),
     check_is_contract_constraints(Env, ContractCs),
     check_bytes_constraints(Env, BytesCs),
+    check_tvars_constraints(Env, TVarsCs),
 
     destroy_constraints().
 
@@ -2329,6 +2364,33 @@ check_bytes_constraint(Env, {add_bytes, Ann, Fun, A0, B0, C0}) ->
         _ -> type_error({unsolved_bytes_constraint, Ann, Fun, A, B, C})
     end.
 
+%% -- Typevars constraints --
+
+check_tvars_constraints(Env, Constraints) ->
+    [ check_tvars_constraint(Env, C) || C <- Constraints ].
+
+check_tvars_constraint(Env, {is_eq, Type = {uvar, Ann, _}}) ->
+    Type1 = unfold_types_in_type(Env, instantiate(Type)),
+    type_is_eq(Type1) orelse type_error({type_not_eq, Ann, Type1});
+check_tvars_constraint(Env, {is_ord, Type = {uvar, Ann, _}}) ->
+    Type1 = unfold_types_in_type(Env, instantiate(Type)),
+    type_is_ord(Type1) orelse type_error({type_not_ord, Ann, Type1}).
+
+type_is_ord({app_t, _, Id, Ts}) -> type_is_ord(Id) andalso lists:all(fun type_is_ord/1, Ts);
+type_is_ord({tuple_t, _, Ts}) -> lists:all(fun type_is_ord/1, Ts);
+type_is_ord({bytes_t, _, _}) -> true;
+type_is_ord({constrained_t, _, Constraints, {tvar, _, _}}) -> lists:keyfind("ord", 3, Constraints) =/= false;
+type_is_ord({id, _, Id}) -> ets_lookup(ord_constraint_types, Id) =/= [];
+type_is_ord(_) -> false.
+
+type_is_eq({app_t, _, Id, Ts}) -> type_is_eq(Id) andalso lists:all(fun type_is_eq/1, Ts);
+type_is_eq({con, _, _}) -> true;
+type_is_eq({qcon, _, _}) -> true;
+type_is_eq({id, _, _}) -> true;
+type_is_eq({qid, _, _}) -> true;
+type_is_eq({constrained_t, _, Constraints, {tvar, _, _}}) -> lists:keyfind("eq", 3, Constraints) =/= false;
+type_is_eq(T) -> type_is_ord(T).
+
 %% -- Field constraints --
 
 check_record_create_constraints(_, []) -> ok;
@@ -2582,6 +2644,7 @@ unify1(_Env, {uvar, A, R}, T, When) ->
 unify1(Env, T, {uvar, A, R}, When) ->
     unify1(Env, {uvar, A, R}, T, When);
 unify1(_Env, {tvar, _, X}, {tvar, _, X}, _When) -> true; %% Rigid type variables
+unify1(_Env, {constrained_t, _, Cs, {tvar, _, X}}, {constrained_t, _, Cs, {tvar, _, X}}, _When) -> true;
 unify1(Env, [A|B], [C|D], When) ->
     unify(Env, A, C, When) andalso unify(Env, B, D, When);
 unify1(_Env, X, X, _When) ->
@@ -2617,6 +2680,10 @@ unify1(Env, {tuple_t, _, As}, {tuple_t, _, Bs}, When)
 unify1(Env, {named_arg_t, _, Id1, Type1, _}, {named_arg_t, _, Id2, Type2, _}, When) ->
     unify1(Env, Id1, Id2, {arg_name, Id1, Id2, When}),
     unify1(Env, Type1, Type2, When);
+unify1(Env, {constrained_t, _, Constraints, Type1 = {fun_t, _, _, _, _}}, Type2, When) ->
+    unify1(Env, constrain_tvars(Type1, Constraints), Type2, When);
+unify1(Env, Type1, {constrained_t, _, Constraints, Type2 = {fun_t, _, _, _, _}}, When) ->
+    unify1(Env, Type1, constrain_tvars(Type2, Constraints), When);
 %% The grammar is a bit inconsistent about whether types without
 %% arguments are represented as applications to an empty list of
 %% parameters or not. We therefore allow them to unify.
@@ -2628,6 +2695,28 @@ unify1(_Env, A, B, When) ->
     cannot_unify(A, B, When),
     false.
 
+%% Propagate the constraints to their corresponding type vars
+-spec constrain_tvars(utype() | [utype()], [constraint()]) -> utype().
+constrain_tvars(Types, Constraints)
+  when is_list(Types) ->
+    [ constrain_tvars(Type, Constraints) || Type <- Types ];
+constrain_tvars({fun_t, Ann, NamedArgs, ArgsT, RetT}, Constraints) ->
+    ConstrainedArgsT = constrain_tvars(ArgsT, Constraints),
+    ConstrainedRetT = constrain_tvars(RetT, Constraints),
+    {fun_t, Ann, NamedArgs, ConstrainedArgsT, ConstrainedRetT};
+constrain_tvars({app_t, Ann, AppT, ArgsT}, Constraints) ->
+    ConstrainedAppT = constrain_tvars(AppT, Constraints),
+    ConstrainedArgsT = constrain_tvars(ArgsT, Constraints),
+    {app_t, Ann, ConstrainedAppT, ConstrainedArgsT};
+constrain_tvars({tuple_t, Ann, ElemsT}, Constraints) ->
+    ConstrainedElemsT = constrain_tvars(ElemsT, Constraints),
+    {tuple_t, Ann, ConstrainedElemsT};
+constrain_tvars(TVar = {tvar, Ann, NameT}, Constraints) ->
+    TVarConstraints = [ C || {constraint, _, {tvar, _, NameC}, C} <- Constraints, NameT == NameC ],
+    {constrained_t, Ann, TVarConstraints, TVar};
+constrain_tvars(Type, _) ->
+    Type.
+
 dereference(T = {uvar, _, R}) ->
     case ets_lookup(type_vars, R) of
         [] ->
@@ -2655,6 +2744,7 @@ occurs_check1(_, {con, _, _}) -> false;
 occurs_check1(_, {qid, _, _}) -> false;
 occurs_check1(_, {qcon, _, _}) -> false;
 occurs_check1(_, {tvar, _, _}) -> false;
+occurs_check1(_, {constrained_t, _, _, _}) -> false;
 occurs_check1(_, {bytes_t, _, _}) -> false;
 occurs_check1(R, {fun_t, _, Named, Args, Res}) ->
     occurs_check(R, [Res, Named | Args]);
@@ -2771,7 +2861,8 @@ all_warnings() ->
     , warn_unused_functions
     , warn_shadowing
     , warn_division_by_zero
-    , warn_negative_spend ].
+    , warn_negative_spend
+    , warn_duplicated_constraints ].
 
 when_warning(Warn, Do) ->
     case lists:member(Warn, all_warnings()) of
@@ -2908,6 +2999,19 @@ warn_potential_negative_spend(Ann, Fun, Args) ->
         _ -> ok
     end.
 
+%% Warnings (Duplicated tvar constraints)
+
+warn_duplicated_constraints(Constraints) ->
+    warn_duplicated_constraints([], Constraints).
+
+warn_duplicated_constraints(_, []) -> ok;
+warn_duplicated_constraints(UniqueConstraints, [Constraint = {constraint, _, {tvar, _, Name1}, {id, _, Constr1}}| Rest]) ->
+    case [ C || C = {constraint, _, {tvar, _, Name2}, {id, _, Constr2}} <- UniqueConstraints,
+                Name1 == Name2 andalso Constr1 == Constr2 ] of
+        []       -> warn_duplicated_constraints([Constraint | UniqueConstraints], Rest);
+        [Unique] -> ets_insert(warnings, {duplicated_constraint, Constraint, Unique})
+    end.
+
 %% Save unification failures for error messages.
 
 cannot_unify(A, B, When) ->
@@ -3299,6 +3403,15 @@ mk_error({unknown_warning, Warning}) ->
 mk_error({empty_record_definition, Ann, Name}) ->
     Msg = io_lib:format("Empty record definitions are not allowed. Cannot define the record `~s`", [Name]),
     mk_t_err(pos(Ann), Msg);
+mk_error({type_not_eq, Ann, Type}) ->
+    Msg = io_lib:format("Values of type `~s` are not comparable by equality", [pp_type("", Type)]),
+    mk_t_err(pos(Ann), Msg);
+mk_error({type_not_ord, Ann, Type}) ->
+    Msg = io_lib:format("Values of type `~s` are not comparable by inequality", [pp_type("", Type)]),
+    mk_t_err(pos(Ann), Msg);
+mk_error({unused_constraint, {constraint, Ann, {tvar, _, Name}, _}}) ->
+    Msg = io_lib:format("The type variable `~s` is constrained but never used", [Name]),
+    mk_t_err(pos(Ann), Msg);
 mk_error(Err) ->
     Msg = io_lib:format("Unknown error: ~p", [Err]),
     mk_t_err(pos(0, 0), Msg).
@@ -3330,6 +3443,10 @@ mk_warning({division_by_zero, Ann}) ->
 mk_warning({negative_spend, Ann}) ->
     Msg = io_lib:format("Negative spend.", []),
     aeso_warnings:new(pos(Ann), Msg);
+mk_warning({duplicated_constraint, {constraint, Ann, {tvar, _, Name}, _}, {constraint, AnnFirst, _, _}}) ->
+    Msg = io_lib:format("The constraint on the type variable `~s` is a duplication of the constraint at ~s",
+                        [Name, pp_loc(AnnFirst)]),
+    aeso_warnings:new(pos(Ann), Msg);
 mk_warning(Warn) ->
     Msg = io_lib:format("Unknown warning: ~p", [Warn]),
     aeso_warnings:new(Msg).
@@ -3554,6 +3671,8 @@ pp({uvar, _, Ref}) ->
     ["?u" | integer_to_list(erlang:phash2(Ref, 16384)) ];
 pp({tvar, _, Name}) ->
     Name;
+pp(T = {constrained_t, _, _, {tvar, _, _}}) ->
+    prettypr:format(aeso_pretty:type(T));
 pp({if_t, _, Id, Then, Else}) ->
     ["if(", pp([Id, Then, Else]), ")"];
 pp({tuple_t, _, []}) ->

src/aeso_ast_to_fcode.erl

@@ -495,6 +495,8 @@ type_to_fcode(_Env, _Sub, {tvar, Ann, "void"}) ->
     fcode_error({found_void, Ann});
 type_to_fcode(_Env, Sub, {tvar, _, X}) ->
     maps:get(X, Sub, {tvar, X});
+type_to_fcode(Env, Sub, {constrained_t, _, _, TVar = {tvar, _, _}}) ->
+    type_to_fcode(Env, Sub, TVar);
 type_to_fcode(_Env, _Sub, {fun_t, Ann, _, var_args, _}) ->
     fcode_error({var_args_not_set, {id, Ann, "a very suspicious function"}});
 type_to_fcode(Env, Sub, {fun_t, _, Named, Args, Res}) ->

src/aeso_pretty.erl

@@ -284,7 +284,9 @@ type(T = {id, _, _})   -> name(T);
 type(T = {qid, _, _})  -> name(T);
 type(T = {con, _, _})  -> name(T);
 type(T = {qcon, _, _}) -> name(T);
-type(T = {tvar, _, _}) -> name(T).
+type(T = {tvar, _, _}) -> name(T);
+type({constrained_t, _, Cs, T}) ->
+    beside([name(T), text(" is "), tuple(lists:map(fun expr/1, Cs))]).
 
 -spec args_type([aeso_syntax:type()]) -> doc().
 args_type(Args) ->

test/aeso_compiler_tests.erl

@@ -265,7 +265,9 @@ warnings() ->
         "The function `called_unused_function2` is defined but never used.">>,
       <<?PosW(48, 5)
         "Unused return value.">>,
-      <<?PosW(60, 5)
+      <<?PosW(53, 44)
+        "The constraint on the type variable `'a` is a duplication of the constraint at line 53, column 34">>,
+      <<?PosW(65, 5)
         "The function `dec` is defined but never used.">>
      ]).
 
@@ -805,6 +807,82 @@ failing_contracts() ->
                      "to arguments\n"
                      "  `1 : int`">>
                   ])
+    , ?TYPE_ERROR(comparable_typevar_constraints,
+                  [<<?Pos(21,30)
+                     "Values of type `'a` are not comparable by equality">>,
+                   <<?Pos(25,37)
+                     "The type variable `'b` is constrained but never used">>,
+                   <<?Pos(56,56)
+                     "Values of type `address` are not comparable by inequality">>,
+                   <<?Pos(59,58)
+                     "Values of type `Chain.ttl` are not comparable by inequality">>,
+                   <<?Pos(62,45)
+                     "Values of type `A` are not comparable by inequality">>,
+                   <<?Pos(69,47)
+                     "Values of type `(int, char) => bool` are not comparable by inequality">>,
+                   <<?Pos(70,47)
+                     "Values of type `(int, char) => bool` are not comparable by equality">>,
+                   <<?Pos(85,71)
+                     "Values of type `list(address)` are not comparable by inequality">>,
+                   <<?Pos(88,77)
+                     "Values of type `option(address)` are not comparable by inequality">>,
+                   <<?Pos(91,76)
+                     "Values of type `(address * int)` are not comparable by inequality">>,
+                   <<?Pos(92,76)
+                     "Values of type `(address * int)` are not comparable by equality">>,
+                   <<?Pos(96,68)
+                     "Values of type `list((int, char) => bool)` are not comparable by inequality">>,
+                   <<?Pos(97,68)
+                     "Values of type `list((int, char) => bool)` are not comparable by equality">>,
+                   <<?Pos(99,74)
+                     "Values of type `option((int, char) => bool)` are not comparable by inequality">>,
+                   <<?Pos(100,74)
+                     "Values of type `option((int, char) => bool)` are not comparable by equality">>,
+                   <<?Pos(102,73)
+                     "Values of type `((int, char) => bool * int)` are not comparable by inequality">>,
+                   <<?Pos(103,73)
+                     "Values of type `((int, char) => bool * int)` are not comparable by equality">>,
+                   <<?Pos(107,71)
+                     "Values of type `map(int, int)` are not comparable by inequality">>,
+                   <<?Pos(110,80)
+                     "Values of type `oracle(int, int)` are not comparable by inequality">>,
+                   <<?Pos(113,98)
+                     "Values of type `oracle_query(int, int)` are not comparable by inequality">>,
+                   <<?Pos(116,90)
+                     "Values of type `custom_datatype(int)` are not comparable by inequality">>,
+                   <<?Pos(119,84)
+                     "Values of type `custom_record(int)` are not comparable by inequality">>,
+                   <<?Pos(124,86)
+                     "Values of type `map(address, address)` are not comparable by inequality">>,
+                   <<?Pos(127,95)
+                     "Values of type `oracle(address, address)` are not comparable by inequality">>,
+                   <<?Pos(130,113)
+                     "Values of type `oracle_query(address, address)` are not comparable by inequality">>,
+                   <<?Pos(133,97)
+                     "Values of type `custom_datatype(address)` are not comparable by inequality">>,
+                   <<?Pos(136,91)
+                     "Values of type `custom_record(address)` are not comparable by inequality">>,
+                   <<?Pos(141,75)
+                     "Values of type `map((int, char) => bool, (int, char) => bool)` are not comparable by inequality">>,
+                   <<?Pos(142,75)
+                     "Values of type `map((int, char) => bool, (int, char) => bool)` are not comparable by equality">>,
+                   <<?Pos(144,84)
+                     "Values of type `oracle((int, char) => bool, (int, char) => bool)` are not comparable by inequality">>,
+                   <<?Pos(145,84)
+                     "Values of type `oracle((int, char) => bool, (int, char) => bool)` are not comparable by equality">>,
+                   <<?Pos(147,102)
+                     "Values of type `oracle_query((int, char) => bool, (int, char) => bool)` are not comparable by inequality">>,
+                   <<?Pos(148,102)
+                     "Values of type `oracle_query((int, char) => bool, (int, char) => bool)` are not comparable by equality">>,
+                   <<?Pos(150,94)
+                     "Values of type `custom_datatype((int, char) => bool)` are not comparable by inequality">>,
+                   <<?Pos(151,94)
+                     "Values of type `custom_datatype((int, char) => bool)` are not comparable by equality">>,
+                   <<?Pos(153,88)
+                     "Values of type `custom_record((int, char) => bool)` are not comparable by inequality">>,
+                   <<?Pos(154,88)
+                     "Values of type `custom_record((int, char) => bool)` are not comparable by equality">>
+                  ])
     , ?TYPE_ERROR(warnings,
                   [<<?Pos(0, 0)
                       "The file `Triple.aes` is included but not used.">>,
@@ -834,7 +912,9 @@ failing_contracts() ->
                      "The function `called_unused_function2` is defined but never used.">>,
                    <<?Pos(48, 5)
                      "Unused return value.">>,
-                   <<?Pos(60, 5)
+                   <<?Pos(53, 44)
+                     "The constraint on the type variable `'a` is a duplication of the constraint at line 53, column 34">>,
+                   <<?Pos(65, 5)
                      "The function `dec` is defined but never used.">>
                   ])
     ].

test/contracts/comparable_typevar_constraints.aes

@@ -0,0 +1,156 @@
+contract A = entrypoint init() = ()
+
+main contract C =
+    datatype custom_datatype('a) = CD('a)
+
+    record custom_record('a) = { f : 'a }
+
+    // pass
+    function
+        passing_ord: 'a is ord ; ('a, 'a) => bool
+        passing_ord(x, y) = x >= y
+
+    // pass
+    function
+        passing_eq: 'a is eq ; ('a, 'a) => bool
+        passing_eq(x, y) = x == y
+
+    // fail because eq is not specified for 'a
+    function
+        fail_no_eq : ('a, 'a) => bool
+        fail_no_eq(x, y) = x == y
+
+    // fail because 'b is not used
+    function
+        fail_unused_tvar: 'a is eq, 'b is eq ; ('a, 'a) => bool
+        fail_unused_tvar(x, y) = x == y
+
+    // Ord types
+
+    function bool_ord(x : bool, y : bool) = x >= y  // pass
+    function bool_eq (x : bool, y : bool) = x == y  // pass
+
+    function int_ord(x : int, y : int) = x >= y  // pass
+    function int_eq (x : int, y : int) = x == y  // pass
+
+    function char_ord(x : char, y : char) = x >= y  // pass
+    function char_eq (x : char, y : char) = x == y  // pass
+
+    function bits_ord(x : bits, y : bits) = x >= y  // pass
+    function bits_eq (x : bits, y : bits) = x == y  // pass
+
+    function bytes_ord(x : bytes(16), y : bytes(16)) = x >= y  // pass
+    function bytes_eq (x : bytes(16), y : bytes(16)) = x == y  // pass
+
+    function string_ord(x : string, y : string) = x >= y  // pass
+    function string_eq (x : string, y : string) = x == y  // pass
+
+    function hash_ord(x : hash, y : hash) = x >= y  // pass
+    function hash_eq (x : hash, y : hash) = x == y  // pass
+
+    function signature_ord(x : signature, y : signature) = x >= y  // pass
+    function signature_eq (x : signature, y : signature) = x == y  // pass
+
+    // Eq types
+
+    function address_ord(x : address, y : address) = x >= y  // fail
+    function address_eq (x : address, y : address) = x == y  // pass
+
+    function event_ord(x : Chain.ttl, y : Chain.ttl) = x >= y  // fail
+    function event_eq (x : Chain.ttl, y : Chain.ttl) = x == y  // pass
+
+    function contract_ord(x : A, y : A) = x >= y  // fail
+    function contract_eq (x : A, y : A) = x == y  // pass
+
+    // Noncomparable types
+
+    type lam = (int, char) => bool
+
+    function lambda_ord(x : lam, y : lam) = x >= y  // fail
+    function lambda_eq (x : lam, y : lam) = x == y  // fail
+
+    // Ord composite types of ord
+
+    function list_of_ord_ord(x : list(int), y : list(int)) = x >= y  // pass
+    function list_of_ord_eq (x : list(int), y : list(int)) = x == y  // pass
+
+    function option_of_ord_ord(x : option(int), y : option(int)) = x >= y  // pass
+    function option_of_ord_eq (x : option(int), y : option(int)) = x == y  // pass
+
+    function tuple_of_ord_ord(x : (int * bool), y : (int * bool)) = x >= y  // pass
+    function tuple_of_ord_eq (x : (int * bool), y : (int * bool)) = x == y  // pass
+
+    // Ord composite types of eq
+
+    function list_of_eq_ord(x : list(address), y : list(address)) = x >= y  // fail
+    function list_of_eq_eq (x : list(address), y : list(address)) = x == y  // pass
+
+    function option_of_eq_ord(x : option(address), y : option(address)) = x >= y  // fail
+    function option_of_eq_eq (x : option(address), y : option(address)) = x == y  // pass
+
+    function tuple_of_eq_ord(x : (address * int), y : (address * int)) = x >= y  // fail
+    function tuple_of_eq_eq (x : (address * int), y : (address * int)) = x == y  // pass
+
+    // Ord composite types of nomcomparable
+
+    function list_of_noncomp_ord(x : list(lam), y : list(lam)) = x >= y  // fail
+    function list_of_noncomp_eq (x : list(lam), y : list(lam)) = x == y  // fail
+
+    function option_of_noncomp_ord(x : option(lam), y : option(lam)) = x >= y  // fail
+    function option_of_noncomp_eq (x : option(lam), y : option(lam)) = x == y  // fail
+
+    function tuple_of_noncomp_ord(x : (lam * int), y : (lam * int)) = x >= y  // fail
+    function tuple_of_noncomp_eq (x : (lam * int), y : (lam * int)) = x == y  // fail
+
+    // Eq composite types of ord
+
+    function map_of_ord_ord(x : map(int, int), y : map(int, int)) = x >= y  // fail
+    function map_of_ord_eq (x : map(int, int), y : map(int, int)) = x == y  // pass
+
+    function oracle_of_ord_ord(x : oracle(int, int), y : oracle(int, int)) = x >= y  // fail
+    function oracle_of_ord_eq (x : oracle(int, int), y : oracle(int, int)) = x == y  // pass
+
+    function oracle_query_of_ord_ord(x : oracle_query(int, int), y : oracle_query(int, int)) = x >= y  // fail
+    function oracle_query_of_ord_eq (x : oracle_query(int, int), y : oracle_query(int, int)) = x == y  // pass
+
+    function datatype_of_ord_ord(x : custom_datatype(int), y : custom_datatype(int)) = x >= y  // fail
+    function datatype_of_ord_eq (x : custom_datatype(int), y : custom_datatype(int)) = x == y  // pass
+
+    function record_of_ord_ord(x : custom_record(int), y : custom_record(int)) = x >= y  // fail
+    function record_of_ord_eq (x : custom_record(int), y : custom_record(int)) = x == y  // pass
+
+    // Eq composite types of eq
+
+    function map_of_eq_ord(x : map(address, address), y : map(address, address)) = x >= y  // fail
+    function map_of_eq_eq (x : map(address, address), y : map(address, address)) = x == y  // pass
+
+    function oracle_of_eq_ord(x : oracle(address, address), y : oracle(address, address)) = x >= y  // fail
+    function oracle_of_eq_eq (x : oracle(address, address), y : oracle(address, address)) = x == y  // pass
+
+    function oracle_query_of_eq_ord(x : oracle_query(address, address), y : oracle_query(address, address)) = x >= y  // fail
+    function oracle_query_of_eq_eq (x : oracle_query(address, address), y : oracle_query(address, address)) = x == y  // pass
+
+    function datatype_of_eq_ord(x : custom_datatype(address), y : custom_datatype(address)) = x >= y  // fail
+    function datatype_of_eq_eq (x : custom_datatype(address), y : custom_datatype(address)) = x == y  // pass
+
+    function record_of_eq_ord(x : custom_record(address), y : custom_record(address)) = x >= y  // fail
+    function record_of_eq_eq (x : custom_record(address), y : custom_record(address)) = x == y  // pass
+
+    // Eq composite types of nomcomparable
+
+    function map_of_noncomp_ord(x : map(lam, lam), y : map(lam, lam)) = x >= y  // fail
+    function map_of_noncomp_eq (x : map(lam, lam), y : map(lam, lam)) = x == y  // fail
+
+    function oracle_of_noncomp_ord(x : oracle(lam, lam), y : oracle(lam, lam)) = x >= y  // fail
+    function oracle_of_noncomp_eq (x : oracle(lam, lam), y : oracle(lam, lam)) = x == y  // fail
+
+    function oracle_query_of_noncomp_ord(x : oracle_query(lam, lam), y : oracle_query(lam, lam)) = x >= y  // fail
+    function oracle_query_of_noncomp_eq (x : oracle_query(lam, lam), y : oracle_query(lam, lam)) = x == y  // fail
+
+    function datatype_of_noncomp_ord(x : custom_datatype(lam), y : custom_datatype(lam)) = x >= y  // fail
+    function datatype_of_noncomp_eq (x : custom_datatype(lam), y : custom_datatype(lam)) = x == y  // pass
+
+    function record_of_nomcomp_ord(x : custom_record(lam), y : custom_record(lam)) = x >= y  // fail
+    function record_of_nomcomp_eq (x : custom_record(lam), y : custom_record(lam)) = x == y  // pass
+
+    entrypoint init() = ()

test/contracts/warnings.aes

@@ -48,6 +48,11 @@ contract Warnings =
     rv()
     2
 
+  // Duplicated constraint on 'a
+  entrypoint
+    duplicated_tvar_constraint : 'a is eq, 'a is eq ; ('a, 'a) => bool
+    duplicated_tvar_constraint (x, y) = x == y
+
 namespace FunctionsAsArgs =
     function f() = g()