KnownNat and friends are derivable

Summary

Using polymorphic data families, DerivingVia, and StandaloneDeriving it is possible to create new instances of KnownNat, KnownSymbol, and KnownChar. This breaks the safety of sameNat, sameSybol, and sameChar, as well as eqTypeRep and testEquality.

Steps to reproduce

{-# language DataKinds #-}
{-# language DerivingVia #-}
{-# language TypeFamilies #-}

import GHC.TypeLits

data family Z :: k

deriving via 0 instance KnownNat Z

And essentially the same thing for KnownSymbol and KnownChar.

Expected behavior

It seems DerivingVia allows deriving via not representationally equal types as long as the types of the methods involved end up being representationally equal. This can be useful, but the KnownX type classes should not be derivable this way as it breaks the assumption that KnownX instances correspond 1-to-1 with types.

Environment

• GHC version used: 9.2.1 and HEAD