Skip to content

Interactions between functors and constaint guards #1444

@yav

Description

@yav

Investigate: There appear to be some issues related to evalType being called on constraints, which leads to `panic

Issue: when instantiating a functor that contains constraint guards, it is possible that some of the constraint guards become
impossible (e.g., if they depend on the parameter). This means that the types corresponding to the functions implementing them
would contain an impossible assumption, which is currently represented with Error, and evalType is not happy with that.
We know that such functions will not be called as they are only called if the guard is true (which it will not) but it looks like our evaluator
eagerly evalutes such types.

Metadata

Metadata

Assignees

Labels

bugSomething not working correctlyparameterized modulesRelated to Cryptol's parameterized modulestype-guards

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions