More structured TCErrorMessage

[yav]

Currently TCErrorMessage just contains a Doc. It would be nice to use a data structure instead as this would make it easier to interact with external tools and give us more flexibility on how/what we show in errors.

[brianhuffman]

Actually, it currently contains a String, not a Doc.

cryptol/src/Cryptol/TypeCheck/TCon.hs

Lines 253 to 256 in ae4406d

	data TCErrorMessage = TCErrorMessage
	{ tcErrorMessage :: !String
	-- XXX: Add location?
	} deriving (Show, Eq, Ord, Generic, NFData)

I should point out that having only a String inside TCErrorMessage is the reason why the Reason line of the error message below prints the Float16 type synonym in a fully-qualified manner. The function that makes the TCErrorMessage needs to put the type into a string, but it doesn't have the name context available to pretty-print the type correctly.

Cryptol> :m Float
Loading module Cryptol
Loading module Float
Float> 1000000 : Float16

[error] at <interactive>:1:1--1:8:
  Unsolvable constraints:
    • Literal 1000000 Float16
        arising from
        use of literal or demoted expression
        at <interactive>:1:1--1:8
    • Reason: 1000000 cannot be represented in Float::Float16

[yav]

This is related to #782

[yav]

This should be done now, so I'll close it