I am working on a project where I keep track of the db-schema I use via a phantom type - that has a KnownSymbol
- which is the schema name.
Just the other day I came upon the following problem - which I don't understand:
Why is it impossible to define withoutProxy
or to rephrase it - why does GHC assume that test
is of kind *
instead of Symbol
in (Proxy :: Proxy test)
, although the type signature says otherwise and ScopedTypeVariables
is enabled.
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE KindSignatures #-}
module T where
import GHC.TypeLits
import Data.Proxy
newtype Phantom (x :: Symbol) y = Phantom y
withProxy :: (KnownSymbol test) => Proxy test -> Phantom test ()
withProxy _ = Phantom ()
withoutProxy :: (KnownSymbol test) => Phantom test ()
withoutProxy = withProxy (Proxy :: Proxy test)
The error I get is most confusing
> ghci test.hs
GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling T ( test.hs, interpreted )
test.hs:14:27: error:
• Couldn't match type ‘*’ with ‘Symbol’
Expected type: Proxy test
Actual type: Proxy test
Use -fprint-explicit-kinds to see the kind arguments
• In the first argument of ‘withProxy’, namely
‘(Proxy :: Proxy test)’
In the expression: withProxy (Proxy :: Proxy test)
In an equation for ‘withoutProxy’:
withoutProxy = withProxy (Proxy :: Proxy test)
Failed, modules loaded: none.
Then enabling -fprint-explicit-kinds
Prelude> :set -fprint-explicit-kinds
Prelude> :r
[1 of 1] Compiling T ( test.hs, interpreted )
test.hs:15:27: error:
• Couldn't match type ‘*’ with ‘Symbol’
Expected type: Proxy Symbol test
Actual type: Proxy * test
• In the first argument of ‘withProxy’, namely
‘(Proxy :: Proxy test)’
In the expression: withProxy (Proxy :: Proxy test)
In an equation for ‘withoutProxy’:
withoutProxy = withProxy (Proxy :: Proxy test)
Failed, modules loaded: none.
Short answer: add forall
withoutProxy :: forall test. (KnownSymbol test) => Phantom test ()
withoutProxy = withProxy (Proxy :: Proxy test)
Without it test
on the second row, is different from the one above.
Or, don't add type-annotation at all:
withoutProxy :: (KnownSymbol test) => Phantom test ()
withoutProxy = withProxy Proxy
Or you could add {-# LANGUAGE PolyKinds #-}
, and then things will unify also, as Proxy :: Proxy test
will be forall k (test :: k). Proxy k test
, where k
is a kind.