Binding types in signatures

Question

What is the most direct way to bind a type variable when pattern matching in a Gadt ?

#!/usr/bin/env stack
-- stack script --resolver lts-13.1
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs, ScopedTypeVariables             #-}
{-# LANGUAGE DataKinds   #-}
module Main where
import Data.Proxy
import GHC.TypeLits    
main :: IO ()
main = undefined

data Kind where
  Index :: Symbol -> Kind

data Gadt (f::Kind) where
  Lit :: KnownSymbol s => Gadt ('Index s)

Binding s directly would fail

format :: Gadt f -> String
format (Lit :: Gadt ('Index s)) = undefined   -- KO

with error

• Couldn't match type ‘f’ with ‘'Index s’
  ‘f’ is a rigid type variable bound by
    the type signature for:
      format :: forall (f :: Kind). Gadt f -> String
  Expected type: Gadt f
  Actual type: Gadt ('Index s)

A type function can extract the type, but aren't there more direct way to do this ?

format (Lit :: Gadt i)  =  symbolVal (Proxy :: TLabel i)

type family TLabel (a::Kind)
type instance TLabel ('Index s  ) = Proxy s

Answer 1

The only way I see is to add a Proxy to bind the type variable with ScopedTypeVariables.

data Gadt a where
  Lit :: KnownNat s => Proxy s -> Gadt ('Index s)

format :: Gadt a -> String
format (Lit (Proxy :: Proxy s)) = undefined

If you are worried about the extra allocation, the field can be unpacked. (EDIT: removed previous mention of Proxy# because that doesn't seem necessary).

import Data.Proxy

-- This should be as efficient as the original Gadt with a nullary Lit
data Gadt a where
  Lit :: {-# UNPACK #-} !(Proxy r) -> Gadt ('Index r)

format :: Gadt a -> String
format (Lit (_ :: Proxy r)) = undefined

---

On the longer term, the following GHC proposal will address this issue: Type Applications in Patterns.

-- The original type
data Gadt a where
  Lit :: forall s. Gadt ('Index s)

format :: Gadt a -> String
format (Lit @s) = ...