Reputation:
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
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
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.
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