Can't handle monomorphic Data because 0-arg constructors aren't wrapped in ETApp

[shingarov]

Consider this example:

type list('a) =
  | Nil
  | Cons (x:'a, xs:list('a))
  ;
/*@ val emptylist : 'a => list('a) */
let emptylist = (x) => {
  let t = Nil;
  t
};

During elaborating let t = Nil; the EImm(Nil) gets wrapped in a ETApp and then synth gets rid of the Nil.

Similarly,

type coord =
  | CCCC (x:int)
  ;
/*@ val cassert : bool[b|b] => int */
let cassert = (b) => {
  0
};
/*@ val eat : coord => int */
let eat = (cc) => {
  1
};
/*@ val check : m:int => int */
let check = (m) => {
    let x = 1;
    let p = CCCC(x);
    let i = eat(p);
    let ok = i < 0;
    cassert(ok)
};

works because in let p = CCCC(x) the CCCC(x) is an EApp and again the synth gets rid of the free CCCC.

However, if we remove polymorphism on 'a in the first example, or the argument to CCCC in the second example, Sprite will crash. This is because the Imm does not get wrapped in neither EApp nor ETApp, it simply remains EImm, so the constraints contain the free variable Nil or CCCC, and Fixpoint crashes with Constraint with free vars.

I am wondering how to best fix this. ETApp and EApp follow the curried style, but this works for nArgs>0. I would best like to follow Lawvere's "elements as morphisms from void". Shall we introduce something like TVoid along TBase and friends so we can pass it as argument to ETApp?