Improve inference

[treeowl]

The original concept of this API is to work "over", "under", or "a la" a single newtype, potentially changing its type arguments but not changing it wholesale. Back in the day, Haskell couldn't express that idea, but now it can (for the most part). We can take advantage of that to improve inference and typed hole error messages.

Fixes #15

Additionally, remove support for GHC versions before 8.4. These have pretty horribly brittle support for Coercible (7.10 being especially different and 8.2 being especially flaky), so supporting them is a bit nightmarish.

[treeowl]

Whew! Looks like I got this, pretty much. There are some ugly tricks to pull for 7.10, and I have no idea why 8.2 rejects my example (presumably a compiler bug), but it looks like the overall idea works. I'm guessing this is probably pretty close to McBride's original intention, which wasn't yet expressible in Haskell at the time. Inference should be quite powerful.

[treeowl]

The major limitation of this version is that newtypes with kind arguments aren't fully supported. That is, given newtype Foo k (a :: k) = ..., n and n' must have the same k. I think that's okay. The main point of this module is convenience, and giving up rarely-needed flexibility for good inference seems appropriate in that context.

[treeowl]

@sjakobi, @chessai, do you think it would be okay to require GHC ≥ 8.4? Coercible seems pretty darn brittle in earlier versions. When faced with my test case, 8.2 complains it can't match the representation of Sum Int with that of Int. Clearly I've run into some dark corner there.... But even without the fancy inference machinery, things seem pretty sensitive until 8.4.

[chessai]

I am definitely okay with that.

[treeowl]

@chessai any general opinions on this PR?

[treeowl]

@kcsongor has a filthy trick that can probably improve some of the type errors when people misuse these functions.

[treeowl]

@sjakobi Have you any thoughts?

[treeowl]

The error messages actually turned out to be much more reasonable than I feared! I do with that :t were a little friendlier to this module, but at least :i. is good. I don't know if there are good tricks for improving :i or not...

[treeowl]

I am having a bit of trouble getting my custom type error to fire. I'll have to see if I can fix that.

[treeowl]

All right. I think I fixed the custom error issue. I couldn't get @kcsongor's dirty trick to improve things here without simultaneously making other things worse, so I think we should skip that. The basic annoyance is that GHC (in :t and type errors) really wants to simplify constraints, which expands friendly-looking things like Newtype n o into garbage. Csongor's trick uses overlapping instances for an otherwise completely unused type to delay the simplification. But this causes us other trouble that seems more serious; we really want GHC to simplify constraints when doing so actually reveals new information. Oh well.

[treeowl]

Is that extra flexibility of not requiring n to be a direct newtype around o sufficiently useful to justify the extra documentation complexity? I don't have a clear feeling about it one way or the other.

[treeowl]

The whole thing goes a bit over my head though so I hope you don't mind if I ping you if issues come up, @treeowl.

For sure. I should add some more comments. The trickiest bit is Similar. We really want n to give us information about n'. It's also nice (for typed holes and error messages, particularly) if n' gives us information about n. Since we may know nothing, a priori, about one of those, we have to be a bit careful not to force a match on one when the other is the one with information. The horrible way to do that (even worse :t results!) is with INCOHERENT typeclass instances. Ignoring that awfulness, the thing to do is to require n' to have a structure calculated from n and the other way around, "in parallel". Similar' n n' matches on n, producing a constraint. Suppose we have n ~ F a b. Then we get

Similar' (F a b) n'
==>
(Similar' (F a) (GetFun n'), n' ~ GetFun n' (GetArg n'))

We have now constrained things only a little: n' is required to have the form p q for some p and q, where F a and p have the same kind and b and q have the same kind. Substituting in p and q, we continue:

(Similar' (F a) p, n' ~ p q)
((Similar' F (GetFun p), p ~ GetFun p (GetArg p)), n' ~ p q)

Let's set r ~ GetFun p and s ~ GetArg p. Then

((Similar' F r, p ~ r s), n' ~ p q)

We've now reached the base case! Yay! So the last step is

((F ~ r, p ~ r s), n' ~ p q)

which then simplifies to

n' ~ F s q

Undoing the substitutions we made,

n' ~ F (GetArg (GetFun n')) (GetArg n')

The arguments in that constraint are completely useless (as far as I know), but we need to put it all together like that to get what we're after: an equality constraint on n' itself that lets GHC know it's F x y for some x and y to be determined. Very often, those are then fixed by the type o' and the Newtype n' o' constraint, which at first seems backwards. Say we consider Sum. We have

type Rep (Sum a) = M1 _ _ (M1 _ _ (M1 _ _ (K1 _ a)))

This can reduce as soon as GHC sees we have Sum whatever! So then the NewtypeF-calculated constraint can constrain the type argument to whatever's required to wrap the new contents. Magic! Yeah, this comment should go in the code.....

[treeowl]

I'm definitely leaning toward requiring Newtype n o as well as Newtype n' o', even though it's not strictly necessary. I think it makes for a better story to tell users about an already somewhat intimidating API. Please let me know what you think about that.

[treeowl]

I've expanded the documentation considerably, and, in a separate commit, imposed the tighter constraints I mentioned. Let me know what you think.

[treeowl]

@sjakobi, have you had a chance to consider this further? Do you have any more questions?

[sjakobi]

Thank you @treeowl!

[chessai]

Sorry for not helping out here; I've been indisposed recently and didn't want to devote too much brainpower to any one task.

[sjakobi]

@chessai No worries! Get well soon! :)