Partial fix for the case when two dirt params are equal

Closes #89

Author: matijapretnar

src/01-language/substitution.ml

@@ -330,7 +330,7 @@ let add_dirt_var_coercion_e dirt_var dc =
   }
 
 let add_dirt_var_coercion dirt_var dc sub =
-  assert (dc = apply_sub_dirtcoer sub dc);
+  assert (Coercion.equal_dirt_coercion dc (apply_sub_dirtcoer sub dc));
   merge (add_dirt_var_coercion_e dirt_var dc) sub
 
 let add_dirt_substitution_e dirt_var dirt =

src/03-typechecker/unification.ml

@@ -293,7 +293,9 @@ and dirt_omega_step ~loc sub resolved unresolved w dcons =
       let w' = DirtCoercionParam.refresh w in
       let d2' = Dirt.Param.refresh d2 in
       let w_ty' =
-        ( { Dirt.effect_set = Effect.Set.empty; row = Dirt.Row.Param d1 },
+        ( (* In case d1 = d2, we need to substitute d1 as well *)
+          Substitution.apply_substitutions_to_dirt dirt_sub
+            { Dirt.effect_set = Effect.Set.empty; row = Dirt.Row.Param d1 },
           {
             Dirt.effect_set = Effect.Set.union ops1 ops2;
             row = Dirt.Row.Param d2';

tests/valid.t

@@ -116,6 +116,10 @@
   20
   - : int = 0
   ======================================================================
+  valid/test1.eff
+  ----------------------------------------------------------------------
+  val testbug : ('a testtype -> 'a) => ('a testtype -> 'a) = <handler>
+  ======================================================================
   valid/test_equality.eff
   ----------------------------------------------------------------------
   - : bool = true

tests/valid/test1.eff

@@ -0,0 +1,10 @@
+(* https://github.com/matijapretnar/eff/issues/89 *)
+
+effect A : unit
+effect B : unit
+
+type 'a testtype = T of (('a testtype -> 'a) list)
+
+let testbug = handler 
+  | effect A k -> fun (T ks) -> continue k () (T ((k ()) :: ks))
+  | effect B k -> fun (T l) -> perform (Print "hello") ; continue k () (T l)