Merge pull request #7454 from roc-lang/ayaz/error-on-invalid-generali…

…zed-types

Restrict usages of type variables in non-generalized contexts

.cargo/config.toml

@@ -39,7 +39,6 @@ ROC_TRACE_COMPACTION                   = "0"
 ROC_PRINT_UNIFICATIONS_DERIVED         = "0"
 ROC_PRINT_MISMATCHES                   = "0"
 ROC_PRINT_FIXPOINT_FIXING              = "0"
-ROC_VERIFY_RIGID_LET_GENERALIZED       = "0"
 ROC_VERIFY_OCCURS_ONE_RECURSION        = "0"
 ROC_CHECK_MONO_IR                      = "0"
 ROC_PRINT_IR_AFTER_SPECIALIZATION      = "0"

crates/cli/tests/benchmarks/AStar.roc

@@ -90,12 +90,12 @@ astar = \cost_fn, move_fn, goal, model ->
                 new_neighbors =
                     Set.difference(neighbors, model_popped.evaluated)
 
-                model_with_neighbors : Model position
+                model_with_neighbors : Model _
                 model_with_neighbors =
                     model_popped
                     |> &open_set(Set.union(model_popped.open_set, new_neighbors))
 
-                walker : Model position, position -> Model position
+                walker : Model _, _ -> Model _
                 walker = \amodel, n -> update_cost(current, n, amodel)
 
                 model_with_costs =

crates/compiler/builtins/roc/Num.roc

@@ -532,7 +532,7 @@ pi = 3.14159265358979323846264338327950288419716939937510
 
 ## Circle constant (τ)
 tau : Frac *
-tau = 2 * pi
+tau = 6.2831853071795864769252867665590057683943387987502
 
 # ------- Functions
 ## Convert a number to a [Str].

crates/compiler/can/src/constraint.rs

@@ -915,7 +915,7 @@ pub struct DefTypes {
     pub loc_symbols: Slice<(Symbol, Region)>,
 }
 
-#[derive(Debug, Clone, Copy)]
+#[derive(Debug, Clone, Copy, PartialEq)]
 pub struct Generalizable(pub bool);
 
 #[derive(Debug, Clone)]

crates/compiler/debug_flags/src/lib.rs

