Skip to content
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

Adding a method with a theory extension breaks @instance #167

Open
kris-brown opened this issue Dec 6, 2024 · 1 comment · May be fixed by #168
Open

Adding a method with a theory extension breaks @instance #167

kris-brown opened this issue Dec 6, 2024 · 1 comment · May be fixed by #168
Assignees
Labels
bug Something isn't working

Comments

@kris-brown
Copy link
Collaborator

kris-brown commented Dec 6, 2024

GATs allow dispatching on types. Below theory T2 adds a new operation with the name h:

@theory T1 begin 
  X::TYPE; h(a::X)::X 
end
@theory T2<:T1 begin 
  Y::TYPE; h(b::Y)::Y 
end

@instance T1{Int} begin h(a::Int) = 1 end

There is a problem when trying to implement an instance of T2.

# ERROR # 
@instance T2{Int,Bool} begin 
  @import h
  h(b::Bool) = false 
end

The @import keyword within the @instance macro is commonly used when something has been implemented already. However, in this case, we cannot @import h because then h(::Bool) is not one of the expected signatures and it errors upon seeing that line.

I'll upload a fix to this soon that is working locally: basically it changes what @import does within the instance macro. Rather than removing expected signatures, whenever we have leftover unimplemented signatures (such as h(::Int) in the case above) we check if the name of the method is in the imports and ignore the missing method error if so.

@kris-brown kris-brown self-assigned this Dec 6, 2024
@kris-brown kris-brown added the bug Something isn't working label Dec 6, 2024
@kris-brown
Copy link
Collaborator Author

A more sophisticated approach would be syntax for @importing specific methods (with a particular signature) but that can be a further enhancement.

@kris-brown kris-brown linked a pull request Dec 7, 2024 that will close this issue
@kris-brown kris-brown linked a pull request Dec 7, 2024 that will close this issue
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant