#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