[Agda] Recursive Sets / refine vs. load

[Peter Hancock]

On 24/03/2012 17: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
>
> module test where
> open import Data.Nat
> open import Data.Bool
> open import Data.Product
> open import Data.Vec
>
> t : Bool → Set
> t true = ℕ
> t false = Σ (t true) {!Vec Bool!}
>
> Why isn't this definition accepted?

I'd like to hear the real explanation, but I imagine that
when Mrs Agda is type checking the second equation, she isn't
paying much attention to the first equation, beyond thinking that
it type checks.  Anymore than if you had written

> t false = Σ (t true) {!Vec Bool!}
> t true = ℕ

I'm not sure she should be blamed.  Is there a general scheme
(like natrec, or elim\exists, or something) she should be taught?
(I'm not trying to be funny. I agree it's sad when you can "give"
something but she won't ^C^L it.  I think it's inevitable.)

Hank