I have this (admittedly weird) code which uses lens and GHC.Records:
{-# LANGUAGE DataKinds, PolyKinds, FlexibleInstances, UndecidableInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
module Main where
import Control.Lens
import GHC.Records
data Glass r = Glass -- just a dumb proxy
class Glassy r where
the :: Glass r
instance Glassy x where
the = Glass
instance (HasField k r v, x ~ r)
-- instance (HasField k r v, Glass x ~ Glass r)
=> HasField k (Glass x) (ReifiedGetter r v) where
getField _ = Getter (to (getField @k))
data Person = Person { name :: String, age :: Int }
main :: IO ()
main = do
putStrLn $ Person "foo" 0 ^. runGetter (getField @"name" the)
The idea is having a HasField
instance that conjures ReifiedGetter
s out of a proxy, just for the hell of it. But it isn't working:
* Ambiguous type variable `r0' arising from a use of `getField'
prevents the constraint `(HasField
"name"
(Glass r0)
(ReifiedGetter Person [Char]))' from being solved.
I don't understand why r0
remains ambiguous. I used the constraint trick, and my intuition is that the instance head should match, then the typechecker would find r0 ~ Person
in the preconditions, and that would remove the ambiguity.
If I change (HasField k r v, x ~ r)
into (HasField k r v, Glass x ~ Glass r)
that removes the ambiguity and it compiles fine. But why does it work, and why doesn't it work the other way?
Perhaps surprisingly, it had to do with Glass
being poly-kinded:
*Main> :kind! Glass
Glass :: k -> *
Meanwhile, unlike the type parameter of Glass
, the "record" in HasField
has to be of kind Type
:
*Main> :set -XPolyKinds
*Main> import GHC.Records
*Main GHC.Records> :kind HasField
HasField :: k -> * -> * -> Constraint
If I add a standalone kind signature like this:
{-# LANGUAGE StandaloneKindSignatures #-}
import Data.Kind (Type)
type Glass :: Type -> Type
data Glass r = Glass
then it typechecks even with (HasField k r v, x ~ r)
.
In fact, with the kind signature, the "constraint trick" ceases to be necessary:
instance HasField k r v => HasField k (Glass r) (ReifiedGetter r v) where
getField _ = Getter (to (getField @k))
main :: IO ()
main = do
print $ Person "foo" 0 ^. runGetter (getField @"name" the)
print $ Person "foo" 0 ^. runGetter (getField @"age" the)
Here, the flow of information during typechecking seems to be:
Person
, so—through runGetter
—the field's type in the HasField
must be ReifiedGetter Person v
and the r
must be Person
.r
is Person
, the source type in the HasField
must be Glass Person
. We can now resolve the trivial Glassy
instance for the the
.k
in the HasField
is given as a type literal: the Symbol
name
.k
and r
, and they jointly determine v
because of the HasField
functional dependency. The instance exists (automagically generated for record types) and now we know that v
is String
. We have successfully disambiguated all types.If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With