Never `Any`-ify during kind inference
#14198 concludes with a new plan: never Any
-ify during kind inference. This ticket tracks this particular problem, separate from #14198.
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 Any
.
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 Any
.
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 Any
.
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 aZonkEnv
that says what to do with empty metavariables. The new choice would cause an error. This new form ofZonkFlexi
would 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
ZonkFlexi
would 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 (closed) in !2313 (closed) does this. Perhaps we can pair this choice with a newZonkFlexi
that panics. That way, we'll know if we've missed a case. -
Simon below proposes Option D: Zap to
Type
instead ofAny
. I (Richard) view D as an add-on to any of the above plans. BecauseType
is not always well-kinded, we can only zap toType
sometimes, and we still need to decide what we do at other times. Personally, I prefer not to treatType
specially 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
ZonkFlexi
could 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.
Thoughts?