Specialization of singleton parameters

Question

I'm playing around with specialization of singletons:

{-# LANGUAGE DataKinds      #-}
{-# LANGUAGE GADTs          #-}
{-# LANGUAGE KindSignatures #-}

module Data.Test where

data SingBool (b :: Bool) where
  STrue :: SingBool 'True
  SFalse :: SingBool 'False

sing :: SingBool b -> Bool
sing SFalse = False
sing STrue  = True
{-# SPECIALIZE sing :: SingBool 'False -> Bool #-}

This specializes to something like the following:

singSFalse :: SingBool 'False -> Bool
singSFalse SFalse = False

I'd expect it to generate an RHS of singSFalse _ = False instead.

Is that coercion unpacked only to satisfy the type-checker or is there actual runtime overhead involved in that pattern match? I imagine that GHC does not discard the pattern match on the argument to account for bottom, in order not to increase laziness. But I want to be sure before I begin to model this through Proxy + a SingI-style type class.

Answer 1

OK, to mostly answer my own question: Knowing that SingBool 'False only has one inhabitant is not enough for GHC to get rid of the pattern match, because we could call the function like singSFalse (error "matched"), e.g. bottom is always another inhabitant.

So, specialization (e.g. inlining based on concrete TypeApplications) does not really work well with singletons (turning those type applications into presumably constant value applications) in Haskell (lazy, non-total) w.r.t. zero cost abstractions.

However, by using a SingI-style type class with a proxy (e.g. singByProxy), we don't have the same problems:

{-# LANGUAGE DataKinds      #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MagicHash      #-}

module Data.Test where

import           GHC.Exts (Proxy#)

class SingIBool (b :: Bool) where
  sing :: Proxy# b -> Bool

instance SingIBool 'False where
  sing _ = False

instance SingIBool 'True where
  sing _ = True

refurbulate :: SingIBool b => Proxy# b -> Int
refurbulate p
  | sing p = 0
  | otherwise = 1

The specialization refurbulate @(Proxy# 'False) will not only be implemented as const False, also there will not be passed any Proxy# argument at the value level, so it's rather coerce False :: Proxy# -> Bool. Neat! However, I don't get to use singletons in the real world :(

---

To recap why singletons fail (to get optimized) and type classes work:

By specializing the type class instance, we get to know the RHS of sing, from which we can deduce totality.

By specializing the singleton, we get to know what value the parameter evaluates to, if evaluation terminates.

Knowing the canonical RHS of a type class method x :: () is more informative than just knowing that a parameter x :: () can only evaluate to one value in a non-total, lazy (e.g. Haskell's) setting.