As described in https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase2.

We would like to have coercion quantifications back in Haskell Core language.

This means in Core we can define types like

\/ (a: k1) . 
  \/ (co : k1 ~ k2)  -- an explicit quantification for the coercion
  -> (a |> co)       -- use the name for an explicit cast
  -> ...