aya-prover / aya-dev

A proof assistant and a dependently-typed language
https://www.aya-prover.org
MIT License
279 stars 16 forks source link

Pat.Ctor#toExpr didn't insert arguments for ownerTele. #609

Closed HoshinoTented closed 1 year ago

HoshinoTented commented 1 year ago

Minimum code:

open data Single (A : Type) | single {A}
def justMatch {A : Type} (s : Single A) : Single A
  | single => s
Aya said ``` In file main.aya:3:4 -> 1 | open data Single (A : Type) | single {A} 2 | def justMatch {A : Type} (s : Single A) : Single A 3 | | single => s ^----^ Error: Cannot check the expression _5 of type A against the type Type 0 at (96-101) [3,4-3,9] ```

The clause | single => s is expanded to | {A}, single {_5} => single {_5} which is incorrect.

ice1000 commented 1 year ago

Thanks!!! I expected this bug, but I didn't come up with a counterexample. Apparently you are better than me lmao