#9318: Type error reported in wrong place with repeated type family expressions -------------------------------------+------------------------------------- Reporter: goldfire | Owner: simonpj Type: bug | Status: new Priority: high | Milestone: 7.10.1 Component: Compiler | Version: 7.8.3 (Type checker) | Keywords: Resolution: | Operating System: Unknown/Multiple Differential Revisions: | Type of failure: None/Unknown Architecture: | Test Case: Unknown/Multiple | Blocking: Difficulty: Unknown | Blocked By: | Related Tickets: | -------------------------------------+------------------------------------- Changes (by simonpj): * cc: dimitris@… (added) * owner: => simonpj * priority: normal => high * milestone: => 7.10.1 Comment: Dimitrios, I'd like to discuss this with you when you get back. The behaviour is terrible, and it's a classic case of rewriting a wanted with a wanted. We have {{{ [W] w1 :: F Int ~ Bool -- From foo [W] w2 :: F Int ~ Char -- From bar }}} We try to solve `w2` first: * we rewrite the `F Int` to `Bool`, * add `w2` to the `inert_solved_funeqs` * make `w3` :: Bool ~ Char` (insoluble, correctly) * bind `w2` to evidence involving `w3` and the axiom But now when we try to solve `w1` we find `w2` in the `inert_solved_funeqs` before looking up in the axioms, and thus rewrite to `Char ~ Bool`. Disaster. The problem is putting `w2` (which is really insoluble) in the `inert_solved_funeqs`. Instead I suspect we should put only ''givens'' in the `inert_solved_funeqs`, namely the evidence from the use of the axiom. So solving the second goal would go more like this * we rewrite the `F Int` to `Bool`, with coercion `co` * add `[G] co : F Int ~ Bool` to `inert_solved_funeqs` * create `[W] w3 :: Bool ~ Char` * bind `w2 = co ; w3` Now `inert_solved_funeqs` contains only givens derived directly from axioms, which we can safely use to solve anything. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9318#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9318: Type error reported in wrong place with repeated type family expressions -------------------------------------+------------------------------------- Reporter: goldfire | Owner: simonpj Type: bug | Status: new Priority: high | Milestone: 7.10.1 Component: Compiler | Version: 7.8.3 (Type checker) | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: None/Unknown | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by simonpj): Capturing work in progress. I've pushed a second iteration to branch `wip/new-flatten-skolems-Aug14`. Still not really right. An interesting case is `indexed-types/should_compile/T3826`; see commments in the source file. Below are my notes {{{ ToDo: * TcInteract, Note [Efficient orientation]? * inert_funeqs, inert_eqs: keep only the CtEvidence. They are all CFunEqCans, CTyEqCans * Update Note [Preparing inert set for implications] * indexed_types/should_compile/T3826 The new flattening story ~~~~~~~~~~~~~~~~~~~~~~~~ * A "flatten-skolem", fsk, is a *unification* variable (ie with an IORef inside it) * A CFunEqCan is always of form [W] x : F xis ~ fsk where x is the witness variable fsk is a flatten skolem xis are function-free CFunEqCans are always [Wanted], never [Given] or [Derived] * Inert set invariant: if [W] F xis1 ~ fsk1, [W] F xis2 ~ fsk2 then xis1 /= xis2 i.e. at most one CFunEqCan with a particular LHS * Each canonical CFunEqCan [W] x : F xis ~ fsk has its own distinct evidence variable x and flatten-skolem fsk. * CFunEqCans are the *only* way that function applications appear in canonical constraints. Function applications in any other constraint must be gotten rid of by flattening, thereby generating fresh CFunEqCans. * Flattening a type (F xis): - Make a new [W] x : F xis ~ fsk with fresh evidence variable x and flatten-skolem fsk - Add it to the work list - Replace (F xis) with fsk in the type you are flattening - You can also add the CFunEqCan to the "flat cache", which simply keeps track of all the function applications you have flattened. If (F xis) is in the cache already, just use its fsk and evidence x, and emit nothing. - No need to substitute in the flat-cache. It's not the end of the world if we start with, say (F alpha ~ fsk1) and (F Int ~ fsk2) and then find alpha := Int. Athat will simply give rise to fsk1 := fsk2 via [Interacting rule] below * Canonicalising ([W} x : F xis ~ fsk) - Flatten xis cos :: xis ~ flat_xis - New wanted x2 :: F flat_xis ~ fsk - Add new wanted to flat cache - Discharge x = F cos ; x2 * Flatten-skolems ONLY get unified when either a) The CFunEqCan takes a step, using an axiom b) During un-flattening at the very, very end They are never unified in any other form of equality. For example [W] fsk ~ Int is stuck; it does not unify with fsk. * We *never* substitute in the RHS (i.e. the fsk) of a CFunEqCan. That would destroy the invariant about the shape of a CFunEqCan, and it would risk wanted/wanted interactions. The only way we learn information about fsk is when the CFunEqCan takes a step. However we *do* substitute in the LHS of a CFunEqCan (else it would never get to fire!) * KEY INSIGHTS: - A flatten-skolem stands for the as-yet-unknown type to which (F xis) will eventually reduce - Although the CFunEqCan is a Wanted, it will almost always eventually be solved, eitehr * [Interacting rule] (inert) x1 : F tys ~ fsk1 (work item) x2 : F tys ~ fsk2 Just solve one from the other: x2 := x1 fsk2 := fsk1 [G] <fsk1> fsk2 ~ fsk1 This just unites the two fsks into one. * [Firing rule] (work item) x : F tys ~ fsk instantiate axiom: co : F tys ~ rhs First flatten rhs, giving flat_co : rhs ~ xi Now unify fsk := xi [G] <xi> : fsk ~ xi x := co ; flat_co discharging the work item UNLESS fsk appears in xi, which can happen, in which case don't unnify but stick [W] fsk ~ xi in the insoluble set. --------------- ---------------- Preparing the inert set for implications type instance F True a b = a type instance F False a b = b [W] x : F c a b ~ fsk [G] gamma ~ fsk (c ~ True) => a ~ gamma (c ~ False) => b ~ gamma --> (c ~ True branch) Push in as given non-canonical [G] g : (c ~ True) [G] x : F c a b ~ fsk (nc) [W] a ~ fsk, --> flatten [G] g : (c ~ True) [G] sym x1 ; x : fsk1 ~ fsk [W] x1 : F c a b ~ fsk1 (canon) [W] a ~ fsk, ---> subst c [G] g : (c ~ True) [G] sym x1 ; x : fsk1 ~ fsk [W] x2 : F True a b ~ fsk1 (canon) x1 = F g a b ; x2 [W] a ~ fsk, ---> step ax : F True a b ~ a [G] g : (c ~ True) [G] sym x1 ; x : fsk1 ~ fsk [W] x2 : F True a b ~ fsk1 (canon) [G] <a> : fsk1 := a x2 = ax [W] a ~ fsk, -------------------------- Simple20 ~~~~~~~~ axiom F [a] = [F a] [G] F [a] ~ a --> [G] fsk ~ a [W] F [a] ~ fsk --> fsk := [fsk2] [G] [fsk2] ~ a [W] F a ~ fsk2 --> [W] F [fsk2] ~ fsk2 -- Back to square 1 }}} -- Ticket URL: GHC The Glasgow Haskell Compiler

