What does it mean to rely on the consistency of a coercion language?

Question

From https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell,

unlike Coq and Agda, Haskell relies on the consistency of a coercion language, which is not threatened by * :: *. See the paper for more details.

The "paper" cited is a broken link, but, by Googling and reading it, I noticed it is describing how to add explicit kind equality to system FC, but not directly addressing the implicit question: what it means to rely on the consistency of a coercion language?

Answer 1

Coq and Agda are dependently typed total languages. They are inspired by their relative type-theoretic foundations, which involve a (typed) lambda calculus which is (strongly) normalizing. This means that reducing any lambda term eventually has to halt.

This property makes it possible to use Coq and Agda as proof systems: one can prove mathematical facts using them. Indeed, by the Curry-Howard correspondence, if

someExpression :: someType

then someType corresponds to a logical (intuitionistic) tautology.

In Haskell, this is not the case, since any type can be "proved" by

undefined :: someType

i.e. we can cheat using a "bottom" value. This makes Haskell, as a logic, inconsistent. We can prove undefined :: Data.Void.Void, which corresponds to the logical "false" proposition, for instance. This is bad, but is the necessary price to pay for having unlimited recursion, which allows for non terminating programs.

By comparison, Coq and Agda have only primitive recursion (which can never recurse forever).

Now, to the point. It is well known that adding the axiom * :: * to Coq / Agda makes the logic to be no longer consistent. We can derive a proof of "false" using Girard's paradox. That would be very bad, since we can then even prove things like lemma :: Int :~: String, and derive a coercion function coerce :: Int -> String.

lemma :: Int :~: String
lemma = -- exploit Girard's paradox here

-- using Haskell syntax:
coerce :: Int -> String
coerce x = case lemma of Refl -> x

If we implemented that naively, coerce would simply perform an unsafe cast, reinterpreting the underlying bits -- after all, that is justified by the lemma, stating that these types are exactly the same! In that way we would even lose runtime type safety. Doom awaits.

In Haskell, even if we don't add * :: * we are inconsistent anyway, so we can simply have

lemma = undefined

and derive coerce anyway! So, adding * :: * does not really increase the number of issues. It is just another source of inconsistency.

One might then wonder why in Haskell coerce is type safe, then. Well, in Haskell case lemma of Refl ->... forces the evaluation of lemma. This can only trigger an exception, or fail to terminate, so the ... part is never reached. Haskell can not optimize coerce as an unsafe cast, unlike Agda / Coq.

There is another aspect of Haskell that the quoted paragraph mentions: the coercion language. Internally, when we write

case lemma1 of
  Refl -> case lemma2 of
    Refl -> ...
      ...
        Refl -> expression

we introduce a lot of type equalities that must be exploited to prove that expression has indeed the required type. In Coq, the programmer must use a sophisticated form of matching (dependent matching) to justify where and how to exploit the type equalities. In Haskell, the compiler writes this proof for us (in Coq the type system is richer, and that would involve higher order unification, I think, which is undecidable). This proof is NOT written in Haskell! Indeed, Haskell is inconsistent, so we can't rely on that. Instead, Haskell uses another custom coercion language for that, which is guaranteed to be consistent. We only need to rely on that.

We can see some glimpses of that internal coercion language if we dump Core. For instance, compiling a transitivity proof

trans :: a :~: b -> b :~: c -> a :~: c
trans Refl Refl = Refl

we get

GADTtransitivity.trans
  :: forall a_au9 b_aua c_aub.
     a_au9 :~: b_aua -> b_aua :~: c_aub -> a_au9 :~: c_aub
[GblId, Arity=2, Caf=NoCafRefs, Str=DmdType]
GADTtransitivity.trans =
  \ (@ a_auB)
    (@ b_auC)
    (@ c_auD)
    (ds_dLB :: a_auB :~: b_auC)
    (ds1_dLC :: b_auC :~: c_auD) ->
    case ds_dLB of _ [Occ=Dead] { Refl cobox0_auF ->
    case ds1_dLC of _ [Occ=Dead] { Refl cobox1_auG ->
    (Data.Type.Equality.$WRefl @ * @ a_auB)
    `cast` ((<a_auB>_N :~: (Sym cobox0_auF ; Sym cobox1_auG))_R
            :: ((a_auB :~: a_auB) :: *) ~R# ((a_auB :~: c_auD) :: *))
    }
    }

Note the cast at the end, which exploits the proof in the coercion language

(<a_auB>_N :~: (Sym cobox0_auF ; Sym cobox1_auG))_R

In this proof, we can see Sym cobox0_auF ; Sym cobox1_auG which I guess uses symmetry Sym and transitivity ; to reach the wanted goal: the proof that Refl :: a_auB :~: a_auB can indeed be safely casted to the wanted a_auB :~: c_auD.

Finally, note that I'm pretty sure that such proofs are then discarded during the compilation by GHC, and that cast ultimately reduces to an unsafe cast at runtime (case still evaluates the two input proofs, to preserve type safety). However, having an intermediate proof strongly ensures that the compiler is doing the right thing.