Trace back unification error #339

MangoIV · 2024-10-27T11:48:45Z

see issue unifier error messages appear in the wrong place #338
add a very basic nix development environment
work in process of annotating the origin of an error
move the type error type into the heap to avoid warning
annotate ast with a bit more information what each of the nodes mean

timsueberkrueb

Left some nitpick comments, looking good so far, otherwise, thanks for contributing :)

flake.nix

lang/parser/src/cst/exp.rs

.envrc

MangoIV · 2024-11-07T14:29:51Z

I rebased on main and now for some reason the output from check doesn't give me any description anymore:

MangoIV · 2024-11-07T14:30:59Z

Ah no, it still does, but not on this example, however, on the smaller err.pol:

MangoIV · 2024-11-07T14:32:09Z

ah! that's because they don't have labels. Please excuse the fuzz.

MangoIV · 2024-11-07T14:50:20Z

I think I like this except due to the empty labels currently used in the macros the underlining of Type looks a bit sketchy.

MangoIV · 2024-11-07T15:02:46Z

Now there's a source span for (1) as well.

I wonder why the nix CI takes so long, the nix build doesn't use any caches... Maybe since the workflow is new it doesn't pick up the secret?

BinderDavid · 2024-11-07T18:17:09Z

Wow, the new error messages already look much better 👍

I wonder why the nix CI takes so long, the nix build doesn't use any caches... Maybe since the workflow is new it doesn't pick up the secret?

I remember something about GH Actions being different on PRs and main due to security reasons? I don't have a good mental model for what happens when you change the configuration of GitHub actions in PRs.

MangoIV · 2024-11-07T18:44:12Z

Yeah me either and it somehow always manages to surprise me so it probably won’t emerge any time soon lol

MangoIV · 2024-11-11T11:57:13Z

I'm currently verifying that the error messages actually make sense.

Here is the error message for 005.pol

I think it does make sense, but do you agree?

MangoIV · 2024-11-11T11:59:40Z

Also in such situations, I'm not entirely sure whether we actually need the information to make sense of the error. Perhaps it should be hidden behind a flag?

BinderDavid · 2024-11-11T14:14:07Z

Also in such situations, I'm not entirely sure whether we actually need the information to make sense of the error. Perhaps it should be hidden behind a flag?

I think most people will primarily interact with the error messages via the LSP editor integration. And the important thing is that you fixed the location of the squiggly lines for that use case (I just checked this myself). Also we don't report multiple errors for the same file currently (cp #65), so there is also a smaller likelihood that users are swamped by pages and pages of error messages.

(LSP supports "related locations" for error messages. We could investigate in the future how well they work with these examples)

MangoIV · 2024-11-11T14:16:17Z

(LSP supports "related locations" for error messages. We could investigate in the future how well they work with these examples)

that would be really nice!

timsueberkrueb · 2024-11-11T14:28:52Z

I think this is a great improvement.

If you allow me to dream up an ideal textual error message for this scenario it might look like this:

Error: T-002

Type mismatch in definition call between:

  │   1: Foo(False)    -- type of self argument
  │   2: Foo(True)     -- type of self parameter
  │ 
    ╭─[file:///home/tim/Dev/polarity-lang/polarity/test/suites/fail-check/002.pol:9:1]
  9 │     Bar : Foo(True),
 10 │     Baz : Foo(False),
    ·           ─────┬────
    ·                ╰── Source of (1)
 11 │ }
 12 │ 
 13 │ def Foo(True).foo() : Nat {
    ·     ────┬────
    ·         ╰── Source of (2)
 14 │     Bar() => Z,
 15 │     Baz() absurd,
 16 │ }
 17 │ 
 18 │ data Unit { Top }
 19 │ 
 20 │ def Unit.example : Nat {
 21 │     Top => Baz.foo
    ·            ─┬─ ─┬─
    ·             |   ╰── expected type (2)
    ·             ╰── got type (1)
 22 │ }
    ╰────

MangoIV · 2024-11-15T15:40:11Z

Is there something you want me to do on this one? Otherwise I'd mark this as ready for review :)

- add an origin field to NotEq unification error - add an origin field to CannotDecide unification error - reuse the span emitted for a data constructor without type for its type - Box the type error in Error to reduce the size of the enum

timsueberkrueb

This is a big improvement to our error messages, thank you!

I left some suggestions. Most of them are nitpicks. Please do check the comments on simplifying the test case, the reason field and whether to use the spans of (co)cases rather than (co)matches.

timsueberkrueb · 2024-11-15T18:30:58Z

.github/workflows/nix.yml

