Why does GHC complain about the missing `Typeable` instance even if I specify is as a type restricti-CodePudding

Why does the following code not compile even if I added the Typeable boundary to satisfy the cast function's requirements?

import           Data.Data

a :: Maybe Int
a = cast f
  where
    f :: Typeable a => a
    f = undefined

app/Main.hs:6:5: error:
    • No instance for (Typeable a0) arising from a use of ‘cast’
    • In the expression: cast f
      In an equation for ‘a’:
          a = cast f
            where
                f :: Typeable a => a
                f = undefined
  |
6 | a = cast f
  |     ^^^^

Maybe Int should implement the type class because the following code compiles.

import           Data.Data

b :: String
b = show $ typeRep (Proxy :: Proxy (Maybe Int))

(I'm not asking how to cast a value, e.g., from Int to String. I'm just curious about this strange error.)

GHC: 9.2.2

CodePudding user response：

The problem is that you never specify the type that f should have before the cast. You could equally well do

a :: Maybe Int
a = cast (f :: Int)
 where f :: Typeable a => a
       f = undefined

(which would yield Just ⊥) or

a :: Maybe Int
a = cast (f :: [String])
 where f :: Typeable a => a
       f = undefined

(which would yield Nothing).

Some constraints would cause the compiler to default an unspecified type, e.g. a Num context would default to Integer. But Typeable does not default to anything, so the compiler baulks.

CodePudding user response：

When you write a polymorphic declaration like that you are basically saying i can produce any a that has a Typeable instance. Then the caller decides which a to instantiate the type variable. For example

b :: String
b = show f
  where
    f :: (Show a) => a
    f = undefined -- for example you cannot write f="x"

this produces a similar error. It is not specified anywhere in the program what a should be used.