Negative type equality - Haskell

We can reify type equality using a thing like:

data Equals a b
  where
  Refl :: a ~ b => Equals a b

if we want to prove that two types are not equal, does it make any sense to reify it as:

data NotEquals a b
  where
  UnRefl :: (a ~ b => Void) -> NotEquals a b

how do you want to use this?

@Georgi Lyubenov // googleson78 it's a long story. there is a function called sameSymbol :: KnownSymbol s => Proxy s -> Proxy s' -> Maybe (s :~: s'). but in the Nothing case, you're actually lacking some evidence. specifically you're lacking the evidence that s is not equal to s', which can for example be used to demonstrate that e.g. a variant indexed by symbols is phantom in the type parameter corresponding to that symbol

hm, but then can you use sameSymbol somehow to produce Either (NotEquals s s') (s :~: s')?

that's the intent, yes

i don't know that I can use sameSymbol specifically to achieve it, it might require a different class

I would choose some representation that is convenient in your case (either what you proposed or UnRefl :: (s :~: s' -> Void) -> NotEquals s s') and then reach for unsafeCoerce in the Nothing case of sameSymbol

because that's what they do to produce the proof of s :~: s' in the first place, i.e. there is probably no way to produce a proof "legally"

at least for the builtin Symbols

another thing that springs to mind is ditching (~) and using CmpSymbol instead in your Equals and NotEquals, but then you lose the convenience that (~) provides and you probably need to unsafeCoerce to recover it

I don't have too much experience manipulating Symbols though, so take my words with a grain of salt :)

Yeah, I suppose that makes sense

Ideally I want to avoid getting too symbol-specific, because I need to implement similar things for both nat and symbol indexed kind structures

I wish we could use something like the agda thing where you use a convenient representation for the type checker and proofs (peano naturals) and then it gets compiled using a more performant representation (Integers) :/

in any case, if it's okay with you, do share what you ended up using, I'm interested

https://www.stackage.org/haddock/lts-15.8/singletons-2.6/Data-Singletons-Decide.html#t:Decision

singletons gives you a Decision (a :~: b)

i've never really figured out how to use that evidence