Issue485

[brianhuffman]

Make pretty printer unfold type synonyms when not in scope.

Fixes #485.

[yav]

I think the change makes sende.

On a side note, some of the tests, I think, illustrate the bug I was mentioning yesterday: shouldn't FloatTests::Small be in scope?

[brianhuffman]

About FloatTests::Small getting unfolded: Yes, I agree that this should be in scope. It should actually be printed as just Small, as it actually appears earlier in the same error message:

  Unsolvable constraints:
    • Literal 7 Small
        arising from
        use of literal or demoted expression
        at <interactive>:1:1--1:2
    • Reason: 7 cannot be represented in FloatTests::Small

I think the actual problem is that the type expression in the "Reason" line is pretty-printed without the appropriate name context. Here's the relevant code, from function solveFLiteralInst:

cryptol/src/Cryptol/TypeCheck/Solver/Class.hs

Lines 515 to 517 in ae4406d

	_ -> Unsolvable $ TCErrorMessage
	$ show n ++ "/" ++ show d ++ " cannot be " ++
	"represented in " ++ show (pp ty)

The problem is using show (pp ty) to insert a pretty-printed type into the string argument to TCErrorMessage. We should instead add another constructor alongside TCErrorMessage that can hold a Doc or a Type, or else just change TCErrorMessage to use Doc instead of String. We should open a separate ticket for this.

[yav]

Good point. TCErrorMessage really should be way more structured than just a Doc. I made #905 to track this.