Tallying error with recursive types
In the presence of recursive types and using a non-empty delta
, we get wrong solutions for tallying. For
# debug tallying ['a] [ [] -> [] , [(Int 'a)*] -> [] ];;
we get the empty solution.
As a result, in CDuce, we have
# let f (x: []): [] = x;;
val f : [ ] -> [ ] = <fun>
# let g (l: [(Int 'a)*]): [] = f l;;
val g : [ (Int 'a)* ] -> [ ] = <fun>
# g [1 2];;
- : [ ] = [ 1 2 ]
where a non-empty list is given type [ ]
.
(Kim, I'm not sure if it's the same problem you mentioned yesterday of the incorrect use of memoization.)