Re: Heterogeneous equality into base?

In a more general type theory, HRefl doesn't imply Refl! You can't show HRefl implies Refl in MLTT. This extra power is granted by dependent pattern matching most dependent type theories or in Haskell by the way we implement ~. In Haskell, today, it works out because we have "uniqueness of identity proofs" or "axiom K".

What does it mean that HRefl doesn't imply Refl? I tried to google Axiom K but quickly got lost :( I naively thought that HRefl is just Refl but without the “kinds have to be equal or else GHC will bark” restriction. Is there some situation (in current Haskell or some variant of Haskell) where we can have HRefl for a pair of types but not Refl?