#9318: Type error reported in wrong place with repeated type family expressions -------------------------------------+------------------------------------- Reporter: goldfire | Owner: simonpj Type: bug | Status: new Priority: high | Milestone: 7.10.1 Component: Compiler | Version: 7.8.3 (Type checker) | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: None/Unknown | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by Richard Eisenberg ): In [changeset:"5eebd990ea7a5bc1937657b101ae83475e20fc7a/ghc"]: {{{ #!CommitTicketReference repository="ghc" revision="5eebd990ea7a5bc1937657b101ae83475e20fc7a" Test #9318 in typecheck/should_fail/T9318 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9318#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9318: Type error reported in wrong place with repeated type family expressions -------------------------------------+------------------------------------- Reporter: goldfire | Owner: simonpj Type: bug | Status: closed Priority: high | Milestone: 7.10.1 Component: Compiler | Version: 7.8.3 (Type checker) | Keywords: Resolution: fixed | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: None/Unknown | Test Case: | typecheck/should_fail/T9318 | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones ): In [changeset:"5760eb598e0dfa451407195f15072204c15233ed/ghc"]: {{{ #!CommitTicketReference repository="ghc" revision="5760eb598e0dfa451407195f15072204c15233ed" Test Trac #9318 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9318#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9318: Type error reported in wrong place with repeated type family expressions -------------------------------------+------------------------------------- Reporter: goldfire | Owner: simonpj Type: bug | Status: closed Priority: high | Milestone: 7.10.1 Component: Compiler | Version: 7.8.3 (Type checker) | Keywords: Resolution: fixed | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: None/Unknown | Test Case: | typecheck/should_fail/T9318 | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by simonpj): Oh yes...ha ha. Can you delete one? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9318#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler