Skip to content

Draft: Use checkTyEqRhs to make types concrete

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

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 a CoercionTy. 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 in T23051.
  • There are some TODOs left in comments; mostly questions to myself.
Edited by sheaf

Merge request reports