Skip to content
New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

#

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

Jump to bottom

An unused implicit argument of an interface method produces an unresolved hole #3474

Open
spcfox opened this issue Jan 21, 2025 · 4 comments · May be fixed by #3475
Open

An unused implicit argument of an interface method produces an unresolved hole #3474

spcfox opened this issue Jan 21, 2025 · 4 comments · May be fixed by #3475

Comments

@spcfox
Copy link
Contributor

spcfox commented Jan 21, 2025

Steps to Reproduce

interface Iface where
  method : {x : Type} -> Type

Expected Behavior

Successful compilation

Observed Behavior

Error: Unsolved holes:
Main.{x:836} introduced at:
@spcfox spcfox changed the title An unused interface method argument produces an unresolved hole An unused implicit argument of an interface method produces an unresolved hole Jan 21, 2025
@spcfox
Copy link
Contributor Author

spcfox commented Jan 21, 2025 •
edited
Loading

The problem is in the method code after elaboration. This is similar to #3467

data Iface : Type where
  MkIface : ({x : Type} -> Type) -> Iface

failing "Unsolved holes"
  method : Iface => {x : Type} -> Type
  method @{MkIface f} = f

@spcfox
Copy link
Contributor Author

spcfox commented Jan 21, 2025 •
edited
Loading

It is strange that the compiler returns code 0:

$ idris2 --check Main.idr; echo $?
1/1: Building Main (Main.idr)
Error: Unsolved holes:
Main.{x:831} introduced at: 
0

But with the manually desugared version (from the previous post) code 1

@spcfox
Copy link
Contributor Author

spcfox commented Jan 22, 2025 •
edited
Loading

This code also produces an unsolved hole:

interface Fail where
  f : Type -> {_ : Type} -> Type

@spcfox spcfox linked a pull request Jan 22, 2025 that will close this issue
Open
1 task
@spcfox
Copy link
Contributor Author

spcfox commented Jan 26, 2025

Another bug that isn't fixed in #3475:

interface Iface where
  method : (x : Double) -> Type

failing "Mismatch between: Double and Int"
  implementation {x : Int} -> Iface where
    method _ = Type

# for free to join this conversation on GitHub. Already have an account? # to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

[ fix #3474 ] Fix implicit arguments in interface methods spcfox/Idris2
1 participant
@spcfox