Find a way to implement strict composition

[ecavallo]

import path
import J

data vacu where
| more (x : vacu)

let Code (m : vacu) (n : vacu) : type =
  elim n [ more n' => Path vacu m n' ]

let test (m : vacu) (p : Path vacu (more m) (more m)) : Path vacu m m =
  J vacu (more m) (lam n _ -> Code m n) (lam _ -> m) (more m) p

raises Failure("rigid_hcom_strict_data: peel_arg"). The bug disappears if I make vacu nonrecursive.

[jonsterling]

@ecavallo Heh, I bet I forgot to deal with neutrals? Let me think about it.

[jonsterling]

Resolved by #230

[jonsterling]

Ahh, my fix didn't quite work. I'm disabling strict composition for now. I want to discuss it with the crew more to see if it can be recovered, but let me say two things:

1. It is very expensive to even find out if we can do a strict composition
2. Even if we can find a way to make that efficient, I am not sure it even makes sense. This thing, where you have to check that all the faces of the system are constructors seems very iffy to me in the open term setting; to really do it properly, you need a way to invert a constructor (like succ) on a neutral, and while we can define this for specific types, such as nat, I don't know if it makes any sense in general.

[favonia]

This is not really closed yet.

[jonsterling]

Well, if we will re-open it, let me at least rename it.