Reproduce problematic case of Ulf Norell's PhD

[BinderDavid]

In his PhD thesis (https://www.cse.chalmers.se/~ulfn/papers/thesis.pdf) Ulf Norell describes a problematic case for unification with metavariables in section 3.1. I am trying to reconstruct that example, but I trigger another bug first.
My attempt is here:

-- Example taken from the PhD of Ulf Norell
-- Chapter 3.1

data Bool { True, False }

data Nat { Z, S(pred: Nat) }

def Bool.neg : Bool {
    True => False,
    False => True,
}

codata Fun(a b: Type) {
    Fun(a,b).ap(a b: Type, x: a) : b
}

-- | The dependent function type.
codata Π(a: Type, p: Fun(a, Type)) {
    Π(a, p).pi_elim(a: Type, p: Fun(a, Type), x: a) : p.ap(a, Type, x)
}

codef F: Fun(Bool, Type) {
    .ap(_,_,x) => x.match {
        True => Bool,
        False => Nat,
    }
}

let T : Type {
    Fun(Π(F.ap(Bool, Type, (? : Bool)), \x. F.ap(Bool, Type, x.neg)),Nat)
}

let error : T { \g. g.pi_elim(Nat, \x. F.ap(Bool, Type, x.neg), 0)}

The error I get is:

Error: T-011

  × Type annotation required for typed hole
    ╭─[file:///Users/david/GitRepos/polarity-lang/polarity/examples/norell.pol:29:1]
 29 │ let T : Type {
 30 │     Fun(Π(F.ap(Bool, Type, (? : Bool)), \x. F.ap(Bool, Type, x.neg)),Nat)
    ·                             ─
 31 │ }
    ╰────

That seems to be wrong, since I explicitly provide a type annotation for that hole... I think we are not correctly switching between inference and checking in the case of type annotations.

[BinderDavid]

The trace ends with the following lines:

[[]] |- ?0.match {
        True => Bool,
        False => Nat
    } <= Type

So it seems that we have lost the type annotation during normalization, and then try to infer it?

[BinderDavid]

Ok, the bug really seems to stem from this here:

polarity/lang/elaborator/src/normalizer/eval.rs

Lines 259 to 266 in db9028b

	impl Eval for Anno {
	type Val = Box<Val>;
	fn eval(&self, prg: &Module, env: &mut Env) -> Result<Self::Val, TypeError> {
	let Anno { exp, .. } = self;
	exp.eval(prg, env)
	}
	}

Because we might normalize a term whose computation is blocked by (? : e) but which we try to typecheck after normalizing in a position where we need to infer a type. I think we need to extend neutral terms by

n := ... | (n : v)