Unboxed equality?

Learn
4

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