Я пытаюсь закодировать некоторую денотационную семантику в Agda на основе программы, которую я написал на Haskell.

data Value = FunVal (Value -> Value)
           | PriVal Int
           | ConVal Id [Value]
           | Error  String

В Агде прямой перевод был бы;

data Value : Set where
    FunVal : (Value -> Value) -> Value
    PriVal : ℕ -> Value
    ConVal : String -> List Value -> Value
    Error  : String -> Value

но я получаю ошибку, связанную с FunVal, потому что;

Значение не является строго положительным, поскольку оно встречается слева от стрелки в типе конструктора FunVal в определении значения.

Что это значит? Могу ли я закодировать это в Agda? Я поступаю неправильно?

Благодарю.