Caledon stalls when inferring some arguments.

[AHartNtkn]

For example, the following will stall when lpn is reached.

defn list : prop → prop
  >| nil = list P
  >| cons = P → list P → list P

defn lp : {P : prop} list P → prop
   | lpn = lp nil
   | lpc = {l : list P} {e : P} lp l → lp (cons e l)

By changing that line to | lpn = lp {P = P} nil, the stalling doesn't happen, but I think Caledon should be smart enough to know that P can't be inferred and report an error instead of stalling.

As an aside, this glitch doesn't occur for this program;

defn num  : prop
   >| zero = num
   >| succ = [n : num] num

defn list : prop -> prop
   >| nil = list P
   >| cons = P -> list P -> list P

defn append : {P : prop} list P -> list P -> list P -> prop
   | nila = {l : list P} append nil l l
   | nilc = {l m n : list P} {a : P} append l m n -> append (cons a l) m (cons a n)

defn length : {P : prop} list P -> num -> prop
  | lengthn = length nil zero
  | lengthc = {l : list P} {e : P} {n : num} length l n -> length (cons e l) (succ n) 

nor this program

defn num  : prop
   >| zero = num
   >| succ = [n : num] num

defn list : prop -> prop
   >| nil = list P
   >| cons = P -> list P -> list P

defn last : {P : prop} list P -> P -> prop
  | lastn = {e : P} last (cons e nil) e
  | lastc = {l : list P} {le e : P} last l e -> last (cons le l) e

defn length : {P : prop} list P -> num -> prop
  | lengthn = length nil zero
  | lengthc = {l : list P} {e : P} {n : num} length l n -> length (cons e l) (succ n) 

but it does occur for this program

defn num  : prop
   >| zero = num
   >| succ = [n : num] num

defn list : prop -> prop
   >| nil = list P
   >| cons = P -> list P -> list P

defn append : {P : prop} list P -> list P -> list P -> prop
   | nila = {l : list P} append nil l l
   | nilc = {l m n : list P} {a : P} append l m n -> append (cons a l) m (cons a n)

defn last : {P : prop} list P -> P -> prop
  | lastn = {e : P} last (cons e nil) e
  | lastc = {l : list P} {le e : P} last l e -> last (cons le l) e

defn length : {P : prop} list P -> num -> prop
  | lengthn = length nil zero
  | lengthc = {l : list P} {e : P} {n : num} length l n -> length (cons e l) (succ n) 

stalling on lengthn. This is an odd glitch which is clearly sensitive to context, but I'm not certain how to describe it beyond these examples.