Draft: Use checkTyEqRhs to make types concrete
This MR is a rework of !11147 (closed), but trying to improve the existing code (in particular checkTyEqRhs
) rather than implementing a separate codepath. (Inconsistencies in behaviour between the makeTypeConcrete
and checkTyEqRhs
functions in that MR might well be a source of bugs.)
This MR aims to fix #23883. It attempts this by making some changes to the way
GHC.Tc.Utils.Unify.checkTyEqRhs
handles concrete type variables:
-
Don't allow unifications between a concrete type variable and a
CastTy
or aCoercionTy
. These are not concrete types. -
Similar to cycle breaker type variables, allow a "breaker" function to be specified which allows recovery. This enables us to make progress decomposing equalities between a concrete type variable and a non-concrete composite type. What this means and why it is important is explained below.
Suppose we want to make
TYPE a[sk]
concrete. We used to simply create a concrete metavariable kappa and emit
[W] kappa[conc] ~# TYPE a[sk]
With this patch, we call checkTyEqRhs
, which will recur into the
TyCon application on the RHS, and we will use the "concrete breaker"
function to create a new concrete metavariable gamma[conc]
and emit
[W] gamma[conc] ~# a[sk]
which is equivalent to decomposing the previous equality with the substitution
kappa[conc] := TYPE gamma[conc]
These changes mean that the compiler no longer panics on calls such as
typeTypeOrConstraint kappa
getRuntimeRep kappa
because we will instead be calling
typeTypeOrConstraint (TYPE gamma) = TypeLike
getRuntimeRep (TYPE gamma) = gamma
TODO:
-
I am getting a panic from typeKind
inT23051
. -
There are some TODOs left in comments; mostly questions to myself.