From 7d5ea6a39e4aa4d0bef52253b072ce3b6bf87f78 Mon Sep 17 00:00:00 2001
From: Gaith Hallak <gaithhallak@gmail.com>
Date: Fri, 20 May 2022 18:24:02 +0400
Subject: [PATCH] Handle builtin types type variables separately

---
 src/aeso_ast_infer_types.erl | 15 +++++++++++--
 test/aeso_compiler_tests.erl | 43 ++++++++++++++++++++++++++++++++++++
 2 files changed, 56 insertions(+), 2 deletions(-)

diff --git a/src/aeso_ast_infer_types.erl b/src/aeso_ast_infer_types.erl
index de75101..ad36319 100644
--- a/src/aeso_ast_infer_types.erl
+++ b/src/aeso_ast_infer_types.erl
@@ -808,9 +808,15 @@ infer(Contracts, Options) ->
         create_options(Options),
         ets_new(defined_contracts, [bag]),
         ets_new(type_vars, [set]),
-        ets_new(type_vars_variance, [set]),
         ets_new(type_vars_uvar, [set]),
         ets_new(warnings, [bag]),
+        ets_new(type_vars_variance, [set]),
+        %% Set the variance for builtin types
+        ets_insert(type_vars_variance, {"list", [covariant]}),
+        ets_insert(type_vars_variance, {"option", [covariant]}),
+        ets_insert(type_vars_variance, {"oracle", [contravariant, covariant]}),
+        ets_insert(type_vars_variance, {"oracle_query", [covariant, contravariant]}),
+
         when_warning(warn_unused_functions, fun() -> create_unused_functions() end),
         check_modifiers(Env, Contracts),
         create_type_errors(),
@@ -2775,7 +2781,12 @@ unify1(Env, {fun_t, _, Named1, Args1, Result1}, {fun_t, _, Named2, Args2, Result
 unify1(Env, {app_t, _, {Tag, _, F}, Args1}, {app_t, _, {Tag, _, F}, Args2}, Variance, When)
   when length(Args1) == length(Args2), Tag == id orelse Tag == qid ->
     Variances = case ets_lookup(type_vars_variance, F) of
-                    [{_, Vs}] -> Vs;
+                    [{_, Vs}] ->
+                        case Variance of
+                            contravariant -> lists:map(fun opposite_variance/1, Vs);
+                            invariant     -> invariant;
+                            _             -> Vs
+                        end;
                     _ -> Variance
                 end,
     unify1(Env, Args1, Args2, Variances, When);
diff --git a/test/aeso_compiler_tests.erl b/test/aeso_compiler_tests.erl
index 31197ce..8c5ea4b 100644
--- a/test/aeso_compiler_tests.erl
+++ b/test/aeso_compiler_tests.erl
@@ -1006,6 +1006,49 @@ failing_contracts() ->
                    <<?Pos(47,13)
                      "Cannot unify `Animal` and `Cat`\n"
                      "when checking the type of the pattern `r17 : rec_d(Cat)` against the expected type `Main.rec_d(Animal)`">>])
+    , ?TYPE_ERROR(polymorphism_variance_switching_oracles,
+                  [<<?Pos(15,13)
+                     "Cannot unify `Cat` and `Animal`\n"
+                     "when checking the type of the pattern `o03 : oracle(Animal, Animal)` against the expected type `oracle(Cat, Animal)`">>,
+                   <<?Pos(16,13)
+                     "Cannot unify `Cat` and `Animal`\n"
+                     "when checking the type of the pattern `o04 : oracle(Animal, Animal)` against the expected type `oracle(Cat, Cat)`">>,
+                   <<?Pos(17,13)
+                     "Cannot unify `Animal` and `Cat`\n"
+                     "when checking the type of the pattern `o05 : oracle(Animal, Cat)` against the expected type `oracle(Animal, Animal)`">>,
+                   <<?Pos(19,13)
+                     "Cannot unify `Cat` and `Animal`\n"
+                     "when checking the type of the pattern `o07 : oracle(Animal, Cat)` against the expected type `oracle(Cat, Animal)`">>,
+                   <<?Pos(20,13)
+                     "Cannot unify `Cat` and `Animal`\n"
+                     "when checking the type of the pattern `o08 : oracle(Animal, Cat)` against the expected type `oracle(Cat, Cat)`">>,
+                   <<?Pos(25,13)
+                     "Cannot unify `Animal` and `Cat`\n"
+                     "when checking the type of the pattern `o13 : oracle(Cat, Cat)` against the expected type `oracle(Animal, Animal)`">>,
+                   <<?Pos(27,13)
+                     "Cannot unify `Animal` and `Cat`\n"
+                     "when checking the type of the pattern `o15 : oracle(Cat, Cat)` against the expected type `oracle(Cat, Animal)`">>,
+                   <<?Pos(31,13)
+                     "Cannot unify `Cat` and `Animal`\n"
+                     "when checking the type of the pattern `q02 : oracle_query(Animal, Animal)` against the expected type `oracle_query(Animal, Cat)`">>,
+                   <<?Pos(33,13)
+                     "Cannot unify `Cat` and `Animal`\n"
+                     "when checking the type of the pattern `q04 : oracle_query(Animal, Animal)` against the expected type `oracle_query(Cat, Cat)`">>,
+                   <<?Pos(38,13)
+                     "Cannot unify `Animal` and `Cat`\n"
+                     "when checking the type of the pattern `q09 : oracle_query(Cat, Animal)` against the expected type `oracle_query(Animal, Animal)`">>,
+                   <<?Pos(39,13)
+                     "Cannot unify `Animal` and `Cat`\n"
+                     "when checking the type of the pattern `q10 : oracle_query(Cat, Animal)` against the expected type `oracle_query(Animal, Cat)`">>,
+                   <<?Pos(41,13)
+                     "Cannot unify `Cat` and `Animal`\n"
+                     "when checking the type of the pattern `q12 : oracle_query(Cat, Animal)` against the expected type `oracle_query(Cat, Cat)`">>,
+                   <<?Pos(42,13)
+                     "Cannot unify `Animal` and `Cat`\n"
+                     "when checking the type of the pattern `q13 : oracle_query(Cat, Cat)` against the expected type `oracle_query(Animal, Animal)`">>,
+                   <<?Pos(43,13)
+                     "Cannot unify `Animal` and `Cat`\n"
+                     "when checking the type of the pattern `q14 : oracle_query(Cat, Cat)` against the expected type `oracle_query(Animal, Cat)`">>])
     ].
 
 -define(Path(File), "code_errors/" ??File).