search

au-ts / cogent

Cogent Project
https://trustworthy.systems/projects/TS/cogent.pml
Other
158 stars 26 forks source link

Simple layout polymorphic function fails #396

Open amblafont opened 3 years ago

amblafont commented 3 years ago

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 commented 3 years ago

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 commented 3 years ago

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

zilinc commented 3 years ago

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