Note [substConcreteTvOrigin]
To report helpful representation-polymorphism errors to the users, we want to
indicate which type caused the error, instead of simply printing kinds.
For example, in
coerce :: forall {r} (a :: TYPE r) (b :: TYPE r). Coercible a b => a -> b
bad :: forall {s} (z :: TYPE s). z -> z
bad = coerce
we want the error message to say (with additional debug info on type variables
for clarity of this explanation):
The first argument of 'coerce' does not have a fixed runtime representation.
Its type is:
a0[tau] :: TYPE r0[conc]
Could not unify s[sk] with r0[conc] because the former is not a concrete
RuntimeRep.
This is more informative than just saying that we could not unify s[sk] with
r0[conc]; it's helpful to users to phrase it in terms of types rather than kinds
whenever possible (especially as the kind variables often have inferred Specificity).
To achieve this, we store the type on which the representation-polymorphism
check is being performed, in the field frr_type of FixedRuntimeRepOrigin.
This is all described in Note [Reporting representation-polymorphism errors] in
GHC.Tc.Types.Origin.
However, we have to be careful in the example above, in which we are
instantiating a built-in representation-polymorphic 'Id'. As described in the
Note [Representation-polymorphism checking built-ins] in GHC.Tc.Utils.Concrete, in such
cases we end up storing types appearing in the original type of the primop,
which means for the situation above with 'coerce' we end up with a ConcreteTvOrigin
which includes type variables bound in the original type of 'coerce':
FixedRuntimeRepOrigin
{ frr_type = a[tv] :: TYPE r[tv]
, frr_context = "first argument of coerce" }
When we instantiate 'coerce' in the previous example, we obtain a substitution
[ r[tv] |-> r0[conc], a |-> a0 :: TYPE r0[conc] ]
which we need to apply to the 'frr_type' field in order for the type variables
in the error message to match up.
This is done by the call to 'substConcreteTvOrigin' in 'instantiateSigma'.
Wrinkle [Extending the substitution]
In certain cases, we need to extend the substitution we get from 'instantiateSigma'.
For example, suppose we have:
bad2 :: forall {s} (z :: TYPE s). z -> z
bad2 = coerce @z
Then 'instantiateSigma' will only instantiate the inferred type variable 'r'
of 'coerce', as it needs to leave 'a' un-instantiated so that the visible
type application '@z' makes sense. In this case, we end up with a substitution
subst: [ r[tv] |-> r0[conc] ]
body_ty: forall (a :: TYPE r[tv]) (b :: TYPE r[tv]). ...
substTy subst body_ty: forall (a' :: TYPE r0[conc]) (b' :: TYPE r0[conc]). ...
Now, we still want a substitution that maps (a :: TYPE r[tv]) to
(a' :: TYPE r0[conc]) in order to apply it to the 'frr_type', so that we don't
mention the un-substed (a :: TYPE r[tv]) in the error message.
To achieve this, we extend the substitution with the outermost quantified type
variables in the leftover (partially-instantiated) type using 'substTyVarBndrs'
to get the full substitution which we use in 'substConcreteTvOrigin'. References 2
- Reporting representation-polymorphism errors GHC.Tc.Types.Origin
- Representation-polymorphism checking built-ins GHC.Tc.Utils.Concrete
Referenced by 2
- GHC.Tc.Utils.Instantiate call site
- GHC.Tc.Utils.TcMType call site