+          authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
+      - name: Evaluate nix code
+        run: nix -Lv flake check
+      - name: build and run polarity using nix


Suggested change

- name: build and run polarity using nix

- name: Build and run polarity using nix

timsueberkrueb · 2024-11-15T18:31:05Z

.github/workflows/nix.yml

+        run: nix -Lv flake check
+      - name: build and run polarity using nix
+        run: nix -Lv run .# -- --help
+      - name: build and run a static polarity exe


Suggested change

- name: build and run a static polarity exe

- name: Build and run a static polarity exe

timsueberkrueb · 2024-11-15T18:36:01Z

contrib/nix/README.md

+- your changes use existing nixpkgs infrastructure where possible
+- your changes do not break any of the existing workflows and everything works as normal for non-nix users
+- your changes do not require changes in regular non-nix development workflows
+- your changes do not introduce any unnecessary IFD


Maybe link to a reference on what IFD is.

good idea, I guess I will have to find one :P (https://nix.dev/manual/nix/2.25/language/import-from-derivation)

flake.nix

timsueberkrueb · 2024-11-15T18:46:43Z

contrib/nix/package.nix

+  meta = {
+    description = "A language with Dependendent Data and Codata Types";
+    homepage = "https://polarity-lang.github.io/";
+    licenses = with lib.licenses; [


On the license field, the docs say:

If the license field is in the form of a list representation, then it means that parts of the package are licensed differently

Is the semantic of the licenses field different? Does this convey SPDX MIT OR Apache-2.0?

I will look that up.

timsueberkrueb · 2024-11-15T18:51:35Z

lang/parser/src/cst/exp.rs

 pub struct Fun {
    pub span: Span,
    pub from: Box<Exp>,
    pub to: Box<Exp>,
 }

 #[derive(Debug, Clone)]
+/// Lambda abstractions \x. e


Suggested change

/// Lambda abstractions \x. e

/// Lambda abstractions (syntactic sugar), e.g. \x. e

timsueberkrueb · 2024-11-15T18:51:50Z

lang/parser/src/cst/exp.rs

 pub struct NatLit {
    pub span: Span,
    pub val: BigUint,
 }

 #[derive(Debug, Clone)]
+/// Function arrow in syntax


Suggested change

/// Function arrow in syntax

/// Function arrow (syntactic sugar), e.g. a -> b

timsueberkrueb · 2024-11-15T19:03:31Z

lang/elaborator/src/result.rs

@@ -35,6 +35,8 @@ pub enum TypeError {
        lhs_span: Option<SourceSpan>,
        #[label("Source of (2)")]
        rhs_span: Option<SourceSpan>,
+        #[label("While elaborating")]
+        reason_span: Option<SourceSpan>,


I'm wondering if there's a better term than reason to describe these fields. As far as I can see, this is always the span of the syntax tree node that is currently being elaborated.
I'm not sure I have a better term though; I've considered elab_origin_span, while_elaborating_span, ast_node_span.

hmm, I will probably take one of your options, I like while_elaborating_span best, for now :)

timsueberkrueb · 2024-11-15T19:04:35Z

lang/elaborator/src/typechecker/decls/definition.rs

@@ -33,7 +33,7 @@ impl CheckToplevel for Def {

            let ws = WithScrutinee { cases, scrutinee: self_param_nf.expect_typ_app()? };
            ws.check_exhaustiveness(ctx)?;
-            let cases = ws.check_ws(ctx, &ret_typ_nf)?;
+            let cases = ws.check_ws(ctx, &ret_typ_nf, span)?;


Do we want the span of the definition or of the case here? The same applies to top-level codefinitions and local (co)matches.

timsueberkrueb · 2024-11-15T19:11:53Z

test/suites/fail-check/009.pol

+
+
+codef ZipWith(n : Type, f : (CoNat -> CoNat -> CoNat), l1:CoList(n), l2: CoList(n)) : CoList(n) {
+}


I think this test case can be simplified. E.g. remove unnecessary (co)definitions, or create a simpler example that produces the same kind of error.

For instance:

data Foo {} data Bar(f: Foo) {} let bar(a: Type): Bar(a) { ? }

MangoIV force-pushed the mangoiv/trace-back-unification-errors branch 3 times, most recently from 831c717 to 5314230 Compare October 27, 2024 12:28

timsueberkrueb reviewed Oct 27, 2024

View reviewed changes

flake.nix Outdated Show resolved Hide resolved

lang/parser/src/cst/exp.rs Outdated Show resolved Hide resolved

.envrc Outdated Show resolved Hide resolved

MangoIV force-pushed the mangoiv/trace-back-unification-errors branch 8 times, most recently from 1233624 to 46e7757 Compare October 28, 2024 13:13

MangoIV force-pushed the mangoiv/trace-back-unification-errors branch from 46e7757 to 1f1ea1d Compare November 7, 2024 10:37

MangoIV force-pushed the mangoiv/trace-back-unification-errors branch 2 times, most recently from 627f6d9 to c8a3963 Compare November 7, 2024 15:01

MangoIV force-pushed the mangoiv/trace-back-unification-errors branch from c8a3963 to 31ef45a Compare November 11, 2024 12:40

[feat] add simple nix development environment

a8346aa

MangoIV added 4 commits November 15, 2024 16:46

[feat] add a workflow that checks the nix code

265f6eb

[chore] documentation updates of the expr ast

c1ce26b

[chore] add testfiles for unificatoin errors

c035ca5

MangoIV force-pushed the mangoiv/trace-back-unification-errors branch from 31ef45a to c035ca5 Compare November 15, 2024 16:01

MangoIV marked this pull request as ready for review November 15, 2024 16:35

timsueberkrueb requested changes Nov 15, 2024

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Trace back unification error #339

Trace back unification error #339

MangoIV commented Oct 27, 2024 •

edited

Loading

timsueberkrueb left a comment

MangoIV commented Nov 7, 2024

MangoIV commented Nov 7, 2024

MangoIV commented Nov 7, 2024

MangoIV commented Nov 7, 2024

MangoIV commented Nov 7, 2024

BinderDavid commented Nov 7, 2024

MangoIV commented Nov 7, 2024

MangoIV commented Nov 11, 2024

MangoIV commented Nov 11, 2024

BinderDavid commented Nov 11, 2024 •

edited

Loading

MangoIV commented Nov 11, 2024

timsueberkrueb commented Nov 11, 2024 •

edited

Loading

MangoIV commented Nov 15, 2024

timsueberkrueb left a comment

timsueberkrueb Nov 15, 2024

timsueberkrueb Nov 15, 2024

timsueberkrueb Nov 15, 2024

MangoIV Nov 15, 2024 •

edited

Loading

timsueberkrueb Nov 15, 2024 •

edited

Loading

MangoIV Nov 15, 2024

timsueberkrueb Nov 15, 2024

timsueberkrueb Nov 15, 2024

timsueberkrueb Nov 15, 2024

MangoIV Nov 15, 2024

timsueberkrueb Nov 15, 2024

timsueberkrueb Nov 15, 2024 •

edited

Loading

	- name: build and run polarity using nix
	- name: Build and run polarity using nix

	- name: build and run a static polarity exe
	- name: Build and run a static polarity exe

	/// Lambda abstractions \x. e
	/// Lambda abstractions (syntactic sugar), e.g. \x. e

	/// Function arrow in syntax
	/// Function arrow (syntactic sugar), e.g. a -> b



		codef ZipWith(n : Type, f : (CoNat -> CoNat -> CoNat), l1:CoList(n), l2: CoList(n)) : CoList(n) {
		}

Trace back unification error #339

Are you sure you want to change the base?

Trace back unification error #339

Conversation

MangoIV commented Oct 27, 2024 • edited Loading

timsueberkrueb left a comment

Choose a reason for hiding this comment

MangoIV commented Nov 7, 2024

MangoIV commented Nov 7, 2024

MangoIV commented Nov 7, 2024

MangoIV commented Nov 7, 2024

MangoIV commented Nov 7, 2024

BinderDavid commented Nov 7, 2024

MangoIV commented Nov 7, 2024

MangoIV commented Nov 11, 2024

MangoIV commented Nov 11, 2024

BinderDavid commented Nov 11, 2024 • edited Loading

MangoIV commented Nov 11, 2024

timsueberkrueb commented Nov 11, 2024 • edited Loading

MangoIV commented Nov 15, 2024

timsueberkrueb left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

MangoIV Nov 15, 2024 • edited Loading

Choose a reason for hiding this comment

timsueberkrueb Nov 15, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

timsueberkrueb Nov 15, 2024 • edited Loading

Choose a reason for hiding this comment

MangoIV commented Oct 27, 2024 •

edited

Loading

BinderDavid commented Nov 11, 2024 •

edited

Loading

timsueberkrueb commented Nov 11, 2024 •

edited

Loading

MangoIV Nov 15, 2024 •

edited

Loading

timsueberkrueb Nov 15, 2024 •

edited

Loading

timsueberkrueb Nov 15, 2024 •

edited

Loading