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

[Dan Doel]

On Fri, Jul 22, 2011 at 4:11 PM, Serguey Zefirov <sergueyz at gmail.com> wrote:
> But "cpu" variable is the same in all places. If we don't dive into
> CPUFunc reduction (to Int or whatever) we can safely match funcVars
> argument and unify cpu.
>
> This is the case when we write generic functions over type family application.

Here is approximately what the checking algorithm knows in the problematic case:

  exprVars (EFunc f) = funcVars f

  exprVars :: FuncVars cpu1 => Expr cpu1 -> [String]
  EFunc f :: Expr cpu1
  funcVars :: FuncVars cpu2 => CPUFunc cpu2 -> [String]
  f :: CPUFunc cpu1

Thus, it can determine:

  CPUFunc cpu2 = CPUFunc cpu1

Now it needs to decide which instance of FuncVars to feed to funcVars.
But it only knows that cpu2 should be such that the above type
equation holds. However, since CPUFunc is a type family, it is not
sound in general to reason from:

  CPUFunc cpu1 = CPUFunc cpu2

to:

  cpu1 = cpu2

So the type checker doesn't. You have nothing there that determines
cpu1 to be the same as cpu2. So you need to make some change that does
determine them to be the same.

In situations like these, it would be handy if there were a way to
specify what type certain variables are instantiated to, but it's sort
of understandable that there isn't, because it'd be difficult to do in
a totally satisfactory way.

-- Dan