Find/construct dictionary from class and type

[conal]

I want to find an instance of a given class for a given type, using whatever instances are visible. An example of particular importance to me:

class Encodable a where
  type Enc a
  encode :: a -> Enc a
  decode :: Enc a -> a

A sample data type (length-typed sequences, using DataKinds):

data Nat = Z | S Nat

data Vec :: Nat -> * -> * where
  ZVec :: Vec Z a
  (:<) :: a -> Vec n a -> Vec (S n) a

instance Encodable (Vec Z a) where
  type Enc (Vec Z a) = ()
  encode ZVec = ()
  decode () = ZVec

instance Encodable (Vec (S n) a) where
  type Enc (Vec (S n) a) = (a, Vec n a)
  encode (a :< as) = (a,as)
  decode (a,as) = a :< as

When manipulating Core, given a type like Vec (S (S Z)) Bool, I want to find/construct the corresponding Encodable dictionary or learn that there isn't one in scope.

[conal]

We've talked about this one. I wanted to get it into issue tracking.

[conal]

I'm still very interested in this feature, exactly for use with the Encodable class, which appears in LambdaCCC.Encode.

[xich]

I've added buildDictionaryT in 15c0165609d3a32efd475624cb7ae21f48f8c0bb, which gives an example of how to invoke the underlying buildDictionary function. If you find yourself needing a different interface, let me know. For instance, if you want to share the dictionary in multiple places, you may want to get the bindings and dictionary variable back separately.

This works on predicate types like Functor Maybe and Monad [] and Monoid (Map k a), but I haven't tried with more exotic things like Monoid (Maybe (forall a. a -> a)), which probably won't work, so let me know if you run into that problem.

[conal]

Fantastic! I'll try it out ASAP and get back to you. Thanks a bunch.

[conal]

Looking good! I'm using buildDictionaryT to construct Encodable instances now. This feature opens up a lot of possibilities for me. Thanks!

[conal]

What does buildDictionaryT do when it can't find an instance? I assumed it'd fail, but I'm instead getting a dictionary construction that refers by name to a non-existent dictionary.

Example below. I (accidentally) used a Vec N1 Integer instead of Vec N1 Int. I have an Encodable instance for Int but not for Integer, so there is no instance for Vec N1 Integer. Instead of failing, buildDictionaryT constructed the following expression:

   (let $dEncodable0 :: Encodable Bool
        $dEncodable0 = $fEncodableBool
        $dEncodable1 :: Encodable Unit
        $dEncodable1 = $fEncodable()
        $dEncodable2 :: Encodable (Vec Z Bool)
        $dEncodable2 = $fEncodableVec0 Bool $dEncodable1
        $dEncodable3 :: Encodable ((:*) Bool (Vec Z Bool))
        $dEncodable3 =
          $fEncodable(,) Bool (Vec Z Bool) $dEncodable0 $dEncodable2
        $dEncodable4 :: Encodable (Vec Z Integer)
        $dEncodable4 = $fEncodableVec0 Integer $dEncodable1
        $dEncodable5 :: Encodable ((:*) Integer (Vec Z Integer))
        $dEncodable5 =
          $fEncodable(,) Integer (Vec Z Integer) $dEncodable $dEncodable4
        $dEncodable6 :: Encodable (Vec (S Z) Bool)
        $dEncodable6 = $fEncodableVec Z Bool $dEncodable3
        $dEncodable7 :: Encodable (Vec (S Z) Integer)
        $dEncodable7 = $fEncodableVec Z Integer $dEncodable5
        $dLambdaCCC.Encode.Encodable(TypeUnary.Vec.Vec(TypeUnary.TyNat.STypeUnary.TyNat.Z)GHC.Integer.Type.Integer->TypeUnary.Vec.Vec(TypeUnary.TyNat.STypeUnary.TyNat.Z)GHC.Types.Bool)
           :: Encodable (Vec (S Z) Integer -> Vec (S Z) Bool)
        $dLambdaCCC.Encode.Encodable(TypeUnary.Vec.Vec(TypeUnary.TyNat.STypeUnary.TyNat.Z)GHC.Integer.Type.Integer->TypeUnary.Vec.Vec(TypeUnary.TyNat.STypeUnary.TyNat.Z)GHC.Types.Bool) =
          $fEncodable(->)
            (Vec (S Z) Integer) (Vec (S Z) Bool) $dEncodable7 $dEncodable6
    in $dLambdaCCC.Encode.Encodable(TypeUnary.Vec.Vec(TypeUnary.TyNat.STypeUnary.TyNat.Z)GHC.Integer.Type.Integer->TypeUnary.Vec.Vec(TypeUnary.TyNat.STypeUnary.TyNat.Z)GHC.Types.Bool))

Then core-lint objects:

In the expression: LambdaCCC.Encode.$fEncodable(,)
                     @ GHC.Integer.Type.Integer
                     @ (TypeUnary.Vec.Vec TypeUnary.TyNat.Z GHC.Integer.Type.Integer)
                     $dEncodable_a4e5
                     $dEncodable4_s4er
$dEncodable_a4e5
  :: LambdaCCC.Encode.Encodable GHC.Integer.Type.Integer
