InternalException about Generalized Variables

[HoshinoTented]

[HoshinoTented]

There is no A in bar's telescope because A was not used in bar's telescope. However, we can't just allowGeneralized = false when resolving the body because we should accept foo.

We can generate more generalized variables after we resolve the body, but this sounds not good:

• The newly generated variables won't be appended to the LocalCtx of the meta which is in the telescope

[ice1000]

IMO bodies should not use generalized variables.

[ice1000]

But I think we can make it work for simple bodies

[HoshinoTented]

So I reopen this.