CornelisRefine on unknown seems to print Aeson JSON instead of ... something?

[silky]

I'm not sure what the intended behaviour is here, but:

I get the error above if I run :CornelisRefine at the hole on line 0.

I suspect the message:

Object (fromList [("constructors",Array [String "zero",String "suc"]),("kind",String "IntroConstructorUnknown")])

Is not what I'm meant to see.

For context, I'm following the PLFA tutorial, it suggests I would see something like:

Don't know which constructor to introduce of zero or suc

at the same point; which seems pretty reasonable, and is clearly what the JSON is actually encoding :)