Skip to content

Instantiate implied bounds explicitly #117

Open
@nikomatsakis

Description

@nikomatsakis

There are a number of soundness holes caused, directly or indirectly, by the way that we handle implied region bounds on functions. The current codebase tries to hack them in "on the side" rather than explicitly instantiating where-clauses in the compiler's logic. Converting implied bounds to be explicit is conceptually easy, but it requires supporting where-clauses (and implied bounds) attached to higher-ranked binders.

Requires #116

Related unsoundness bugs:

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    Status

    No status

    Milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions