Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Why isn't the "constraint trick" working in this manually defined HasField instance?

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 ReifiedGetters 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?

like image 937
danidiaz Avatar asked Apr 07 '20 12:04

danidiaz


1 Answers

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:

  • We know we have a Person, so—through runGetter—the field's type in the HasField must be ReifiedGetter Person v and the r must be Person.
  • Because r is Person, the source type in the HasField must be Glass Person. We can now resolve the trivial Glassy instance for the the.
  • The key k in the HasField is given as a type literal: the Symbol name.
  • We check the instance preconditions. We know 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.
like image 93
danidiaz Avatar answered Nov 10 '22 21:11

danidiaz