Newtype over (~#)

[Igor Popov]

Hello list!

Recently I've had this idea of letting Haskell source handle unboxed
equalities (~#) by the means of an unboxed newtype. The idea is pretty
straightforward: in Core Constraint is Type and (=>) is (->), so a
datatype like

data Eq a b = (a ~ b) => Refl

could become a newtype because it only has a single "field": (a ~ b).
Furthermore now that we have unlifted newtypes, we could write it as a
newtype over (~#), of kind TYPE (TupleRep []).

Defining such a datatype is of course impossible in source Haskell, but
what I came up with is declaring a plugin that magically injects the
necessary bits into the interface file.

Sounds like it should be straightforward: define a newtype (:~:#) with a
constructor whose representation type is:

forall k (a :: k) (b :: k). (a ~# b) -> a :~:# b

The worker constructor is implemented by a coercion (can even be
eta-reduced):

axiom N::~:# :: forall {k}. (:~:#) = (~#)
Refl# = \ (@ k) (@ (a :: k)) (@ (b :: k)) (v :: a ~# b) ->
   v `cast` (Sym (N::~:#) <k>_N) <a>_N <b>_N

And the wrapper constructor has a Haskell-ish type:

$WRefl# :: forall k (b :: k). b :~:# b
$WRefl# = \ (@ k) (@ (b :: k)) ->
   Refl# @ k @ a @ b @~ <b>_N

Caveat: we don't actually get to specify the unwrappings ourselves, and
we have to rely on mkDataConRep generating the right wrapper based on
the types and the EqSpec (because this will have to be done every time
the constructor is loaded from an iface). In this case the machinery is
not convinced that a wrapper is required, unless we ensure that
dataConUserTyVarsArePermuted by fiddling around with ordering of
variables. This is a minor issue (which I think I can work around) but
could be addressed on the GHC side.

I've indeed implemented a plugin that declares these, but we run into a
more major issue: the simplifier is not ready for such code! Consider a
simple utility function:

sym# :: a :~:# b -> b :~:# a
sym# Refl# = Refl#

This gets compiled into:

sym# = \ (@ k) (@ (a :: k)) (@ (b :: k)) (ds :: a :~:# b) ->
   case ds `cast` N::~:# <k>_N <a>_N <b>_N of
       co -> $WRefl# @ k @ b `cast` ((:~:#) <k>_N <b> (Sym co))_R

which seems valid but then the simplifier incorrectly inlines the
unfolding of $WRefl# and arrives at code that is not even well-scoped
(-dcore-lint catches this):

sym# = \ (@ k) (@ (a :: k)) (@ (b :: k)) (ds :: a :~:# b) ->
   case ds `cast` N::~:# <k>_N <a>_N <b>_N of
       co -> v `cast` (Sym (N::~: <k>_N)) <b>_N <b>_N
           ; ((:~:#) <k>_N <b>_N (Sym co))_R

Actually the problem manifests itself even earlier: when creating an
unfolding for the wrapper constructor with mkCompulsoryUnfolding we run
the unfolding term through simpleOptExpr once before memorizing the
unfolding, and this produces an unfolding for $WRefl# that is broken
(ill-scoped) in a similar fashion:

$WRefl = \ (@ k) (@ (b :: k)) ->
   v `cast` Sym (N::~:# <k>_N) <b>_N <b>_N

And we can verify that the issue is localized here: applying
simpleOptExpr to:

(\ (v :: a ~# a) -> v `cast` <a ~# a>_R)
   @~ <a>_N

results in:

v

The former term is closed and the latter is not.

There is an invariant on mkPrimEqPred (though oddly not on
mkReprPrimEqPred) that says that the related types must not be
coercions (we're kind of violating this here).

I have several questions here:
- Is there a good reason for the restriction that equalities should not
  contain other equalities?
- Should this use case be supported? Coercions are almost first class
  citizens in Core (are they?), makes sense to let source Haskell have a
  bit of that?
- Does it make sense to include this and a few similar types (unboxed
  Coercion and Dict) as a wired in type packaged with GHC in some form?

-- mniip
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20210205/059d1547/attachment.html>