Skip to content

GitLab

Closed
Created by Richard Eisenberg@raeDeveloper

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:

#17301 (closed):

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.

#14198:

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.

#17562 (closed):

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 a ZonkEnv that says what to do with empty metavariables. The new choice would cause an error. This new form of ZonkFlexi 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 does this. Perhaps we can pair this choice with a new ZonkFlexi that panics. That way, we'll know if we've missed a case.

  • Simon below proposes Option D: Zap to Type instead of Any. I (Richard) view D as an add-on to any of the above plans. Because Type is not always well-kinded, we can only zap to Type sometimes, and we still need to decide what we do at other times. Personally, I prefer not to treat Type 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?

Edited by Simon Peyton Jones