Compiling

{-# LANGUAGE DataKinds #-}

module Test where

import GHC.TypeLits
import Data.Proxy

testAA :: Bool
testAA = symbolVal (Proxy :: Proxy "A") == symbolVal (Proxy :: Proxy "A")

testAB :: Bool
testAB = symbolVal (Proxy :: Proxy "A") == symbolVal (Proxy :: Proxy "B")

with

ghc -O -ddump-simpl -dsuppress-all Test.hs

yields:

-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
testAA2
testAA2 = "A"#

-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
testAA1
testAA1 = unpackCString# testAA2

-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
testAB1
testAB1 = "B"#

-- RHS size: {terms: 4, types: 0, coercions: 0, joins: 0/0}
testAB
testAB = eqString testAA1 (unpackCString# testAB1)

-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
testAA
testAA = eqString testAA1 testAA1

Removing testAA makes testAB simplify to False, and so does removing testAB's type signature.

I would expect each definition to simplify to True or False, no matter whether it has a type signature or whether the same string is used elsewhere in the same file.