Can I use arrow meta to change generics on types b...

# arrow-meta

[redrield]

Can I use arrow meta to change generics on types before code analysis?

[raulraja]

Are the calculated types already in the AST as if the user or source codegen typed them?

[raulraja]

If that is the case you can use the quote system to transform the sources before analysis

[raulraja]

If you need the type checked info then you can modify the IR tree with the meta DSL but at that point it would have to be already valid Kotlin and for what I understood earlier the issue is that it does not typecheck

[raulraja]

You can also.alter the type checker like the type proofs system does in meta in the sv-test-proofs branch

[raulraja]

To actually make it type check if you know it's right

[raulraja]

The ProofsPlugin does that for all type relationships that are proven to have a morphism between them.

[redrield]

Where can I find code for ProofsPlugin?

[raulraja]

https://github.com/arrow-kt/arrow-meta/tree/sv-test-proofs/compiler-plugin/src/main/kotlin/arrow/meta/plugins/proofs

[raulraja]

Using a custom typechecker like that one you could tell the compiler those typecheck then you have to provide a cast or something in IR where the impossible cast would happen

[raulraja]

Or replace the types in quotes before typechecking if you don't want to deal with the typechecker

[raulraja]

Did you have to build or create some kind of HList in your library for dimensions or does it include any predicates like AllOf where you have arity of N type parameters ?

[redrield]

In the few locations in the linear algebra library where a concrete instance was required, the numeric superclass enforced a val i: Int in subclasses, just used that

[redrield]

Also, is there somewhere I can find example uses of Proofs? @raulraja

[raulraja]

The prelude module is full of proofs for union types etc

[raulraja]

The syntax can be seen exercised in the tests of the compiler-plugin module

[raulraja]

Sorry, on my phone or I'd provide links