<div dir="ltr">Hello list!<br><br>Recently I've had this idea of letting Haskell source handle unboxed<br>equalities (~#) by the means of an unboxed newtype. The idea is pretty<br>straightforward: in Core Constraint is Type and (=>) is (->), so a<br>datatype like<br><br>     data Eq a b = (a ~ b) => Refl<br><br>could become a newtype because it only has a single "field": (a ~ b).<br>Furthermore now that we have unlifted newtypes, we could write it as a<br>newtype over (~#), of kind TYPE (TupleRep []).<br><br>Defining such a datatype is of course impossible in source Haskell, but<br>what I came up with is declaring a plugin that magically injects the<br>necessary bits into the interface file.<br><br>Sounds like it should be straightforward: define a newtype (:~:#) with a<br>constructor whose representation type is:<br><br>        forall k (a :: k) (b :: k). (a ~# b) -> a :~:# b<br><br>The worker constructor is implemented by a coercion (can even be<br>eta-reduced):<br><br>      axiom N::~:# :: forall {k}. (:~:#) = (~#)<br>     Refl# = \ (@ k) (@ (a :: k)) (@ (b :: k)) (v :: a ~# b) -><br>     v `cast` (Sym (N::~:#) <k>_N) <a>_N <b>_N<br><br>And the wrapper constructor has a Haskell-ish type:<br><br>    $WRefl# :: forall k (b :: k). b :~:# b<br>        $WRefl# = \ (@ k) (@ (b :: k)) -><br>      Refl# @ k @ a @ b @~ <b>_N<br><br>Caveat: we don't actually get to specify the unwrappings ourselves, and<br>we have to rely on mkDataConRep generating the right wrapper based on<br>the types and the EqSpec (because this will have to be done every time<br>the constructor is loaded from an iface). In this case the machinery is<br>not convinced that a wrapper is required, unless we ensure that<br>dataConUserTyVarsArePermuted by fiddling around with ordering of<br>variables. This is a minor issue (which I think I can work around) but<br>could be addressed on the GHC side.<br><br>I've indeed implemented a plugin that declares these, but we run into a<br>more major issue: the simplifier is not ready for such code! Consider a<br>simple utility function:<br><br>     sym# :: a :~:# b -> b :~:# a<br>       sym# Refl# = Refl# <br><br>This gets compiled into:<br><br>     sym# = \ (@ k) (@ (a :: k)) (@ (b :: k)) (ds :: a :~:# b) -><br>           case ds `cast` N::~:# <k>_N <a>_N <b>_N of<br>            co -> $WRefl# @ k @ b `cast` ((:~:#) <k>_N <b> (Sym co))_R<br><br>which seems valid but then the simplifier incorrectly inlines the<br>unfolding of $WRefl# and arrives at code that is not even well-scoped<br>(-dcore-lint catches this):<br><br>      sym# = \ (@ k) (@ (a :: k)) (@ (b :: k)) (ds :: a :~:# b) -><br>           case ds `cast` N::~:# <k>_N <a>_N <b>_N of<br>            co -> v `cast` (Sym (N::~: <k>_N)) <b>_N <b>_N<br>                   ; ((:~:#) <k>_N <b>_N (Sym co))_R<br><br>Actually the problem manifests itself even earlier: when creating an<br>unfolding for the wrapper constructor with mkCompulsoryUnfolding we run<br>the unfolding term through simpleOptExpr once before memorizing the<br>unfolding, and this produces an unfolding for $WRefl# that is broken<br>(ill-scoped) in a similar fashion:<br><br>     $WRefl = \ (@ k) (@ (b :: k)) -><br>       v `cast` Sym (N::~:# <k>_N) <b>_N <b>_N<br><br>And we can verify that the issue is localized here: applying<br>simpleOptExpr to:<br><br>  (\ (v :: a ~# a) -> v `cast` <a ~# a>_R)<br>         @~ <a>_N<br><br>results in:<br><br> v<br><br>The former term is closed and the latter is not.<br><br>There is an invariant on mkPrimEqPred (though oddly not on<br>mkReprPrimEqPred) that says that the related types must not be<br>coercions (we're kind of violating this here).<br><br>I have several questions here:<br>- Is there a good reason for the restriction that equalities should not<br>  contain other equalities?<br>- Should this use case be supported? Coercions are almost first class<br>  citizens in Core (are they?), makes sense to let source Haskell have a<br>  bit of that?<br>- Does it make sense to include this and a few similar types (unboxed<br>  Coercion and Dict) as a wired in type packaged with GHC in some form?<br><br>-- mniip<br></div>