[GHC] #13161: Unexpected error about untouchable variable

[GHC]

#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