Fix #14369 by making injectivity warnings finer-grained
ClosedPublic

Authored by RyanGlScott on Oct 18 2017, 11:25 AM.

Details

Summary

Previously, GHC would always raise the possibility that a
type family might not be injective in certain error messages, even if
that type family actually was injective. Fix this by actually
checking for a type family's lack of injectivity before emitting
such an error message.

Test Plan

./validate

Diff Detail

Repository
rGHC Glasgow Haskell Compiler
Lint
Automatic diff as part of commit; lint not applicable.
Unit
Automatic diff as part of commit; unit tests not applicable.
RyanGlScott created this revision.Oct 18 2017, 11:25 AM
simonpj accepted this revision.Oct 19 2017, 5:52 AM
simonpj added a subscriber: simonpj.

Thanks!

This revision is now accepted and ready to land.Oct 19 2017, 5:52 AM
This revision was automatically updated to reflect the committed changes.

I remember spotting the lack of a check here some time ago, but then I convinced myself that only non-injective type families could ever get to that case in TcErrors. Did you look into why this case was getting triggered? Should perhaps a different error message altogether have been produced?

Looking at the program in the ticket, I don't think the injectivity of Demote is at issue. Instead, I would want an error saying that a1 is ambiguous, where a1 is the implicit instantiating argument to x in Sing x. To be more explicit, here are your key lines:

f :: forall (x :: forall a. Maybe a) a. SingKind a => Sing x -> Maybe (Demote a)
f = fromSing

This elaborates to

f :: forall (x :: forall a. Maybe a) b. SingKind b => Sing (Maybe alpha) (x alpha) -> Maybe (Demote b)

But then GHC solves and generalizes, yielding

f :: forall (c :: Type) (x :: forall (a :: Type). Maybe a) (b :: Type). SingKind b => Sing (Maybe c) (x c) -> Maybe (Demote b)

Then the real problem is that Demote (Maybe c) doesn't equal Maybe (Demote b). GHC reduces the left to be Maybe (Demote c), yielding the inequality between (Demote c) and (Demote b). But, really, the root problem is that c shouldn't have been generalized over; it is underconstrained in the type. I'm not sure how to print this out, but I suspect that a different code path in TcErrors is more appropriate.

I remember spotting the lack of a check here some time ago, but then I convinced myself that only non-injective type families could ever get to that case in TcErrors. Did you look into why this case was getting triggered?

I'll admit that I did not.

Should perhaps a different error message altogether have been produced?

Indeed, it does seem like there could be room for improvement here. Would you be willing to open a separate Trac ticket for this? (I don't quite understand all of the moving parts here, so you could likely give a better description of what's going on here than I could.)