Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 170
    • Issues 170
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 25
    • Merge requests 25
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • IrisIris
  • Issues
  • #165
Closed
Open
Issue created Mar 06, 2018 by Ralf Jung@jungOwner

Better (?) approach to control typeclass resolution based on whether some arguments are evars

Right now, some of our typeclasses have extra variants called KnownXXX that use Hint Mode to only apply when certain arguments are not evars. This has lead to an explosion in the number of typeclasses.

Maybe a better approach would be to change the way we write some instances, and make sure they can only succeed if some arguments are not evars. I described such a solution at https://gitlab.mpi-sws.org/FP/iris-coq/commit/a9d41b6374f44fd93629f99cfecfea3549baa0b1#note_25278.

One possible concern is that applying such instances should fail as early as possible; if they have other premises, those shouldn't be resolved unless the evar check passes. On the other hand, the KnownXXX classes introduce additional coercions that typeclass resolution will try all the time, which could also be a performance issue.

Assignee
Assign to
Time tracking