Note [Return arguments with a fixed RuntimeRep]

GHC/Tc/Utils/Unify.hs:723 compiler

The functions

  - matchExpectedFunTys,
  - matchActualFunTy,
  - matchActualFunTys,

peel off argument types, as explained in Note [matchExpectedFunTys].
It's important that these functions return argument types that have
a fixed runtime representation, otherwise we would be in violation
of the representation-polymorphism invariants of
Note [Representation polymorphism invariants] in GHC.Core.

This is why all these functions have an additional invariant,
that the argument types they return all have a syntactically fixed RuntimeRep,
in the sense of Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete.

Example:

  Suppose we have

    type F :: Type -> RuntimeRep
    type family F a where { F Int = LiftedRep }

    type Dual :: Type -> Type
    type family Dual a where
      Dual a = a -> ()

    f :: forall (a :: TYPE (F Int)). Dual a
    f = \ x -> ()

  The body of `f` is a lambda abstraction, so we must be able to split off
  one argument type from its type. This is handled by `matchExpectedFunTys`
  (see 'GHC.Tc.Gen.Match.tcLambdaMatches'). We end up with desugared Core that
  looks like this:

    f :: forall (a :: TYPE (F Int)). Dual (a |> (TYPE F[0]))
    f = \ @(a :: TYPE (F Int)) ->
          (\ (x :: (a |> (TYPE F[0]))) -> ())
          `cast`
          (Sub (Sym (Dual[0] <(a |> (TYPE F[0]))>)))

  Two important transformations took place:

    1. We inserted casts around the argument type to ensure that it has
       a fixed runtime representation, as required by invariant (I1) from
       Note [Representation polymorphism invariants] in GHC.Core.
    2. We inserted a cast around the whole lambda to make everything line up
       with the type signature.

References 3

Referenced by 4