Resolving a Function Call in an Existential Type

Upon reading this page on existentials in Haskell, I was compelled to test the limits of this behavior, so I wrote the following code snippet:

{-# LANGUAGE ExistentialQuantification #-}

data Showable = forall a. Show a => MkShowable a

pack :: Show a => a -> Showable
pack = MkShowable

instance Show Showable where
    show (MkShowable x) = show x

The Showable type is very similar to the ShowBox type created in the aforementioned link. Then I created this contrived example to illustrate my question.

showSomething :: Bool -> Showable
showSomething True = pack 1
showSomething False = pack "ABC"

main :: IO ()
main = do
  x <- getLine
  let y = read x
  print $ showSomething y

This code (which works fine) asks the user for input (which should be 'True' or 'False'), and then prints out 1 if it is True or "ABC" if it is False.

But I'm failing to fully understand how the system does this. Mathematically, it makes perfect sense. But I don't see how the computer is able to resolve it. To me, it looks like the system makes a decision at runtime concerning whether to call Int's show instance or String's show function, but that would imply the existence of a something like C++'s vtables, which I don't believe Haskell has a concept of.

My question is: how does it resolve that? The system can't know in advance whether I'm going to input true or false, so it can't know which show to call at compile-time, yet it clearly works in both cases.

Solution

One way how to implement type classes is passing a dictionary of functions that implement a type class under the hood. For example a function with signature

f :: Show a => T

would be translated into

f' :: (a -> String) -> T

by the compiler and whenever show is used inside f, it's replaced by the additional argument (in reality there would be more functions, all that are declared in Show).

Similarly the data type

forall a . Show a => MkShowable a

would be translated into

forall a . MkShowable' (a -> String) a

So the transformed code might look like this:

{-# LANGUAGE ExistentialQuantification #-}

data Showable' = forall a . MkShowable' (a -> String) a

pack' :: Show a => a -> Showable'
pack' = MkShowable' show

instance Show Showable' where
    show (MkShowable' f x) = f x

showSomething :: Bool -> Showable'
showSomething True = pack' 1
showSomething False = pack' "ABC"

When pack is called, the show implementation is passed to the constructor as well so that it's available when needed.