[Agda] Is this a bug?

[Andreas Abel]

For your info: The error is raised in the coverage checker, not during 
splitting individual clauses.

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 suspect an issue with the coverage checker...

Andreas

On 5/4/11 3:49 PM, Nils Anders Danielsson wrote:
> 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
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/