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` _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