Skip to content

Concreteness: emit "ki ~ TYPE alpha"

sheaf requested to merge sheaf/ghc:T23883-Krzysztof into master

This MR is @monoidal's way of tackling #23883.

It consists of two commits:

  1. Krzysztof's fix to #23883.
  2. A refactor of makeTypeConcrete to use checkTyEqRhs instead of re-implementing its own logic.

TODO:

  • I am getting panics in typeKind in tests T23051 and T23176 due to escaping kind variables in a forall. Not sure what is the cause.

The fix

With the first commit, Krzysztof slightly refined the constraint we emitted when performing a representation polymorphism check on a type. For example, on:

ty :: ki

we now require the precondition that ki is of the form TYPE rep or CONSTRAINT rep. Then, we end up create a concrete metavariable alpha[conc] :: RuntimeRep and emit

ki ~# TYPE alpha
 -- or
ki ~# CONSTRAINT alpha

rather than simply ki ~ beta[conc], which is what we used to do.

This change prevents the compiler crashing in functions such as getRuntimeRep, which expect a kind to be of the form TYPE xyz or CONSTRAINT xyz. These functions would panic on a bare metavariable such as beta[conc] as above.

The refactor

With the second commit, Sam refactored makeTypeConcrete to call checkTyEqRhs with the appropriate parameters. This avoids duplicating subtle logic in two places in the compiler.

In the process, a bug in checkTyEqRhs was discovered: it would unconditionally succeed when unifying a concrete LHS with a filled metavariable RHS, without checking that the contents of the metavariable is concrete. Now we correctly fail with a concreteness error; see GHC.Tc.Utils.Unify.checkTyVar.check_tv.

Edited by sheaf

Merge request reports