Jesper Cockx

After a discussion at dinner yesterday, I am now much more positive about the possibility of a `--no-definitional-singleton-types` flag, because it would not just improve performance but also make it...

I would argue that we do not want to suggest `--overlapping-instances`, but instead suggest that you make your instances non-overlapping.

> A possible problem with the alternative approach is that we might get code duplication, because we have two ways to represent top-level functions: either as regular functions, or as...

> I tried https://github.com/agda/cubical/pull/1037 to come up with a better way to organize the notation in the cubical library and I don't see how to do that without overlapping instances....

@nad > I suggested two flags because the default could be "off" for record types with η-equality and erased fields (which have presumably not been used a lot yet), and...

> We were previously just looking into miGeneralizable field and disabled sharing if it is YesGeneralizeVar or YesGeneralizeMeta. > > But that didn't cover all the cases. That's strange, I...

One other way to handle generalized metas is to always instantiate metas if the solution is a variable or a metavariable. This would fire also in cases where the meta...

I have an experiment I would like to do that requires this flag, so I will try to implement a first version of it.

My motivation for adding this flag would be to make the occurs checker more powerful and efficient when we can assume there are no record types with all fields irrelevant...

I think I mean "an unapplied variable or a metavariable applied to (a subset of) the variables in scope".