what is the type of: matches m s = m == fromSing s?

Question

Using the singletons library, this simple function compiles and works. But, ghci and ghc disagree about the type signature of it, and if either of their suggestions is pasted into the code, it will fail to compile.

What type signature will GHC accept? ghc-7.10.3, singletons-2.0.1

{-# LANGUAGE DataKinds, PolyKinds, TypeOperators, TypeFamilies, GADTs, UndecidableInstances, FlexibleContexts #-}

import Data.Proxy (KProxy(..))
import Data.Singletons
import Data.Singletons.Prelude

-- ghc rejects this type signature, but if I leave it off, ghci :t shows exactly this.
matches :: (Eq (DemoteRep 'KProxy), SingKind 'KProxy) => DemoteRep 'KProxy -> Sing a -> Bool
matches m s = m == fromSing s

t :: Sing True
t = sing

demo :: Bool
demo = matches True t

GHC's error with above type signature:

Couldn't match type ‘DemoteRep 'KProxy’ with ‘DemoteRep 'KProxy’
NB: ‘DemoteRep’ is a type function, and may not be injective
The kind variable ‘k2’ is ambiguous
Use -fprint-explicit-kinds to see the kind arguments
Expected type: DemoteRep 'KProxy -> Sing a -> Bool
  Actual type: DemoteRep 'KProxy -> Sing a -> Bool
In the ambiguity check for the type signature for ‘matches’:
  matches :: forall (k :: BOX)
                    (k1 :: BOX)
                    (k2 :: BOX)
                    (k3 :: BOX)
                    (a :: k3).
             (Eq (DemoteRep 'KProxy), SingKind 'KProxy) =>
             DemoteRep 'KProxy -> Sing a -> Bool
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature for ‘matches’:
  matches :: (Eq (DemoteRep KProxy), SingKind KProxy) =>
             DemoteRep KProxy -> Sing a -> Bool

ghc -Wall suggests a different type signature, but the BOX stuff won't be accepted either:

Top-level binding with no type signature:
         matches :: forall (k :: BOX) (a :: k).
                    (Eq (DemoteRep 'KProxy), SingKind 'KProxy) =>
                    DemoteRep 'KProxy -> Sing a -> Bool

Answer 1

'KProxy at the type level is like Proxy at the value level: it has a phantom. Just as we write Proxy :: Proxy a with the phantom type a at the value level, we have to turn on kind signatures and write 'KProxy :: KProxy k with a phantom kind k at the type level. Hopefully that analogy makes a kind of sense. Here's what it looks like:

{-# LANGUAGE DataKinds, PolyKinds, TypeOperators, TypeFamilies, GADTs, UndecidableInstances, FlexibleContexts, KindSignatures #-}

import Data.Proxy (KProxy(..))
import Data.Singletons
import Data.Singletons.Prelude

matches ::
  ( Eq (DemoteRep ('KProxy :: KProxy k))
  , SingKind ('KProxy :: KProxy k)
  ) => DemoteRep ('KProxy :: KProxy k) -> Sing (a :: k) -> Bool
matches m s = m == fromSing s

This type variable k will occur in both DemoteRep ... and Sing ..., which is what lets us type-check m == fromSing s.

GHCi, though sweet and usually smart, has no idea that the type signature needs "another level of indirection" and needs an introduced kind variable.

Aside

I would caution aginst the majority opinion here that -fprint-explicit-kinds is helpful:

λ> :t matches
matches
  :: (Eq (DemoteRep * ('KProxy *)), SingKind * ('KProxy *)) =>
     DemoteRep * ('KProxy *) -> Sing * a -> Bool

That, to me, doesn't really point a finger at what's happening here. I was only able to piece together everything by looking up the signatures for DemoteRep, 'KProxy, and Sing with the handy-dandy :info command.