[Haskell-cafe] Simple GADTs, type families and type classes combination with type error.

[Dan Doel]

On Fri, Jul 22, 2011 at 11:12 AM, Serguey Zefirov <sergueyz at gmail.com> wrote:
> ---------------------------------------------------------------------------------------------------------------------
> {-# LANGUAGE GADTs, TypeFamilies #-}
>
> class CPU cpu where
>        type CPUFunc cpu
>
> data Expr cpu where
>        EVar :: String -> Expr cpu
>        EFunc :: CPU cpu => CPUFunc cpu -> Expr cpu
>
> class CPU cpu => FuncVars cpu where
>        funcVars :: CPUFunc cpu -> [String]
>
> exprVars :: FuncVars cpu => Expr cpu -> [String]
> exprVars (EVar v) = [v]
> -- an offending line:
> exprVars (EFunc f) = funcVars f
> ---------------------------------------------------------------------------------------------------------------------
>
> I tried to split creation and analysis constraints. CPU required for
> creation of expressions, FuncVars required for analysis. It all looks
> nice but didn't work.
>
> (In our real code EVar is slightly more complicated, featuring "Var
> cpu" argument)
>
> It looks like GHC cannot relate parameters "inside" and "outside" of
> GADT constructor.
>
> Not that I hesitate to add a method to a CPU class, but I think it is
> not the right thing to do. So if I can split my task into two classes,
> I will feel better.

GHC cannot decide what instance of FuncVars to use. The signature of
funcVars is:

    funcVars :: FuncVars cpu => CPUFunc cpu -> [String]

This does not take any arguments that allow cpu to be determined. For
instance, if there were instances (rolling them into one declaration
for simplicity):

    instance FuncVars Int where
      type CPUFunc Int = Int
      ...

    instance FuncVars Char where
      type CPUFunc Char = Int

Then GHC would see that CPUFunc cpu = Int, but from this, it cannot
determine whether cpu = Int or cpu = Char. CPUFunc is not
(necessarily) injective.

Making CPUFunc a data family as Felipe suggested fixes this by CPUFunc
essentially being a constructor of types, not a function that
computes. So it would be impossible for CPUFunc a = CPUFunc b unless a
= b.

Also, if you have a class whose only content is an associated type,
there's really no need for the class at all. It desugars into:

    type family CPUFunc a :: *

    class CPU a

So it's just a type family and an empty class, which will all have
exactly the same cases defined. You could instead use just the family.

-- Dan