[Agda] type check cost

[Nils Anders Danielsson]

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.

-- 
/NAD