Show instance for a dependent type

Question

I am playing with dependent types in ghc 8, and I am running into a problem creating a Show instance for my type.

#!/usr/bin/env stack
-- stack exec --resolver=lts-7.14 --package singletons -- ghci
{-# LANGUAGE GADTs, ScopedTypeVariables, TypeInType, TemplateHaskell, LambdaCase, TypeApplications #-}

import Data.Kind
import Data.Singletons.Prelude
import Data.Singletons.TypeLits

 data EmailAddress :: Symbol -> Symbol -> * where
  EmailAddress :: (KnownSymbol a, KnownSymbol b) => EmailAddress a b 

-- works
testEmail :: EmailAddress "blah" "blah.com"
testEmail = EmailAddress

I wanted to be able to show my address.

instance Show (EmailAddress a b)
  where show = showEmailAddress

showEmailAddress :: forall a b. EmailAddress a b -> String
showEmailAddress = \case
  EmailAddress -> symbolVal (Proxy :: Proxy a) ++ "@" ++ symbolVal (Proxy :: Proxy b)

test1 = show testEmail -- works

Now I want to make a runtime EmailAddress from a user supplied string. To start out I will get an address from a singleton. Just taking one string for now.

fromString' :: Sing i -> EmailAddress i i
fromString' = \case
  SSym -> EmailAddress

test2 = fromString' @"asdf" sing -- works

The final piece of the puzzle is that I feel like I should be able to do something like the following.

fromString :: String -> EmailAddress a a
fromString str = case toSing str of
   SomeSing s -> fromString' s

But it doesn't work. No matter what type signatures I apply to various parts of the function, I cannot get it to typecheck, I always get the following error Couldn't match type ‘a’ with ‘a1’ error on the following code.

fromString1 :: String -> EmailAddress a a
fromString1 str = case toSing str of
   SomeSing s -> fromString' s

fromString2 :: forall a. String -> EmailAddress a a
fromString2 str = case toSing str of
   SomeSing (s :: Sing a) -> fromString' s

fromString3 :: forall a. String -> EmailAddress a a
fromString3 str = case toSing str of
   (SomeSing s :: Sing (a :: Symbol)) -> fromString' s

This is the full error. I don't understand where the a1 is coming from in this.

Existentials5.hs:45:20: error:
• Couldn't match type ‘a’ with ‘a1’
  ‘a’ is a rigid type variable bound by
    the type signature for:
      fromString3 :: forall (a :: Symbol). String -> EmailAddress a a
    at Existentials5.hs:43:16
  ‘a1’ is a rigid type variable bound by
    a pattern with constructor:
      SomeSing :: forall k k1 (k2 :: k1) (a :: k). Sing a -> SomeSing k,
    in a case alternative
    at Existentials5.hs:45:5
  Expected type: EmailAddress a a
    Actual type: EmailAddress a1 a1
• In the expression: fromString' s
  In a case alternative: (SomeSing s) -> fromString' s
  In the expression:
    case toSing str of { (SomeSing s) -> fromString' s }
• Relevant bindings include
    s :: Sing a1 (bound at Existentials5.hs:45:14)
    fromString3 :: String -> EmailAddress a a
      (bound at Existentials5.hs:44:1)

Answer 1

fromString :: String -> EmailAddress a a is impossible. fromString @a "" would give us KnownSymbol a for any a, which can't happen, because GHC erases all types from programs, including Symbol-s. We can't just conjure a runtime String corresponding to a. This is the reason why we have to use singletons in the first place.

From another perspective, the issue with String -> EmailAddress a a is that the input String can't be used in any meaningful way, because we need a KnownSymbol a output for a particular a.

If we have non-singleton runtime data, we can convert that to an existential singleton with toSing. We can then do runtime checks to learn about properties of the resulting singleton.