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

Simple layout polymorphic function fails #396

Open
amblafont opened this issue Mar 19, 2021 · 3 comments
Open

Simple layout polymorphic function fails #396

amblafont opened this issue Mar 19, 2021 · 3 comments

Comments

@amblafont
Copy link
Contributor

Cogent fails to compile this function, on master:

main : all (l :~ {a : U8} ). {a : U8} layout l -> {a : U8} layout l
main x = x

I get the output:

Parsing...
Resolving dependencies...
Typechecking...
Error: The layout of type 
   R ❲a : U8 (present) | ✗❳ [U]
 does not fit the layout of type 
   R ❲a : U8 (present) | ✗❳ [W] ()
   in the definition at ("simplepoly.cogent" (line 3, column 1))
   for the function main
Error: The layout of type 
   R ❲a : U8 (present) | ✗❳ [U]
 does not fit the layout of type 
   R ❲a : U8 (present) | ✗❳ [W] ()
   in the definition at ("simplepoly.cogent" (line 3, column 1))
   for the function main
Compilation failed!
@amblafont
Copy link
Contributor Author

The above example is expected to fail because l is a layout for a pointer. However, the following also fails:

main : all (l :~ (#{a : U8}) ). {a : U8} layout l -> {a : U8} layout l
main x = x

@amblafont
Copy link
Contributor Author

it also fails on main : all (t, l :~ t ). t layout l -> t layout l

@zilinc zilinc closed this as completed in 8d7e015 Mar 19, 2021
@zilinc zilinc reopened this Mar 19, 2021
@zilinc
Copy link

zilinc commented Mar 19, 2021

8d7e015 fixes the first problem, and also parens around the RHS of :~ is no longer required.

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

2 participants