mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-26 05:01:34 +03:00
97ee3d4cd3
We already did this, but missed a few cases due to the way arguments are elaborated. So now, when checking an LHS, we don't allow LHS argument types to be inferred from the pattern, but rather they must be inferred from elsewhere. To do this, we keep track of the constraints which would be solved when inferring the type, and make sure they don't solve any new metavariables. Fixes #1510, and also now gets the error location right as a bonus!
12 lines
587 B
Plaintext
12 lines
587 B
Plaintext
Processing as TTImp
|
|
Written TTC
|
|
Yaffle> Bye for now!
|
|
Processing as TTImp
|
|
Vect2:25:1--26:1:{pat 0 {b:28} : Type} => {pat 0 {a:27} : Type} => ($resolved380 {b:28}[1] {a:27}[0] $resolved361 ($resolved370 {a:27}[0]) ($resolved370 {b:28}[1])) is not a valid impossible pattern because it typechecks
|
|
Yaffle> Bye for now!
|
|
Processing as TTImp
|
|
Vect3:25:1--26:1:Not a valid impossible pattern:
|
|
Vect3:25:9--25:11:When unifying: Main.Nat and (Main.Vect ?Main.{n:22}_[] ?Main.{b:20}_[])
|
|
Vect3:25:9--25:11:Type mismatch: Main.Nat and (Main.Vect ?Main.{n:22}_[] ?Main.{b:20}_[])
|
|
Yaffle> Bye for now!
|