Typechecker loops

[anshwad10]

Impredicativity in Arend allows encoding the Girard-Hurken paradox in an inconsistent context; In the following code:

\import HLevel
\import Logic
\import Paths.Meta

\class Girard (all-prop : \Pi (A : \Set) -> isProp A) {
  \data V
    | set (A : \Prop) (f : A -> V)
    \where
      \use \level Vprop : isProp V => all-prop V

  \func \infix 4 in (x y : V) : \Prop \elim y
    | set A f => \Sigma (i : A) (f i = x)

  \func foundation (x : V) (p : x in x) : Empty \elim x, p
    | set A f, (i , p) => foundation (f i) (rewrite p (i , p))

  \func V' : V => set V (\lam x => x)

  \func VinV : V' in V' => (V', idp)

  \func loopy : Empty => foundation V' VinV
}

Attempting to normalize loopy causes the typechecker to go in an infinite loop. This is inspired by the 1lab which also has similar issues due to impredicativity.

[anshwad10]

I don't think we should assert that 'every term has a normal form' and that the 'comparision algorithm always terminates' in the documentation, without at least mentioning this exception