Runtime error

[sjcjoosten]

I asked Synquid (via 'try online') a question that is a variation on the replicate problem, given below. I got this error (truncated for brevity):

/var/www/comcom/tmp/Synquid/9586857029030353/Synquid.sq:29: Error:
Cannot match shape 'List (A4)'
with shape 'Int'
when checking...

The way I read this error is as if synquid is synthesizing something that is not type correct, and then fail because of it. Therefore I believe this would be a bug in synquid. I'm not sure whether synquid should be able to give me sufficiently strong refinements for this particular input, but I do expect synquid's output to be either a solution or a more reasonable error message.

Not sure if and how you would like to see bugs like these reported, let me know or just take your liberties in editing this issue. Thanks for the amazing work in building Synquid!

-- Type synonym for natural numbers (_v denotes the "value variable")
type Nat = {Int | _v >= 0}

-- List data type: just like in Haskell
data List a where
	Nil :: List a
	Cons :: x: a -> xs: List a -> List a
  
-- Measures define recursive properties of datatypes, which we can mention in refinements; 
-- this measure is also marked as a termination metric for recursive calls
termination measure len :: List a -> {Int | _v >= 0} where
  Nil -> 0
  Cons x xs -> 1 + len xs 
  
-- Synquid composes programs from component functions;
-- here are some standard integer components we might need
one :: {Int | _v == 1}
minus :: x: Int -> {Int | _v == (0 - x)}
plus :: x: Int -> y: Int -> {Int | _v == x + y}
leq :: x: Int -> y: Int -> {Bool | _v == (x <= y)}
	
-- Our synthesis goal: a function that returns 'n' copies of 'x'
replicate :: n: Nat -> x: a -> {List a | len _v == n}
replicate = ??