Conditions for omitting type declarations in a where clause

Question

The tutorial section on where clauses gives 2 conditions for being able to omitt the type declaration of a function f in a where clause:

• f appears in the right hand side of the top level definition
• The type of f can be completely determined from its first application

My question is: what is the relation between these two conditions? 'and', 'or', 'mutually exclusive', does one imply the other?

Answer 1

Both conditions must be met, e.g.:

test1 : List Int -> List Int
test1 xs = map inc xs
  where
    inc a = 1 + a

Let's look at counter examples, where only one condition is fulfilled.

test2 : List Int -> List Int
test2 xs = map proxy xs
  where
    inc a = 1 + a
    proxy : Int -> Int
    proxy a = inc a

Here, inc does not appear on the right hand side, but could be determined to be Int -> Int.

test3 : List Int -> List Int
test3 xs = map (cast . inc . cast) xs
  where
    inc a = 1 + a

Next, inc appears on the right hand side, but the type cannot be determined (as it could be Nat -> Nat, Int32 -> Int32, …), and thus the type of cast can't either.

Both test2 and test3 compile only when given a type declaration to inc.