Estou tentando codificar alguma semântica denotacional no Agda com base em um programa que escrevi em Haskell.

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

Na Agda, a tradução direta seria;

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

mas eu recebo um erro relacionado ao FunVal porque;

Valor não é estritamente positivo, porque ocorre à esquerda de uma seta no tipo do construtor FunVal na definição de Valor.

O que isto significa? Posso codificar isso no Agda? Estou fazendo o caminho errado?

Obrigado.