Ich versuche, eine Denotationssemantik in Agda zu kodieren, basierend auf einem Programm, das ich in Haskell geschrieben habe.

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

n Agda wäre die direkte Übersetzung;

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

aber ich bekomme eine Fehlermeldung bezüglich des FunVal weil;

Value ist nicht unbedingt positiv, da es im Typ des Konstruktors FunVal in der Definition von Value links von einem Pfeil vorkommt.

Was bedeutet das? Kann ich das in Agda kodieren? Gehe ich falsch vor?

Vielen Dank