haskellproxyphantom-types

Phantoms and Proxies - lead to ghostly error


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.

Solution

  • 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.