search

djspiewak / skolems

A microlibrary for Scala encodings of higher-rank quantifiers
Apache License 2.0
60 stars 8 forks source link

Add an implicit applied Forall instance #3

Closed joroKr21 closed 4 years ago

djspiewak commented 4 years ago

I still don't get how it works in 2.13 here (it fails in the repl), but Travis certainly thinks it doesn't work in 2.12 or 2.11. I wonder if there's a way to work around that?

joroKr21 commented 4 years ago

Since the error is diverging implicit expansion could it be byname implicits?

djspiewak commented 4 years ago

My guess is that the reason it diverges is it doesn't find the Forall which is actually in scope, and instead tries to fabricate one using Forall.materialize, which in turn seeks out the same instance which we were hunting for in the first place, hence the loop.