Typeclasses. New errors when switching from ML to a layered effect
- Dominant language
- F*
- Stars
- 3.1k
- Forks
- 267
- Avg merge
- 10h 45m
- Merged PRs (30d)
- 54
Description
I used type classes to define a `import` function. Everything works great if I use only the `ML` effect and it also worked with a dm4all effect. Now, I am trying to migrate to layered effects and I get some errors.
To reproduce:
Clone the code here: https://github.com/andricicezar/fstar-io/tree/bug_2128
Try to check this file which should work fine (ML effect): https://github.com/andricicezar/fstar-io/blob/bug_2128/unkn.fst
Try to check this file which should fail in two places (layered effect): https://github.com/andricicezar/fstar-io/blob/bug_2128/unknM4.fst
You can find the errors as comments in the file. There are two different problems/errors on line 38 and 51.
FStar version: e0ba9134812b74dc112be287c108ccff8f1ab064
Contributor guide
Assessment
This issue has not been assessed yet.