Strings from symbolVal not simplified at compile time

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.

Trac metadata

Trac field	Value
Version	8.6.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (CodeGen)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed weight to 5

added Tbug Trac import code generation labels

changed the description

(Corrected description and simplified example.)

Same with 8.2.2 and 8.4.4.

This seems relevant to efficiently using row types for records: in order to avoid string comparison at run time, string-based field access needs can be converted to index-based access at compile time. However this requires these string comparisons to be simplified.

Another way to do this would be to use a constraint solver plugin and avoid using symbolVal at all. As soon as you use symbolVal you are deferring computation to runtime.

It seems that using symbolVal allows things to be deferred to run time, but then this may not always be necessary.

Here is a slightly more motivated example:

{-# LANGUAGE DataKinds, GADTs #-}

module Test where

import GHC.TypeLits
import Data.Proxy
import Data.Type.Equality

get :: KnownSymbol s => Proxy s -> (Int,Int) -> Int
get s (a,_) | Just Refl <- sameSymbol s (Proxy :: Proxy "fst") = a
get s (_,b) | Just Refl <- sameSymbol s (Proxy :: Proxy "snd") = b

x = get (Proxy :: Proxy "fst") (1,2)

This yields

x1 = I# 1#
x2 = I# 2#

get2 = patError lvl_r1GM
get6 = "fst"#
get4 = "snd"#
get5 = unpackCString# get6
get8 = unpackCString# get4
get7 = eqString get5 get5

x = case get7 of {
      False ->
        case eqString get5 get8 of {
          False -> get2;
          True -> x2
        };
      True -> x1
    }

instead of just x = I# 1#.

So s, and thus the dictionary for KnownSymbol s, cannot be determined at compile time in all cases (e.g. it may come from under an existential). But in the common case where it is known, why not simplify comparisons on it, as is done with non-type-level strings?

I'm not quite sure how a constraint solver plugin would address this particular problem (while of course it could be very useful for dealing with ordering and uniqueness of row entries).

Of course if you do not statically know s then you can't perform the simplification and so you shouldn't expect the comparison to happen before runtime. If you use symbolVal then you are accepting that the computation will happen at runtime as the type gets turned into a value.

My point is that if you want something to happen at compile time you are better off making sure it happens at compile time yourself. Comparing strings like this at compile time requires special logic in the compiler so won't work for general cases. Writing a constraint solver plugin for your own version of sameSymbol :: SameSymbol s1 s2 => Proxy s1 -> Proxy s2 -> Maybe (s1 :~: s2) seems like the most robust way to ensure that the comparison is evaluated statically.

I do not aim to ensure that the comparison is evaluated statically in all cases: it can't, as both your and my previous posts state. Obtaining guarantees on staging seems neither desirable nor possible here.

Instead, I'd simply like the string comparison to happen at compile time when possible, and otherwise at run time. Yes, this is more fragile than the approach you lay out, but crucially it allows the same code to be used when the string is not known at compile time.

As it stands the behaviour of symbolVal seems non-uniform or at least surprising in several ways:

1. While "A" == "A" is simplified to True at compile time, symbolVal (Proxy :: Proxy "A") == symbolVal (Proxy :: Proxy "A") isn't.

2. For type-level numbers natVal (Proxy :: Proxy 42) == natVal (Proxy :: Proxy 42) is simplified to True at compile time.

3. Removing the type signature testAB :: Bool (first bit of code), makes testAB simplify to False at compile time. Why does adding a type signature inhibit the simplifier?

4. Removing testAA makes testAB simplify to False as well. Why does adding another definition inhibit the simplifier?

If there are technical reasons for type-level strings to behave in these ways I'd be curious to learn about them.

added Pnormal label

mentioned in merge request !6259 (closed)

mentioned in commit 2e7c89a3

mentioned in commit fac5d721

mentioned in commit 8577bc17

closed with commit 901c79d8

mentioned in commit 901c79d8