koka-lang / koka

Koka language compiler and interpreter
http://koka-lang.org
Other
3.16k stars 151 forks source link

Unresolved implicit parameter #468

Closed TimWhiting closed 1 month ago

TimWhiting commented 4 months ago

Discussed in https://github.com/koka-lang/koka/discussions/467

Originally posted by **woojamon** February 8, 2024 May I ask why the `show` function is not implicity resolved in the example below? ```koka // main.kk type myType MyCase(value:int) fun show(result:error) : pure string match result Ok(m) -> "MyCase" Error(x) -> exn/show(x) fun eq(left:error, right:error) : pure bool match (left,right) (Ok(_),Ok(_)) -> True (Error(l), Error(r)) -> l.message == r.message _ -> False pub fun myFun(p1:a, p2:a, ?eq:(a,a) -> pure bool, ?show:a -> pure string) "hello" fun main() myFun(Ok(MyCase(1)),Ok(MyCase(2))) ``` > main.kk(19,36): error: cannot resolve implicit parameter context : myFun(Ok(MyCase(1)),Ok(MyCase(2))) parameter : ?show : (error) -> pure string candidates: ... hint : add a (implicit) parameter to the function signature?

This seems like a bug

TimWhiting commented 4 months ago

@woojamon

Explicitly adding ,?show=show works, but the above example without the explicit show should ideally work as well.

Ahh, I think I figured it out. The main function isn't in the same recursive definition group as show because it doesn't use show explicitly. This means that it could be type checked prior to show is defined. You can move the datatype / helper function to its own file, or even do something as simple as calling show("") and it type checks fine.

woojamon commented 4 months ago

Ok, I'll move some things to their own files. Thanks!

woojamon commented 4 months ago

Wait, why doesn't eq suffer the same problem then?

TimWhiting commented 4 months ago

It just happens to be typed checked prior to main, or is uniquely named.