[Agda] type inference error?

[Jacques Carette]

As far as I know, matita does this kind of disambiguation, and reports 
are that it works quite well.  See
http://matita.cs.unibo.it/PAPERS/disambiguation-errors.pdf
for a description of the algorithm.

Jacques

On 13-01-09 03:45 PM, Andreas Abel wrote:
> Constructor disambiguation only works outside in, not inside out.  So 
> if you have
>
>   suc x : Nat,
>
> Agda will infer x : Nat.  This simply works because the type of the 
> constructor application suc x contains the name of the datatype (here: 
> Nat) the constructor belongs to.
>
> But to disambiguate suc x from x : Nat, Agda would have to check all 
> the datatypes if they contain a constructor that takes Nat as first 
> argument.  (Just imagine you had defined the second suc of type Nat -> 
> Bot.)  Agda does not do this.  [It is not impossible to implement some 
> heuristics to try this, but it does not fall under the scheme of 
> bidirectional type checking.]
>
> Alternative:
>
>   lem : \forall x -> _==_ {A = Nat} (suc x) (suc x)
>
> (Would look nicer if we had hidden argument application for mixfix ops).
>
> Cheers,
> Andreas
>
> P.S.: Agda 1 had a notation
>
>   suc at Nat
>
> for manual constructor disambiguation.  Not a bad idea, maybe we 
> should restore it.
>
>
> On 09.01.13 6:33 PM, Darryl wrote:
>> To my knowledge, Agda has basically *never* had (or never had reliable)
>> constructor disambiguation. Anyone using Nat and Level will have
>> experienced this.
>> - darryl
>>
>> ------------------------------------------------------------------------
>>
>> Hi,
>>
>> Is the following a known error in Agda?
>> My student have found this.
>>
>> ---------------------------------------
>> data ℕ : Set where
>>    zero : ℕ
>>    suc : ℕ → ℕ
>>
>> data _≡_ {A : Set} (x : A) : A → Set where
>>    refl : x ≡ x
>>
>> data ⊥ : Set where
>>    suc : ⊥ → ⊥
>>
>> -- it looks like Agda can't tell (suc : ℕ → ℕ) apart from the other suc
>> -- this is unreasonable: the type of suc should be inferred from the
>> -- fact that (x : ℕ)
>>
>> lemma : (x : ℕ) → suc x ≡ suc x
>> lemma _ = refl
>> ---------------------------------------
>>
>>
>> Peter
>
>