search

au-ts / cogent

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

TypeCheck fails for builtin array types #413

Closed gteege closed 2 years ago

gteege commented 2 years ago

The following code

f : U32[5] -> U32

causes the error message

Parsing...
Resolving dependencies...
Typechecking...
Desugaring and typing...
cogent: toTCExpr: unification term variable ?0 found: the 'impossible' happened!
If you see this, please report this bug to
    <https://github.com/au-ts/cogent/issues>

The code 

f : U32#[5] -> U32
f a = 0

causes the error message

Parsing...
Resolving dependencies...
Typechecking...
Error: Constraint
   Solved A U32 [?0] [U]
cannot be solved, or is unsatisfiable.
   with relevant unifiers:
      • The unknown ?0 originates from the term 5
        of type U32[5]
        at location"./ArrayTypeCheckImposs.cogent" (line 1, column 1)
   in the definition at ("ArrayTypeCheckImposs.cogent" (line 1, column 1))
   for the function f
Compilation failed!

It happens in master branch in commit 92e2f41db1c53ef (Jul 4 2022) compiled by make INSTALL_FLAGS='--flags="+builtin-arrays -docgent -refinement-types -haskell-backend"' The problem first occurs after commit ad090b620936671846 (Sep 29 2021) It also makes the tests in cogent/tests/tests/ext-array fail.

gteege commented 2 years ago

I also tried compiling with make INSTALL_FLAGS='--flags="+builtin-arrays -docgent +refinement-types -haskell-backend"' but it did not change anything.