Never `Any`-ify during kind inference
Here are some examples of
Any-ification during kind inference:
data B a data TySing ty where SB :: TySing (B a) data ATySing where MkATySing :: TySing ty -> ATySing type family Forget ty :: ATySing where Forget (B a) = MkATySing SB
The RHS of that type family equation is really
MkATySing @alpha (SB @alpha), and the
alpha gets zonked to
type T = forall a. Proxy a
The RHS of the type synonym is really
forall (a :: kappa). Proxy @kappa a, and the
kappa gets zonked to
class (forall a. a b ~ a c) => C b c
The superclass constraint is really
forall (a :: Type -> kappa). (~) @kappa (a b) (a c)), and the
kappa gets zonked to
We want to stop zonking to
Any, preferring to error instead. But how should we implement?
Option A: Use a new variant of
ZonkFlexi, a choice carried around in a
ZonkEnvthat says what to do with empty metavariables. The new choice would cause an error. This new form of
ZonkFlexiwould be used in the final zonks in e.g. TcTyClsDecls. Open question: how to get a decent error message? I think we'd have to pass around the original, top-level type in order to report it. By the time we have just the unbound metavariable, we have no context to report.
Option B: Similar to (A), but don't report an error in the zonker. Instead, the new variant of
ZonkFlexiwould insert some magical error type. Then, the validity checker could do an early pass, looking for the error type; it can then report a nice error message.
Option C: Look for all cases where
Any-ification might happen, and detect each one separately. This can produce lovely error messages. The solution for #17562 in !2313 does this. Perhaps we can pair this choice with a new
ZonkFlexithat panics. That way, we'll know if we've missed a case.
Simon below proposes Option D: Zap to
Any. I (Richard) view D as an add-on to any of the above plans. Because
Typeis not always well-kinded, we can only zap to
Typesometimes, and we still need to decide what we do at other times. Personally, I prefer not to treat
Typespecially with -XPolyKinds` enabled, and so I'd prefer that we don't do this.
EDIT: Also, we can consider Option E: Report poor error messages, saying something about an unconstrained kind variable. Users would be helped only via the context (the "In the data declaration for
Wurble" bits). This would mean building up useful contexts in the zonker.
Option F: The new constructor for
ZonkFlexicould carry the top-level type we are trying to zonk. If we encounter an unconstrained metavariable, we just look at this bit of context to produce the error message. Perhaps this could be combined with the context-building in Option E for good effect. This is the first solution I'm actually happy with.