[Agda] Agda type inference oddity on functions

[Alan Jeffrey]

Hi everyone,

An issue in the context of being able to implement functions with 
default values for implicit parameters (the "Pie In The Sky" thread). 
There may be a roadblock, caused by some odd behaviour around when Agda 
can infer that a term has function type.

Attached is a program that defines a function whose only effect is to 
enforce that its argument is a function.  The version in the file is 
level-polymorphic and deals with dependent functions, but its simpler 
cousin is:

   isFun : {A B : Set} -> (A -> B) -> (A -> B)
   isFun f = f

Then we can show that there are contexts such that:

a) isFun (lambda x -> x) type-infers, but (lambda x -> x) does not.
b) (isFun f x) type-infers, but (f x) does not.

That is, the type inference engine doesn't infer that lambda-terms or 
applied terms have function type, which seems odd to me.

Also, eta-expansion can cause terms to fail to type-infer, that is there 
are types such that:

   ok : A -> B -> C
   ok f = f -- type-infers

   nok : A -> B -> C
   nok f x = f x -- fails

Bug, or feature?  (I had a look in the issue-tracker, didn't find it 
there...)

A.
-------------- next part --------------
{-# OPTIONS --universe-polymorphism #-}

open import Level
open import Data.Bool
open import Data.Nat

module Odd where

-- This module demonstrates that the Agda type inference algorithm
-- doesn't add constraints in that f is a function, even when
-- f is a lambda term or has been applied.  Concretely, we define
-- a function isFun, such that (isFun f) returns f, but only
-- typechecks when f is a function.  Then we show contexts where
-- (isFun (λ x → x)) typechecks, but (λ x → x) does not, and where
-- (isFun f x) typechecks, but (f x) does not.
-- Oh, and we also show that eta-expansion can turn a typechecking
-- term into a non-typechecking term.

isFun : {a b : Level} → {A : Set a} → {F : A → Set b} → 
  ((a : A) → (F a)) → ((a : A) → (F a))
isFun f = f

-- Example follows.  Note that F is injective, and the
-- inference algorithm recognizes it as such.

F : Bool → Set
F true  = ℕ → ℕ
F false = â„•

A : Set
A = {b : Bool} → (F b)

bool : {b : Bool} → (F b) → Bool
bool {b} x = b

-- x1 fails, x2 passes: Agda can't infer that a λ-term is a function

x1 : Bool
x1 = bool (λ x → x)

x2 : Bool
x2 = bool (isFun (λ x → x))

-- x3 fails, x4 passes: Agda can't infer that an applied term is a function

x3 : A → ℕ → ℕ
x3 f x = f x

x4 : A → ℕ → ℕ
x4 f x = isFun f x

-- And just for some extra weirdness, eta-contracting
-- x3 causes it to typecheck!

x5 : A → ℕ → ℕ
x5 f = f