Skip to content

Fix unification of concrete type variables, removing IsRefl#

sheaf requested to merge sheaf/ghc:synEq into master

This patch fixes the unification of concrete type variables. The subtlety was that unifying concrete metavariables is more subtle than other metavariables, as decomposition is possible. See the Note [Unifying concrete metavariables], which explains how we unify a concrete type variable with a type ty by concretising ty, using the function GHC.Tc.Utils.Concrete.concretise.

This can be used to perform an eager syntactic check for concreteness, allowing us to remove the IsRefl# special predicate. Instead of emitting two constraints rr ~# concrete_tv and IsRefl# rr concrete_tv, we instead concretise rr. If this succeeds we can fill concrete_tv, and otherwise we directly emit an error message to the typechecker environment instead of deferring. We still need the error message to be passed on (instead of directly thrown), as we might benefit from further unification in which case we will need to zonk the stored types. To achieve this, we change the wc_holes field of WantedConstraints to wc_errors, which stores general delayed errors. For the moement, a delayed error is either a hole, or a syntactic equality error.

hasFixedRuntimeRep_MustBeRefl is now hasFixedRuntimeRep_syntactic, and hasFixedRuntimeRep has been refactored to directly return the most useful coercion for PHASE 2 of FixedRuntimeRep.

This patch also adds a field ir_frr to the InferResult datatype, holding a value of type Maybe FRROrigin. When this value is not Nothing, this means that we must fill the ir_ref field with a type which has a fixed RuntimeRep. When it comes time to fill such an ExpType, we ensure that the type has a fixed RuntimeRep by performing a representation-polymorphism check with the given FRROrigin. This is similar to what we already do to ensure we fill an Infer ExpType with a type of the correct TcLevel. This allows us to properly perform representation-polymorphism checks on Infer ExpTypes.

The fillInferResult function had to be moved to GHC.Tc.Utils.Unify to avoid a cyclic import now that it calls hasFixedRuntimeRep.

This patch also changes the code in matchExpectedFunTys to make use of the coercions, which is now possible thanks to the previous change. This implements PHASE 2 of FixedRuntimeRep in some situations. For example, the test cases T13105 and T17536b are now both accepted.

Edited by sheaf

Merge request reports