Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Foralls do not typecheck #86

Closed
yannham opened this issue Jun 10, 2020 · 0 comments
Closed

Foralls do not typecheck #86

yannham opened this issue Jun 10, 2020 · 0 comments

Comments

@yannham
Copy link
Member

yannham commented Jun 10, 2020

[EDIT] I misunderstood something and jumped to conclusions. Polymorphic instantiation works (almost, see #88) fine

Describe the bug
Valid programs annotated with polymorphic types, that is with a Promise(ty, foo) where ty contains a forall, do not typecheck.

For example, executing (with some preparation first, see To reproduce) src/examples/forall.ncl containing

let f = Promise(forall a. (forall b. a -> b ->  a), fun x => fun y => x) in
f

with nickel <src/examples/forall.ncl results in the error message:

Typechecked: Err("The following types dont match Arrow(Constant(1), Concrete(Arrow(Constant(2), Constant(1)))) 
 -- Forall(Ident(\"a\"), Concrete(Forall(Ident(\"b\"), Concrete(Arrow(Concrete(Var(Ident(\"a\"))), Concrete(Arrow(Concrete(Var(Ident(\"b\"))), Concrete(Var(Ident(\"a\"))))))))))")
[...]

To Reproduce
This is not directly visible as there is a strict parameter, currently set to false when the typechecker starts, which basically disable typechecking if not set. It corresponds to "dynamic typing" mode, but it should still enforce the type of Promise: why it does not is a different matter. A quick way to isolate this issue is set it to true from the beginning, but then automatically included contracts do not typecheck anymore:

  • set strict to true in typecheck.rs
  • disable the automatic inclusion of the basic contracts by setting include_contracts to false in program.rs
  • cargo build
  • target/debug/nickel <src/examples/forall.ncl

Expected behavior
The program should be accepted by the typechecker:

Typechecked: Ok(Types(Arrow(Types(Dyn), Types(Arrow(Types(Dyn), Types(Dyn))))))
[...]
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant