CODEWITHSUNDEEP
haskellsingleton-type
user512596
user512596

Reputation:

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

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

Upvotes: 1

Views: 125

Answers (2)

dfeuer
dfeuer

Reputation: 48631

The trouble is that you're using (essentially) a kind class, but you're not pinning down kinds properly. In particular, the three occurrences of 'KProxy could all refer to different kinds. A common approach would be to name the proxy using an equality constraint, and use that name repeatedly. This saves a bit of typing compared to giving every proxy a signature:

matches :: (kproxy ~ ('KProxy :: KProxy k),
            Eq (DemoteRep kproxy),
            SingKind kproxy)
        => DemoteRep kproxy
            -> Sing (a :: k) -> Bool

This makes it clear that the proxies should all be the same, and in particular should have the same kind as the type passed to Sing.

Upvotes: 1

hao
hao

Reputation: 10238

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

Upvotes: 5

Related Questions