-
Notifications
You must be signed in to change notification settings - Fork 16
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Printed names of meta-context variables for a hole do not match with their defined names #208
Comments
I haven't looked closely at this yet, but my suspicion is that the
refinement substitution generated by splitting is messing up the names
of the variables that were there on the outside.
I'll look into this this afternoon, hopefully.
|
It turns out that this is a lot more complicated than I first anticipated. The name changes are actually intentional. Beluga can't figure out what the indices of variables appearing in a branch are during indexing, because the refinement substitution isn't computed until type reconstruction. So during type reconstruction these variables get properly indexed using the Properly fixing this will probably require thinking really hard about how to eliminate apxnorm to avoid this reindexing at a later time. |
As a demonstration, when I have these holes,
bin/beluga <this file>
prints these contexts/typesFor me, it looks strange because I defined
Sn-Sne
withmlam R, N =>
, so I think the Meta-context should useR
andN
instead ofM
andN1
in this case. Though I'm not sure whether this behavior is intended or not....The text was updated successfully, but these errors were encountered: