Metatheory does not match implementation

[L-as]

Summary

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

MkCons is polymorphic from what I can tell.

Steps to reproduce the behavior

Try using MkCons on a list of integers.

Actual Result

It works

Expected Result

It shouldn't work according to the documentation.

Describe the approach you would take to fix this

I would change the signature.

System info

.

[effectfully]

The metatheory in general does not agree with the actual implementation w.r.t. builtins at the moment. This is to be fixed.

[effectfully]

This is being worked on currently.

[effectfully]

MkCons is polymorphic from what I can tell.

Fixed by #5157.

Thanks for reporting!

The metatheory in general does not agree with the actual implementation w.r.t. builtins at the moment. This is to be fixed.

Slowly but steadily we're moving in this direction.