samth/var — Issue #3: Unroll is not total, FLAT v HOC not right for rec/c
Author: dvanhorn
Created: 2011-10-20 00:41:34+00:00
State: open

Here's a contract:

```(rec/c X (or/c (cons/c X X) (-> (pred string? †)))))```

Notice that it is a legit contract according to our grammar -- productive and `FLAT` on the left and `HOC` on the right of the `or/c`.

But then

```(unroll (rec/c X (or/c (cons/c X X) (-> (pred string? †)))))```

ain't a contract because it's `HOC` on the left and right. So unroll is not total.

The problem is that `X` is considered `FLAT`, which isn't right -- but it's not `HOC` either. It really depends on the contract in which it's bound. In this case, it's always `HOC`. But imagine:

```(rec/c X (or/c (cons/c X X) empty))```

here, `X` is always `FLAT`.

Here's a program that demonstrates the bad unrolling.

#lang var
(module f racket
(require)
(define v
(cons (-- (λ () "a")) (-- (λ () "b"))))
(provide/contract
[v (rec/c X (or/c (cons/c X X) (-> string?)))]))

(require 'f)
v