Tesla Zhang‮

> > Then the instance should raise a type error saying that unsolved meta at location > > Because meta should be solved within the definition? btw, this is why...

> > aya-prover/aya-prover-proto#503 when > > I think its unrelated to most general unifiers but this weekend maybe Ik but I'm very looking forward to it

> > I suggest asking in AK's discord server. Have you joined it yet? > > No. Could you invite me? https://discord.gg/89c3EXtx

@re-xyr Just post in #general

@re-xyr Yeah

@re-xyr IMO this meta should be solved..

@tonfeiz This is very easy: allow the tycking to be parameterized by some options. For example, there can be an option to disable the level solver and level errors.

@tonfeiz Just the one I mentioned, it's called type-in-type

@tonfeiz But just for now. Maybe add more.

I don't plan to include it in the most recent release