Spurious type checking error generated when using a lambda involving types without a type signature

[AHartNtkn]

Describe the bug
When implementing a simple type class going through a type alias, functions which should type check don't, and the error it gives doesn't make much sense.

Desktop (please complete the following information):

• OS: Ubuntu
• Juvix Version: 0.6.9-b954100

To Reproduce
Steps to reproduce the behavior:

1. Clone this repo: https://github.com/anoma/nspec/tree/anthony/bug-report
2. Go to the file nspec/docs/prelude.juvix.md and attempt to type check it (you may need to remove the ? in nspec/docs/.juvix-build/0.6.9/deps/[...]/Package.juvix).
3. On line 506, the line right {B} {A} x will be highlighted with the error

The expression right {B} {A} x has type:   Result B A but is expected to have type:   Result A _ B A

Expected behavior
I don't believe this should produce an error at all, but Result also only takes two arguments, so the error reporting that it should take four is nonsense anyway.

Screenshots
N/A

Additional context
N/A

[paulcadman]

This is the file referenced in the report: https://github.com/anoma/nspec/blob/5fb908529f043729dee45324987863b7ae297cbb/docs/prelude.juvix.md

[paulcadman]

You can explicitly declare the type of swap in the instance as a workaround for now:

instance
EitherCommutativeProduct : CommutativeProduct Either :=
mkCommutativeProduct@{
  swap {A B} : Result A B -> Result B A := \{ e :=
    case e of {
      | (left x) := right {B} {A} x
      | (right x) := left x
    }};
};

alternatively with clearer style:

instance
EitherCommutativeProduct : CommutativeProduct Either :=
  mkCommutativeProduct@{
    swap {A B} : Result A B -> Result B A
      | (left x) := right {B} {A} x
      | (right x) := left x;
  };

See: https://github.com/anoma/nspec/tree/paul/anthony/bug-report-workaound for a branch containing this fix.

[janmasrovira]

I've updated the title of the issue to better describe it