[Agda] type check cost

[Sergei Meshveliani]

On Tue, 2017-08-22 at 13:26 +0200, Nils Anders Danielsson wrote:
> On 2017-08-20 15:22, Sergei Meshveliani wrote:
> > I wrote earlier of the example, when type-checking  (s , t)  costs
> > infinitely much, while adding the type declaration for this pair makes
> > it cost small. And I expect that in the first variant the result is
> > going to be "unsolved metas".
> 
> I wonder if it would be useful to emit a warning when there are
> long-lived (in some sense) metas that have not been frozen.
> 


I recall of the possibility of type checking under emacs. 
emacs will mark by color the place at which the type checker hangs for
long.
What may this mean?
1) It it loops forever, then this is a bug in the type checker. Right?
   But what if the user program contains a function for a proof that is
declared TERMINATING, and which does not in fact terminate -- ?

2) The outcome may occur "unsolved metas".
3) In can end with, say, "Error: foo is not of type Foo."  ?
4) This may end with success after 50 hours, why not?

If I see that emacs shows me the point in a program at which the type
checker thinks more than 30 minutes, then may be, it has sense to try to
declare more types around this place in the program, I wonder.

Regards,

------
Sergei