[Agda] Is this a bug?

[Nils Anders Danielsson]

On 2011-05-03 18:30, Sivaram Gowkanapalli wrote:
> Just wondering if this is a bug.

It's not. Consider the following code:

  g : Type Bool → Set
  g t = ?

Try to split on t (using C-c C-c). You get the following error message:

   Cannot pattern match on constructor isℕ, since the inferred indices
   [ℕ] cannot be unified with the expected indices [Bool] for some
   when checking that the expression ? has type ℕ

Agda's unification machinery can neither see that ℕ and Bool are equal,
nor that they are distinct. Another example:

   f : ℕ ≢ Bool
   f ()

   ℕ ≡ Bool should be empty, but that's not obvious to me
   when checking that the clause f () has type ℕ ≢ Bool

-- 
/NAD