I think the intention is to have that proposal (which proposes a language change) be superseded by this idea (which does not change the language).
Oh, I did not know that. I’ll ignore the proposal for now, in that case.
All that would take is putting Coercion in TysWiredIn, and moving Coercion from Data.Type.Coercion to somewhere in ghc-prim.
I don’t think it’s quite as simple as that. Yes, we can wire it into the compiler; but we still need a module that defines the info table, curried data constructor etc for the type. And we have no way to do that.
We could utterly lie and say
data Coercion a b where
Coercion :: Coercion a a
That would generate the right bits in in the .o file, and we’d totally ignore the .hi file. Gruesome but I think it would work.
But rather than all this circumlocution, why don’t we just make it possible to write ~# and ~R# directly. Even if we dodge the need right now, it’ll surely come back.
If that is lexically tiresome, we could I suppose provide builtin-aliases for them, as if we had
type NomEq# = (~#)
type ReprEq# = (~R#)
Simon
From: Ryan Scott
Simple is good. But what is this dead simple idea?
I'm referring to David's first e-mail on this thread: https://mail.haskell.org/pipermail/ghc-devs/2018-September/016191.html All that would take is putting Coercion in TysWiredIn, and moving Coercion from Data.Type.Coercion to somewhere in ghc-prim.
Maybe this thread belongs with the proposal, unless I’m misunderstanding.
I think the intention is to have that proposal (which proposes a language change) be superseded by this idea (which does not change the language).
Ryan S.
On Wed, Sep 5, 2018 at 10:20 AM, Simon Peyton Jones