Experiment with normalizing defs during type checking

[anka-213]

This is mostly an experiment to see if it could be done.

---

This allows more dependently typed programs to typecheck. For example the commented out line here:

https://github.com/GrammaticalFramework/gf-contrib/blob/a9697fbecbf3320fdf7c4543d9f8478b0c92a9c2/typetheory/Types.gf#L69-L72

Here's a self-contained example:

abstract DepType = {
    cat
        Set ;
        El Set ;
    data
        Sigma : (A : Set) -> (El A -> Set) -> Set ;
        pair : (A : Set) -> (B : El A -> Set) -> (a : El A) -> El (B a) -> El (Sigma A B) ;
    fun
        p : (A : Set) -> (B : El A -> Set) -> El (Sigma A B) -> El A ;
        q : (A : Set) -> (B : El A -> Set) -> (c : El (Sigma A B)) -> El (B (p A B c)) ;

    def
        p _ _ (pair _ _ a _) = a ;
        -- The line below type-checks with this patch but not without it
        q X Y (pair X Y x y) = y ;
    fun
        -- Lexicon
        P : Set ;

}

Without this patch the program above gives the error:

DepType.gf:
   DepType.gf:14:
     Happened in the definition of function q
      {x <> p X Y (pair X Y x y)}

with it it type checks

[krangelov]

Personally, I feel that trying to patch the current type checker is a lost cause. You can patch something up and another problem will pop up somewhere else. If you really want a good type checker, look at Ulf Norel's thesis and try to replicate it. There are far too many corner cases that don't work in the current implementation.

For type checking in the concrete syntax, an extension of:

Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich. Practical type inference for arbitrary-rank types.

is a better starting point.

Some changes are suspicious. For instance why does VApp take a list of arguments now? Why VCn takes a list of definitions?

[anka-213]

@krangelov This was more of an experiment than something intended to be merged (hence being a draft and "Experiment" in the title), but thank you for looking at it! I did it in response to a question about why the above program didn't type check.

I mostly did things in the simplest possible way I could think of and at a later stage possibly clean things up and do them in a more sensible way.

[anka-213]

@krangelov To answer your concrete questions: VApp takes a list so it's easier to find the head of an application and VCn contains a list of definitions because that was the easiest (but definitely not the best) way I could think of to pass that information on to the place that needed it.

But yes, reverting those changes would probably help with whatever caused the test failures. I only ever tested the type checker, so I apparently didn't notice that I broke the other parts of the compiler.