Note [substConcreteTvOrigin]

GHC/Tc/Utils/TcMType.hs:1076 compiler

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

Referenced by 2