Add decideSymbol, decideNat, decideChar, decTypeRep and decT

[phadej]

-- sameSymbol returns Maybe (a :~: b)
decideSymbol :: (KnownSymbol a, KnownSymbol b) =>
              proxy1 a -> proxy2 b -> Either (a :~: b -> Void) (a :~: b)
decideSymbol x y
  | symbolVal x == symbolVal y  = Right (unsafeCoerce Refl)
  | otherwise                   = Left (\Refl -> errorWithoutStackTrace ("decideSymbol: A proof of " ++ show (symbolVal x) ++ " :~: " ++ show (symbolVal y)))
  
-- decideNat and decideChar similarly for Natural and Char.

-- the eqTypeRep returns Maybe (a :~: b)
decTypeRep :: forall k1 k2 (a :: k1) (b :: k2).
             TypeRep a -> TypeRep b -> Either (a :~~: b -> Void) (a :~~: b)
decTypeRep a b
  | sameTypeRep a b = Right (unsafeCoerce HRefl)
  | otherwise       = Left (\HRefl -> errorWithoutStackTrace ("decTypeRep: got a proof of " ++ show a ++ " :~~: " ++ show b))
  
-- | eqT returns Maybe (a :~: b)
decT :: forall a b. (Typeable a, Typeable b) => Either (a :~: b -> Void) (a :~: b)
decT = ...

The sameSymbol, sameNat, sameChar and eqTypeRep could be safely† re-implemented using these new combinators:

sameSymbol a b = either (const Nothing) Maybe (decSymbol a b)

but it's probably better to not change their implementations, as they are quite simple anyway.

† by safely I mean without relying on any internal implementation details. Thus if we had decide variants from the beginning, libraries could have defined Maybe (a :~: b) variants if they needed them, but defining decide variants using same functions is relying on (undocumented!) implementation details.

---

This unsafe code already exists in singletons-base, and I argue that such unsafe stuff is better to define next to the actual types.

https://hackage.haskell.org/package/singletons-base-3.1.1/docs/src/GHC.TypeLits.Singletons.Internal.html#line-111

instance SDecide Symbol where
  (SSym :: Sing n) %~ (SSym :: Sing m)
    | Just r <- sameSymbol (Proxy :: Proxy n) (Proxy :: Proxy m)
    = Proved r
    | otherwise
    = Disproved (\Refl -> error errStr)
    where errStr = "Broken Symbol singletons"

and https://hackage.haskell.org/package/singletons-base-3.1.1/docs/src/Data.Singletons.Base.TypeRepTYPE.html#line-93

instance SDecide (TYPE rep) where
  tra %~ trb =
    case eqTypeRep tra trb of
      Just HRefl -> Proved Refl
      Nothing    -> Disproved (\Refl -> error "Type.Reflection.eqTypeRep failed")

cc @RyanGlScott

[treeowl]

I think those should be decideKnownSymbol, etc., with a similar decideTypeable. Do we have/will we get the actual singleton types in base? If so, the functions called decideSymbol etc. should take those.

[RyanGlScott]

You should be able to implement decTypeRep without unsafeCoerce:

decTypeRep :: forall k1 k2 (a :: k1) (b :: k2).
              TypeRep a -> TypeRep b -> Either (a :~~: b -> Void) (a :~~: b)
decTypeRep a b =
  case eqTypeRep a b of
    Just e  -> Right e
    Nothing -> Left (\HRefl -> errorWithoutStackTrace ("decTypeRep: got a proof of " ++ show a ++ " :~~: " ++ show b))

I don't have a strong opinion on the naming.

Do we have/will we get the actual singleton types in base?

Yes, those exist now that #85 has been implemented.

[treeowl]

Do we have/will we get the actual singleton types in base?

Yes, those exist now that #85 has been implemented.

In that case, I think we should definitely have comparison functions that take them, and optionally have the class-based versions.

[phadej]

You should be able to implement decTypeRep without unsafeCoerce:

Yes, but I still need error "which shouldn't ever be reached".

So one might rather implement eqTypeRep using decTypeRep, not the other way around without using some internal implementation knowledge.

[phadej]

If so, the functions called decideSymbol etc. should take those.

There are functions named

sameNat :: (KnownNat a, KnownNat b) => proxy1 a -> proxy2 b -> Maybe (a :~: b)

thus

decideNat :: (KnownSymbol a, KnownSymbol b) =>
              proxy1 a -> proxy2 b -> Either (a :~: b -> Void) (a :~: b)

The singletons versions could be named

decideSNat :: SNat a -> SNat b -> Either (a :~: b -> Void) (a :~: b)

but I in fact omitted them, as I have a follow up to this proposal in mind adding decideEquality :: f a -> f b -> Either (a :~: b -> Void) (a :~: b) to TestEquality f.

[treeowl]

I suggest adding the full set you're considering to the proposal.

[phadej]

I suggest adding the full set you're considering to the proposal.

What do you mean by "the full set"? I'm considering just the four mentioned in the title.

EDIT: there isn't eqSNat :: SNat a -> SNat b -> Maybe (a :~: b) as that's exactly the specialization of testEquality. One can argue there should be, but that wasn't asked for in #85. One can argue that those would make sense as there is eqTypeRep, but eqTypeRep has more general type, so it's actually more powerful than testEquality @TypeRep.

And as there isn't eqSNat having named decideSNat would be weird. I'd rather leave these for the future. (If someone needs decideSNat right away, that one can be implemented safely using proposed decideNat).

[phadej]

I'm also not sure what the GHC.TypeLits interface will look like in GHC-9.6 and happy to postpone advancing this proposal forward until it's out.

[treeowl]

There are four different kinds: Type, Nat, Symbol, and Char. For each of them, I would definitely want a version that accepts explicit singleton/TypeRep arguments. It may also be useful to have, for each, a version that takes those implicitly as class constraints. I'm suggesting that you specify whether you want explicit ones, implicit ones, or both, and that you propose names for all four/eight. Your proposal as it stands has a mix of implicit and explicit, with no scheme for differentiating them by name.

[phadej]

I'm suggesting that you specify whether you want explicit ones, implicit ones, or both

I propose only implicit (type-class) ones for Nat, Symbol and Char, and both for Typeable/TypeRep.

The reason for having explicit one for TypeRep is because it's hetero-kinded: :~~: - double tilde.

The reason for not having explicit (singleton) ones for Nat, Symbol and Char is because I'd rather add a decideEquality to TestEquality type-class, but that is a breaking change and I don't want to dilute this proposal with breaking change concerns. If that future proposal is rejected, there's an alternative to add decideSNat etc later.

[treeowl]

I see now.

[Bodigrim]

I'd probably wait until GHC 9.6 is out and we gain some experience with changes approved in #85 before proceeding with this proposal, but it's proposal's right to trigger a vote if they wish so.

[phadej]

This and #85 are orthogonal, so I'd wish to trigger the vote.

[Bodigrim]

@phadej could you please raise a draft MR which we can vote on?