Is it possible to have a type class for both constants and expressions in DSL?

Question

Suppose, I have a DSL with computations in LangL r a. I might want to have functions work both with constants (0 :: Int, "lala" :: String) and DSL expressions (LangL r a). So, I implement a type class. However, any way I try to implement it, I stumble into problems.

Here's a minimal example of a problem when using type families:

{-# LANGUAGE DeriveAnyClass        #-}
{-# LANGUAGE DeriveFunctor         #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE StandaloneDeriving    #-}
{-# LANGUAGE TypeFamilies          #-}

data LangL r a = LangL a
deriving instance Functor (LangL r)
deriving instance Applicative (LangL r)

class DSLEntity r a where
  type ValueOf a
  entityValue :: a -> LangL r (ValueOf a)

instance DSLEntity r (LangL r a) where
  type ValueOf (LangL r a) = a
  entityValue = id

instance DSLEntity r Int where
  type ValueOf Int = Int
  entityValue = pure

foo :: LangL r Int -> LangL r Int
foo m = entityValue (entityValue m)

GHC gives the following output:

    • Ambiguous type variable ‘r0’ arising from a use of ‘entityValue’
      prevents the constraint ‘(DSLEntity
                                  r (LangL r0 Int))’ from being solved.
      Relevant bindings include
        m :: LangL r Int (bound at temp.hs:25:5)
        foo :: LangL r Int -> LangL r Int
          (bound at temp.hs:25:1)
      Probable fix: use a type annotation to specify what ‘r0’ should be.
      These potential instance exist:
        instance DSLEntity r (LangL r a)
          -- Defined at temp.hs:16:10
    • In the expression: entityValue (entityValue m)
      In an equation for ‘foo’: foo m = entityValue (entityValue m)
   |
temp.hs:25:22-34: error: …
    • Ambiguous type variable ‘r0’ arising from a use of ‘entityValue’
      prevents the constraint ‘(DSLEntity
                                  r0 (LangL r Int))’ from being solved.
      Relevant bindings include
        m :: LangL r Int (bound at temp.hs:25:5)
        foo :: LangL r Int -> LangL r Int
          (bound at temp.hs:25:1)
      Probable fix: use a type annotation to specify what ‘r0’ should be.
      These potential instance exist:
        instance DSLEntity r (LangL r a)
          -- Defined at /temp.hs:16:10
    • In the first argument of ‘entityValue’, namely ‘(entityValue m)’
      In the expression: entityValue (entityValue m)
      In an equation for ‘foo’: foo m = entityValue (entityValue m)
   |

The problem is clear. There is no dependency between r parameter of LangL r a and r parameter of DSLEntity. However, we cannot add such a dependency because for Int instance it actually does not exist.

I'm rather confused and would like to know if it's possible to accomplish what I'm trying to do. If not, why?

Answer 1

You can use:

instance (r ~ r') => DSLEntity r' (LangL r a) where

instead of:

instance DSLEntity r (LangL r a) where

It's a little arcane what this actually does.

Your original instance declaration says that GHC can only use that instance when it can prove that the r in LangL r a is the same type in the argument and in the result of entityValue. But entityValue :: a -> LangL r (ValueOf a), so any type at all can be used as the input (and require GHC to go looking for a matching instance). In particular, any LangL r0 a can appear as the input, even for non-matching r. So in entityValue (entityValue m), the first one could be used at any r0, and the second will convert it back to the r used in the type of foo. Since GHC can't establish which r you're talking about in the middle, you get the problem that the ambiguous type variable prevents it from knowing which DSLEntity instance it should choose to resolve the constraint.

Whereas instance (r ~ r') => DSLEntity r' (LangL r a) says that this instance applies for any types r and r', but using it adds the constraint that r and r' are equal. This sounds the same as just writing instance DSLEntity r (LangL r a), but it actually isn't because of the rule that GHC doesn't consider constraints when choosing instances, only afterwards. Now GHC doesn't need to prove that r and r' are equal in order to choose this instance, it will choose the instance any time the second parameter of a DSLEntity constraint looks like LangL _ _, and then after that it will know that in order to typecheck the constraint r ~ r' must hold, so it will go ahead and assume that (if it's possible; otherwise you get a type error).

You can see the difference pretty clearly by looking at the type of entityValue . entityValue. With your original instance, you get:

λ :t entityValue . entityValue 
entityValue . entityValue
  :: (DSLEntity r1 (LangL r2 (ValueOf a)), DSLEntity r2 a) =>
     a -> LangL r1 (ValueOf a)

And with the new instance you get this:

λ :t entityValue . entityValue 
entityValue . entityValue
  :: DSLEntity r a => a -> LangL r (ValueOf a)