On Fri, Jul 22, 2011 at 4:11 PM, Serguey Zefirov
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