Note [hasFixedRuntimeRep]

GHC/Tc/Utils/Concrete.hs:329 compiler 1 ticket

The 'hasFixedRuntimeRep' function is responsible for taking a type 'ty'
and emitting a constraint to ensure that 'ty' has a fixed `RuntimeRep`,
as outlined in Note [The Concrete mechanism].

To do so, we compute the kind 'ki' of 'ty', create a new concrete metavariable
`concrete_tv` of kind `ki`, and emit a constraint `ki ~# concrete_tv`,
which will only be solved if we can prove that 'ty' indeed has a fixed RuntimeRep.

If we can solve the equality constraint, i.e. produce a coercion
`kco :: ki ~# concrete_tv`, then 'hasFixedRuntimeRep' returns the coercion

  co = GRefl ty kco :: ty ~# ty |> kco

The RHS of the coercion `co` is `ty |> kco`. The kind of this type is
concrete (by construction), which means that `ty |> kco` is an FRRType
in the sense of Note [Fixed RuntimeRep], so that we can directely compute
its runtime representation using `typePrimRep`.

  [Wrinkle: Typed Template Haskell]
    We don't perform any checks when type-checking a typed Template Haskell quote:
    we want to allow representation polymorphic quotes, as long as they are
    monomorphised at splice site.

    Example:

      Module1

        repPolyId :: forall r (a :: TYPE r). CodeQ (a -> a)
        repPolyId = [|| \ x -> x ||]

      Module2

        import Module1

        id1 :: Int -> Int
        id1 = $$repPolyId

        id2 :: Int# -> Int#
        id2 = $$repPolyId

    We implement this skip by inspecting the TH stage in `hasFixedRuntimeRep`.

    A better solution would be to use 'CodeC' constraints, as in the paper
      "Staging With Class", POPL 2022
        by Ningning Xie, Matthew Pickering, Andres Löh, Nicolas Wu, Jeremy Yallop, Meng Wang
    but for the moment, as we will typecheck again when splicing,
    this shouldn't cause any problems in practice.  See ticket #18170.

    Test case: rep-poly/T18170a.

References 2

Referenced by 8