Why is MkPairData `Data -> Data -> Pair Data Data`?

[L-as]

https://github.com/input-output-hk/plutus/blob/master/plutus-metatheory/src/Algorithmic.lagda#L150

Perhaps I'm misunderstanding how Data maps to CBOR and backward.

I'm wondering why it's not a -> b -> Pair a b.

[ghost]

Data <-> CBOR serialization/deserialization is defined at PlutusCore/Data.hs:

https://github.com/input-output-hk/plutus/blob/da4f85cdd2a3a261ce540e8dc51d2a3c5fa89ed2/plutus-core/plutus-core/src/PlutusCore/Data.hs#L56-L59

I'm wondering why it's not a -> b -> Pair a b.

There is a note about functions over built-in types mentioned at MkPairData definition that goes into details.

https://github.com/input-output-hk/plutus/blob/da4f85cdd2a3a261ce540e8dc51d2a3c5fa89ed2/plutus-core/plutus-core/src/PlutusCore/Default/Builtins.hs#L104-L110

I hope that helps.

[L-as]

Thanks!