#9211: Untouchable type variable (regression from 7.6) -------------------------------------+------------------------------------ Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by simonpj): This looks right to me, and 7.4 looks wrong. There really is an equality `(f ~ g)` in the context, and so it's in general unsafe to fix `b` to `Bool`. That's what the !OutsideIn paper is all about. In this case the equality is trivial but presumably it's not trivial in your real example. For a trivial equality like this, perhaps GHC is over-conservative, but lifting that would require yet more special-case pleading. And I'm not sure it'd fix your real example anyway. In short, I don't know how to help. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9211#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9211: Untouchable type variable (regression from 7.6) -------------------------------------+------------------------------------ Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by oleg): My real examples are not that different from the one I posted. Here is one of the recent ones: {{{ unsafeLam :: (Applicative m, AppPermutable i, SSym repr, LamPure repr) => (forall j. (j ~ (->) (repr a))) => (i :. j) (repr a) -> (m :. (i :. j)) (repr b)) -> (m :. i) (repr (a->b)) }}} As you can see, I use the type equality constraint to give an abbreviation to a complex type that appears several times in a complex expression. In the above example, 'j' is used as an abbreviation for '(->) (repr a)' that occurs twice in a large type. OCaml has the convenient notation 'type as x -> x -> x' to give an abbreviation to a type. I was happy that I found something similar in Haskell. Alas, as this ticket shows, sometimes it doesn't work. I have fixed my problem by getting rid of the abbreviation. (Giving the local type annotation in the real case proved to be too messy. The compiler kept complaining and needing more and more annotations.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9211#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9211: Untouchable type variable (regression from 7.6) -------------------------------------+------------------------------------ Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by oleg): Indeed I use the equality constraint to essentially let-bind a type variable, which is quite handy. I'm glad to hear that it is also easy to implement. I, too, am curious what Dimitrios thinks. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9211#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9211: Untouchable type variable (regression from 7.6) -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones ): In [changeset:"5770029a1f8509a673b2277287fc8fe90b9b6002/ghc"]: {{{ #!CommitTicketReference repository="ghc" revision="5770029a1f8509a673b2277287fc8fe90b9b6002" Simon's major commit to re-engineer the constraint solver The driving change is this: * The canonical CFunEqCan constraints now have the form [G] F xis ~ fsk [W] F xis ~ fmv where fsk is a flatten-skolem, and fmv is a flatten-meta-variable Think of them as the name of the type-function application See Note [The flattening story] in TcFlatten. A flatten-meta-variable is distinguishable by its MetaInfo of FlatMetaTv This in turn led to an enormous cascade of other changes, which simplify and modularise the constraint solver. In particular: * Basic data types * I got rid of inert_solved_funeqs altogether. It serves no useful role that inert_flat_cache does not solve. * I added wl_implics to the WorkList, as a convenient place to accumulate newly-emitted implications; see Note [Residual implications] in TcSMonad. * I eliminated tcs_ty_binds altogether. These were the bindings for unification variables that we have now solved by unification. We kept them in a finite map and did the side-effecting unification later. But in cannonicalisation we had to look up in the side-effected mutable tyvars anyway, so nothing was being gained. Our original idea was that the solver would be pure, and would be a no-op if you discarded its results, but this was already not-true for implications since we update their evidence bindings in an imperative way. So rather than the uneasy compromise, it's now clearly imperative! * I split out the flatten/unflatten code into a new module, TcFlatten * I simplified and articulated explicitly the (rather hazy) invariants for the inert substitution inert_eqs. See Note [eqCanRewrite] and See Note [Applying the inert substitution] in TcFlatten * Unflattening is now done (by TcFlatten.unflatten) after solveFlats, before solving nested implications. This turned out to simplify a lot of code. Previously, unflattening was done as part of zonking, at the very very end. * Eager unflattening allowed me to remove the unpleasant ic_fsks field of an Implication (hurrah) * Eager unflattening made the TcSimplify.floatEqualities function much simpler (just float equalities looking like a ~ ty, where a is an untouchable meta-tyvar). * Likewise the idea of "pushing wanteds in as givens" could be completely eliminated. * I radically simplified the code that determines when there are 'given' equalities, and hence whether we can float 'wanted' equalies out. See TcSMonad.getNoGivenEqs, and Note [When does an implication have given equalities?]. This allowed me to get rid of the unpleasant inert_no_eqs flag in InertCans. * As part of this given-equality stuff, I fixed Trac #9211. See Note [Let-bound skolems] in TcSMonad * Orientation of tyvar/tyvar equalities (a ~ b) was partly done during canonicalisation, but then repeated in the spontaneous-solve stage (trySpontaneousSolveTwoWay). Now it is done exclusively during canonicalisation, which keeps all the code in one place. See Note [Canonical orientation for tyvar/tyvar equality constraints] in TcCanonical }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9211#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9211: Untouchable type variable (regression from 7.6) -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: fixed | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: indexed- | types/should_compile/T9211 | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => closed * testcase: => indexed-types/should_compile/T9211 * resolution: => fixed -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9211#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler