Fix unification of concrete type variables, removing IsRefl#
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.