I couldn’t find anything on Google. I want something like `:~:`

that is unboxed, i.e. a `ZeroBitType`

.

Does this exist?

I couldn’t find anything on Google. I want something like `:~:`

that is unboxed, i.e. a `ZeroBitType`

.

Does this exist?

Not that I’m aware of, but you can more-or-less write it yourself:

```
{-# LANGUAGE
MagicHash, UnliftedNewtypes, UnboxedTuples,
GADTs, DataKinds, ExplicitNamespaces, RoleAnnotations
#-}
module ZeroBitEq (
type (~#),
refl#,
withRefl#,
) where
-- base
import GHC.Exts (ZeroBitType)
import Unsafe.Coerce (unsafeCoerce)
import Data.Type.Equality ((:~:)(..))
type role (~#) nominal nominal
type (~#) :: k -> k -> ZeroBitType
newtype a ~# b = UnsafeRefl# (# #)
refl# :: (# #) -> a ~# a
refl# = UnsafeRefl#
withRefl# :: forall a b r. a ~# b -> (a ~ b => r) -> r
withRefl# !_ r = case unsafeCoerce Refl :: a :~: b of
Refl -> r
```

3 Likes

I do something similar in Bluefin, not for type equality but for a type level subset relation. It involves implementing the witness as

```
newtype In (a :: Effects) (b :: Effects) = In# (# #)
```

and then implementing some axioms, and some theorems on top of those axioms.

2 Likes

Indeed; though I didn’t look too closely back then, I actually glimpsed this magic when I looked over bluefin previously.

Your `have`

and `inComp`

also roughly correspond to my `withRefl#`

, but I notice that you only seem to be using `inComp`

for transitivity? In a project I’m currently working on, I have similar proof tokens for scoping, where the `Category`

instance provides reflexivity and transitivity:

```
data Scope
type role (~<) nominal nominal
type (~<) :: Scope -> Scope -> Type
data a ~< b = UnsafeSubScopeProof
instance Category (~<) where
id = UnsafeSubScopeProof
!_ . !_ = UnsafeSubScopeProof
```

Like `~`

and `:>`

, it also has a constraint form `<|`

:

```
reflect :: p ~< q -> (p <| q => r) -> r
```

But here’s the clever part—GHC can actually *infer* reflexivity and transitivity if you phrase the class just right! Ultimately, I don’t actually need the value level proof tokens, they just give you better error messages in prototyping.

```
type (<|) = SubScope
class SubScopeEndo (s :: Scope)
class (SubScopeEndo p => SubScopeEndo q) => SubScope p q where
auto :: p ~< q
instance (SubScopeEndo p => SubScopeEndo q) => SubScope p q where
auto = UnsafeSubScopeProof
```

Credit to the authors of *The Foil* for this technique.

1 Like

Thanks! I already do this but it seems like something that you’d expect to be in `base`

.

Ultimately we’d want `:~:`

to be unboxed itself (or perhaps more precisely, unlifted, zero-width). I’m not actually sure why it’s not. I guess part of the reason is that `~`

is a lifted constraint. I don’t understand that either. Type equality doesn’t require any non-trivial information. Couldn’t it be an unlifted, zero-width constraint?

1 Like

afaiu it is. i.e. the `~`

in real GADTs (not the ones made with lifted equality and `-XExistentialTypes`

) compile to an unlifted equality (`~#`

). However, there’s no syntax for unlifted equality, because iirc it doesn’t have the right kind to even fit into the surface level syntax or something like this. You can, however, make GHC reveal what it’s really doing, by asking it what `(~~)`

is. In order to do so, open a `GHCi`

, then import `GHC.Types`

, set `-fprint-equality-relations`

and type `:i (~~)`

.

You can also see it if you define a

```
module Eq where
import Prelude ()
data Eq a b where
Refl :: Eq a a
```

and then look at the core of the `Refl`

constructor.

2 Likes