@@ -95,22 +95,6 @@ flags! {
     /// Prints all type variables entered for fixpoint-fixing.
     ROC_PRINT_FIXPOINT_FIXING
 
-    /// Verifies that after let-generalization of a def, any rigid variables in the type annotation
-    /// of the def are indeed generalized.
-    ///
-    /// Note that rigids need not always be generalized in a def. For example, they may be
-    /// constrained by a type from a lower rank, as `b` is in the following def:
-    ///
-    ///   F a : { foo : a }
-    ///   foo = \arg ->
-    ///     x : F b
-    ///     x = arg
-    ///     x.foo
-    ///
-    /// Instead, this flag is useful for checking that in general, introduction is correct, when
-    /// chainging how defs are constrained.
-    ROC_VERIFY_RIGID_LET_GENERALIZED
-
     /// Verifies that an `occurs` check indeed only contains non-recursive types that need to be
     /// fixed-up with one new recursion variable.
     ///

crates/compiler/load/tests/test_reporting.rs

@@ -1522,18 +1522,18 @@ mod test_reporting {
         from_annotation_if,
         indoc!(
             r"
-            x : Num.Int *
+            x : Num.Int _
             x = if Bool.true then 3.14 else 4
 
             x
             "
         ),
-        @r"
+        @r###"
     ── TYPE MISMATCH in /code/proj/Main.roc ────────────────────────────────────────
 
     Something is off with the `then` branch of this `if` expression:
 
-    4│      x : Num.Int *
+    4│      x : Num.Int _
     5│      x = if Bool.true then 3.14 else 4
                                   ^^^^
 
@@ -1547,27 +1547,27 @@ mod test_reporting {
 
     Tip: You can convert between integers and fractions using functions
     like `Num.to_frac` and `Num.round`.
-    "
+    "###
     );
 
     test_report!(
         from_annotation_when,
         indoc!(
             r"
-            x : Num.Int *
+            x : Num.Int _
             x =
                 when True is
                     _ -> 3.14
 
             x
             "
         ),
-        @r"
+        @r###"
     ── TYPE MISMATCH in /code/proj/Main.roc ────────────────────────────────────────
 
     Something is off with the body of the `x` definition:
 
-    4│       x : Num.Int *
+    4│       x : Num.Int _
     5│       x =
     6│>          when True is
     7│>              _ -> 3.14
@@ -1582,7 +1582,7 @@ mod test_reporting {
 
     Tip: You can convert between integers and fractions using functions
     like `Num.to_frac` and `Num.round`.
-    "
+    "###
     );
 
     test_report!(
@@ -1910,7 +1910,7 @@ mod test_reporting {
         from_annotation_complex_pattern,
         indoc!(
             r"
-            { x } : { x : Num.Int * }
+            { x } : { x : Num.Int _ }
             { x } = { x: 4.0 }
 
             x
@@ -1921,7 +1921,7 @@ mod test_reporting {
 
     Something is off with the body of this definition:
 
-    4│      { x } : { x : Num.Int * }
+    4│      { x } : { x : Num.Int _ }
     5│      { x } = { x: 4.0 }
                     ^^^^^^^^^^
 
@@ -2047,18 +2047,18 @@ mod test_reporting {
         missing_fields,
         indoc!(
             r"
-            x : { a : Num.Int *, b : Num.Frac *, c : Str }
+            x : { a : Num.Int _, b : Num.Frac _, c : Str }
             x = { b: 4.0 }
 
             x
             "
         ),
-        @r"
+        @r###"
     ── TYPE MISMATCH in /code/proj/Main.roc ────────────────────────────────────────
 
     Something is off with the body of the `x` definition:
 
-    4│      x : { a : Num.Int *, b : Num.Frac *, c : Str }
+    4│      x : { a : Num.Int _, b : Num.Frac _, c : Str }
     5│      x = { b: 4.0 }
                 ^^^^^^^^^^
 
@@ -2075,7 +2075,7 @@ mod test_reporting {
         }
 
     Tip: Looks like the c and a fields are missing.
-    "
+    "###
     );
 
     // this previously reported the message below, not sure which is better
@@ -3448,7 +3448,7 @@ mod test_reporting {
             x : AList Num.I64 Num.I64
             x = ACons 0 (BCons 1 (ACons "foo" BNil ))
 
-            y : BList a a
+            y : BList _ _
             y = BNil
 
             { x, y }
@@ -4189,9 +4189,8 @@ mod test_reporting {
             RBTree k v : [Node NodeColor k v (RBTree k v) (RBTree k v), Empty]
 
             # Create an empty dictionary.
-            empty : RBTree k v
-            empty =
-                Empty
+            empty : {} -> RBTree k v
+            empty = \{} -> Empty
 
             empty
             "
@@ -11218,10 +11217,10 @@ All branches in an `if` must have the same type!
 
             import Decode exposing [decoder]
 
-            main =
-                my_decoder : Decoder (a -> a) fmt where fmt implements DecoderFormatting
-                my_decoder = decoder
+            my_decoder : Decoder (_ -> _) _
+            my_decoder = decoder
 
+            main =
                 my_decoder
             "#
         ),
@@ -11230,12 +11229,12 @@ All branches in an `if` must have the same type!
 
     This expression has a type that does not implement the abilities it's expected to:
 
-    7│      my_decoder = decoder
-                         ^^^^^^^
+    6│  my_decoder = decoder
+                     ^^^^^^^
 
     I can't generate an implementation of the `Decoding` ability for
 
-        a -> a
+        * -> *
 
     Note: `Decoding` cannot be generated for functions.
     "
@@ -11251,10 +11250,10 @@ All branches in an `if` must have the same type!
 
             A := {}
 
-            main =
-                my_decoder : Decoder {x : A} fmt where fmt implements DecoderFormatting
-                my_decoder = decoder
+            my_decoder : Decoder {x : A} _
+            my_decoder = decoder
 
+            main =
                 my_decoder
             "#
         ),
@@ -11263,8 +11262,8 @@ All branches in an `if` must have the same type!
 
     This expression has a type that does not implement the abilities it's expected to:
 
-    9│      my_decoder = decoder
-                         ^^^^^^^
+    8│  my_decoder = decoder
+                     ^^^^^^^
 
     I can't generate an implementation of the `Decoding` ability for
 
@@ -11514,20 +11513,19 @@ All branches in an `if` must have the same type!
 
              import Decode exposing [decoder]
 
-             main =
-                 my_decoder : Decoder {x : Str, y ? Str} fmt where fmt implements DecoderFormatting
-                 my_decoder = decoder
+             my_decoder : Decoder {x : Str, y ? Str} _
+             my_decoder = decoder
 
-                 my_decoder
+             main = my_decoder
              "#
         ),
         @r"
     ── TYPE MISMATCH in /code/proj/Main.roc ────────────────────────────────────────
 
     This expression has a type that does not implement the abilities it's expected to:
 
-    7│      my_decoder = decoder
-                         ^^^^^^^
+    6│  my_decoder = decoder
+                     ^^^^^^^
 
     I can't generate an implementation of the `Decoding` ability for
 
@@ -14111,11 +14109,10 @@ All branches in an `if` must have the same type!
 
             import Decode exposing [decoder]
 
-            main =
-                my_decoder : Decoder (U32, Str) fmt where fmt implements DecoderFormatting
-                my_decoder = decoder
+            my_decoder : Decoder (U32, Str) _
+            my_decoder = decoder
 
-                my_decoder
+            main = my_decoder
             "#
         )
     );
@@ -14128,20 +14125,19 @@ All branches in an `if` must have the same type!
 
             import Decode exposing [decoder]
 
-            main =
-                my_decoder : Decoder (U32, {} -> {}) fmt where fmt implements DecoderFormatting
-                my_decoder = decoder
+            my_decoder : Decoder (U32, {} -> {}) _
+            my_decoder = decoder
 
-                my_decoder
+            main = my_decoder
             "#
         ),
         @r"
     ── TYPE MISMATCH in /code/proj/Main.roc ────────────────────────────────────────
 
     This expression has a type that does not implement the abilities it's expected to:
 
-    7│      my_decoder = decoder
-                         ^^^^^^^
+    6│  my_decoder = decoder
+                     ^^^^^^^
 
     I can't generate an implementation of the `Decoding` ability for
 
@@ -15997,4 +15993,66 @@ All branches in an `if` must have the same type!
         Str -> {}
     "#
     );
+
+    test_report!(
+        invalid_generic_literal,
+        indoc!(
+            r#"
+            module [v]
+
+            v : *
+            v = 1
+            "#
+        ),
+        @r###"
+    ── TYPE MISMATCH in /code/proj/Main.roc ────────────────────────────────────────
+
+    Something is off with the body of the `v` definition:
+
+    3│  v : *
+    4│  v = 1
+            ^
+
+    The body is a number of type:
+
+        Num *
+
+    But the type annotation on `v` says it should be:
+
+        *
+
+    Tip: The type annotation uses the type variable `*` to say that this
+    definition can produce any type of value. But in the body I see that
+    it will only produce a `Num` value of a single specific type. Maybe
+    change the type annotation to be more specific? Maybe change the code
+    to be more general?
+    "###
+    );
+
+    test_report!(
+        invalid_generic_literal_list,
+        indoc!(
+            r#"
+            module [v]
+
+            v : List *
+            v = []
+            "#
+        ),
+        @r###"
+    ── TYPE VARIABLE IS NOT GENERIC in /code/proj/Main.roc ─────────────────────────
+
+    This type variable has a single type:
+
+    3│  v : List *
+                 ^
+
+    Type variables tell me that they can be used with any type, but they
+    can only be used with functions. All other values have exactly one
+    type.
+
+    Hint: If you would like the type to be inferred for you, use an
+    underscore _ instead.
+    "###
+    );
 }