aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/bug_11140.v
AgeCommit message (Collapse)Author
2020-08-19Adding the example of bug #2904 into the test suite, and reorganising the ↵Martin Bodin
test files. Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> Co-authored-by: Hugo Herbelin <Hugo.Herbelin@inria.fr>
2020-01-06Fix #11140: Bidirectionality hints perform (surprising?) simplificationMaxime Dénès
We typecheck arguments like previously, using bidirectionality hints, but ultimately replace them with user-provided arguments on which we replay coercion traces. This is a fix which should be easy to backport, but there are two directions of future work: - Coercion traces for `Program` coercions (in these cases, we currently use the inferred arguments) - Separate the Coercion API in two phases: inference and application of coercions. It will make the approach taken here cleaner, and probably make it easier to interleave typing steps with coercion inference. Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>