#13161: Unexpected error about untouchable variable -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): This is expected behavior, for a sufficiently nuanced expectation. The argument to builder is type-checked with an assumed equality, `Foo (Foo m) ~ Foo m`. Type variables brought into scope outside an assumed equality cannot be influenced by anything that arises with an equality assumption, because perhaps the equality assumption affects how that outer variable should be solved. In your case, GHC must infer the index `a` to the type `Builder`. We see that `a` should be `Expr l` for some `l`, looking at the type of `finish`. But what `l`? The only way to know would be to unify `l` with `X`, the result of the `app` -- but that `X` was derived with an assumed equality in scope. So we have an error. It is fixed by your type signature, which tells GHC what `l` should be, and it is fixed by removing the equality assumption, which avoid triggering the "untouchable variable" behavior. The beginning of section 5 of the [https://www.microsoft.com/en- us/research/publication/outsideinx-modular-type-inference-with-local- assumptions/ OutsideIn paper] gives a nice introduction to untouchable variables, accessible to intermediate (or better) Haskell programmers and with no need to read anything before section 5. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13161#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler