Dependent type checking fallback

[maxkurze1]

Type checking for dependent Koika functions

The default type checker only tries to construct the checked term by using vm_compute. However, when a Koika function depends on some variable, say s, this check will get stuck on a term like forall s, ... EqDec.ec_dec s s .... This equality is rather computed than proven, but for this computation it is necessary to know the exact value of s.

To circumvent this problem (and it is really more a workaround than a solution), I built a tactic, that carefully computes the type leaving eq_dec occurrences untouched. These occurrences are then (if possible) rewritten with a proof.

This workaround is incorporated into the normal type checking algorithm as a fallback, in other words, the type checker will first try to construct the term using vm_compute (which should be faster) and only if this fails it will try to compute it using the new tactic.

[maxkurze1]

Even using vm_compute here turns out to be too aggressive in certain situations;

Working on a patch... probably fixed in a couple of minutes

[maxkurze1]

Now the tactic uses cbn instead of vm_compute which should be conservative enough

[maxkurze1]

There is still some work to do here.
At the moment, I am able to construct a proof that the type checking succeeds. However, this proof term is massive, and it is part of the resulting term which bloats all following proofs and makes it hard to work with the action.

It would be nice to abstract the proof term and only keep the fact that it exists.

[sertel]

Please provide a hint database to register manual proofs.
Garvit actually has started to write some "machinery" for type-checking in a more modular way. That we can also contribute to this PR.