Concreteness: emit "ki ~ TYPE alpha"
This MR is @monoidal's way of tackling #23883.
It consists of two commits:
- Krzysztof's fix to #23883.
- A refactor of
makeTypeConcrete
to usecheckTyEqRhs
instead of re-implementing its own logic.
TODO:
-
I am getting panics in typeKind
in testsT23051
andT23176
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
.