mirror of
https://github.com/anoma/juvix.git
synced 2025-01-05 22:46:08 +03:00
90f607e6ce
In the following case:
```
module WrongConstructorArity;
inductive T {
A : T;
};
f : T → T;
f (A i) ≔ i;
end;
```
The typechecker fails when checking the clause `f (A i) := i` because of
the extra constructor argument. However if typechecking continues then
the variable `i` on the rhs does not have a type so we must short-circuit.
|
||
|---|---|---|
| .. | ||
| negative | ||
| positive | ||