#7220: Confusing error message in type checking related to type family, fundep,
and higher-rank type
------------------------------------------+---------------------------------
Reporter: tsuyoshi | Owner: simonpj
Type: bug | Status: closed
Priority: normal | Milestone: 7.8.1
Component: Compiler (Type checker) | Version: 7.6.1-rc1
Resolution: fixed | Keywords:
Os: Unknown/Multiple | Architecture: Unknown/Multiple
Failure: None/Unknown | Difficulty: Unknown
Testcase: typecheck/should_fail/T7220 | Blockedby:
Blocking: | Related:
------------------------------------------+---------------------------------
Changes (by simonpj):
* status: new => closed
* testcase: => typecheck/should_fail/T7220
* resolution: => fixed
Comment:
"I cannot think of any reason why it should relate the type (forall b. (C
A b, TF b ~ Y) => b) with Y". Here's why:
{{{
u :: (C A b, TF b ~ Y) => b
u = undefined
v :: X
v = (f :: (forall b. (C A b, TF b ~ Y) => b) -> X) u
}}}
* GHC instanatiates the occurence of `u`, given type just `beta`, where
`beta` is a fresh unification variable. Plus constraints `(C A beta, TF
beta ~ Y)`.
* Now it tries to unify `beta` with the expected arugment type of the `(f
:: sig)` expression. This argument type is `(forall b. (C A b, TF b ~ Y)
=> b)`
* So GHC (until today) would unify `beta := forall b. (C A b, TF b ~ Y)
=> b`.
* So the constraint `(TF beta ~ Y)` turns into (TF (forall b. (C A b, TF
b ~ Y) => b) ~ Y)`, and that's the error you saw.
But really GHC should not have taken the third step above (at least not
without `-XImpredicativeTypes`). With the patch that fixes #6069 and
#7264 it no longer does so, yielding instead
{{{
T7220.hs:24:6:
Cannot instantiate unification variable `b0'
with a type involving foralls: forall b. (C A b, TF b ~ Y) => b
Perhaps you want -XImpredicativeTypes
In the expression: f :: (forall b. (C A b, TF b ~ Y) => b) -> X
In the expression: (f :: (forall b. (C A b, TF b ~ Y) => b) -> X) u
In an equation for `v':
v = (f :: (forall b. (C A b, TF b ~ Y) => b) -> X) u
}}}
which isn't fantastic but is perhaps less confusing than before.
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/7220#comment:3>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
