Idris2/tests/ttimp/eta002/expected

Processing as TTImp
Eta:16:1--17:1:When elaborating right hand side of Main.etaBad:
Eta:16:10--17:1:When unifying: (Main.Eq ({arg:12} : Integer) -> ({arg:13} : Integer) -> Main.Test)) ({arg:12} : Integer) -> ({arg:13} : Integer) -> Main.Test)) \(x : Char) => \(y : ?Main.{_:18}_[x[0]]) => (Main.MkTest x[1] y[0]) \(x : Char) => \(y : ?Main.{_:18}_[x[0]]) => (Main.MkTest x[1] y[0])) and (Main.Eq (x : Char) -> (y : ?Main.{_:18}_[x[0]]) -> Main.Test)) ({arg:12} : Integer) -> ({arg:13} : Integer) -> Main.Test)) Main.MkTest \(x : Char) => \(y : ?Main.{_:18}_[x[0]]) => (Main.MkTest x[1] y[0]))
	Eta:16:10--17:1:Type mismatch: Integer and Char
Yaffle> Bye for now!
Add test script They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here! 2020-05-19 20:25:18 +03:00			`Processing as TTImp`
[ new ] `--install-with-src`; refactoring around `FC`s (#1450) Why: * To implement robust cross-project go-to-definition in LSP i.e you can jump to definition of any global name coming from library dependencies, as well as from the local project files. What it does: * Modify `FC`s to carry `ModuleIdent` for .idr sources, file name for .ipkg sources or nothing for interactive runs. * Add `--install-with-src` to install the source code alongside the ttc binaries. The source is installed into the same directory as the corresponding ttc file. Installed sources are made read-only. * As we install the sources pinned to the related ttc files we gain the versioning of sources for free. 2021-06-05 14:53:22 +03:00			`Eta:16:1--17:1:When elaborating right hand side of Main.etaBad:`
Check LHS arguments are polymorphic enough 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! 2021-06-13 15:31:40 +03:00			Eta:16:10--17:1:When unifying: (Main.Eq ({arg:12} : Integer) -> ({arg:13} : Integer) -> Main.Test)) ({arg:12} : Integer) -> ({arg:13} : Integer) -> Main.Test)) \(x : Char) => \(y : ?Main.{_:18}_[x[0]]) => (Main.MkTest x[1] y[0]) \(x : Char) => \(y : ?Main.{_:18}_[x[0]]) => (Main.MkTest x[1] y[0])) and (Main.Eq (x : Char) -> (y : ?Main.{_:18}_[x[0]]) -> Main.Test)) ({arg:12} : Integer) -> ({arg:13} : Integer) -> Main.Test)) Main.MkTest \(x : Char) => \(y : ?Main.{_:18}_[x[0]]) => (Main.MkTest x[1] y[0]))
[ new ] `--install-with-src`; refactoring around `FC`s (#1450) Why: * To implement robust cross-project go-to-definition in LSP i.e you can jump to definition of any global name coming from library dependencies, as well as from the local project files. What it does: * Modify `FC`s to carry `ModuleIdent` for .idr sources, file name for .ipkg sources or nothing for interactive runs. * Add `--install-with-src` to install the source code alongside the ttc binaries. The source is installed into the same directory as the corresponding ttc file. Installed sources are made read-only. * As we install the sources pinned to the related ttc files we gain the versioning of sources for free. 2021-06-05 14:53:22 +03:00			`Eta:16:10--17:1:Type mismatch: Integer and Char`
Add test script They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here! 2020-05-19 20:25:18 +03:00			`Yaffle> Bye for now!`