[Agda] Is this a bug?

[Nils Anders Danielsson]

On 2011-05-04 17:55, Andreas Abel wrote:
> But Nisse, should not this fail then also?
>
> f : (A : Set) → Type A → ℕ
> f .Bool isBool = zero
> f .ℕ    isℕ    = succ zero
>
> Agda does unify A with Bool in the first case.  If Agda could not tell
> apart Bool and Nat, then it could not unify A with Bool.

I don't follow you. Unifying a variable and a data type doesn't strike
me as problematic.

-- 
/NAD