[Agda] Recursive Sets / refine vs. load

[Brandon Moore]

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?

Brandon
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20120324/07c2bf95/attachment.html