Type error in one function causes wrong type error report in another function in the presence of functionally dependent types

[Lemming]

When trying to reduce my problem in #5970 to a simple program I encountered an even more obvious bug. The problem is essentially as follows: I have

correct :: T
correct = ...

wrong :: T
wrong = f correct

where 'wrong' has a type error and 'correct' is type correct. If I outcomment 'wrong' then GHC correctly confirms type-correctness of 'correct', but if 'wrong' is enabled then GHC claims a type error in both 'wrong' and 'correct'. To me it looks like the type-checker is trying to unify types across function boundaries. This would explain both non-linear growth of type-checking time and the observed effect of incorrect type errors. See attached program for a working example.

[simonpj]

Can you explain how to reproduce? Is monoBar the correct? Or monoFoo?

[Lemming]

Sorry ... monoFoo is correct and monoBar is incorrect. But when I compile that module GHC reports two type errors: One for monoFoo and one for monoBar. If I remove monoBar, then monoFoo is accepted by GHC.

The result of monoBar is Double, thus fromB=Double. The argument of polyBar in monoBar is of type Float, thus fromA=Float. From the functional dependencies it follows toB=Bool and toA=Char. Thus id would need type Char -> Bool, which is a type error and this one is correctly spotted by GHC. But additionally also a type error for monoBar is reported, although monoBar is correct. It has type Float and it follows to=Char, but the 'to' type is not used in monoBar.

[simonpj]

OK I see what is happening. From the two definitions we get these "wanted" constraints:

monoFoo:   mf1: C Float alpha

monoBar:   mb1: C Float beta, 
           mb2: C Double beta

where alpha and beta are otherwise-unconstrained unification variables.

Now if we first do fundeps wrt the instance decls, we get alpha = Char from mf1, beta = Char from mb1 and beta = Bool from mb2, the latter two yield an error.

But if we first do fundeps between the wanted constraints, we get alpha = beta, so that leaves us with (mf1: C Float alpha, mb2: C Double alpha). Now we can solve mb2 via the fundep with the instance to give alpha=Bool, and that leaves an error for the innocent mf1!

Even this isn't quite what happens. Functional dependencies are a pain.

Simon

[Lemming]

Would you suggest that I convert my code to type families?

[simonpj]

I would certainly give type families a try, yes. I'd be interested to hear how it goes.

[Lemming]

Replying to simonpj:

I would certainly give type families a try, yes. I'd be interested to hear how it goes.

I have converted some of my code to type families. Unfortunately, since I depend on the llvm package, the code is now quite inconsistent, because llvm uses a lot of functional dependencies and it uses in turn the type-level package that requires even more functional dependencies. Thus for now I cannot get rid of the problematic code. My hope is that we can remove all of these functional dependencies when the type level naturals (#4385) become part of GHC HEAD.

[simonpj]

OK. So the error message is a bit odd. Could be fixed, with some work. But as I undrestand it, this ticket is not standing in anyone's path. It's just a "nice to have" possible improvement, right?

[Lemming]

At first I thought that the type checker is wrong, since it reports a type error where no type error is. If I understand you correctly, then GHC still correctly identifies type correct and type incorrect programs, only the error message is misleading. If so, then this bug has no high priority for me. You may simply add "if this type error message confuses you, then better switch to type families" to every type error message concerning functional dependencies. :-)

[Lemming]

Now I got the same problem with type families and without functional dependencies.

[Lemming]

Replying to Lemming:

Now I got the same problem with type families and without functional dependencies.

I have opened a new ticket for the issue with type families: #7010.

[simonpj]

Recent changes in the type inference engine mean that you now get just one error, and on monoBar. To be honest I'm not 100% certain of why this has come right, and that means I'm not certain that the solution is robust (mabye it's a fluke). But I'm sort of time, so I'm closing the ticket. But I'm adding the test as a regression test so we'll know immediately if it stops working.

Thanks for the example.

Simon