[Agda] Is this a bug?

[Andreas Abel]

Some further analysis:

If I reduce g to one clause:

   g : (A : Set) → Type A → Type A → ℕ
   g .Bool isBool isBool = zero

Then I get the message:

   Cannot split on the constructor isℕ
   when checking the definition of g

At, least this message is confusing, since my program does not try to 
split on isNat.  Reconstructing coverage checking, it first splits at 
the first Type A with first match isBool.  This instantiates A to Bool. 
  Then it splits at the second, Type Bool, yielding first match isBool 
and second match isNat, where it has to unify Bool with Nat.  This 
fails, because Nat cannot be unified with Bool.  But since we do not 
positively have Nat != Bool, it does not say that isNat is impossible, 
it only says something is wrong, and it cannot split.

The question is: what goes wrong if we say Nat is distinct from Bool?
Of course, we get a different theory, where type equality is interpreted 
as the least relation closed under the rules for definitional equality. 
  At least in the models that justify type checking, you usually have 
this...

Cheers,
Andreas

On 5/4/11 5:55 PM, Andreas Abel wrote:
> 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/