[LclId, Str=DmdType] is out of scope
<no location info>: Warning:
In the expression: LambdaCCC.Encode.$fEncodable(,)
                     @ GHC.Integer.Type.Integer
                     @ (TypeUnary.Vec.Vec TypeUnary.TyNat.Z GHC.Integer.Type.Integer)
                     $dEncodable_a4ef
                     $dEncodable1_s4eB
$dEncodable_a4ef
  :: LambdaCCC.Encode.Encodable GHC.Integer.Type.Integer
[LclId, Str=DmdType] is out of scope

I'm working around this issue for now by defining buildDictionaryT' = (lintExpr >> id) . buildDictionaryT (where these id and (.) are from Category) and using it in place of buildDictionaryT.

[xich]

Ah thanks for pointing this out!

buildDictionaryT is a think wrapper around GHC's solveWantedsTcM, which gives back a list of unsolved constraints. When I was originally experimenting with this, I just dropped these on the floor and left myself a comment to deal with it later... then promptly forgot about it. :-P

I'll look into handling them properly as an error.

[conal]

Appears to be broken now. Please see dict-test.

[xich]

I rolled back to HERMIT right when I added buildDictionaryT, and dict-test doesn't work then either (does the same thing), so I'm not sure this example ever worked.

It's curious that it is returning the Id we generate rather than an expression for that Id. That makes me think the underlying solvedWantedsTcM is silently failing. I'll poke around a bit more this afternoon and see what I can come up with.

[xich]

I use buildDictionaryT to generate the dictionaries for our type class proofs and it works there... but the dictionaries I'm generating are very simple (Monad for Maybe, etc). So maybe this is an import issue?

I changed the module name to Main and added:

main :: IO ()
main = print $ succ test1

and then things worked... (the let bindings were generated)

test1 :: Bool
test1 =
  succ
    Bool
    (let $dGHC.Enum.EnumGHC.Types.Bool :: Enum Bool
         $dGHC.Enum.EnumGHC.Types.Bool = $fEnumBool
     in $dGHC.Enum.EnumGHC.Types.Bool)
    False

Changing main to: main = print "hello" doesn`t work.

So I'm guessing this is an issue where the instances aren't visible in some cache that solveWantedsTcM uses. I'll investigate more.

[conal]

@xich: Thank you for investigating! I guess what happened on my end was that I used to refer in the module being transformed to the type class for which I was using buildDictionaryT. I hadn't realized that the those references were helping buildDictionaryT work.

I've updated dict-test with improved examples and a more accurate description of the issue. I had forgotten that Bool is in Enum. Now there's a String example, which incorrectly succeeds and generates an an-of-scope name.

[conal]

For now, I'm working around the problem with a tweak to buildDictionaryT that checks for empty bindings (null bnds):

buildDictionaryT :: Transform c HermitM Type CoreExpr
buildDictionaryT = contextfreeT $ \ ty -> do
    dflags <- getDynFlags
    binder <- newIdH ("$d" ++ filter (not . isSpace) (showPpr dflags ty)) ty
    guts <- getModGuts
    (i,bnds) <- liftCoreM $ buildDictionary guts binder
    if null bnds
      fail "couldn't build dictionary"
     else return $ case bnds of
                     [NonRec v e] | i == v -> e -- the common case that we would have gotten a single non-recursive let
                     _ -> mkCoreLets bnds (varToCoreExpr i)

Now in dict-test, I use this definition if the CPP symbol MyBuildDict is defined.

[conal]

I think this bogus success (with no bindings) has been around for a while. I'd been using buildDictionaryT in combination with lintExprR to generate a failure.

[xich]

I've pushed some changes in 18694aef8b214994fe33b27da7710647caec0203 which should catch the typechecker errors correctly and turn them into transformation failures.

I've also looked into trying to dynamically load the necessary instances into whatever is needed so they are found without needing to explicitly reference them in the source, but haven't gotten anywhere yet.

[xich]

Just a note to self: assuming I can even load the right module interface, I'm not sure which module to load it for. For Enum Int, I'd need to load GHC.Enum (the module that defines the Enum class). But for an Enum instance for a custom data type, the instance would be in the module defining the type, not GHC.Enum.

[conal]

Thanks for 18694ae. Works for me.

[conal]

I just got bitten again by the problem mentioned here. Any ideas on what's going on there?

[xich]

I have a working theory as to what is happening, but its taking a long time to track down.

When the source mentions pred or succ explicitly, I believe the proper module/instance gets loaded by the typechecker (or maybe the renamer?) into its instance environment... which is passed through to the ModGuts, which is where we get the environment to rebuild a new typechecking environment for dictionary creation. If the source does not mention pred or succ, the instance is never loaded, so the dictionary-building code can't find it... and isn't smart enough to load it on it's own.

So I'm trying to track down where in GHC this is done, so I can duplicate it on our side.

[conal]

Wow. Sounds like a difficult trail to follow. Thanks very much for the continuing detective work.

[xich]

After lots of digging, this turned out to have a rather simple fix (I think). Could you pull down c555e37e94e847eeb8417f1a67e93d950160d532 and give it a try?

I tested on your dict-test repo, removing the binding for foo. Before, it failed on all three with no instance found. After, it succeeds on test1 and test2, and fails on test3, as expected.

[conal]

Works for me, too. w00t! Thanks.