Solve holes in nats in typeEqRigid #82
Description
We are not even trying to solve holes, this is probably what's hitting us with examples such as
unfull(n :: #, v :: Vec(Bool, full(n))) -> Nat
unfull(n, _) = n
two :: Nat
two = unfull(!, [false, false, false])
with error message (on branch just-nat-solving (#70) or inference-wip/fork)
Expected vector of length (2^(VPar In check_defs_1_two_1_Eval 0) - 1)
from the type: Vec(Bool, (2^(VPar In check_defs_1_two_1_Eval 0) - 1))
but got vector: [false(()),false(()),false(())]
of length (> 0)