Deal with destructuring tag unions behind opaques correctly

Closes #2702

compiler/constrain/src/pattern.rs

@@ -504,12 +504,22 @@ pub fn constrain_pattern(
             );
 
             // Link the entire wrapped opaque type (with the now-constrained argument) to the type
-            // variables of the opaque type
+            // variables of the opaque type.
-            // TODO: better expectation here
+            //
-            let link_type_variables_con = constraints.equal_types(
+            // For example, suppose we have `O k := [ A k, B k ]`, and the pattern `@O (A s) -> s == ""`.
-                (**specialized_def_type).clone(),
+            // Previous constraints will have solved `typeof s ~ Str`, and we have the
-                Expected::NoExpectation(arg_pattern_type),
+            // `specialized_def_type` being `[ A k1, B k1 ]`, specializing `k` as `k1` for this opaque
-                Category::OpaqueWrap(*opaque),
+            // usage.
+            // We now want to link `typeof s ~ k1`, so to capture this relationship, we link
+            // the type of `A s` (the arg type) to `[ A k1, B k1 ]` (the specialized opaque type).
+            //
+            // This must **always** be a presence constraint, that is enforcing
+            // `[ A k1, B k1 ] += typeof (A s)`, because we are in a destructure position and not
+            // all constructors are covered in this branch!
+            let link_type_variables_con = constraints.pattern_presence(
+                arg_pattern_type,
+                PExpected::NoExpectation((**specialized_def_type).clone()),
+                PatternCategory::Opaque(*opaque),
                 loc_arg_pattern.region,
             );
 

compiler/solve/tests/solve_expr.rs

@@ -5573,4 +5573,57 @@ mod solve_expr {
             r#"[ A, B, C ]"#,
         )
     }
+
+    #[test]
+    // https://github.com/rtfeldman/roc/issues/2702
+    fn tag_inclusion_behind_opaque() {
+        infer_eq_without_problem(
+            indoc!(
+                r#"
+                Outer k := [ Empty, Wrapped k ]
+
+                insert : Outer k, k -> Outer k
+                insert = \m, var ->
+                    when m is
+                        $Outer Empty -> $Outer (Wrapped var)
+                        $Outer (Wrapped _) -> $Outer (Wrapped var)
+
+                insert
+                "#
+            ),
+            r#"Outer k, k -> Outer k"#,
+        )
+    }
+
+    #[test]
+    fn tag_inclusion_behind_opaque_infer() {
+        infer_eq_without_problem(
+            indoc!(
+                r#"
+                Outer k := [ Empty, Wrapped k ]
+
+                when ($Outer Empty) is
+                    $Outer Empty -> $Outer (Wrapped "")
+                    $Outer (Wrapped k) -> $Outer (Wrapped k)
+                "#
+            ),
+            r#"Outer Str"#,
+        )
+    }
+
+    #[test]
+    fn tag_inclusion_behind_opaque_infer_single_ctor() {
+        infer_eq_without_problem(
+            indoc!(
+                r#"
+                Outer := [ A, B ]
+
+                when ($Outer A) is
+                    $Outer A -> $Outer A
+                    $Outer B -> $Outer B
+                "#
+            ),
+            r#"Outer"#,
+        )
+    }
 }

compiler/unify/src/unify.rs

@@ -180,10 +180,12 @@ fn unify_context(subs: &mut Subs, pool: &mut Pool, ctx: Context) -> Outcome {
         //        println!("\n --------------- \n");
         let content_1 = subs.get(ctx.first).content;
         let content_2 = subs.get(ctx.second).content;
+        let mode = if ctx.mode.is_eq() { "~" } else { "+=" };
         println!(
-            "{:?} {:?} ~ {:?} {:?}",
+            "{:?} {:?} {} {:?} {:?}",
             ctx.first,
             roc_types::subs::SubsFmtContent(&content_1, subs),
+            mode,
             ctx.second,
             roc_types::subs::SubsFmtContent(&content_2, subs),
         );
@@ -334,7 +336,13 @@ fn unify_alias(
                         problems.extend(merge(subs, ctx, *other_content));
                     }
 
-                    // if problems.is_empty() { problems.extend(unify_pool(subs, pool, real_var, *other_real_var)); }
+                    // THEORY: if two aliases or opaques have the same name and arguments, their
+                    // real_var is the same and we don't need to check it.
+                    // See https://github.com/rtfeldman/roc/pull/1510
+                    //
+                    // if problems.is_empty() && either_is_opaque {
+                    //     problems.extend(unify_pool(subs, pool, real_var, *other_real_var, ctx.mode));
+                    // }
 
                     problems
                 } else {