Trace back unification error

[MangoIV]

• see issue #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

[MangoIV]

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

[MangoIV]

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

[MangoIV]

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

[MangoIV]

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]

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]

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]

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

[MangoIV]

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]

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]

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]

(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]

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]

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

[MangoIV]

I have replaced all reason occurences with while_elaborating_span

[timsueberkrueb]

I have one final concern. More often than not, the nix CI workflows take > 10m which is more than twice as much as the average time of our current workflows. It seems this is mainly due to them not always using the cached Rust build. Can you look into that, @MangoIV?

[MangoIV]

I think in future it would be nice to make few of the spans optional. I do now know if this is possible in rust somehow but in Haskell you can use this HKD or type family pattern to opt in to the possibility of things missing where it's needed and use the non-missing version then:

-- HKD: 
data SpanH f = MkSpan {contents :: f String, location :: f Location}
type OptionalSpan = SpanH Maybe
type Span = SpanH Identity

-- type families
type data Optionality = Optional | Required
data SpanH (o :: Optionality) = MkSpan {contents :: F o String, location :: F o Location} 
type family F (o :: Optionality) where 
  F Optional a = Maybe a
  F Required a = a

[MangoIV]

It seems this is mainly due to them not always using the cached Rust build. Can you look into that

@timsueberkrueb I think this is because the new workflow is not on main yet and hence it doesn't do any caching in between worfklow runs as this requires access to a secret added by David. If the problems persist after merging, I will open an MR to revert the nix workflow and look into getting better caching for the build.

[MangoIV]

mmmh it actually takes quite a bit of time just compiling polarity itself. the nixpkgs rust build does not use any of the cached dependencies. I did also add a worfklow that builds polarity with musl again, which doubles the compile time as well.

So I think

• currently, if there's any change on polarity, it needs 10 minutes
• can be halved if we don't build the static exe
• can be substantially lowered by not using nixpkgs' rust support but something like crate2nix instead.

[MangoIV]

maybe I should remove the workflow then and just limit on checking that the nix code evaluates :)

[timsueberkrueb]

I think in future it would be nice to make few of the spans optional. I do now know if this is possible in rust somehow but in Haskell you can use this HKD or type family pattern to opt in to the possibility of things missing where it's needed and use the non-missing version then:

-- HKD: 
data SpanH f = MkSpan {contents :: f String, location :: f Location}
type OptionalSpan = SpanH Maybe
type Span = SpanH Identity

-- type families
type data Optionality = Optional | Required
data SpanH (o :: Optionality) = MkSpan {contents :: F o String, location :: F o Location} 
type family F (o :: Optionality) where 
  F Optional a = Maybe a
  F Required a = a

This is possible in Rust, but we decided to limit the use of type-level programming for the implementation to keep it approachable and easy to understand for people unfamiliar with Rust, but also to keep it more open to change and refactoring.

Instead, we use Option<Span> when a span is optional and we should document any invariants that apply.

[timsueberkrueb]

maybe I should remove the workflow then and just limit on checking that the nix code evaluates :)

Yes, you can always add a more cache-efficient workflow later or alternatively, a workflow that takes longer but runs on main or approved merge requests only.

[BinderDavid]

maybe I should remove the workflow then and just limit on checking that the nix code evaluates :)

Yes, you can always add a more cache-efficient workflow later or alternatively, a workflow that takes longer but runs on main or approved merge requests only.

The duration of a GitHub action on main doesn't slow us down in development, so we could just run the nix action only on main, and fix issues afterwards whenever something breaks with the nix build (which shouldn't be that frequent). We similarly already have the action which publishes the website that isn't tested in PRs.

[MangoIV]

the nix workflow should only run on main now :)

[MangoIV]

One cool thing about the static build is that we could theoretically add the executable it produces to a release for people who just want to run the exe without having to install a rust toolchain :)

[BinderDavid]

One cool thing about the static build is that we could theoretically add the executable it produces to a release for people who just want to run the exe without having to install a rust toolchain :)

Yes! The endgame would be to have the installation experience of Lean: You just have to install the vscode plugin, and the plugin installs the executable for you :)