Handle SubCo (coercion)

[conal]

Adds support for Coercion's SubCo constructor for navigation, transformation, and pretty-printing. Now instead of

Unsupported Coercion Constructor ; Unsupported Coercion Constructor

I see

Sub (Sym (TFCo:R:RepRTree[0] (Nth:0 dt) <Int>_N))
; Sub (TFCo:R:RepRTree[0] <Z>_N <Int>_N)

Much more helpful!

I haven't added UnivCo yet.

  | UnivCo FastString Role Type Type -- :: "e" -> _ -> _ -> e

I can give this one a try also. For univCoT and friends, I wonder what Transform source type to use for the FastString. For instance, it could be FastString or String. The latter might be more convenient, and the former more efficient (avoiding two conversions). I'm leaning toward FastString. Thoughts?

[ecaustin]

I'd probably argue for using String, at least in the external definition of univCoT provided to the user. This would save some (admittedly minor) headaches when adding this to the new hermit-shell. Alternatively, if we wanted to make our own newtype wrapper to String called FastString I'd also support that, as it would mirror the way we handled other string-like things in the past.

Do UnivCo constructors show up frequently enough in practice where the overhead of converting between String and FastString would matter?

[conal]

@ecaustin Thanks for the feedback. I sure wouldn't mind some speed loss for externals. Are there external forms of things like univCoT (and appT, letT, etc)? I haven't seen any.

I don't know how common UnivCo is. The GHC source code has the following to say:

The `UnivCo` ("universal coercion") serves two rather separate functions: - the implementation for `unsafeCoerce#` - placeholder for phantom parameters in a `TyConAppCo`

I don't have any uses of UnivCo, which means I neither need its support nor am able to test it right now. Maybe best tabled for now.

[xich]

This looks great, thanks!

As for univCoT, we don't usually have a Transform argument for string-like things, because it doesn't really make sense to descend into them. We usually just pass them into the combining function, which can modify them. Same goes for Roles.

So I would expect it's type signature to be:

univCoT ::
  Transform c m Type a1
  -> Transform c m Type a2
  -> (FastString -> Role -> a1 -> a2 -> b)
  -> Transform c m Coercion b

and there would be univCoAllR and univCoAnyR in the same fashion as others.

[ecaustin]

@conal Ignore what I said. You're right, the external definitions only cover derived, monadic transformations, not primitive ones like univCoT, appT, etc.

Sorry about that, I did a quick scan of the hermit-shell commands to see how we handled string-like things without even thinking if it was applicable to this discussion.

I would agree with the type that Drew provided in his comment.

[xich]

FWIW, I think we should probably expose the congruence combinators in the new shell, because it supports types rich enough to actually use them. We didn't before because the old shell because the shell language was first order and monomorphic.

[conal]

@xich Thanks for the advice. I'm adding UnivCo support now.

[ecaustin]

@xich The new shell isn't fully higher-order because we don't have any way to serialize arbitrary functions. I'm assuming that's why we haven't exposed the congruence combinators yet, as it's not obvious how to communicate a combining function to the server.