Revision 72aa198b460b1ada73f66f35edc05901fe503f8c authored by Anish Tondwalkar on 01 August 2019, 07:53:00 UTC, committed by Anish Tondwalkar on 01 August 2019, 07:53:00 UTC
The problem is that when we have an ~> under an forall, at the term level we have a tabs, and that means we have to swtich from checking (at the type with the implicit parameter) to synthing (plus a subtyping check). But when we synth, this implicit parameter is simply not in scope: since it's not bound anywhere in the term, it can't be added to the context during synthesis.
1 parent 95a7cd4
stack.yaml
resolver: lts-12.15
packages:
- '.'
flags: {}
extra-deps:
- tasty-rerun-1.1.12
- './liquid-fixpoint/'
# liquid-fixpoint and deps
#- github: ucsd-progsys/liquid-fixpoint
# commit: 76fad453f5e3c7945179c9e311cc7b9fd9e08f03
- dotgen-0.4.2
- fgl-visualize-0.1.0.1
- intern-0.9.2
- located-base-0.1.1.1
- text-format-0.3.2
extra-package-dbs: []
Computing file changes ...
