Confusing deriveArgDict behaviour/error messages

[jonathanlking]

Consider the following toy example:

{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE UndecidableInstances #-}
module Example where

import Data.Constraint.Extras.TH (deriveArgDict)

data A a where
  MkA :: B a -> A a

data B a where
  MkB :: B ()

deriveArgDict ''A
deriveArgDict ''B

Compiling this errors with:

    • Could not deduce: c a
        arising from a use of ‘Data.Constraint.Dict’
      from the context: Data.Constraint.Extras.ConstraintsFor A c
        bound by the type signature for:
                   Data.Constraint.Extras.argDict :: forall a.
                                                     Data.Constraint.Extras.ConstraintsFor A c =>
                                                     A a -> Data.Constraint.Dict (c a)
    • In the expression: Data.Constraint.Dict
      In a case alternative: MkA {} -> Data.Constraint.Dict
      In the expression: \case MkA {} -> Data.Constraint.Dict
    • Relevant bindings include
        argDict :: A a -> Data.Constraint.Dict (c a)
   |
   | deriveArgDict ''A
   | ^^^^^^^^^^^^^^^^^

Dumping the splices (with -ddump-splices) we can see the generated code is:

instance Data.Constraint.Extras.ArgDict c A where
  type Data.Constraint.Extras.ConstraintsFor A c = ()
  Data.Constraint.Extras.argDict
    = \case MkA {} -> Data.Constraint.Dict

When instead I would expect it to generate:

instance Data.Constraint.Extras.ArgDict c A where
  type Data.Constraint.Extras.ConstraintsFor A c = (Data.Constraint.Extras.ConstraintsFor B c)
  Data.Constraint.Extras.argDict
    = \case MkA x -> Data.Constraint.Extras.argDict x

As the ArgDict instance for B has not been generated yet, hasArgDictInstance is False in deriveArgDict, so no ConstraintsFor B c/recursive call to argDict is generated.

A solution to this is to make sure deriveArgDict ''B comes before deriveArgDict ''A, which does generate the expected code, but this can be difficult to work out just from the error message.

I am curious what the hasArgDictInstance check actually prevents? Can we remove it, always "optimistically" generate constraints and just let GHC's constraint solver handle this for us (failing if the constraint can't be satisfied).

I have patched our copy of constraints-extras in our codebase to do this and haven't noticed any errors, but am very possibly missing something!

[Ericson2314]

A solution to this is to make sure deriveArgDict ''B comes before deriveArgDict ''A, which does generate the expected code, but this can be difficult to work out just from the error message.

Check out https://github.com/gelisam/klister This is the proper solution to keep order independence and I hope we get it someday in Haskell. @david-christiansen being HF director is auspicious for this :)

I am curious what the hasArgDictInstance check actually prevents? Can we remove it, always "optimistically" generate constraints and just let GHC's constraint solver handle this for us (failing if the constraint can't be satisfied).

I don't understand this. Are you asking why we can't also do Data.Constraint.Extras.argDict x --- why we sometimes need to do Data.Constraint.Dict instead?

[david-christiansen]

Haskell languages changes are up to the GHC Steering Committee, not me :-) I'm glad you think Klister is promising, though, and I hope to someday have some time to do work on it again.

[Ericson2314]

Well that's why I used a vague work like "auspicious" :) For now, I just want to collect a Real World™ instance of the problem that solves to refer to sometime later.

[jonathanlking]

Thanks for sharing klister with me, I hadn't heard about it before and it looks interesting! ✨

I don't understand this. Are you asking why we can't also do Data.Constraint.Extras.argDict x --- why we sometimes need to do Data.Constraint.Dict instead?

Sorry, I don't think I asked the question very well, let me try again:

I've found that removing the hasArgDictInstance check makes the problem I described go away.
If I removed it (e.g. jonathanlking@e395ee1), what could go wrong? (i.e. what is the function of it?)