#12660: singletons doesn't compile with GHC 8.0.2 snapshot -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: normal | Milestone: 8.0.2 Component: Compiler | Version: Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by bgamari): `TcCanonical.canEvVar` calls `TcCanonical.canEvNC` which has no cost center but does have a `traceTcS`. Compiling `singletons` with `-ddump-tc- trace` shows that the compiler indeed seems to be looping in the typechecker, {{{ ... Following filled tyvar s_aov1[fuv:20] = n1_alUY[ssk] GHC.TypeLits.- n0_alUX[ssk] flattenTyVarFinal x2_alWb[sk] :: Nat Nat <Nat>_N :: Nat ~ Nat flattenTyVar1 (x2_alWb[sk] :: Nat) <Nat>_N :: Nat ~ Nat flattenTyVar2 n1_alUY[ssk] x2_alWb[sk] flattenTyVarFinal x1_alWa[sk] :: Nat Nat <Nat>_N :: Nat ~ Nat flattenTyVar1 (x1_alWa[sk] :: Nat) <Nat>_N :: Nat ~ Nat flattenTyVar2 n0_alUX[ssk] x1_alWa[sk] flatten/flat-cache hit GHC.TypeLits.- [x2_alWb[sk], x1_alWa[sk]] s_aov1[fuv:20] Following filled tyvar s_aov1[fuv:20] = n1_alUY[ssk] GHC.TypeLits.- n0_alUX[ssk] ... }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12660#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12660: singletons doesn't compile with GHC 8.0.2 snapshot -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: normal | Milestone: 8.0.2 Component: Compiler | Version: Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I see what's going on, but I don't know why things are the way they are nor how to fix. The problem is, essentially, that we unflatten and then continue solving. Then, we have a fuv (flattening unification variable) that's filled in with the function it equals. So the flattener ends up bouncing between the function application and its fuv (as found in the flat-cache). The unflattening is happening in `TcInteract.solve_simple_wanteds`, as called from `solveSimpleWanteds`. But then the `go` loop in the latter goes around again. It does so in the same instance of the `TcS` monad, so that flat-cache is retained, even though unflattening has happened. And then we're in trouble. Questions: 1. Should the flat-cache be wiped every time we unflatten? 2. Should we even allow unflattening in the `TcS` monad? I always thought unflattening was about restoring nice-looking types for error messages and something that should happen just as we leave the `TcS` monad. But we shouldn't resume solving after unflattening, I think. I'm afraid I've reached the limit of what I can do with this ticket. Simon? :) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12660#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12660: singletons doesn't compile with GHC 8.0.2 snapshot -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: normal | Milestone: 8.0.2 Component: Compiler | Version: Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Note that the problem does not exist in HEAD -- the problem is in the 8.0 branch. But to get singletons to work with HEAD, you'll need the HEAD of `th- desugar`, from github.com/goldfirere/th-desugar. Clone from there and install; singletons should install on top of that without trouble (I think). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12660#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12660: singletons doesn't compile with GHC 8.0.2 snapshot -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: highest | Milestone: 8.0.2 Component: Compiler | Version: Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * priority: normal => highest -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12660#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12660: singletons doesn't compile with GHC 8.0.2 snapshot -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: highest | Milestone: 8.0.2 Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): This is an 8.0.2 release blocker, no? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12660#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12660: singletons doesn't compile with GHC 8.0.2 snapshot -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: highest | Milestone: 8.0.2 Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I'm looking at this -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12660#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12660: singletons doesn't compile with GHC 8.0.2 snapshot -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: highest | Milestone: 8.0.2 Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I now know what is happening. * At some point we have a Given {{{ [G] Tuple3Sym3 x1 x2 y ~ Tuple3Sym3 n0 n1 n2 }}} * Currently we make derived constraints from injectivity from Givens, so we get {{{ [D] n1 ~ x2 }}} This becomes part of the "model". * Inside a further nest of implication constraints we are processing the Givens, and end up adding this to the inert set: {{{ [G] (n1 - n0) ~ fsk (CFunEqCan) }}} * But since that can be rewritten by the model, we emit a derived "shadow" of the Given: {{{ [D] (n1 - n0) ~ fsk (CNonCanonical) }}} * When processing that Derived constraint, we add {{{ [D] (n1 - n0) ~ fuv (CFunEqCan) }}} to the flat-cache * Now we finish processing the Givens and start doing the Wanteds. We get a hit in the flat-cache, so 'fuv' nwo shows up in the residual wanteds. Then during un-flattening we unify that fuv. At this point the assumption is that CFunEqCan can't reappear. But it's still there in the flat-cache, and when we re-solve the Wanteds we find hit again. But this time fuv is unified and chaos results. What to do? I can think of a number of alternatives. 1. For now the simple thing to do is to start processing the Wanteds with an empty flat-cache. This is easily done in `nestTcS`. But it's unsatisfactory because it discards useful Given entries in the flat-cache. Still, it's a 2-line quick-and-dirty fix that does solve the problem (I tried it). 2. We could address the unsatisfactory aspect of (1) by selectively purging the flat-cache, but I dislike that. Seems like a lot of work (both code and execution time) for an edge case. 3. We could simply not generate derived shadows for Given constraints. This is clean, simple, and will generate fewer deriveds. I have been unable to construct an example where we need to rewrite a Given with a (derived) model constraints to make useful progress. Can anyone else construct one? 4. We could still emit derived shadows from Givens, but in a less aggressive way, so that they don't pollute the flat-cache I'm going to try (3). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12660#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12660: singletons doesn't compile with GHC 8.0.2 snapshot -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: merge Priority: highest | Milestone: 8.0.2 Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => merge Comment: OK, (3) from comment:14 seemed to work. I couldn't come up with a small test case, but `singletons` compiles when I apply this patch to the 8.0 branch. But I have not pushed the patch to 8.0; hence marking this as 'merge' Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12660#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler