Note [Coercion tokens]

GHC/CoreToStg.hs:204 compiler

In coreToStgArgs, we drop type arguments completely, but we replace
coercions with a special coercionToken# placeholder. Why? Consider:

  f :: forall a. Int ~# Bool -> a
  f = /\a. \(co :: Int ~# Bool) -> error "impossible"

If we erased the coercion argument completely, we’d end up with just
f = error "impossible", but then f `seq` () would be ⊥!

This is an artificial example, but back in the day we *did* treat
coercion lambdas like type lambdas, and we had bug reports as a
result. So now we treat coercion lambdas like value lambdas, but we
treat coercions themselves as zero-width arguments — coercionToken#
has representation VoidRep — which gets the best of both worlds.

(For the gory details, see also the (unpublished) paper, “Practical
aspects of evidence-based compilation in System FC.”)

References 0

This Note does not link to any other.

Referenced by 4