[Agda] Recursive Sets / refine vs. load

[Nils Anders Danielsson]

On 2012-03-24 18:12, Brandon Moore wrote:
> The following definition looks reasonable to me,
> the type of the hole is reported as ℕ → Set,
> and refine/give accepts what I've written there,
> but then typechecking the file fails, saying
> t true !=< ℕ of type Set

[...]

> t : Bool → Set
> t true = ℕ
> t false = Σ (t true) {!Vec Bool!}
>
> Why isn't this definition accepted?

Because (non-mutual) definitions are not unfolded before they have been
type-checked. Unfortunately this does not apply to goals: Agda forgets
that t should not unfold when Vec Bool is type-checked. This is a
long-standing bug:

   http://code.google.com/p/agda/issues/detail?id=118

-- 
/NAD