[Agda] Suspicious Infirmity of Type Inferencer

[Nils Anders Danielsson]

On 2009-11-10 10:13, Vag Vagoff wrote:
> Why compiler compels me to type types and kinds in specified locations?
> (marked by double parenthesis)
>
> It is possible to enforce typechecker to do eta reduction while term
> normalization?
> (so I could write I ≡ S K S instead of ∀ {x} I x ≡ S K S x)

Agda has η-equality for function types. I believe that your problem is
related to Agda's strange handling of implicit arguments, see
http://thread.gmane.org/gmane.comp.lang.agda/443/focus=445.

> B : ∀ {a b c : ((Set)) } → (b → c) → (a → b) → a → c -- [!]
> B x y z = x (y z)

The types of a, b and c are not inferable here. If you replaced Set with
Set₁ the code would still be type correct. (Unless some other code in
the file constrains the type variables in a suitable way.)

> test-I₁ : ∀ {a} {x : a} → I x ≡ S {_} { ((a → a)) } K K x  -- [!]
> test-I₁ = ≡-refl

If you specify the types of S, K and I properly the code is almost
accepted without the hint:

  S : {A B C : Set} → (A → B → C) → (A → B) → A → C
  S x y z = x z (y z)

  K : {A B : Set} → A → B → A
  K x y = x

  I : {A : Set} → A → A
  I x = x

  test : {A : Set} {x : A} → I x ≡ S K K x
  test = ≡-refl

The only problem is that the second argument to the last K is not
inferred. This argument cannot be inferred, because any value of type
Set would be accepted.

The following code is accepted:

  test : {A B : Set} → I ≡ S K (K {A} {B})
  test = ≡-refl

--
/NAD


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.