условие для пропуска объявления типа в котором положение

Question

tutorial раздел на where пунктах дают 2 условие для возможности omitt типа объявления функции f в пункте where:

• f появляется в правая часть определения верхнего уровня
• Тип f может быть полностью определен из его первого применения

Мой вопрос: какова связь между этими двумя условиями? 'и', 'или', 'взаимно исключающий', означает ли это другое?

Answer 1

должны быть выполнены оба условия, например .:

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

Давайте посмотрим на примеры счетчика, где только одно условие выполнено.

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

Здесь inc не появляется на правой стороне, но может быть определено Int -> Int.

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

Далее inc появляется на правой стороне, но тип не может быть определена (как это может быть Nat -> Nat, Int32 -> Int32, ...), и, таким образом, тип cast не могу.

И test2, и test3 скомпилировать только при условии объявления типа inc.