Error with len > 3 but not len <= 3

[michael-swan]

Changing a line in the "list replicate" example on the ComCom website from:

replicate :: n: Nat -> x: a -> {List a | len _v == n}

to:

replicate :: x: a -> {List a | len _v == 4}

we see the following error:

/var/www/comcom/tmp/Synquid/0719913783814785/Synquid.sq:29: Error:
Cannot match shape 'Bool'
with shape '_'
when checking neq :: X1:_ -> X0:_ -> _
in
\x .
match neq ?? ?? with

If you instead use:

replicate :: x: a -> {List a | len _v == 3}

the following result is produced:

replicate = \x . Cons x (Cons x (Cons x Nil))

From my trivial investigation it appears that the simplifyContraint' function does not contain a case for one of the types being an LetT _ _ AnyT which I presume would constitute an empty constraint. This is me just guessing because it looks like simplifyContraint' already handles the AnyT case and that is the only RType whose pretty-printed shape could match "_" while also not being AnyT.

[nadia-polikarpova]

Hi Michael! Thanks for reporting, but this is not a bug, this is expected behavior (albeit not user-friendly :))

When Synquid cannot find a program that type-checks, it simply reports the type error it got from trying the very last program candidate in the search space. This type error is completely meaningless to the user, and it's just there as an artifact of the implementation. Just read this as "synthesis failed".

The reason it fails with with len > 3 is because of the search space bounds. You can increase the bound on the depth of applications Synquid is considering using the -a parameter. E.g. you can synthesize replicate :: x: a -> {List a | len _v == 10 } if you pass -a 10 as a command-line arg.

[michael-swan]

Ah got it, thanks!