[Agda] type inference error?

[Andreas Abel]

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


-- 
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/